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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this : ∀ (n : ℕ), (map (algebraMap K g.SplittingField) g).coeff n ∈ ↑(integralClosure R g.SplittingField).toSubring
n : ℕ
⊢ g.coeff n ∈ ↑(integralClosure R K).toSubring

Tactic:
obtain ⟨p, hp, he⟩ := SetLike.mem_coe.mp (this n)

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this : ∀ (n : ℕ), (map (algebraMap K g.SplittingField) g).coeff n ∈ ↑(integralClosure R g.SplittingField).toSubring
n : ℕ
p : R[X]
hp : p.Monic
he : eval₂ (algebraMap R g.SplittingField) ((map (algebraMap K g.SplittingField) g).coeff n) p = 0
⊢ g.coeff n ∈ ↑(integralClosure R K).toSubring
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
inst✝¹ : IsDomain R
hB : B.Nondegenerate
inst✝ : IsTorsionFree R S
N : Submodule R M
hN : Submodule.span S ↑N = ⊤
⊢ Function.Injective ⇑(B.dualSubmoduleToDual N)

Tactic:
by
  intro x y e
  ext
  apply LinearMap.ker_eq_bot.mp hB.ker_eq_bot
  apply LinearMap.ext_on hN
  intro z hz
  simpa using congr_arg (algebraMap R S) (LinearMap.congr_fun e ⟨z, hz⟩)

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
b : Basis ι S M
⊢ B.dualSubmodule (B.flip.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

Tactic:
by
  classical
  let := b.finiteDimensional_of_finite
  rw [dualSubmodule_span_of_basis _ hB.flip, dualSubmodule_span_of_basis B hB,
    dualBasis_dualBasis_flip hB]

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
⊢ minpoly R (r • s) = (minpoly R s).scaleRoots r

Tactic:
let K := FractionRing R
  let L := FractionRing S
  let : Algebra K L := FractionRing.liftAlgebra _ _
  apply map_injective _ (FaithfulSMul.algebraMap_injective R K)
  rw [← minpoly.isIntegrallyClosed_eq_field_fractions K L (hs.smul r),
    map_scaleRoots _ _ _ (by simpa [minpoly.ne_zero_iff]),
    ← minpoly.isIntegrallyClosed_eq_field_fractions K L hs]
  simp_rw [Algebra.smul_def, map_mul, ← IsScalarTower.algebraMap_apply,
    IsScalarTower.algebraMap_apply R K L]
  refine eq_of_monic_of_associated (minpoly.monic ?_) ?_
    (associated_of_dvd_dvd (minpoly.dvd _ _ ?_) ?_)
  · refine isIntegral_algebraMap.mul (hs.map (IsScalarTower.toAlgHom R S L)).tower_top
  · simpa [monic_scaleRoots_iff] using minpoly.monic
      (hs.map (IsScalarTower.toAlgHom R S L)).tower_top
  · exact scaleRoots_aeval_eq_zero (minpoly.aeval _ _)
  · rw [← Polynomial.scaleRoots_dvd_iff _ _ (r := (algebraMap R K r)⁻¹) (IsUnit.mk0 _ (by simpa)),
      ← scaleRoots_mul, mul_inv_cancel₀ (by simpa), scaleRoots_one]
    refine minpoly.dvd _ _ ?_
    nth_rw 1 [← inv_mul_cancel_left₀ (b := algebraMap S L s)
      (a := algebraMap K L (algebraMap R K r)) (by simpa), ← map_inv₀]
    exact scaleRoots_aeval_eq_zero (minpoly.aeval _ _)

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: z : 𝓞 ℚ
⊢ ↑(ringOfIntegersEquiv z) = (algebraMap (𝓞 ℚ) ℚ) z

Tactic:
by
  obtain ⟨z, rfl⟩ := Rat.ringOfIntegersEquiv.symm.surjective z
  simp

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

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
⊢ (Algebra.trace K ↥K⟮x⟯) ((Algebra.trace (↥K⟮x⟯) L) x) =
    finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x)

