mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_4
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
⊢ ∀ ⦃i i' : ↑X⦄, ↑i ∈ C ↑i' → i = i'

pp: case refine_5
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
⊢ ∀ (i : ↑X), z ∉ C ↑i

Tactic:
·

Goal state after:
case refine_4
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
⊢ ∀ ⦃i i' : ↑X⦄, ↑i ∈ C ↑i' → i = i'
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
heE : e ∈ M.E
he : ¬M.IsColoop e
⊢ ∃ C, M.IsCircuit C ∧ e ∈ C

Tactic:
simp only [isColoop_iff_forall_mem_isBase, not_forall, exists_prop] at he
  obtain ⟨B, hB, heB⟩ := he
  exact ⟨M.fundCircuit e B, hB.fundCircuit_isCircuit heE heB, .inl rfl⟩

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ M.closure (M.closure X ∪ K) = M.closure X ∪ K

Tactic:
subset_antisymm_iff,

Goal state after:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ M.closure (M.closure X ∪ K) ⊆ M.closure X ∪ K ∧ M.closure X ∪ K ⊆ M.closure (M.closure X ∪ K)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
h : C₁ ≠ C₂
e : α
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

Tactic:
have hnss : ¬ (C₁ ⊆ C₂) := fun hss ↦ h <| hC₁.eq_of_subset_isCircuit hC₂ hss

Goal state after:
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
h : C₁ ≠ C₂
e : α
hnss : ¬C₁ ⊆ C₂
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case pos
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
h : C₁ ≠ C₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∈ C₁
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

pp: case neg
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
h : C₁ ≠ C₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∉ C₁
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

Tactic:
·

Goal state after:
case pos
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
h : C₁ ≠ C₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∈ C₁
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case pos
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
h : C₁ ≠ C₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∈ C₁
he₂ : e ∈ C₂
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

pp: case neg
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
h : C₁ ≠ C₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∈ C₁
he₂ : e ∉ C₂
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

Tactic:
·

Goal state after:
case pos
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
h : C₁ ≠ C₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∈ C₁
he₂ : e ∈ C₂
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
⊢ M.closure I = F

Tactic:
subset_antisymm_iff,

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
⊢ M.closure I ⊆ F ∧ F ⊆ M.closure I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
⊢ ∀ t' ∈ {F | M.IsFlat F ∧ I ∩ M.E ⊆ F}, F ⊆ t'

pp: α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
⊢ F ∈ {F | M.IsFlat F ∧ I ∩ M.E ⊆ F}

Tactic:
·

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
⊢ ∀ t' ∈ {F | M.IsFlat F ∧ I ∩ M.E ⊆ F}, F ⊆ t'
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
this :
  ∀ {α : Type u_1} {M : Matroid α} {e : α} {R : Set α},
    R ⊆ M.E → e ∈ R → ((M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R)
heR : e ∉ R
⊢ (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R

pp: α✝ : Type u_1
M✝ : Matroid α✝
e✝ : α✝
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
heR : e ∈ R
⊢ (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R

Tactic:
·

Goal state after:
case inr
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
this :
  ∀ {α : Type u_1} {M : Matroid α} {e : α} {R : Set α},
    R ⊆ M.E → e ∈ R → ((M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R)
heR : e ∉ R
⊢ (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
hd : M.Dep I
⊢ False

pp: case refine_2
α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
x : α
hx : x ∈ I
⊢ x ∈ M.E

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
hd : M.Dep I
⊢ False
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case pos
α : Type u_1
M : Matroid α
X : Set α
e : α
inst✝ : M.Finitary
he : e ∈ M.closure X
heY : e ∈ X
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I

pp: case neg
α : Type u_1
M : Matroid α
X : Set α
e : α
inst✝ : M.Finitary
he : e ∈ M.closure X
heY : e ∉ X
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I

Tactic:
·

Goal state after:
case pos
α : Type u_1
M : Matroid α
X : Set α
e : α
inst✝ : M.Finitary
he : e ∈ M.closure X
heY : e ∈ X
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inl
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I M₁.loops
⊢ M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)

pp: case inr
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I M₁.loops
⊢ M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)

Tactic:
·

Goal state after:
case inl
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I M₁.loops
⊢ M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: case refine_1
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I : Set β
hI : (M.map f hf).IsBasis I (f '' X)
⊢ lift.{u, v} #↑I ≤ lift.{v, u} (⨆ B, #↑↑B)

pp: case refine_2
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.IsBasis I X
⊢ lift.{v, u} #↑I ≤ lift.{u, v} (⨆ B, #↑↑B)

Tactic:
·

Goal state after:
case refine_1
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
I : Set β
hI : (M.map f hf).IsBasis I (f '' X)
⊢ lift.{u, v} #↑I ≤ lift.{v, u} (⨆ B, #↑↑B)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case inl
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I

pp: case inr
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∉ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I

Tactic:
·

Goal state after:
case inl
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case pos
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)

pp: case neg
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : ¬M.Indep I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)

Tactic:
·

Goal state after:
case pos
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
inst✝ : M.Loopless
hI : ∅.Subsingleton
hIE : ∅ ⊆ M.E
⊢ M.Indep ∅

pp: case inr
α : Type u_1
M : Matroid α
inst✝ : M.Loopless
x : α
hI : {x}.Subsingleton
hIE : {x} ⊆ M.E
⊢ M.Indep {x}

Tactic:
·

Goal state after:
case inl
α : Type u_1
M : Matroid α
inst✝ : M.Loopless
hI : ∅.Subsingleton
hIE : ∅ ⊆ M.E
⊢ M.Indep ∅
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case e'_2
α : Type u_1
M : Matroid α
K✝ K : Set α
⊢ (¬∃ B, M.IsBase B ∧ B ⊆ M.E \ K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty

Tactic:
simp_rw [not_exists, subset_sdiff, not_and, not_disjoint_iff_nonempty_inter, ← and_imp,
    and_iff_left_of_imp IsBase.subset_ground, inter_comm K]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case inl
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
⊢ M.Indep (insert e I \ {e}) ↔ e ∈ M.E \ M.closure (I \ {e}) ∨ e ∈ I

pp: case inr
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
hne : e ≠ f
⊢ M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I

Tactic:
·

Goal state after:
case inl
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
⊢ M.Indep (insert e I \ {e}) ↔ e ∈ M.E \ M.closure (I \ {e}) ∨ e ∈ I
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
x✝ : ∃ x, M.IsCircuit x ∧ x.Subsingleton
hC : M.IsCircuit ∅
hCs : ∅.Subsingleton
⊢ ∃ x ∈ M.E, M.IsLoop x

pp: case inr
α : Type u_1
M : Matroid α
x✝ : ∃ x, M.IsCircuit x ∧ x.Subsingleton
e : α
hC : M.IsCircuit {e}
hCs : {e}.Subsingleton
⊢ ∃ x ∈ M.E, M.IsLoop x

Tactic:
·

Goal state after:
case inl
α : Type u_1
M : Matroid α
x✝ : ∃ x, M.IsCircuit x ∧ x.Subsingleton
hC : M.IsCircuit ∅
hCs : ∅.Subsingleton
⊢ ∃ x ∈ M.E, M.IsLoop x
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: case refine_1
α : Type u
β : Type v
M : Matroid β
f : α → β
X I : Set α
hI : M.IsBasis' (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
⊢ lift.{v, u} #↑I ≤ lift.{u, v} (⨆ B, #↑↑B)

pp: case refine_2
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
⊢ lift.{u, v} #↑I ≤ lift.{v, u} (⨆ B, #↑↑B)

Tactic:
·

Goal state after:
case refine_1
α : Type u
β : Type v
M : Matroid β
f : α → β
X I : Set α
hI : M.IsBasis' (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
⊢ lift.{v, u} #↑I ≤ lift.{u, v} (⨆ B, #↑↑B)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case inl
α : Type u_2
M : Matroid α
f : α
B : Set α
hB : M.IsBase B
hfE : f ∈ M.E
he : f ∈ B
hf : f ∉ M.closure (B \ {f})
⊢ M.IsBase (insert f (B \ {f}))

pp: case inr
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : f ∈ M.E
hne : f ≠ e
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
·

Goal state after:
case inl
α : Type u_2
M : Matroid α
f : α
B : Set α
hB : M.IsBase B
hfE : f ∈ M.E
he : f ∈ B
hf : f ∉ M.closure (B \ {f})
⊢ M.IsBase (insert f (B \ {f}))
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊆ I
hJ : M.Indep J
⊢ M.closure J ∩ I = J

Tactic:
subset_antisymm_iff,

Goal state after:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊆ I
hJ : M.Indep J
⊢ M.closure J ∩ I ⊆ J ∧ J ⊆ M.closure J ∩ I
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.removeLoops.Indep = M.Indep

Tactic:
by
  ext I
  rw [removeLoops_eq_restrict, restrict_indep_iff, and_iff_left_iff_imp]
  exact fun h e ↦ h.isNonloop_of_mem

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
⊢ M.closure (⋂₀ Js) = ⋂ J ∈ Js, M.closure J

Tactic:
subset_antisymm_iff,

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
⊢ M.closure (⋂₀ Js) ⊆ ⋂ J ∈ Js, M.closure J ∧ ⋂ J ∈ Js, M.closure J ⊆ M.closure (⋂₀ Js)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
I J X : Set α
inst✝ : M.InvariantCardinalRank
hIX : M.IsBasis I X
hJX : M.IsBasis J X
⊢ #↑(J \ I) + #↑(I ∩ J) = #↑J

Tactic:
← mk_union_of_disjoint (disjoint_sdiff_left.mono_right inter_subset_left),

Goal state after:
α : Type u
M : Matroid α
I J X : Set α
inst✝ : M.InvariantCardinalRank
hIX : M.IsBasis I X
hJX : M.IsBasis J X
⊢ #↑(J \ I ∪ I ∩ J) = #↑J
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.closure (M.E \ K ∪ {e}) ⊆ M.closure (M.E \ K)

pp: α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ {e} ⊆ M.E

Tactic:
·

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.closure (M.E \ K ∪ {e}) ⊆ M.closure (M.E \ K)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.closure i
he' : e ∉ M.closure (⋂₀ Js)
⊢ False

Tactic:
have heEI : e ∈ M.E \ I := by
    refine ⟨M.closure_subset_ground _ (he _ hne.some_mem), fun heI ↦ he' ?_⟩
    refine mem_closure_of_mem _ (fun X hX' ↦ ?_) hiI.subset_ground
    rw [← hI.closure_inter_eq_self_of_subset (hIs X hX')]
    exact ⟨he X hX', heI⟩

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.closure i
he' : e ∉ M.closure (⋂₀ Js)
heEI : e ∈ M.E \ I
⊢ False
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: case hC
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := ⋯
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R := ⋯
v : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R := ⋯
hf : Function.Injective ⇑u
h1 :
  Polynomial.aeval (X i) =
    ((supported R (insert i s)).val.comp ↑(supportedEquivMvPolynomial (insert i s)).symm).comp
      (Polynomial.aeval (X ⟨i, ⋯⟩))
⊢ ((((supported R (insert i s)).val.comp
                  ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                      (supportedEquivMvPolynomial (insert i s)).symm)).comp
              (mapAlgHom (Polynomial.aeval f))).comp
          ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s))).comp
      CAlgHom =
    ((AlgHom.restrictScalars R (Polynomial.aeval ((Polynomial.aeval (X i)) f))).comp
          ↑(Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm)).comp
      CAlgHom

pp: case hX
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := ⋯
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R := ⋯
v : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R := ⋯
hf : Function.Injective ⇑u
h1 :
  Polynomial.aeval (X i) =
    ((supported R (insert i s)).val.comp ↑(supportedEquivMvPolynomial (insert i s)).symm).comp
      (Polynomial.aeval (X ⟨i, ⋯⟩))
⊢ ((((supported R (insert i s)).val.comp
                ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                    (supportedEquivMvPolynomial (insert i s)).symm)).comp
            (mapAlgHom (Polynomial.aeval f))).comp
        ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s)))
      Polynomial.X =
    ((AlgHom.restrictScalars R (Polynomial.aeval ((Polynomial.aeval (X i)) f))).comp
        ↑(Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm))
      Polynomial.X

Tactic:
·

Goal state after:
case hC
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := ⋯
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R := ⋯
v : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R := ⋯
hf : Function.Injective ⇑u
h1 :
  Polynomial.aeval (X i) =
    ((supported R (insert i s)).val.comp ↑(supportedEquivMvPolynomial (insert i s)).symm).comp
      (Polynomial.aeval (X ⟨i, ⋯⟩))
⊢ ((((supported R (insert i s)).val.comp
                  ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                      (supportedEquivMvPolynomial (insert i s)).symm)).comp
              (mapAlgHom (Polynomial.aeval f))).comp
          ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s))).comp
      CAlgHom =
    ((AlgHom.restrictScalars R (Polynomial.aeval ((Polynomial.aeval (X i)) f))).comp
          ↑(Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm)).comp
      CAlgHom
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: case pos
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : (B' \ B).Finite
⊢ #↑(B \ B') ≤ #↑(B' \ B)

pp: case neg
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : ¬(B' \ B).Finite
⊢ #↑(B \ B') ≤ #↑(B' \ B)

Tactic:
·

Goal state after:
case pos
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : (B' \ B).Finite
⊢ #↑(B \ B') ≤ #↑(B' \ B)
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: case hC
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := mapAlgHom (Polynomial.aeval f)
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (((supported R (insert i s)).val.comp
            ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                (supportedEquivMvPolynomial (insert i s)).symm)).comp
        g).comp
    ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s))
v : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.restrictScalars R (Polynomial.aeval ((Polynomial.aeval (X i)) f))).comp
    ↑(Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm)
hf : Function.Injective ⇑u
h1 :
  Polynomial.aeval (X i) =
    ((supported R (insert i s)).val.comp ↑(supportedEquivMvPolynomial (insert i s)).symm).comp
      (Polynomial.aeval (X ⟨i, ⋯⟩))
i✝ : ↑s
⊢ (((((supported R (insert i s)).val.comp
                    ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                        (supportedEquivMvPolynomial (insert i s)).symm)).comp
                (mapAlgHom (Polynomial.aeval f))).comp
            ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s))).comp
        CAlgHom)
      (X i✝) =
    (((AlgHom.restrictScalars R (Polynomial.aeval ((Polynomial.aeval (X i)) f))).comp
            ↑(Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm)).comp
        CAlgHom)
      (X i✝)

Tactic:
simp [Set.subtypeInsertEquivOption, Subalgebra.algebraMap_eq, optionEquivLeft_symm_apply]

Goal state after:
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: case hX
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := ⋯
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R := ⋯
v : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R := ⋯
hf : Function.Injective ⇑u
h1 :
  Polynomial.aeval (X i) =
    ((supported R (insert i s)).val.comp ↑(supportedEquivMvPolynomial (insert i s)).symm).comp
      (Polynomial.aeval (X ⟨i, ⋯⟩))
⊢ ((((supported R (insert i s)).val.comp
                ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                    (supportedEquivMvPolynomial (insert i s)).symm)).comp
            (mapAlgHom (Polynomial.aeval f))).comp
        ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s)))
      Polynomial.X =
    ((AlgHom.restrictScalars R (Polynomial.aeval ((Polynomial.aeval (X i)) f))).comp
        ↑(Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm))
      Polynomial.X

Tactic:
·

Goal state after:
case hX
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := ⋯
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R := ⋯
v : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R := ⋯
hf : Function.Injective ⇑u
h1 :
  Polynomial.aeval (X i) =
    ((supported R (insert i s)).val.comp ↑(supportedEquivMvPolynomial (insert i s)).symm).comp
      (Polynomial.aeval (X ⟨i, ⋯⟩))
⊢ ((((supported R (insert i s)).val.comp
                ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                    (supportedEquivMvPolynomial (insert i s)).symm)).comp
            (mapAlgHom (Polynomial.aeval f))).comp
        ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s)))
      Polynomial.X =
    ((AlgHom.restrictScalars R (Polynomial.aeval ((Polynomial.aeval (X i)) f))).comp
        ↑(Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm))
      Polynomial.X