Theorem: Matroid.mapEquiv_circuit_iff (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
C : Set β
f : α ≃ β
⊢ (M.mapEquiv f).Circuit C ↔ M.Circuit (⇑f.symm '' C)
Tactic:
rw [mapEquiv_eq_map, map_circuit_iff]
State after:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α ≃ β
⊢ (∃ C₀, M.Circuit C₀ ∧ C = ⇑f '' C₀) ↔ M.Circuit (⇑f.symm '' C)

State before:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α ≃ β
⊢ (∃ C₀, M.Circuit C₀ ∧ C = ⇑f '' C₀) ↔ M.Circuit (⇑f.symm '' C)
Tactic:
exact ⟨by rintro ⟨C, hC, rfl⟩; simpa, fun h ↦ ⟨_, h, by simp⟩⟩
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α ≃ β
⊢ (∃ C₀, M.Circuit C₀ ∧ C = ⇑f '' C₀) → M.Circuit (⇑f.symm '' C)
Tactic:
rintro ⟨C, hC, rfl⟩
State after:
case intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α ≃ β
C : Set α
hC : M.Circuit C
⊢ M.Circuit (⇑f.symm '' (⇑f '' C))

State before:
case intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α ≃ β
C : Set α
hC : M.Circuit C
⊢ M.Circuit (⇑f.symm '' (⇑f '' C))
Tactic:
simpa
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α ≃ β
h : M.Circuit (⇑f.symm '' C)
⊢ C = ⇑f '' (⇑f.symm '' C)
Tactic:
simp
State after:
no goals