Tactic:
conv in x => rw [← AdjoinSimple.algebraMap_gen K x]

Goal state after:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
⊢ (Algebra.trace K ↥K⟮x⟯) ((Algebra.trace (↥K⟮x⟯) L) ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x))) =
    finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x)
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
⊢ finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x) = ↑(finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff

Tactic:
trace_adjoinSimpleGen (.of_finite K x),

Goal state after:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
⊢ finrank (↥K⟮x⟯) L • -(minpoly K x).nextCoeff = ↑(finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hx : IsIntegral K x
pb : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis hx
⊢ IsSeparable K pb.gen

Tactic:
have := Algebra.isSeparable_tower_bot_of_isSeparable K K⟮x⟯ L

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hx : IsIntegral K x
pb : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis hx
this : Algebra.IsSeparable K ↥K⟮x⟯
⊢ IsSeparable K pb.gen
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case refine_2
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
h : G
⊢ (a - eval b r - h⁻¹ • if h⁻¹ • Q = Q then a else 0) ∈ h⁻¹ • Q

Tactic:
split_ifs with hh

Goal state after:
case pos
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
h : G
hh : h⁻¹ • Q = Q
⊢ a - eval b r - h⁻¹ • a ∈ h⁻¹ • Q

case neg
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
h : G
hh : ¬h⁻¹ • Q = Q
⊢ a - eval b r - h⁻¹ • 0 ∈ h⁻¹ • Q
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ ↑(Units.mk0 a ha ^ (q - 1)) = 1

Tactic:
rw [← Fintype.card_units, pow_card_eq_one]
        rfl

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

Goal state before:
pp: case inr
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ (m * m).natAbs
⊢ p ∣ m.natAbs

Tactic:
Int.natAbs_mul

Goal state after:
case inr
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ m.natAbs * m.natAbs
⊢ p ∣ m.natAbs
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
x : K
⊢ x ∈ (X ^ q - X).roots.toFinset

Tactic:
Multiset.mem_toFinset,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
x : K
⊢ x ∈ (X ^ q - X).roots
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case succ.zero
p a d k : ℕ
hk : k ∈ range p
hd : p * a = d
⊢ p ∣ (p ^ 0 * d) ^ k * ↑(p.choose (k + 1))

Tactic:
cases k <;> simp [← hd, mul_assoc, pow_succ']

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Goal state before:
pp: M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Free ℤ M
inst✝ : Module.Finite ℤ M
N : Submodule ℤ M
⊢ Finite (M ⧸ N) ↔ finrank ℤ ↥N = finrank ℤ M

Tactic:
refine ⟨fun h ↦ le_antisymm (finrank_le N) <|
    ((LinearMap.lsmul ℤ M (Nat.card (M ⧸ N))).codRestrict N
      fun x ↦ ?_).finrank_le_finrank_of_injective ?_, fun h ↦ finiteQuotientOfFreeOfRankEq N h⟩
  · simpa using! AddSubgroup.nsmul_index_mem N.toAddSubgroup x
  · refine (LinearMap.lsmul_injective ?_).codRestrict _
    exact Int.ofNat_ne_zero.mpr <| Nat.card_ne_zero.mpr
      ⟨Set.nonempty_iff_univ_nonempty.mpr Set.univ_nonempty, 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'
hp : Prime p
d : α
⊢ d ∣ p ^ i p → d ∣ ∏ p' ∈ s, p' ^ i p' → ¬Prime d

Tactic:
hdp

Goal state after:
α : 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'
hp : Prime p
d : α
hdp : d ∣ p ^ i p
⊢ d ∣ ∏ p' ∈ s, p' ^ i p' → ¬Prime d
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: case calc_2
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
⊢ ∏ i, (a i).natAbs = Nat.card (M ⧸ N)

Tactic:
simp_rw [Nat.card_congr (quotientEquivPiZMod N b h).toEquiv, Nat.card_pi, Nat.card_zmod, a]

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : Nontrivial R
inst✝¹ : IsDomain S
inst✝ : Algebra.IsIntegral R S
hP : P.LiesOver ⊥
⊢ ⊥.inertiaDeg' P = finrank R S

Tactic:
rw [inertiaDeg', dif_pos (over_def P (⊥ : Ideal R)).symm]
  replace hP : P = ⊥ := eq_bot_of_liesOver_bot R P
  rw [Algebra.finrank_eq_of_equiv_equiv (RingEquiv.quotientBot R).symm
    ((quotEquivOfEq hP).trans (RingEquiv.quotientBot S)).symm]
  rfl

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

Goal state before:
pp: K : Type u_4
L : Type u_5
F : Type u_6
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field F
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K F
E : Type u_7
inst✝⁶ : Field E
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra L F
inst✝³ : IsScalarTower K L F
inst✝² : IsAlgClosed E
inst✝¹ : Algebra.IsSeparable K F
inst✝ : FiniteDimensional K F
pb : PowerBasis K L
⊢ ∏ σ, σ ((algebraMap L F) pb.gen) = (∏ σ, σ pb.gen) ^ finrank L F

Tactic:
by
  have : FiniteDimensional L F := FiniteDimensional.right K L F
  have : Algebra.IsSeparable L F := Algebra.isSeparable_tower_top_of_isSeparable K L F
  let : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
  rw [Fintype.prod_equiv algHomEquivSigma (fun σ : F →ₐ[K] E => _) fun σ => σ.1 pb.gen,
    ← Finset.univ_sigma_univ, Finset.prod_sigma, ← Finset.prod_pow]
  · refine Finset.prod_congr rfl fun σ _ => ?_
    let : Algebra L E := σ.toRingHom.toAlgebra
    simp_rw [Finset.prod_const]
    congr
    exact AlgHom.card L F E
  · intro σ
    simp only [algHomEquivSigma, Equiv.coe_fn_mk, AlgHom.domRestrict, AlgHom.comp_apply,
      IsScalarTower.coe_toAlgHom']

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
⊢ f (a * b) = f a * f b

Tactic:
by
  let := Classical.decEq α
  by_cases ha0 : a = 0
  · rw [ha0, zero_mul, h0, zero_mul]
  by_cases hb0 : b = 0
  · rw [hb0, mul_zero, h0, mul_zero]
  by_cases hf1 : f 1 = 0
  · calc
      f (a * b) = f (a * b * 1) := by rw [mul_one]
      _ = 0 := by simp only [h1 isUnit_one, hf1, mul_zero]
      _ = f a * f (b * 1) := by simp only [h1 isUnit_one, hf1, mul_zero]
      _ = f a * f b := by rw [mul_one]
  have : Nontrivial α := ⟨⟨_, _, ha0⟩⟩
  let : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
  suffices
      f (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ ((normalizedFactors a).count p + (normalizedFactors b).count p)) =
      f (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (normalizedFactors a).count p) *
      f (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (normalizedFactors b).count p) by
    obtain ⟨ua, a_eq⟩ := prod_normalizedFactors ha0
    obtain ⟨ub, b_eq⟩ := prod_normalizedFactors hb0
    rw [← a_eq, ← b_eq, mul_right_comm (Multiset.prod (normalizedFactors a)) ua
        (Multiset.prod (normalizedFactors b) * ub), h1 ua.isUnit, h1 ub.isUnit, h1 ua.isUnit, ←
      mul_assoc, h1 ub.isUnit, mul_right_comm _ (f ua), ← mul_assoc]
    congr
    rw [← (normalizedFactors a).map_id, ← (normalizedFactors b).map_id,
      Finset.prod_multiset_map_count, Finset.prod_multiset_map_count,
      Finset.prod_subset (Finset.subset_union_left (s₂ := (normalizedFactors b).toFinset)),
      Finset.prod_subset (Finset.subset_union_right (s₂ := (normalizedFactors b).toFinset)), ←
      Finset.prod_mul_distrib]
    · simp_rw [id, ← pow_add, this]
    all_goals simp only [Multiset.mem_toFinset]
    · intro p _ hpb
      simp [hpb]
    · intro p _ hpa
      simp [hpa]
  refine multiplicative_prime_power _ _ _ ?_ ?_ @h1 @hpr @hcp
  all_goals simp only [Multiset.mem_toFinset, Finset.mem_union]
  · rintro p (hpa | hpb) <;> apply prime_of_normalized_factor <;> assumption
  · rintro p (hp | hp) q (hq | hq) hdvd <;>
      rw [← normalize_normalized_factor _ hp, ← normalize_normalized_factor _ hq] <;>
      exact
        normalize_eq_normalize hdvd
          ((prime_of_normalized_factor _ hp).irreducible.dvd_symm
            (prime_of_normalized_factor _ hq).irreducible hdvd)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case pos
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : r = 0
⊢ absNorm (span {r}) = (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs

Tactic:
simp only [hr, Ideal.span_zero, Ideal.absNorm_bot,
      LinearMap.det_zero'', Set.singleton_zero, map_zero, Int.natAbs_zero]

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ ↑((S.leftInvEquiv hS).symm x) * ↑x = 1

Tactic:
convert! S.mul_leftInvEquiv hS ((S.leftInvEquiv hS).symm x)
  simp

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case pos
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDedekindDomain S
inst✝² : IsDedekindDomain R
inst✝¹ : FaithfulSMul R S
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hw : Irreducible w
hw_bot : w ≠ ⊥
inst✝ : w.LiesOver v
hp_bot : map f p ≠ ⊥
hvp : v = p
⊢ emultiplicity w (map f p) = ↑(v.ramificationIdx' w) * emultiplicity v p

Tactic:
simp [hvp, (FiniteMultiplicity.of_prime_left hp hp.ne_zero).emultiplicity_self,
      ramificationIdx'_eq_normalizedFactors_count hp_bot (isPrime_of_prime hw.prime) hw_bot,
      emultiplicity_eq_count_normalizedFactors hw hp_bot]

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

Goal state before:
pp: case h₂
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B✝ : Type w
inst✝³ : CommRing B✝
inst✝² : FormallyUnramified R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type w
inst✝¹ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [inst : Algebra R (B ⧸ I)], Function.Injective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
inst✝ : Algebra R B
g₁ g₂ : A →ₐ[R] B
x : A
e : (Ideal.Quotient.mk J) (g₁ x) = (Ideal.Quotient.mk J) (g₂ x)
⊢ (Ideal.Quotient.mk I) (g₁ x - g₂ x) ∈ Ideal.map (Ideal.Quotient.mk I) J

Tactic:
Ideal.mem_quotient_iff_mem hIJ,

Goal state after:
case h₂
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B✝ : Type w
inst✝³ : CommRing B✝
inst✝² : FormallyUnramified R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type w
inst✝¹ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [inst : Algebra R (B ⧸ I)], Function.Injective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
inst✝ : Algebra R B
g₁ g₂ : A →ₐ[R] B
x : A
e : (Ideal.Quotient.mk J) (g₁ x) = (Ideal.Quotient.mk J) (g₂ x)
⊢ g₁ x - g₂ x ∈ J
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
P₁ : Extension R A
P₂ : Extension R A
f : P₁.Hom P₂
inst✝¹ : FormallySmooth R P₁.Ring
inst✝ : FormallySmooth R P₂.Ring
x : P₁.H1Cotangent
⊢ (↑A (map (P₁.homInfinitesimal P₂)) ∘ₗ map P₁.toInfinitesimal) x = (↑A (map P₂.toInfinitesimal) ∘ₗ map f) x

Tactic:
← map_comp,

Goal state after:
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
P₁ : Extension R A
P₂ : Extension R A
f : P₁.Hom P₂
inst✝¹ : FormallySmooth R P₁.Ring
inst✝ : FormallySmooth R P₂.Ring
x : P₁.H1Cotangent
⊢ (map ((P₁.homInfinitesimal P₂).comp P₁.toInfinitesimal)) x = (↑A (map P₂.toInfinitesimal) ∘ₗ map f) x
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
P₁ : Extension R A
P₂ : Extension R A
f : P₁.Hom P₂
inst✝¹ : FormallySmooth R P₁.Ring
inst✝ : FormallySmooth R P₂.Ring
x : P₁.H1Cotangent
⊢ (map ((P₁.homInfinitesimal P₂).comp P₁.toInfinitesimal)) x = (↑A (map P₂.toInfinitesimal) ∘ₗ map f) x

Tactic:
← map_comp,

Goal state after:
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
P₁ : Extension R A
P₂ : Extension R A
f : P₁.Hom P₂
inst✝¹ : FormallySmooth R P₁.Ring
inst✝ : FormallySmooth R P₂.Ring
x : P₁.H1Cotangent
⊢ (map ((P₁.homInfinitesimal P₂).comp P₁.toInfinitesimal)) x = (map (P₂.toInfinitesimal.comp f)) x
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case mul_X
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 σ
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower (Q.comp P).Ring (Q.comp P).Ring T
p : MvPolynomial (ι ⊕ σ) R
n : ι ⊕ σ
IH :
  (δAux R Q) ((Q.ofComp P).toAlgHom p) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2
⊢ (δAux R Q) ((Q.ofComp P).toAlgHom (p * X n)) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) (p * X n))).2

Tactic:
simp only [map_mul, Hom.toAlgHom_X, ofComp_val, δAux_mul,
      ← @IsScalarTower.algebraMap_smul Q.Ring T, algebraMap_apply, Hom.algebraMap_toAlgHom,
      algebraMap_self, map_aeval, RingHomCompTriple.comp_eq, comp_val, RingHom.id_apply,
      IH, Derivation.leibniz, tmul_add, tmul_smul, ← cotangentSpaceBasis_apply, coe_eval₂Hom,
      ← @IsScalarTower.algebraMap_smul (Q.comp P).Ring T, aeval_X, map_smul, Prod.snd_add,
      Prod.smul_snd, map_add]
    obtain (n | n) := n
    · simp only [Sum.elim_inl, δAux_X, smul_zero, aeval_X,
        CotangentSpace.compEquiv, LinearEquiv.trans_apply, Basis.repr_symm_apply, zero_add,
        Basis.repr_self, Finsupp.linearCombination_single, Basis.prod_apply, LinearMap.coe_inl,
        LinearMap.coe_inr, Function.comp_apply, one_smul, map_zero]
    · simp only [Sum.elim_inr, Function.comp_apply, algHom_C, δAux_C,
        CotangentSpace.compEquiv, LinearEquiv.trans_apply, Basis.repr_symm_apply,
        algebraMap_smul, Basis.repr_self, Finsupp.linearCombination_single, Basis.prod_apply,
        LinearMap.coe_inr, Basis.baseChange_apply, one_smul, LinearMap.baseChange_tmul,
        toKaehler_cotangentSpaceBasis, add_left_inj, LinearMap.coe_inl]
      rfl

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

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
x : P
⊢ ((IsScalarTower.toAlgHom R P S).comp (sectionOfRetractionKerToTensorAux l hl σ hσ hf')) ((algebraMap P S) x) =
    (AlgHom.id R S) ((algebraMap P S) x)

Tactic:
simp [sectionOfRetractionKerToTensorAux_algebraMap, RingHom.mem_ker.mp]

Goal state after: