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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
h : Function.Injective ⇑(LinearMap.lTensor k l)
this✝² : Free R (N ⧸ l.range)
this✝¹ : Projective R ↥l.range
l' : M →ₗ[R] ↥l.ker
hl' : l' ∘ₗ l.ker.subtype = LinearMap.id
this✝ : Module.Finite R ↥l.ker
H : Function.Injective ⇑(LinearMap.lTensor k l.ker.subtype)
this : Subsingleton (k ⊗[R] ↥l.ker)
⊢ l.ker = ⊥

Tactic:
← Submodule.subsingleton_iff_eq_bot,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
h : Function.Injective ⇑(LinearMap.lTensor k l)
this✝² : Free R (N ⧸ l.range)
this✝¹ : Projective R ↥l.range
l' : M →ₗ[R] ↥l.ker
hl' : l' ∘ₗ l.ker.subtype = LinearMap.id
this✝ : Module.Finite R ↥l.ker
H : Function.Injective ⇑(LinearMap.lTensor k l.ker.subtype)
this : Subsingleton (k ⊗[R] ↥l.ker)
⊢ Subsingleton ↥l.ker
Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
⊢ tensorProductTo R S T ⁻¹' (basicOpen a).carrier ×ˢ (basicOpen t).carrier ⊆ ↑(basicOpen f)

Tactic:
rintro x ⟨hx₁ : a ⊗ₜ[R] (1 : T) ∉ x.asIdeal, hx₂ : (1 : S) ⊗ₜ[R] t ∉ x.asIdeal⟩
      (hx₃ : f ∈ x.asIdeal)

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
x : PrimeSpectrum (S ⊗[R] T)
hx₁ : a ⊗ₜ[R] 1 ∉ x.asIdeal
hx₂ : 1 ⊗ₜ[R] t ∉ x.asIdeal
hx₃ : f ∈ x.asIdeal
⊢ False
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
I : FractionalIdeal R⁰ K
hI : (↑(I ^ n)).IsPrincipal
⊢ (↑I).IsPrincipal

Tactic:
by
  obtain (rfl | ⟨u, rfl⟩) := GroupWithZero.eq_zero_or_unit I
  · simp [bot_isPrincipal]
  rw [← ClassGroup.mk_eq_one_iff, ← orderOf_eq_one_iff, ← Nat.dvd_one, ← hn,
    Nat.dvd_gcd_iff]
  refine ⟨?_, orderOf_dvd_card⟩
  rw [orderOf_dvd_iff_pow_eq_one, ← map_pow, ClassGroup.mk_eq_one_iff]
  exact_mod_cast hI

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

Goal state before:
pp: R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst✝⁷ : CommRing Rₚ
inst✝⁶ : Algebra R Rₚ
inst✝⁵ : IsLocalization.AtPrime Rₚ p.asIdeal
inst✝⁴ : AddCommGroup Mₚ
inst✝³ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝² : IsLocalizedModule p.asIdeal.primeCompl f
inst✝¹ : Module Rₚ Mₚ
inst✝ : IsScalarTower R Rₚ Mₚ
⊢ p ∈ freeLocus R M ↔ Free Rₚ Mₚ

Tactic:
set e := (IsLocalization.algEquiv p.asIdeal.primeCompl
      (Localization.AtPrime p.asIdeal) Rₚ).toRingEquiv
  apply Module.Free.iff_of_equiv (σ := e)
  refine { __ := IsLocalizedModule.iso p.asIdeal.primeCompl f, map_smul' := ?_ }
  intro r x
  obtain ⟨r, s, rfl⟩ := IsLocalization.exists_mk'_eq p.asIdeal.primeCompl r
  apply ((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units f s)).1
  simp [e, ← map_smul, ← smul_assoc]

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 := 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 : R
hx : x ∈ ↑p'.primeCompl
⊢ (algebraMap R (Localization S)) x ∈ p.asIdeal.primeCompl

Tactic:
exact hx

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q₁ q₂ : ↑(comap (algebraMap R S) ⁻¹' {p})
⊢ q₁ ≤ q₂ → (preimageEquivFiber R S p) q₁ ≤ (preimageEquivFiber R S p) q₂

Tactic:
intro H x hx

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q₁ q₂ : ↑(comap (algebraMap R S) ⁻¹' {p})
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
hx : x ∈ ((preimageEquivFiber R S p) q₁).asIdeal
⊢ x ∈ ((preimageEquivFiber R S p) q₂).asIdeal
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 := 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 : R
hx : x ∈ ↑p'.primeCompl
⊢ (algebraMap R (Localization S)) x ∈ p.asIdeal.primeCompl

Tactic:
exact hx

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsSolvable G
H : Subgroup G
hH : H ≠ ⊥
⊢ ⁅H, H⁆ < H

Tactic:
rw [← nontrivial_iff_ne_bot] at hH

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSolvable G
H : Subgroup G
hH : Nontrivial ↥H
⊢ ⁅H, H⁆ < H
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
h : Normal F K
inst✝ : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K)) F K := Module.Basis.ofVectorSpace F K
⊢ Set.range ⇑s ⊆ ↑(Subalgebra.toSubmodule (Algebra.adjoin F ((∏ x, minpoly F (s x)).rootSet K)))

Tactic:
Set.range_subset_iff

Goal state after:
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K)) F K := Module.Basis.ofVectorSpace F K
⊢ ∀ (y : ↑(Module.Basis.ofVectorSpaceIndex F K)),
    s y ∈ ↑(Subalgebra.toSubmodule (Algebra.adjoin F ((∏ x, minpoly F (s x)).rootSet K)))
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: case inr
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p).Splits ∧
    (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)).Splits
⊢ IsIntegral F x ∧ (Polynomial.map (algebraMap F E) (minpoly F x)).Splits

Tactic:
obtain ⟨hL1, hL2⟩ := hL
    let j : E →ₐ[F] L := IsSplittingField.lift E p hL1
    rw [← j.comp_algebraMap, ← Polynomial.map_map] at hL2
    refine ⟨hx, Splits.of_splits_map (j : E →+* L) hL2 fun a ha ↦ ?_⟩
    rw [Polynomial.map_map, j.comp_algebraMap] at ha
    let : Algebra F⟮x⟯ L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toRingHom.toAlgebra
    let j' : E →ₐ[F⟮x⟯] L := IsSplittingField.lift E (p.map (algebraMap F F⟮x⟯)) ?_
    · change a ∈ j.range
      rw [← IsSplittingField.adjoin_rootSet_eq_range E p j,
            IsSplittingField.adjoin_rootSet_eq_range E p (j'.restrictScalars F)]
      exact ⟨x, (j'.commutes _).trans (algHomAdjoinIntegralEquiv_symm_apply_gen F hx _)⟩
    · rwa [Polynomial.map_map, ← IsScalarTower.algebraMap_eq]

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
E : Type u_3
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : AlgebraicIndependent F x
i : FractionRing (MvPolynomial ι F) →ₐ[F] E := IsFractionRing.liftAlgHom ⋯
⊢ (↑i).comp (algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F))) = ↑(aeval x)

Tactic:
by ext <;> simp [i]

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

Goal state before:
pp: α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∃ B, M.IsBase B

Tactic:
exact M.exists_isBase

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
⊢ Finite (IntermediateField F E)

Tactic:
let f : F[X] := minpoly F α

Goal state after:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
f : F[X] := minpoly F α
⊢ Finite (IntermediateField F E)
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₀ = f '' f ⁻¹' J

Tactic:
hbj.image_eq

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 '' f ⁻¹' J = f '' f ⁻¹' J
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
inst✝ : M.Finite
⊢ {N | N ≤r M} ⊆ (fun R ↦ M ↾ R) '' {b | b ⊆ M.E}

Tactic:
rintro _ ⟨R, hR, rfl⟩; exact ⟨_, hR, rfl⟩

Goal state after:
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
⊢ M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)

Tactic:
by
  refine Indep.isBasis_of_forall_insert ?_ inter_subset_right (fun e he ↦ ?_)
  · rw [dual_indep_iff_exists]
    exact ⟨B, hB, disjoint_of_subset_left inter_subset_left disjoint_sdiff_left⟩
  simp only [sdiff_inter_self_eq_sdiff, mem_sdiff, not_and, not_not, imp_iff_right he.1.1] at he
  simp_rw [dual_dep_iff_forall, insert_subset_iff, and_iff_right he.1.1,
    and_iff_left (inter_subset_left.trans sdiff_subset)]
  refine fun B' hB' ↦ by_contra (fun hem ↦ ?_)
  rw [nonempty_iff_ne_empty, not_ne_iff, ← union_singleton, sdiff_inter_sdiff,
    union_inter_distrib_right, union_empty_iff, singleton_inter_eq_empty, sdiff_eq,
    inter_right_comm, inter_eq_self_of_subset_right hB'.subset_ground, ← sdiff_eq,
    sdiff_eq_empty] at hem
  obtain ⟨f, hfb, hBf⟩ := hB.exchange hB' ⟨he.2, hem.2⟩
  have hi : M.Indep (insert f (B ∩ X)) := by
    refine hBf.indep.subset (insert_subset_insert ?_)
    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]
  exact hfb.2 (hBX.mem_of_insert_indep (Or.elim (hem.1 hfb.1) (False.elim ∘ hfb.2) id) hi).1

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 : Finset α
⊢ (IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).Indep ↑I ↔ Indep I

Tactic:
simp only [IndepMatroid.ofFinset]
  exact ⟨fun h ↦ h _ Subset.rfl, fun h J hJI ↦ indep_subset h hJI⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
h : M✶.RankPos
hB : M.IsBase B
⊢ B ≠ M.E

Tactic:
rintro rfl; exact M.ground_not_isBase hB

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep (Subtype.val '' ⇑f ⁻¹' ⇑f '' I)
⊢ M.Indep (Subtype.val '' I)

Tactic:
rwa [preimage_image_eq _ f.injective] at hI

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I

Tactic:
by
  rw [IsCircuit, minimal_iff_forall_ssubset, and_congr_right_iff]
  exact fun h ↦ ⟨fun h' I hIC ↦ ((not_dep_iff (hIC.subset.trans h.subset_ground)).1 (h' hIC)),
    fun h I hIC ↦ (h hIC).not_dep⟩

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}
h : ∀ (B : Set α), M✶.IsBase B → e ∈ M✶.E \ B
B : Set α
hB : M.IsBase B
⊢ e ∈ B

Tactic:
obtain ⟨-, heB : e ∈ B⟩ := by simpa using h (M.E \ B) hB.compl_isBase_dual

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}
h : ∀ (B : Set α), M✶.IsBase B → e ∈ M✶.E \ B
B : Set α
hB : M.IsBase B
heB : e ∈ B
⊢ e ∈ B
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)}
⊢ M.closure I = F

Tactic:
have hIF : M.IsBasis I F := hI.isBasis_setOfPred_insert_isBasis

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
⊢ M.closure I = F
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.Indep (∅ ∪ M.coloops)

Tactic:
union_coloops_indep_iff

Goal state after:
α : Type u_1
M : Matroid α
⊢ M.Indep ∅
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
B : { B // M.IsBase B }
⊢ #↑↑B ≤ #↑↑⟨↑B, ⋯⟩

Tactic:
by rfl

Goal state after:
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 ∧ J ⊆ M.closure J ∩ I

Tactic:
and_iff_left (subset_inter (M.subset_closure _) hJI)

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
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
⊢ Transcendental R (X i)

Tactic:
by
  simpa using transcendental_polynomial_aeval_X R i (Polynomial.transcendental_X R)

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
⊢ LinearIndependent R x

Tactic:
rw [linearIndependent_iff_injective_finsuppLinearCombination]
  have : Finsupp.linearCombination R x =
      (MvPolynomial.aeval x).toLinearMap.comp (Finsupp.linearCombination R X) := by
    ext
    simp
  rw [this]
  refine (algebraicIndependent_iff_injective_aeval.mp hx).comp ?_
  rw [← linearIndependent_iff_injective_finsuppLinearCombination]
  exact linearIndependent_X _ _

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Unique ι
i : MvPolynomial ι R ≃ₐ[R] Polynomial R := uniqueAlgEquiv R ι
⊢ Injective ⇑(aeval x) ↔ Injective ⇑(Polynomial.aeval (x default))

Tactic:
have key : aeval (R := R) x = (Polynomial.aeval (R := R) (x default)).comp i := by
    ext y
    simp [i, Subsingleton.elim y default]

Goal state after:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Unique ι
i : MvPolynomial ι R ≃ₐ[R] Polynomial R := uniqueAlgEquiv R ι
key : aeval x = (Polynomial.aeval (x default)).comp ↑i
⊢ Injective ⇑(aeval x) ↔ Injective ⇑(Polynomial.aeval (x default))
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
ind : AlgebraicIndependent R fun i ↦ x ↑i
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i ↦ x ↑i) → ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x '' t))) (x i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t \ s
hu : u ⊆ t \ s
ha' : a ∉ u
h : AlgebraicIndependent R fun i ↦ x ↑i
this : a ∉ t ∩ s ∪ u
⊢ AlgebraicIndependent R fun i ↦ x ↑i

Tactic:
convert!
    (((image_eq_range .. ▸ h.option_iff_transcendental <| x a).2 <|
              H _ (hfin.subset (union_subset inter_subset_left <| hu.trans sdiff_subset)) h a ha.2
                this).comp
          _ (subtypeInsertEquivOption this).injective).comp
      (Equiv.setCongr union_insert) (Equiv.injective _) with
    x

Goal state after:
ι : Type u_1
R : Type u_3
A : Type v
x✝ : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
ind : AlgebraicIndependent R fun i ↦ x✝ ↑i
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i ↦ x✝ ↑i) → ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x✝ '' t))) (x✝ i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t \ s
hu : u ⊆ t \ s
ha' : a ∉ u
h : AlgebraicIndependent R fun i ↦ x✝ ↑i
this : a ∉ t ∩ s ∪ u
x : ↑(t ∩ s ∪ insert a u)
⊢ x✝ ↑x = (((fun o ↦ o.elim (x✝ a) fun i ↦ x✝ ↑i) ∘ ⇑(subtypeInsertEquivOption this)) ∘ ⇑(Equiv.setCongr ⋯)) x
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Subsingleton R
x : ι → A
this✝ : Subsingleton A
h : IsTranscendenceBasis R x
hι : IsEmpty ι
this : range x ⊆ {0} → range x = {0}
⊢ False

Tactic:
simp [range_eq_empty, eq_comm (a := ∅)] at this

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
s : Set ι
i : ι
hi : i ∉ s
⊢ (AlgebraicIndependent ↥(adjoin R (x '' s)) fun i_1 ↦ x ↑i_1) ↔ Transcendental (↥(adjoin R (x '' s))) (x i)

Tactic:
rw [algebraicIndependent_singleton_iff ⟨i, rfl⟩]

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

Goal state before:
pp: case e'_1
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s : Set ι
i : ι
⊢ (AlgebraicIndependent ↥(adjoin R (x '' s)) fun i_1 ↦ x ↑i_1) ↔ Transcendental (↥(adjoin R (x '' s))) (x i)

Tactic:
rw [algebraicIndependent_singleton_iff ⟨i, rfl⟩]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: F : Type u_1
inst✝ : CommSemiring F
q : ℕ
f g : F[X]
hf : IsSeparableContraction q f g
⊢ ∃ m, g.natDegree * q ^ m = f.natDegree

Tactic:
by
  obtain ⟨m, rfl⟩ := hf.2
  use m
  rw [natDegree_expand]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
hIX : M.IsBasis I X
hX : M.Spanning X
⊢ M.Spanning I

Tactic:
rwa [hIX.spanning_iff_spanning]

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

Goal state before:
pp: case refine_1
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
r : R
⊢ (Polynomial.aeval a) (Polynomial.C ((algebraMap R ↥(adjoin R (range x))) r)) = (aeval fun o ↦ o.elim a x) (C r)

Tactic:
aeval_C,

Goal state after:
case refine_1
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
r : R
⊢ (Polynomial.aeval a) (Polynomial.C ((algebraMap R ↥(adjoin R (range x))) r)) = (algebraMap R A) r
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:
by
  have := hx.isAlgebraic
  set S := range x
  let : Algebra (adjoin F S) (IntermediateField.adjoin F S) :=
    (Subalgebra.inclusion (IntermediateField.algebra_adjoin_le_adjoin F S)).toRingHom.toAlgebra
  have : IsScalarTower (adjoin F S) (IntermediateField.adjoin F S) E :=
    IsScalarTower.of_algebraMap_eq (congrFun rfl)
  exact Algebra.IsAlgebraic.extendScalars (R := adjoin F S) (Subalgebra.inclusion_injective _)

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

Goal state before:
pp: case pos
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
s : Set A
inst✝ : NoZeroDivisors A
h : Injective ⇑(algebraMap R A)
this✝ : IsDomain A
this : FaithfulSMul R A
alg : (matroid R A).Spanning s
⊢ (matroid R A).cRank ≤ #↑s

Tactic:
exact alg.cRank_le_cardinalMk

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ (C 0).natSepDegree = 0

Tactic:
natSepDegree_C

Goal state after:
F : Type u
inst✝ : Field F
⊢ 0 = 0
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ (C 1).natSepDegree = 0

Tactic:
natSepDegree_C

Goal state after:
F : Type u
inst✝ : Field F
⊢ 0 = 0
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case prime
F : Type u
inst✝ : Field F
f : F[X]
q n : ℕ
hprime : Nat.Prime q
hchar✝ : CharP F q
this : Fact (Nat.Prime q)
⊢ ((expand F (q ^ n)) f).natSepDegree = f.natSepDegree

Tactic:
simpa only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_def, map_expand,
    Fintype.card_coe] using Fintype.card_eq.2
      ⟨(f.map (algebraMap F (AlgebraicClosure F))).rootsExpandPowEquivRoots q n⟩

Goal state after: