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

Goal state before:
pp: case refine_4
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
⊢ Disjoint J B'

Tactic:
obtain ⟨B₁, hB₁, hI'B₁, hB₁I⟩ := (hB'.indep.subset hI').exists_isBase_subset_union_isBase hB''

Goal state after:
case refine_4
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∩ X ∪ B' \ X ∪ B''
⊢ Disjoint J B'
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E B I : Set α
hIE : I ⊆ E
⊢ (uniqueBaseOn I E).IsBase B ↔ B = I

Tactic:
uniqueBaseOn,

Goal state after:
α : Type u_1
E B I : Set α
hIE : I ⊆ E
⊢ (freeOn I ↾ E).IsBase B ↔ B = I
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I J : Set α
⊢ (uniqueBaseOn I E).Indep J ↔ J ⊆ I ∩ E

Tactic:
uniqueBaseOn,

Goal state after:
α : Type u_1
E I J : Set α
⊢ (freeOn I ↾ E).Indep J ↔ J ⊆ I ∩ E
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I J : Set α
hIE : I ⊆ E
⊢ (uniqueBaseOn I E).Indep J ↔ J ⊆ I

Tactic:
uniqueBaseOn,

Goal state after:
α : Type u_1
E I J : Set α
hIE : I ⊆ E
⊢ (freeOn I ↾ E).Indep J ↔ J ⊆ I
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
⊢ (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite

Tactic:
rw [finite_iff_bddAbove, bddAbove_def]

Goal state after:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
⊢ ∃ x, ∀ y ∈ ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, y ≤ x
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
I : Set α
⊢ uniqueBaseOn I I = freeOn I

Tactic:
uniqueBaseOn,

Goal state after:
α : Type u_1
I : Set α
⊢ freeOn I ↾ I = freeOn I
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ {B | M✶.IsBase B} = (fun X ↦ M.E \ X) '' {B | M.IsBase B}

Tactic:
ext B

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
⊢ B ∈ {B | M✶.IsBase B} ↔ B ∈ (fun X ↦ M.E \ X) '' {B | M.IsBase B}
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N ≤r M
⊢ N.E ⊆ M.E

Tactic:
by
  obtain ⟨R, hR, rfl⟩ := h; exact hR

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J : Set β
hIJ : I ⊆ f ⁻¹' J
hJ : N.Indep J
hJf : J ⊆ range f
hJX : J ⊆ f '' X
hJmax : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t
J₀ : Set α
hIJ₀ : I ⊆ J₀
hJ₀X : J₀ ⊆ X
hbj : BijOn f J₀ (f '' f ⁻¹' J)
⊢ f '' J₀ = J

Tactic:
← image_preimage_eq_of_subset hJf,

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J : Set β
hIJ : I ⊆ f ⁻¹' J
hJ : N.Indep J
hJf : J ⊆ range f
hJX : J ⊆ f '' X
hJmax : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → J ⊆ t → J = t
J₀ : Set α
hIJ₀ : I ⊆ J₀
hJ₀X : J₀ ⊆ X
hbj : BijOn f J₀ (f '' f ⁻¹' J)
⊢ f '' J₀ = f '' f ⁻¹' J
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
⊢ B ∩ X ⊆ B \ {e}

Tactic:
simp_rw [subset_sdiff, and_iff_right inter_subset_left, disjoint_singleton_right,
      mem_inter_iff, iff_false_intro he.1.2, and_false, not_false_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E
I : Set α
⊢ (IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).Indep I ↔
    ∀ (J : Finset α), ↑J ⊆ I → Indep J

Tactic:
by
  simp only [IndepMatroid.ofFinset, ofFinitaryCardAugment_indep]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
B : Set α
⊢ (N.comap f).IsBase B ↔ N.IsBasis (f '' B) (f '' f ⁻¹' N.E) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E

Tactic:
rw [← isBasis_ground_iff, comap_isBasis_iff]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
B : Set α
⊢ N.IsBasis (f '' B) (f '' (N.comap f).E) ∧ InjOn f B ∧ B ⊆ (N.comap f).E ↔
    N.IsBasis (f '' B) (f '' f ⁻¹' N.E) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y J : Set α
hI : M.IsBasis I X
hJ : M.IsBasis J Y
hJX : J ⊆ X
hIY : I ⊆ Y
⊢ M.IsBasis I Y

Tactic:
have hI' := hI.isBasis_subset (subset_inter hI.subset hIY) inter_subset_left
  have hJ' := hJ.isBasis_subset (subset_inter hJX hJ.subset) inter_subset_right
  exact hI'.transfer hJ' inter_subset_right hJ

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬M.IsBasis I X
hJ : M.IsBasis J X
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)

Tactic:
rw [← isBase_restrict_iff] at hI'; rw [← isBase_restrict_iff] at hJ
  obtain ⟨e, he, hi⟩ := (hI.indep_restrict_of_subset hIX).exists_insert_of_not_isBase hI' hJ
  exact ⟨e, he, (restrict_indep_iff.mp hi).1⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ N.IsBase (f '' ((N.comapOn E f).E \ B)) ∧ (N.comapOn E f).E \ B ⊆ E ↔ N✶.IsBase (f '' B) ∧ B ⊆ E

Tactic:
dual_isBase_iff _,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ N.IsBase (f '' ((N.comapOn E f).E \ B)) ∧ (N.comapOn E f).E \ B ⊆ E ↔ N.IsBase (N.E \ f '' B) ∧ B ⊆ E

α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ f '' B ⊆ N.E
Module: Mathlib.Combinatorics.Matroid.Rank.Finite

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
⊢ M.IsRkFinite (Y \ X) ↔ M.IsRkFinite Y

Tactic:
rw [← hX.isRkFinite_union_iff, union_sdiff_self, hX.isRkFinite_union_iff]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C X : Set α
hC : M.IsCircuit C
hXC : X ⊂ C
⊢ M.Indep X

Tactic:
rw [← not_dep_iff (hXC.subset.trans hC.subset_ground)]
  exact fun h ↦ hXC.ne ((isCircuit_iff.1 hC).2 h hXC.subset)

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
⊢ ¬M.Indep {e} ∧ e ∈ M.E ↔ (∀ (x : Set α), M.IsBase x → e ∈ M.E) ∧ ∀ (x : Set α), M.IsBase x → e ∉ x

Tactic:
refine ⟨fun h ↦ ⟨fun _ _ ↦ h.2, fun B hB heB ↦ h.1 (hB.indep.subset (by simpa))⟩,
      fun h ↦ ⟨fun hi ↦ ?_, h.1 _ M.exists_isBase.choose_spec⟩⟩

Goal state after:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
h : (∀ (x : Set α), M.IsBase x → e ∈ M.E) ∧ ∀ (x : Set α), M.IsBase x → e ∉ x
hi : M.Indep {e}
⊢ False
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set β
⊢ (M.mapEquiv f).IsBasis I X ↔ M.IsBasis (⇑f.symm '' I) (⇑f.symm '' X)

Tactic:
by
  rw [mapEquiv_eq_map, map_isBasis_iff']
  refine ⟨fun h ↦ ?_, fun h ↦ ⟨_, _, h, by simp, by simp⟩⟩
  obtain ⟨I, X, hIX, rfl, rfl⟩ := h
  simpa

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk (X ∪ M.E) = M.eRank

Tactic:
eRk_union_ground

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRank = M.eRank
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ Ii.encard + M.eRk (IX ∪ IY) ≤ IX.encard + IY.encard

Tactic:
← encard_union_add_encard_inter,

Goal state after:
α : Type u_1
M : Matroid α
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ Ii.encard + M.eRk (IX ∪ IY) ≤ (IX ∪ IY).encard + (IX ∩ IY).encard
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
h : M.eRk X < M.eRk Y
⊢ ∃ y ∈ Y \ X, M.eRk (insert y X) = M.eRk X + 1

Tactic:
have hz : ¬ Y ∩ M.E ⊆ M.closure X := by
    contrapose! h
    simpa using M.eRk_mono h

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
h : M.eRk X < M.eRk Y
hz : ¬Y ∩ M.E ⊆ M.closure X
⊢ ∃ y ∈ Y \ X, M.eRk (insert y X) = M.eRk X + 1
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
x : α
hx he : x ∈ M.E
h : x ∈ M.closure (M.E \ {x})
⊢ x ∈ M.closure (M.E \ {x})

pp: case inr
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
h : e ∈ M.closure (M.E \ {e})
x : α
hx : x ∈ M.E
hne : x ≠ e
⊢ x ∈ M.closure (M.E \ {e})

Tactic:
· assumption

Goal state after:
case inr
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
h : e ∈ M.closure (M.E \ {e})
x : α
hx : x ∈ M.E
hne : x ≠ e
⊢ x ∈ M.closure (M.E \ {e})
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
⊢ ¬M.Indep (insert x I) ∧ x ∈ M.E ∧ I ⊆ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)

Tactic:
and_iff_left hI.subset_ground,

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
⊢ ¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
rw [hI.mem_closure_iff, dep_iff, insert_subset_iff, and_iff_left hI.subset_ground,
    imp_iff_not_or]

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
⊢ ¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (¬M.Indep (insert x I) ∨ x ∈ I)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
⊢ lift.{u, v} ((M.map f hf).cRk (f '' X)) = lift.{v, u} (M.cRk X)

Tactic:
nth_rw 1 [cRk, cRank, le_antisymm_iff, lift_iSup bddAbove_of_small, cRk, cRank, cRk, cRank]
  nth_rw 2 [lift_iSup bddAbove_of_small]
  simp only [ciSup_le_iff bddAbove_of_small, Subtype.forall, isBase_restrict_iff',
    isBasis'_iff_isBasis hX, isBasis'_iff_isBasis (show f '' X ⊆ (M.map f hf).E from image_mono hX)]
  refine ⟨fun I hI ↦ ?_, fun I hI ↦ ?_⟩
  · obtain ⟨I, X', hIX, rfl, hXX'⟩ := map_isBasis_iff'.1 hI
    rw [mk_image_eq_of_injOn_lift _ _ (hf.mono hIX.indep.subset_ground), lift_le]
    obtain rfl : X = X' := by rwa [hf.image_eq_image_iff hX hIX.subset_ground] at hXX'
    exact hIX.cardinalMk_le_cRk
  rw [← mk_image_eq_of_injOn_lift _ _ (hf.mono hI.indep.subset_ground), lift_le]
  exact (hI.map hf).cardinalMk_le_cRk

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

Goal state before:
pp: α : Type u_1
M : Matroid α
K : Set α
⊢ M.IsCocircuit K ↔ Minimal (fun X ↦ ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K

Tactic:
have aux : M✶.Dep = fun X ↦ (∀ B, M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E := by
    ext; apply dual_dep_iff_forall
  rw [isCocircuit_def, isCircuit_def, aux, iff_comm]
  refine minimal_iff_minimal_of_imp_of_forall (fun _ h ↦ h.1) fun X hX ↦
    ⟨X ∩ M.E, inter_subset_left, fun B hB ↦ ?_, inter_subset_right⟩
  rw [inter_assoc, inter_eq_self_of_subset_right hB.subset_ground]
  exact hX B hB

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

Goal state before:
pp: α : Type u_1
E : Set α
⊢ (loopyOn E).Loopless ↔ E = ∅

Tactic:
by
  simp [loopless_iff_forall_not_isLoop, eq_empty_iff_forall_notMem]

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

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

Tactic:
ext B

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
⊢ M.removeLoops.IsBase B ↔ M.IsBase B
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y

Tactic:
← cRk_union_closure_eq,

Goal state after:
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ M.cRk (X ∩ Y) + M.cRk (M.closure X ∪ M.closure Y) ≤ M.cRk X + M.cRk Y
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : 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'
⊢ #↑(B \ B') ≤ #↑(B' \ B)

Tactic:
by_cases h : (B' \ B).Finite

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)

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)
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)

Tactic:
← cast_ncard h,

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).ncard
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:
· simp [Set.subtypeInsertEquivOption, h1, optionEquivLeft_symm_apply]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
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 : Infinite ↑(B' \ B)
S : (a : α) → a ∈ B' \ B → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite ↑(S a ha)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ a, S ↑a ⋯
⊢ B \ B' ⊆ U

Tactic:
rw [← sdiff_inter_self_eq_sdiff, sdiff_subset_iff, inter_comm]

Goal state after:
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 : Infinite ↑(B' \ B)
S : (a : α) → a ∈ B' \ B → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite ↑(S a ha)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ a, S ↑a ⋯
⊢ B ⊆ B ∩ B' ∪ U
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
I E X : Set α
⊢ (uniqueBaseOn I E).closure X = X ∩ I ∩ E ∪ E \ I

Tactic:
uniqueBaseOn,

Goal state after:
α : Type u_2
I E X : Set α
⊢ (freeOn I ↾ E).closure X = X ∩ I ∩ E ∪ E \ I
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
⊢ ∃ u, s ⊆ u ∧ Maximal (fun x ↦ AlgebraicIndepOn R _root_.id x ∧ x ⊆ t) u

Tactic:
by
  refine zorn_subset_nonempty { u : Set A | AlgebraicIndependent R ((↑) : u → A) ∧ u ⊆ t}
    (fun c hc chainc hcn ↦ ⟨⋃₀ c, ⟨?_, ?_⟩, fun _ ↦ subset_sUnion_of_mem⟩) s ⟨hs, hst⟩
  · exact algebraicIndependent_sUnion_of_directed hcn chainc.directedOn (fun x hxc ↦ (hc hxc).1)
  exact fun x ⟨w, hyc, hwy⟩ ↦ (hc hyc).2 hwy

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
hs : AlgebraicIndepOn R _root_.id s
⊢ ∃ t, s ⊆ t ∧ IsTranscendenceBasis R Subtype.val

Tactic:
by
  simpa [← isTranscendenceBasis_iff_maximal]
    using exists_maximal_algebraicIndependent s _ (subset_univ _) hs

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
x✝ : IsEmpty ι
⊢ Algebra.IsAlgebraic R A

Tactic:
have := hx.isAlgebraic

Goal state after:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
x✝ : IsEmpty ι
this : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
⊢ Algebra.IsAlgebraic R A
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
F : Type u_2
E : Type u_3
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : IsTranscendenceBasis F x
⊢ Algebra.IsAlgebraic (↥(IntermediateField.adjoin F (range x))) E

Tactic:
have := hx.isAlgebraic

Goal state after:
ι : Type u
F : Type u_2
E : Type u_3
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (range x))) E
⊢ Algebra.IsAlgebraic (↥(IntermediateField.adjoin F (range x))) E
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inl
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : IsTranscendenceBasis R Subtype.val
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
h✝ : Subsingleton R
⊢ IsTranscendenceBasis R Subtype.val

Tactic:
rw [isTranscendenceBasis_iff_of_subsingleton] at B_base ⊢

Goal state after:
case inl
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : Nonempty { x // x ∈ B }
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
h✝ : Subsingleton R
⊢ Nonempty { x // x ∈ I }
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : IsDomain A
inst✝ : FaithfulSMul R A
s : Set A
⊢ (matroid R A).Spanning s ↔ ∃ t ⊆ s, (matroid R A).IsBase t

Tactic:
and_comm (a := _ ⊆ s)

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : IsDomain A
inst✝ : FaithfulSMul R A
s : Set A
⊢ (matroid R A).Spanning s ↔ ∃ t, (matroid R A).IsBase t ∧ t ⊆ s
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ (aeval (rootOfSplits ⋯ ⋯)) f = 0

Tactic:
simp only [← eval_map_algebraMap, eval_rootOfSplits]

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
eq : v i = v j
x : ι
hxj : x ∉ {j}
hxi : x ∈ s
⊢ v ↑⟨x, ⋯⟩ = ((fun x ↦ v ↑x) ∘ ⇑((Equiv.image (Equiv.swap j i) s).trans (Equiv.setCongr ⋯)).symm) ⟨x, ⋯⟩

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne hxj (ne_of_mem_of_not_mem hxi hi)]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝¹ : Field F
q : ℕ
inst✝ : ExpChar F q
n : ℕ
y : F
⊢ (X - C y).natSepDegree = 1

Tactic:
natSepDegree_X_sub_C

Goal state after:
F : Type u
inst✝¹ : Field F
q : ℕ
inst✝ : ExpChar F q
n : ℕ
y : F
⊢ 1 = 1
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_2
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
x✝ : ∃ n y, f = (expand F (q ^ n)) (X - C y)
n : ℕ
y : F
h : f = (expand F (q ^ n)) (X - C y)
⊢ (X - C y).natSepDegree = 1

Tactic:
natSepDegree_X_sub_C

Goal state after:
case refine_2
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
x✝ : ∃ n y, f = (expand F (q ^ n)) (X - C y)
n : ℕ
y : F
h : f = (expand F (q ^ n)) (X - C y)
⊢ 1 = 1