Theorem: Matroid.map_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 : α → β
hf : InjOn f M.E
⊢ (M.map f hf).Circuit C ↔ ∃ C₀, M.Circuit C₀ ∧ C = f '' C₀
Tactic:
simp only [circuit_iff, map_dep_iff, forall_exists_index, and_imp]
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 : α → β
hf : InjOn f M.E
⊢ ((∃ D₀, M.Dep D₀ ∧ C = f '' D₀) ∧ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ C → I = C) ↔
    ∃ C₀, (M.Dep C₀ ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀) ∧ C = f '' 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 : α → β
hf : InjOn f M.E
⊢ ((∃ D₀, M.Dep D₀ ∧ C = f '' D₀) ∧ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ C → I = C) ↔
    ∃ C₀, (M.Dep C₀ ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀) ∧ C = f '' C₀
Tactic:
constructor
State after:
case mp
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α → β
hf : InjOn f M.E
⊢ ((∃ D₀, M.Dep D₀ ∧ C = f '' D₀) ∧ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ C → I = C) →
    ∃ C₀, (M.Dep C₀ ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀) ∧ C = f '' C₀

case mpr
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α → β
hf : InjOn f M.E
⊢ (∃ C₀, (M.Dep C₀ ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀) ∧ C = f '' C₀) →
    (∃ D₀, M.Dep D₀ ∧ C = f '' D₀) ∧ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ C → I = C

State before:
case mpr
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α → β
hf : InjOn f M.E
⊢ (∃ C₀, (M.Dep C₀ ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀) ∧ C = f '' C₀) →
    (∃ D₀, M.Dep D₀ ∧ C = f '' D₀) ∧ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ C → I = C
Tactic:
rintro ⟨C₀, ⟨h,h'⟩, rfl⟩
State after:
case mpr.intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C₀ : Set α
h : M.Dep C₀
h' : ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀
⊢ (∃ D₀, M.Dep D₀ ∧ f '' C₀ = f '' D₀) ∧ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C₀ → I = f '' C₀

State before:
case mpr.intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C₀ : Set α
h : M.Dep C₀
h' : ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀
⊢ (∃ D₀, M.Dep D₀ ∧ f '' C₀ = f '' D₀) ∧ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C₀ → I = f '' C₀
Tactic:
refine ⟨⟨C₀, h, rfl⟩, ?_⟩
State after:
case mpr.intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C₀ : Set α
h : M.Dep C₀
h' : ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀
⊢ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C₀ → I = f '' C₀

State before:
case mpr.intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C₀ : Set α
h : M.Dep C₀
h' : ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀
⊢ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C₀ → I = f '' C₀
Tactic:
rintro _ D hD rfl hss
State after:
case mpr.intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C₀ : Set α
h : M.Dep C₀
h' : ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀
D : Set α
hD : M.Dep D
hss : f '' D ⊆ f '' C₀
⊢ f '' D = f '' C₀

State before:
case mpr.intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C₀ : Set α
h : M.Dep C₀
h' : ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀
D : Set α
hD : M.Dep D
hss : f '' D ⊆ f '' C₀
⊢ f '' D = f '' C₀
Tactic:
rw [h' hD ((hf.image_subset_image_iff hD.subset_ground h.subset_ground).1 hss)]
State after:
no goals

State before:
case mp
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
C : Set β
f : α → β
hf : InjOn f M.E
⊢ ((∃ D₀, M.Dep D₀ ∧ C = f '' D₀) ∧ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ C → I = C) →
    ∃ C₀, (M.Dep C₀ ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀) ∧ C = f '' C₀
Tactic:
rintro ⟨⟨C, hC, rfl⟩, h⟩
State after:
case mp.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C : Set α
hC : M.Dep C
h : ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C → I = f '' C
⊢ ∃ C₀, (M.Dep C₀ ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀) ∧ f '' C = f '' C₀

State before:
case mp.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C : Set α
hC : M.Dep C
h : ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C → I = f '' C
⊢ ∃ C₀, (M.Dep C₀ ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀) ∧ f '' C = f '' C₀
Tactic:
refine ⟨C, ⟨hC, fun D hD hDC ↦ ?_⟩, rfl⟩
State after:
case mp.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C : Set α
hC : M.Dep C
h : ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C → I = f '' C
D : Set α
hD : M.Dep D
hDC : D ⊆ C
⊢ D = C

State before:
case mp.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C : Set α
hC : M.Dep C
h : ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C → I = f '' C
D : Set α
hD : M.Dep D
hDC : D ⊆ C
⊢ D = C
Tactic:
rw [← hf.image_eq_image_iff hD.subset_ground hC.subset_ground]
State after:
case mp.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C : Set α
hC : M.Dep C
h : ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C → I = f '' C
D : Set α
hD : M.Dep D
hDC : D ⊆ C
⊢ f '' D = f '' C

State before:
case mp.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C : Set α
hC : M.Dep C
h : ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C → I = f '' C
D : Set α
hD : M.Dep D
hDC : D ⊆ C
⊢ f '' D = f '' C
Tactic:
exact h _ hD rfl (image_subset f hDC)
State after:
no goals