𝕜 : Type ?u.5508
ι : Type ?u.5511
κ : Type ?u.5514
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ s'
t : Finset β
⊢ ∀ ⦃a : α × β⦄, a ∈ interedges r s t → ¬a ∈ interedges r s' t
𝕜 : Type ?u.5508
ι : Type ?u.5511
κ : Type ?u.5514
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s s' : Finset α
hs : Disjoint s s'
t : Finset β
⊢ Disjoint (interedges r s t) (interedges r s' t)
rw [Finset.disjoint_left] at hs⊢
𝕜 : Type ?u.5508
ι : Type ?u.5511
κ : Type ?u.5514
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ s'
t : Finset β
a✝ : α × β
hx : a✝ ∈ interedges r s t
hy : a✝ ∈ interedges r s' t
⊢ False
𝕜 : Type ?u.5508
ι : Type ?u.5511
κ : Type ?u.5514
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ s'
t : Finset β
⊢ ∀ ⦃a : α × β⦄, a ∈ interedges r s t → ¬a ∈ interedges r s' t
intro _ hx hy
𝕜 : Type ?u.5508
ι : Type ?u.5511
κ : Type ?u.5514
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ s'
t : Finset β
a✝ : α × β
hx : a✝.fst ∈ s ∧ a✝.snd ∈ t ∧ r a✝.fst a✝.snd
hy : a✝.fst ∈ s' ∧ a✝.snd ∈ t ∧ r a✝.fst a✝.snd
⊢ False
𝕜 : Type ?u.5508
ι : Type ?u.5511
κ : Type ?u.5514
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ s'
t : Finset β
a✝ : α × β
hx : a✝ ∈ interedges r s t
hy : a✝ ∈ interedges r s' t
⊢ False
rw [mem_interedges_iff] at hx hy
no goals
𝕜 : Type ?u.5508
ι : Type ?u.5511
κ : Type ?u.5514
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ s'
t : Finset β
a✝ : α × β
hx : a✝.fst ∈ s ∧ a✝.snd ∈ t ∧ r a✝.fst a✝.snd
hy : a✝.fst ∈ s' ∧ a✝.snd ∈ t ∧ r a✝.fst a✝.snd
⊢ False
exact hs hx.1 hy.1