Theorem: Matroid.Iso.circuit_image (Matroid/Circuit.lean)

State before:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
hC : M.Circuit ↑C
⊢ N.Circuit ↑(⇑e '' C)
Tactic:
simp_rw [circuit_iff, ← e.dep_image_iff, and_iff_right hC.dep]
State after:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
hC : M.Circuit ↑C
⊢ ∀ ⦃I : Set β⦄, N.Dep I → I ⊆ ↑(⇑e '' C) → I = ↑(⇑e '' C)

State before:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
hC : M.Circuit ↑C
⊢ ∀ ⦃I : Set β⦄, N.Dep I → I ⊆ ↑(⇑e '' C) → I = ↑(⇑e '' C)
Tactic:
intro I hI hIC
State after:
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
hC : M.Circuit ↑C
I : Set β
hI : N.Dep I
hIC : I ⊆ ↑(⇑e '' C)
⊢ I = ↑(⇑e '' C)

State before:
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
hC : M.Circuit ↑C
I : Set β
hI : N.Dep I
hIC : I ⊆ ↑(⇑e '' C)
⊢ I = ↑(⇑e '' C)
Tactic:
obtain ⟨I,rfl⟩ := Subset.eq_image_val hI.subset_ground
State after:
case intro
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
hC : M.Circuit ↑C
I : Set ↑N.E
hI : N.Dep ↑I
hIC : ↑I ⊆ ↑(⇑e '' C)
⊢ ↑I = ↑(⇑e '' C)

State before:
case intro
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
hC : M.Circuit ↑C
I : Set ↑N.E
hI : N.Dep ↑I
hIC : ↑I ⊆ ↑(⇑e '' C)
⊢ ↑I = ↑(⇑e '' C)
Tactic:
replace hC := hC.eq_of_dep_subset (e.symm.image_dep hI)
State after:
case intro
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
I : Set ↑N.E
hI : N.Dep ↑I
hIC : ↑I ⊆ ↑(⇑e '' C)
hC : ↑(⇑e.symm '' I) ⊆ ↑C → ↑(⇑e.symm '' I) = ↑C
⊢ ↑I = ↑(⇑e '' C)

State before:
case intro
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
I : Set ↑N.E
hI : N.Dep ↑I
hIC : ↑I ⊆ ↑(⇑e '' C)
hC : ↑(⇑e.symm '' I) ⊆ ↑C → ↑(⇑e.symm '' I) = ↑C
⊢ ↑I = ↑(⇑e '' C)
Tactic:
simp only [image_subset_iff, preimage_val_image_val_eq_self, image_symm_eq_preimage,
  preimage_subset_iff, image_val_inj] at hIC hC
State after:
case intro
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
I : Set ↑N.E
hI : N.Dep ↑I
hIC : I ⊆ ⇑e '' C
hC : I ⊆ ⇑e '' C → ⇑e ⁻¹' I = C
⊢ ↑I = ↑(⇑e '' C)

State before:
case intro
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
I : Set ↑N.E
hI : N.Dep ↑I
hIC : I ⊆ ⇑e '' C
hC : I ⊆ ⇑e '' C → ⇑e ⁻¹' I = C
⊢ ↑I = ↑(⇑e '' C)
Tactic:
simp [← hC hIC]
State after:
no goals