Theorem: Matroid.ground_circuit_iff (Matroid/Constructions/Truncate.lean)

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
⊢ M.Circuit M.E ↔ M = circuitOn M.E
Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
State after:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
h : M.Circuit M.E
⊢ M = circuitOn M.E

case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
h : M = circuitOn M.E
⊢ M.Circuit M.E

State before:
case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
h : M = circuitOn M.E
⊢ M.Circuit M.E
Tactic:
rw [h]
State after:
case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
h : M = circuitOn M.E
⊢ (circuitOn M.E).Circuit (circuitOn M.E).E

State before:
case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
h : M = circuitOn M.E
⊢ (circuitOn M.E).Circuit (circuitOn M.E).E
Tactic:
exact circuitOn_ground_circuit M.ground_nonempty
State after:
no goals

State before:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
h : M.Circuit M.E
⊢ M = circuitOn M.E
Tactic:
refine eq_of_circuit_iff_circuit_forall rfl <| fun C hC ↦ ?_
State after:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C✝ : Set α
inst✝ : M.Nonempty
h : M.Circuit M.E
C : Set α
hC : C ⊆ M.E
⊢ M.Circuit C ↔ (circuitOn M.E).Circuit C

State before:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C✝ : Set α
inst✝ : M.Nonempty
h : M.Circuit M.E
C : Set α
hC : C ⊆ M.E
⊢ M.Circuit C ↔ (circuitOn M.E).Circuit C
Tactic:
rw [circuitOn_circuit_iff h.nonempty]
State after:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C✝ : Set α
inst✝ : M.Nonempty
h : M.Circuit M.E
C : Set α
hC : C ⊆ M.E
⊢ M.Circuit C ↔ C = M.E

State before:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C✝ : Set α
inst✝ : M.Nonempty
h : M.Circuit M.E
C : Set α
hC : C ⊆ M.E
⊢ M.Circuit C ↔ C = M.E
Tactic:
exact ⟨fun h' ↦ h'.eq_of_subset_circuit h hC, by rintro rfl; assumption⟩
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C✝ : Set α
inst✝ : M.Nonempty
h : M.Circuit M.E
C : Set α
hC : C ⊆ M.E
⊢ C = M.E → M.Circuit C
Tactic:
rintro rfl
State after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
h : M.Circuit M.E
hC : M.E ⊆ M.E
⊢ M.Circuit M.E

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
h : M.Circuit M.E
hC : M.E ⊆ M.E
⊢ M.Circuit M.E
Tactic:
assumption
State after:
no goals