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

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

case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M ↾ C = circuitOn C
⊢ M.Circuit C

State before:
case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M ↾ C = circuitOn C
⊢ M.Circuit C
Tactic:
have h' := restrict_circuit_iff hC (C := C)
State after:
case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M ↾ C = circuitOn C
h' : (M ↾ C).Circuit C ↔ M.Circuit C ∧ C ⊆ C
⊢ M.Circuit C

State before:
case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M ↾ C = circuitOn C
h' : (M ↾ C).Circuit C ↔ M.Circuit C ∧ C ⊆ C
⊢ M.Circuit C
Tactic:
rwa [and_iff_left Subset.rfl, h, iff_true_intro (circuitOn_ground_circuit hCne), true_iff] at h'
State after:
no goals

State before:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M.Circuit C
⊢ M ↾ C = circuitOn C
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 α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M.Circuit C
C' : Set α
hC' : C' ⊆ (M ↾ C).E
⊢ (M ↾ C).Circuit C' ↔ (circuitOn C).Circuit C'

State before:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M.Circuit C
C' : Set α
hC' : C' ⊆ (M ↾ C).E
⊢ (M ↾ C).Circuit C' ↔ (circuitOn C).Circuit C'
Tactic:
rw [restrict_circuit_iff h.subset_ground, circuitOn_circuit_iff h.nonempty,
  and_iff_left (show C' ⊆ C from hC')]
State after:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M.Circuit C
C' : Set α
hC' : C' ⊆ (M ↾ C).E
⊢ M.Circuit C' ↔ C' = C

State before:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M.Circuit C
C' : Set α
hC' : C' ⊆ (M ↾ C).E
⊢ M.Circuit C' ↔ C' = C
Tactic:
exact ⟨fun h' ↦ h'.eq_of_subset_circuit h hC', fun h' ↦ by rwa [h']⟩
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hCne : C.Nonempty
hC : autoParam (C ⊆ M.E) _auto✝
h : M.Circuit C
C' : Set α
hC' : C' ⊆ (M ↾ C).E
h' : C' = C
⊢ M.Circuit C'
Tactic:
rwa [h']
State after:
no goals