mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
I✝ : ClassGroup R
hI✝ : ∀ (y : ClassGroup R), y = I✝
eq_one : ∀ (J : ClassGroup R), J = 1
I : Ideal R
hI : ¬I = ⊥
⊢ Submodule.IsPrincipal I

Tactic:
· exact (ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_iff_ne_zero.mpr hI)).mp (eq_one _)

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: case h'
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := ⋯
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := ⋯
Mₚ : Type (max uR uM) := ⋯
this✝¹ : Algebra (Localization S) Rₚ := ⋯
this✝ : IsScalarTower R (Localization S) Rₚ
this : IsLocalization (Submonoid.map (algebraMap R (Localization S)) p'.primeCompl) Rₚ
⊢ ∀ (x : ↥p.asIdeal.primeCompl), ∃ m, m * ↑x ∈ Submonoid.map (algebraMap R (Localization S)) p'.primeCompl

Tactic:
rintro ⟨x, hx⟩

Goal state after:
case h'
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝¹ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝ : IsScalarTower R (Localization S) Rₚ
this : IsLocalization (Submonoid.map (algebraMap R (Localization S)) p'.primeCompl) Rₚ
x : Localization S
hx : x ∈ p.asIdeal.primeCompl
⊢ ∃ m, m * ↑⟨x, hx⟩ ∈ Submonoid.map (algebraMap R (Localization S)) p'.primeCompl
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: case h'
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := ⋯
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := ⋯
Mₚ : Type (max uR uM) := ⋯
this✝⁶ : Algebra (Localization S) Rₚ := ⋯
this✝⁵ : IsScalarTower R (Localization S) Rₚ
this✝⁴ : IsLocalization.AtPrime Rₚ p.asIdeal
this✝³ : Module (Localization S) Mₚ := ⋯
this✝² : IsScalarTower R (Localization S) Mₚ
this✝¹ : IsScalarTower (Localization S) Rₚ Mₚ
l : LocalizedModule S M →ₗ[Localization S] LocalizedModule p'.primeCompl M := ⋯
this✝ : IsLocalizedModule p'.primeCompl (↑R l)
this : IsLocalizedModule (Algebra.algebraMapSubmonoid (Localization S) p'.primeCompl) l
⊢ ∀ (x : ↥p.asIdeal.primeCompl), ∃ m, m * ↑x ∈ Algebra.algebraMapSubmonoid (Localization S) p'.primeCompl

Tactic:
rintro ⟨x, hx⟩

Goal state after:
case h'
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝⁶ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝⁵ : IsScalarTower R (Localization S) Rₚ
this✝⁴ : IsLocalization.AtPrime Rₚ p.asIdeal
this✝³ : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
this✝² : IsScalarTower R (Localization S) Mₚ
this✝¹ : IsScalarTower (Localization S) Rₚ Mₚ
l : LocalizedModule S M →ₗ[Localization S] LocalizedModule p'.primeCompl M :=
  LinearMap.extendScalarsOfIsLocalization S (Localization S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
this✝ : IsLocalizedModule p'.primeCompl (↑R l)
this : IsLocalizedModule (Algebra.algebraMapSubmonoid (Localization S) p'.primeCompl) l
x : Localization S
hx : x ∈ p.asIdeal.primeCompl
⊢ ∃ m, m * ↑⟨x, hx⟩ ∈ Algebra.algebraMapSubmonoid (Localization S) p'.primeCompl
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case ind
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
⊢ IsSolvable ↥H

Tactic:
| ind H hH
   => 

Goal state after:
case ind
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
⊢ IsSolvable ↥H
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : Group.IsSolvable (Perm X)
⊢ Cardinal.lift.{max ?u.26 u_3, 0} (Cardinal.mk (Fin 5)) ≤ Cardinal.lift.{?u.26, u_3} (Cardinal.mk X)

Tactic:
Cardinal.mk_fin,

Goal state after:
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : Group.IsSolvable (Perm X)
⊢ Cardinal.lift.{max ?u.26 u_3, 0} ↑5 ≤ Cardinal.lift.{?u.26, u_3} (Cardinal.mk X)
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: F✝ : Type u_1
K✝ : Type u_2
inst✝¹² : Field F✝
inst✝¹¹ : Field K✝
inst✝¹⁰ : Algebra F✝ K✝
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst✝⁹ : Field K₁
inst✝⁸ : Field K₂
inst✝⁷ : Field K₃
inst✝⁶ : Algebra F✝ K₁
inst✝⁵ : Algebra F✝ K₂
inst✝⁴ : Algebra F✝ K₃
ϕ : K₁ →ₐ[F✝] K₂
χ : K₁ ≃ₐ[F✝] K₂
ψ : K₂ →ₐ[F✝] K₃
ω : K₂ ≃ₐ[F✝] K₃
F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
⊢ ∀ (x : K), (map (algebraMap F K) (minpoly F x)).Splits

Tactic:
by
    intro x
    obtain h | h := le_iff_lt_or_eq.mp (finrank_eq_two F K ▸ minpoly.natDegree_le x)
    · exact Splits.of_natDegree_le_one <| natDegree_map_le.trans (by rwa [Nat.le_iff_lt_add_one])
    · exact Splits.of_natDegree_eq_two ((natDegree_map _).trans h)
        ((eval_map_algebraMap _ _).trans (minpoly.aeval F x))

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ ¬M.RankInfinite ↔ M.RankFinite

Tactic:
rw [← not_rankFinite_iff, not_not]

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case inl
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
F_inf : IsEmpty (Fintype F)
⊢ ∃ α, F⟮α⟯ = ⊤

Tactic:
let P : IntermediateField F E → Prop := fun K => ∃ α : E, F⟮α⟯ = K

Goal state after:
case inl
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
F_inf : IsEmpty (Fintype F)
P : IntermediateField F E → Prop := fun K ↦ ∃ α, F⟮α⟯ = K
⊢ ∃ α, F⟮α⟯ = ⊤
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M.IsBasis (B' ∩ (R ∩ M.E)) (R ∩ M.E)
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R

Tactic:
rw [hB'.inter_isBasis_iff_compl_inter_isBasis_dual, sdiff_inter_sdiff] at hI'

Goal state after:
α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
⊢ B ⊆ R ∩ M.E ∪ B'

Tactic:
exact hBIB'.trans (union_subset_union_left _ (subset_inter hIY hI.subset_ground))

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.IsBase ∅ ↔ M = loopyOn M.E

Tactic:
simp only [isBase_iff_maximal_indep, Maximal, empty_indep, empty_subset,
    subset_empty_iff, true_implies, true_and, ext_iff_indep, loopyOn_ground,
    loopyOn_indep_iff]

Goal state after:
α : Type u_1
M : Matroid α
⊢ (∀ ⦃y : Set α⦄, M.Indep y → y = ∅) ↔ ∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
⊢ M ↾ I = freeOn I ↔ M.Indep I

Tactic:
eq_freeOn_iff,

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
⊢ (M ↾ I).E = I ∧ (M ↾ I).Indep I ↔ M.Indep I
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: case h
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
I : Set α
hI : P I
hIX : I ⊆ X
hP : ∀ (Y : Set α), P Y → ∃ n₀, Y.encard = ↑n₀ ∧ n₀ ≤ n
Y : Set α
hY : P Y
n₀ : ℕ
heq : Y.encard = ↑n₀
hle : n₀ ≤ n
⊢ (↑n₀).toNat ≤ n

Tactic:
ENat.toNat_natCast

Goal state after:
case h
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
I : Set α
hI : P I
hIX : I ⊆ X
hP : ∀ (Y : Set α), P Y → ∃ n₀, Y.encard = ↑n₀ ∧ n₀ ≤ n
Y : Set α
hY : P Y
n₀ : ℕ
heq : Y.encard = ↑n₀
hle : n₀ ≤ n
⊢ n₀ ≤ n
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ M✶.IsBase B ↔ M.IsBase (M.E \ B)

Tactic:
by
  rw [isBase_compl_iff_maximal_disjoint_isBase, isBase_iff_maximal_indep, maximal_subset_iff,
    maximal_subset_iff]
  simp [dual_indep_iff_exists', hB]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
h : M✶.RankPos
⊢ ¬M.IsBase M.E

Tactic:
by
  rwa [rankPos_iff, dual_isBase_iff, sdiff_empty] at h

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y J : Set α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
hXY : X ⊆ Y
hJY : M.IsBasis J Y
⊢ (M ↾ Y).IsBase I

Tactic:
rw [← isBase_restrict_iff] at hJY

Goal state after:
α : Type u_1
M : Matroid α
I X Y J : Set α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
hXY : X ⊆ Y
hJY : (M ↾ Y).IsBase J
⊢ (M ↾ Y).IsBase I
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
hB : IsBase B
hfin : B.Finite
X : Set α
x✝¹ : X ⊆ E
Y : Set α
x✝ : ∃ B, IsBase B ∧ Y ⊆ B
B' : Set α
hB' : IsBase B'
hYB' : Y ⊆ B'
⊢ Y.encard ≤ B'.encard

Tactic:
exact encard_mono hYB'

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 β
inst✝ : N.Finitary
f : α → β
⊢ (N.comap f).Finitary

Tactic:
refine ⟨fun I hI ↦ ?_⟩
  rw [comap_indep_iff, indep_iff_forall_finite_subset_indep]
  simp only [forall_subset_image_iff]
  refine ⟨fun J hJ hfin ↦ ?_,
    fun x hx y hy ↦ (hI _ (pair_subset hx hy) (by simp)).2 (by simp) (by simp)⟩
  obtain ⟨J', hJ'J, hJ'⟩ := (surjOn_image f J).exists_bijOn_subset
  rw [← hJ'.image_eq] at hfin ⊢
  exact (hI J' (hJ'J.trans hJ) (hfin.of_finite_image hJ'.injOn)).1

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure (X \ M.loops) = M.closure X

Tactic:
by
  rw [← M.closure_union_loops_eq (X \ M.loops), sdiff_union_self, ← closure_empty,
    closure_union_closure_right_eq, union_empty]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
⊢ [M.IsColoop e, e ∈ M.coloops, M.IsCocircuit {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B,
      (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E, ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X,
      ¬M.Spanning (M.E \ {e})].TFAE

Tactic:
tfae_have 1 ↔ 7 := by
    wlog he : e ∈ M.E
    · exact iff_of_false (fun h ↦ he h.mem_ground) <| by simp [he, M.ground_spanning]
    rw [spanning_iff_compl_coindep sdiff_subset, ← dual_isLoop_iff_isColoop, ← singleton_dep,
      sdiff_sdiff_cancel_left (by simpa), ← not_indep_iff (by simpa)]

Goal state after:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
tfae_1_iff_7 : M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})
⊢ [M.IsColoop e, e ∈ M.coloops, M.IsCocircuit {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B,
      (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E, ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X,
      ¬M.Spanning (M.E \ {e})].TFAE
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_3
α : 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), ↑i ∈ C ↑i

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:
· simp only [Subtype.forall, ← singleton_subset_iff (s := C _)]
    exact fun e heX ↦ by simp [← hC.2 e heX]

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'

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
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
X Y : Set α
⊢ (loopyOn Y).eRk X = 0

Tactic:
obtain ⟨I, hI⟩ := (loopyOn Y).exists_isBasis' X
  rw [hI.eRk_eq_encard, loopyOn_indep_iff.1 hI.indep, encard_empty]

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

Goal state before:
pp: α : Type u_1
X : Set α
⊢ (freeOn X).eRank = X.encard

Tactic:
by
  rw [eRank_def, freeOn_ground, (freeOn_indep_iff.2 rfl.subset).eRk_eq_encard]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X Y X' : Set α
h : M.closure X = M.closure X'
⊢ M.closure (X ∪ Y) = M.closure (X' ∪ Y)

Tactic:
rw [← M.closure_union_closure_left_eq, h, M.closure_union_closure_left_eq]

Goal state after:
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
F' : Set α
hF' : M.IsFlat F'
hIF' : I ∩ M.E ⊆ F'
e : α
he : M.IsBasis I (insert e I)
⊢ e ∈ F'

Tactic:
rw [inter_eq_left.mpr (hIF.subset.trans hIF.subset_ground)] at hIF'

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
F' : Set α
hF' : M.IsFlat F'
hIF' : I ⊆ F'
e : α
he : M.IsBasis I (insert e I)
⊢ e ∈ F'
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
by_cases hI : M.Indep I
  · rw [hI.insert_indep_iff, and_iff_right hI, or_iff_not_imp_right]
  simp [hI, show ¬ M.Indep (insert e I) from fun h ↦ hI <| h.subset <| subset_insert _ _]

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

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

Tactic:
simp [loopless_iff_forall_not_isLoop, eq_empty_iff_forall_notMem]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
X : Set α
he : e ∉ M.E
⊢ M.fundCocircuit e X = {e}

Tactic:
rwa [fundCocircuit, fundCircuit_eq_of_notMem_ground]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I J : Set α
h : M.Indep (I ∪ J)
⊢ M.closure (⋂ b, bif b then I else J) = M.closure I ∩ M.closure J

Tactic:
closure_iInter_eq_iInter_closure_of_iUnion_indep,

Goal state after:
α : Type u_2
M : Matroid α
I J : Set α
h : M.Indep (I ∪ J)
⊢ ⋂ i, M.closure (bif i then I else J) = M.closure I ∩ M.closure J

case h
α : Type u_2
M : Matroid α
I J : Set α
h : M.Indep (I ∪ J)
⊢ M.Indep (⋃ i, bif i then I else J)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
⊢ toENat M.cRank = M.eRank

Tactic:
obtain h | h := M.rankFinite_or_rankInfinite

Goal state after:
case inl
α : Type u
M : Matroid α
h : M.RankFinite
⊢ toENat M.cRank = M.eRank

case inr
α : Type u
M : Matroid α
h : M.RankInfinite
⊢ toENat M.cRank = M.eRank
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊂ I
⊢ M.closure J ⊂ M.closure I

Tactic:
obtain ⟨e, heI, heJ⟩ := exists_of_ssubset hJI

Goal state after:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊂ I
e : α
heI : e ∈ I
heJ : e ∉ J
⊢ M.closure J ⊂ M.closure I
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
⊢ fixedBy α g⁻¹ = fixedBy α g

Tactic:
by
  ext
  rw [mem_fixedBy, mem_fixedBy, inv_smul_eq_iff, eq_comm]

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

Goal state before:
pp: ι : Type u
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ IsTranscendenceBasis R X

Tactic:
refine isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic.2 ⟨algebraicIndependent_X .., ?_⟩

Goal state after:
ι : Type u
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ Algebra.IsAlgebraic (↥(adjoin R (range X))) (MvPolynomial ι R)
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ 𝓝 1 = B.filter

Tactic:
B.nhds_eq

Goal state after:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ B.N 1 = B.filter
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ (𝓝 x₀).HasBasis (fun V ↦ V ∈ B) fun V ↦ (fun y ↦ x₀ * y) '' V

Tactic:
B.nhds_eq

Goal state after:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ (B.N x₀).HasBasis (fun V ↦ V ∈ B) fun V ↦ (fun y ↦ x₀ * y) '' V
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ IsTopologicalGroup G

Tactic:
refine IsTopologicalGroup.of_nhds_one ?_ ?_ ?_ ?_

Goal state after:
case refine_1
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)

case refine_2
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)

case refine_3
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)

case refine_4
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ (x₀ : G), Tendsto (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E✝ : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E✝
inst✝³ : Algebra F E✝
E : Type v
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree F ↥L = finrank F ↥L
⊢ finSepDegree F ↥(IntermediateField.restrictScalars F (↥L)⟮x⟯) =
    finrank F ↥(IntermediateField.restrictScalars F (↥L)⟮x⟯)

Tactic:
have heq : _ * _ = _ * _ := congr_arg₂ (· * ·) h <|
    (finSepDegree_adjoin_simple_eq_finrank_iff L E x (IsAlgebraic.of_finite L x)).2 <|
      IsSeparable.tower_top L (Algebra.IsSeparable.isSeparable F x)

Goal state after:
F : Type u
E✝ : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E✝
inst✝³ : Algebra F E✝
E : Type v
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree F ↥L = finrank F ↥L
heq : finSepDegree F ↥L * finSepDegree ↥L ↥(↥L)⟮x⟯ = finrank F ↥L * finrank ↥L ↥(↥L)⟮x⟯
⊢ finSepDegree F ↥(IntermediateField.restrictScalars F (↥L)⟮x⟯) =
    finrank F ↥(IntermediateField.restrictScalars F (↥L)⟮x⟯)
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: case a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
⊢ L ≤ IntermediateField.fixedField L.fixingSubgroup

Tactic:
exact (IntermediateField.le_iff_le L.fixingSubgroup L).mpr le_rfl

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: case ind
F✝ : Type u
E✝ : Type v
inst✝¹¹ : Field F✝
inst✝¹⁰ : Field E✝
inst✝⁹ : Algebra F✝ E✝
q✝ : ℕ
inst✝⁸ : ExpChar F✝ q✝
inst✝⁷ : IsPurelyInseparable F✝ E✝
inst✝⁶ : FiniteDimensional F✝ E✝
E : Type v
inst✝⁵ : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_1 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E], finrank F E = m → ∃ n, m = q ^ n
F : Type v
inst✝⁴ : Field F
inst✝³ : Algebra F E
inst✝² : ExpChar F q
inst✝¹ : IsPurelyInseparable F E
inst✝ : FiniteDimensional F E
hd : finrank F E = d
⊢ ∃ n, d = q ^ n

Tactic:
| ind d IH =>

Goal state after: