mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K L : IntermediateField F E
inst✝³ : Normal F ↥K
inst✝² : FiniteDimensional F ↥K
inst✝¹ : FiniteDimensional (↥L) E
inst✝ : IsGalois (↥L) E
h : K ⊓ L = ⊥
x✝ : ↥K
x : E
hx₁ : x ∈ K
hx₂ : ⟨x, hx₁⟩ ∈ fixedField (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E).range
⊢ ⟨x, hx₁⟩ ∈ ⊥

Tactic:
obtain ⟨⟨y, hy⟩, rfl⟩ : x ∈ Set.range (algebraMap L E) := by
    refine mem_bot.mp <| (IsGalois.mem_bot_iff_fixed _).mpr fun φ ↦ ?_
    rw [← restrictRestrictAlgEquivMapHom_apply K L φ ⟨x, hx₁⟩]
    rw [mem_fixedField_iff] at hx₂
    exact congr_arg ((↑) : K → E) <| hx₂ (restrictRestrictAlgEquivMapHom F K L E φ) ⟨φ, rfl⟩

Goal state after:
F : Type u_1
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K L : IntermediateField F E
inst✝³ : Normal F ↥K
inst✝² : FiniteDimensional F ↥K
inst✝¹ : FiniteDimensional (↥L) E
inst✝ : IsGalois (↥L) E
h : K ⊓ L = ⊥
x✝ : ↥K
y : E
hy : y ∈ L
hx₁ : (algebraMap (↥L) E) ⟨y, hy⟩ ∈ K
hx₂ : ⟨(algebraMap (↥L) E) ⟨y, hy⟩, hx₁⟩ ∈ fixedField (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E).range
⊢ ⟨(algebraMap (↥L) E) ⟨y, hy⟩, hx₁⟩ ∈ ⊥
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case pos
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : IsIntegral R x
⊢ (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1

pp: case neg
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : ¬IsIntegral R x
⊢ (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1

Tactic:
· rw [← natDegree_minpolyDiv_succ hx]; rfl

Goal state after:
case neg
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : ¬IsIntegral R x
⊢ (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : ¬∃ s, Nonempty (Basis (↥s) R S)
⊢ trace R S = 0

Tactic:
by ext s; simp [trace_apply, LinearMap.trace, h]

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

Goal state before:
pp: F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable E K
x : K
x✝¹ : x ∈ ⊤
S : IntermediateField F K := separableClosure F K
L : IntermediateField E K := adjoin E ↑S
this✝ : Algebra.IsSeparable (↥L) K
i : ↥S →+* ↥L := Subsemiring.inclusion ⋯
x✝ : Algebra ↥S ↥L := i.toAlgebra
this : IsScalarTower (↥S) (↥L) K
⊢ x ∈ L

Tactic:
have := Algebra.IsAlgebraic.trans F E K

Goal state after:
F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable E K
x : K
x✝¹ : x ∈ ⊤
S : IntermediateField F K := separableClosure F K
L : IntermediateField E K := adjoin E ↑S
this✝¹ : Algebra.IsSeparable (↥L) K
i : ↥S →+* ↥L := Subsemiring.inclusion ⋯
x✝ : Algebra ↥S ↥L := i.toAlgebra
this✝ : IsScalarTower (↥S) (↥L) K
this : Algebra.IsAlgebraic F K
⊢ x ∈ L
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁶ : Group G
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
inst✝² : MulSemiringAction G B
H : Type u_5
inst✝¹ : Group H
inst✝ : MulSemiringAction H B
e : H ≃* G
he : ∀ (h : H) (x : B), e h • x = h • x
⊢ IsGaloisGroup H A B ↔ IsGaloisGroup G A B

Tactic:
refine ⟨fun h ↦ h.of_mulEquiv e.symm fun g x ↦ ?_, fun h ↦ h.of_mulEquiv e he⟩

Goal state after:
G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁶ : Group G
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
inst✝² : MulSemiringAction G B
H : Type u_5
inst✝¹ : Group H
inst✝ : MulSemiringAction H B
e : H ≃* G
he : ∀ (h : H) (x : B), e h • x = h • x
h : IsGaloisGroup H A B
g : G
x : B
⊢ e.symm g • x = g • x
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
hpos : NeZero n
a : ZMod n
⊢ a.valMinAbs.natAbs = min a.val (n - a.val)

Tactic:
rw [valMinAbs_def_pos]
  have := a.val_lt
  omega

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

Goal state before:
pp: case pos.zero
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
hn : finrank (↥(separableClosure K L)) L = 1
⊢ (trace K ↥(separableClosure K L)) (finrank (↥(separableClosure K L)) L • x) =
    0 ((algebraMap (↥(separableClosure K L)) L) x)

Tactic:
IntermediateField.finrank_eq_one_iff_eq_top,

Goal state after:
case pos.zero
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
hn : separableClosure K L = ⊤
⊢ (trace K ↥(separableClosure K L)) (finrank (↥(separableClosure K L)) L • x) =
    0 ((algebraMap (↥(separableClosure K L)) L) x)
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case pos.succ.zero
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
H : ¬Algebra.IsSeparable K L
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
n : ℕ
inst✝ : CharZero K
this : 1 ≠ 0
hn : finrank (↥(separableClosure K L)) L = 1
⊢ (trace K ↥(separableClosure K L)) (finrank (↥(separableClosure K L)) L • x) =
    0 ((algebraMap (↥(separableClosure K L)) L) x)

Tactic:
IntermediateField.finrank_eq_one_iff_eq_top,

Goal state after:
case pos.succ.zero
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
H : ¬Algebra.IsSeparable K L
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
n : ℕ
inst✝ : CharZero K
this : 1 ≠ 0
hn : separableClosure K L = ⊤
⊢ (trace K ↥(separableClosure K L)) (finrank (↥(separableClosure K L)) L • x) =
    0 ((algebraMap (↥(separableClosure K L)) L) x)
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
n : ℕ := ⋯
nzero : ↑(Fintype.card ↥G) = 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := ⋯
hu : orderOf u = p
h : u = 1
⊢ 1 = p

Tactic:
rw [← hu, h, orderOf_one]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : ↑a.valMinAbs ^ 2 + ↑b.valMinAbs ^ 2 = ↑x
⊢ a.valMinAbs ^ 2 + b.valMinAbs ^ 2 ≡ x [ZMOD ↑p]

Tactic:
← ZMod.intCast_eq_intCast_iff

Goal state after:
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : ↑a.valMinAbs ^ 2 + ↑b.valMinAbs ^ 2 = ↑x
⊢ ↑(a.valMinAbs ^ 2 + b.valMinAbs ^ 2) = ↑x
Module: Mathlib.RingTheory.ZMod

Goal state before:
pp: n : ℕ
⊢ IsReduced (ZMod n) ↔ Squarefree n ∨ n = 0

Tactic:
← RingHom.ker_isRadical_iff_reduced_of_surjective
      (ZMod.ringHom_surjective <| Int.castRingHom <| ZMod n),

Goal state after:
n : ℕ
⊢ (RingHom.ker (Int.castRingHom (ZMod n))).IsRadical ↔ Squarefree n ∨ n = 0
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Free ℤ M
inst✝² : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst✝¹ : EquivLike E M ↥N
inst✝ : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ ↑e'
f_apply : ∀ (x : M), f x = ↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))) x) := fun x ↦ rfl
ha : ∀ (i : Free.ChooseBasisIndex ℤ M), f (b' i) = a i • b' i
⊢ (LinearMap.det f).natAbs = ((LinearMap.toMatrix b' b') f).det.natAbs

Tactic:
LinearMap.det_toMatrix

Goal state after:
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Free ℤ M
inst✝² : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst✝¹ : EquivLike E M ↥N
inst✝ : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ ↑e'
f_apply : ∀ (x : M), f x = ↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))) x) := fun x ↦ rfl
ha : ∀ (i : Free.ChooseBasisIndex ℤ M), f (b' i) = a i • b' i
⊢ (LinearMap.det f).natAbs = (LinearMap.det f).natAbs
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁸ : Group G
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsFractionRing B L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : MulSemiringAction G B
inst✝³ : MulSemiringAction G L
inst✝² : SMulDistribClass G B L
hAB : Algebra.IsInvariant A B G
inst✝¹ : SMulCommClass G A B
inst✝ : Algebra.IsIntegral A B
hc : ∀ (a : A), (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) ((algebraMap A B) a)
this✝ : Nontrivial A
this : Nontrivial B
x y : B
hy : y ∈ nonZeroDivisors B
h : ∀ (g : G), g • ((algebraMap B L) x / (algebraMap B L) y) = (algebraMap B L) x / (algebraMap B L) y
hy' : (algebraMap B L) y ≠ 0
b : B
a : A
hb : x * (algebraMap A B) a = b * y
ha : (algebraMap B L) ((algebraMap A B) a) ≠ 0
hxy : (algebraMap B L) x / (algebraMap B L) y = (algebraMap B L) b / (algebraMap B L) ((algebraMap A B) a)
⊢ ∀ (g : G), g • b = b

Tactic:
simpa [ha, hxy, smul_div₀', ← algebraMap.coe_smul'] using h

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq α
s : Finset α
i : α → ℕ
p : α
hps : p ∉ s
is_prime : ∀ q ∈ insert p s, Prime q
is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'
⊢ IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')

Tactic:
by
  have hp := is_prime _ (Finset.mem_insert_self _ _)
  refine (isRelPrime_iff_no_prime_factors <| pow_ne_zero _ hp.ne_zero).mpr ?_
  intro d hdp hdprod hd
  apply hps
  replace hdp := hd.dvd_of_dvd_pow hdp
  obtain ⟨q, q_mem', hdq⟩ := hd.exists_mem_multiset_dvd hdprod
  obtain ⟨q, q_mem, rfl⟩ := Multiset.mem_map.mp q_mem'
  replace hdq := hd.dvd_of_dvd_pow hdq
  have : p ∣ q := dvd_trans (hd.irreducible.dvd_symm hp.irreducible hdp) hdq
  convert! q_mem using 0
  rw [Finset.mem_val,
    is_coprime _ (Finset.mem_insert_self p s) _ (Finset.mem_insert_of_mem q_mem) this]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : Algebra R S
inst✝² : Nontrivial S
inst✝¹ : Free R S
inst✝ : Module.Finite R S
⊢ (norm R) 0 = 0

Tactic:
nontriviality

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : Algebra R S
inst✝² : Nontrivial S
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a✝ : Nontrivial R
⊢ (norm R) 0 = 0
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : ¬IsIntegral K x
⊢ (norm K) (AdjoinSimple.gen K x) = 1

Tactic:
norm_eq_one_of_not_exists_basis

Goal state after:
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : ¬IsIntegral K x
⊢ 1 = 1

case h
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : ¬IsIntegral K x
⊢ ¬∃ s, Nonempty (Basis (↥s) K ↥K⟮x⟯)
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
⊢ Function.LeftInverse (fun x ↦ ⟨↑(IsUnit.unit ⋯)⁻¹, ⋯⟩) (↑S.fromCommLeftInv).toFun

Tactic:
intro x
      ext
      simp [← Units.mul_eq_one_iff_inv_eq]

Goal state after:
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : IsNoetherian R M → Module.Finite R M
tfae_1_to_3 : Module.Finite R M → IsArtinian R M
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsNoetherian R M ∧ IsArtinian R M].TFAE

Tactic:
tfae_have 4 → 2 := And.left

Goal state after:
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : IsNoetherian R M → Module.Finite R M
tfae_1_to_3 : Module.Finite R M → IsArtinian R M
tfae_4_to_2 : IsNoetherian R M ∧ IsArtinian R M → IsNoetherian R M
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsNoetherian R M ∧ IsArtinian R M].TFAE
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
n : ℕ
hgt : ¬map f p ≤ P ^ n
⊢ p.ramificationIdx' P < n

Tactic:
rcases n with - | n
  · simp at hgt
  · rw [Nat.lt_succ_iff]
    have : ∀ k, map f p ≤ P ^ k → k ≤ n := by
      refine fun k hk => le_of_not_gt fun hnk => ?_
      exact hgt (hk.trans (Ideal.pow_le_pow_right hnk))
    rw [ramificationIdx'_eq_find ⟨n, this⟩]
    exact Nat.find_min' ⟨n, this⟩ this

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : QuasiFinite R S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ QuasiFinite A (A ⊗[R] S)

Tactic:
by
  refine ⟨fun P hP ↦ ?_⟩
  let p := P.under R
  let := Localization.AtPrime.algebraOfLiesOver p P
  let e : P.Fiber (A ⊗[R] S) ≃ₐ[P.ResidueField] P.ResidueField ⊗[p.ResidueField] (p.Fiber S) :=
    (Algebra.TensorProduct.cancelBaseChange _ _ _ _ _).trans
      (Algebra.TensorProduct.cancelBaseChange _ _ _ _ _).symm
  exact .of_surjective e.symm.toLinearMap e.symm.surjective

Goal state after:
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
| ∑ i ∈ f.support, 1 ⊗ₜ[R] x * f i ⊗ₜ[R] b i

Tactic:
simp only [TensorProduct.tmul_mul_tmul, one_mul, mul_comm x (b _),
      ← show ∀ i, Finsupp.linearCombination _ b (a i) = b i * x from
          fun _ ↦ b.linearCombination_repr _]

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
| ∑ i ∈ f.support, f i ⊗ₜ[R] (Finsupp.linearCombination R ⇑b) (a i)
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
hx : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) (Extension.Cotangent.mk ⟨x, hx'⟩) = 0
⊢ (Q.ofComp P).toAlgHom x ∈ Q.ker ^ 2

Tactic:
simpa only [map_mk, val_mk, val_zero, Ideal.toCotangent_eq_zero] using! congr(($hx).val)

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
surj : Function.Surjective ⇑f.kerSquareLift
⊢ ∃ g, f.kerSquareLift.comp g = AlgHom.id R A

Tactic:
have sqz : RingHom.ker f.kerSquareLift.toRingHom ^ 2 = ⊥ := by
    rw [AlgHom.ker_kerSquareLift, Ideal.cotangentIdeal_square]

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
surj : Function.Surjective ⇑f.kerSquareLift
sqz : RingHom.ker f.kerSquareLift.toRingHom ^ 2 = ⊥
⊢ ∃ g, f.kerSquareLift.comp g = AlgHom.id R A
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
Q : Generators S T ι
i : ι
⊢ (δAux R Q) (X i) = 0

Tactic:
by
  rw [X, δAux_monomial]
  simp only [Derivation.map_one_eq_zero, tmul_zero]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case hz.fst
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : ↥Q.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ 0 =
    (LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
        ↑(CotangentSpace.compEquiv Q P))
      ((Q.comp P).toExtension.cotangentComplex y)

Tactic:
rw [CotangentSpace.fst_compEquiv, Extension.CotangentSpace.map_cotangentComplex, hy, hx]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
r : S
hr : C r ∈ Q.ker
⊢ (δ Q P) ⟨Extension.Cotangent.mk ⟨C r, hr⟩, ⋯⟩ = 1 ⊗ₜ[S] (D R S) r

Tactic:
rw [δ_eq_δAux, δAux_C]

Goal state after:
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FormallyUnramified K L
inst✝ : EssFiniteType K L
this : Module.Finite K L
⊢ Algebra.IsSeparable K L

Tactic:
rw [← separableClosure.eq_top_iff]

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FormallyUnramified K L
inst✝ : EssFiniteType K L
this : Module.Finite K L
⊢ separableClosure K L = ⊤
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this : CotangentSpace.map P.toInfinitesimal = ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm
⊢ Function.Bijective ⇑(CotangentSpace.map P.toInfinitesimal)

Tactic:
by
    rw [this]; exact (tensorKaehlerQuotKerSqEquiv _ _ _).symm.bijective

Goal state after:
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: case smul
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝¹ : FormallyUnramified (ResidueField R) (ResidueField S)
this✝ : FormallyUnramified R (ResidueField S)
x✝ a x : S
hx : x ∈ Submodule.span S (⇑(algebraMap R S) '' ↑(maximalIdeal R))
a✝ : 1 ⊗ₜ[S] (KaehlerDifferential.D R S) x = 0
this : (residue S) x = 0
⊢ 1 ⊗ₜ[S] (KaehlerDifferential.D R S) (a • x) = 0

Tactic:
simp [*, TensorProduct.tmul_add, TensorProduct.smul_tmul', ← Algebra.algebraMap_eq_smul_one]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
s : Finset ι
S : ι → Set α
a : α
ha : a ∉ ⋃ i ∈ s, S i
i : ι
hi : i ∈ s
⊢ ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0

Tactic:
have ha : a ∉ S i := by aesop

Goal state after:
case neg
ι : Type u_1
α : Type u_2
s : Finset ι
S : ι → Set α
a : α
ha✝ : a ∉ ⋃ i ∈ s, S i
i : ι
hi : i ∈ s
ha : a ∉ S i
⊢ ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
v w : { x // x.asIdeal ∣ I }
⊢ (fun v ↦ ⟨(↑v).asIdeal, ⋯⟩) v = (fun v ↦ ⟨(↑v).asIdeal, ⋯⟩) w → v = w

Tactic:
hvw

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
v w : { x // x.asIdeal ∣ I }
hvw : (fun v ↦ ⟨(↑v).asIdeal, ⋯⟩) v = (fun v ↦ ⟨(↑v).asIdeal, ⋯⟩) w
⊢ v = w