Theorem: Matroid.eq_of_circuit_iff_circuit_forall (Matroid/Circuit.lean)

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ C ⊆ M₁.E, M₁.Circuit C ↔ M₂.Circuit C
⊢ M₁ = M₂
Tactic:
have h' : ∀ C, M₁.Circuit C ↔ M₂.Circuit C := by
  exact fun C ↦ (em (C ⊆ M₁.E)).elim (h C)
    (fun hC ↦ iff_of_false (mt Circuit.subset_ground hC)
      (mt Circuit.subset_ground (fun hss ↦ hC (hss.trans_eq hE.symm))))
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ C ⊆ M₁.E, M₁.Circuit C ↔ M₂.Circuit C
h' : ∀ (C : Set α), M₁.Circuit C ↔ M₂.Circuit C
⊢ M₁ = M₂

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ C ⊆ M₁.E, M₁.Circuit C ↔ M₂.Circuit C
h' : ∀ (C : Set α), M₁.Circuit C ↔ M₂.Circuit C
⊢ M₁ = M₂
Tactic:
refine' eq_of_indep_iff_indep_forall hE fun I hI ↦ _
State after:
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ C ⊆ M₁.E, M₁.Circuit C ↔ M₂.Circuit C
h' : ∀ (C : Set α), M₁.Circuit C ↔ M₂.Circuit C
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I

State before:
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ C ⊆ M₁.E, M₁.Circuit C ↔ M₂.Circuit C
h' : ∀ (C : Set α), M₁.Circuit C ↔ M₂.Circuit C
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I
Tactic:
simp_rw [indep_iff_forall_subset_not_circuit hI, h',
  indep_iff_forall_subset_not_circuit (hI.trans_eq hE)]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ C ⊆ M₁.E, M₁.Circuit C ↔ M₂.Circuit C
⊢ ∀ (C : Set α), M₁.Circuit C ↔ M₂.Circuit C
Tactic:
exact fun C ↦ (em (C ⊆ M₁.E)).elim (h C)
  (fun hC ↦ iff_of_false (mt Circuit.subset_ground hC)
    (mt Circuit.subset_ground (fun hss ↦ hC (hss.trans_eq hE.symm))))
State after:
no goals