𝕜 : Type ?u.2805
ι : Type ?u.2808
κ : Type ?u.2811
α : 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 : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
x : α × β
⊢ x.fst ∈ s₂ ∧ x.snd ∈ t₂ ∧ r x.fst x.snd → x.fst ∈ s₁ ∧ x.snd ∈ t₁ ∧ r x.fst x.snd
𝕜 : Type ?u.2805
ι : Type ?u.2808
κ : Type ?u.2811
α : 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 : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
x : α × β
⊢ x ∈ interedges r s₂ t₂ → x ∈ interedges r s₁ t₁
simp_rw [mem_interedges_iff]
no goals
𝕜 : Type ?u.2805
ι : Type ?u.2808
κ : Type ?u.2811
α : 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 : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
x : α × β
⊢ x.fst ∈ s₂ ∧ x.snd ∈ t₂ ∧ r x.fst x.snd → x.fst ∈ s₁ ∧ x.snd ∈ t₁ ∧ r x.fst x.snd
exact fun h ↦ ⟨hs h.1, ht h.2.1, h.2.2⟩