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

Goal state before:
pp: F : Type u_3
inst✝² : Field F
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP F p
x✝ : Fintype ↥⊥ := fintypeBot F p
⊢ (X ^ p - X).roots = univ.val

Tactic:
conv_lhs => rw [← card_bot F p, ← Fintype.card_eq_nat_card]

Goal state after:
F : Type u_3
inst✝² : Field F
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP F p
x✝ : Fintype ↥⊥ := fintypeBot F p
⊢ (X ^ Fintype.card ↥⊥ - X).roots = univ.val
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
ha : a ≠ 0
hb : x * (algebraMap A B) a = b * y
⊢ (algebraMap B L) ((algebraMap A B) a) ≠ 0

Tactic:
simpa [← hc]

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 : α
hdp : d ∣ p ^ i p
hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'
hd : Prime d
⊢ False

Tactic:
apply hps

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
hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'
hd : Prime d
⊢ p ∈ s
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:
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: 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
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∏ a, ∏ s, ⟨a, s⟩.fst pb.gen = ∏ x, x pb.gen ^ finrank L F

Tactic:
refine Finset.prod_congr rfl fun σ _ => ?_
    let : Algebra L E := σ.toRingHom.toAlgebra
    simp_rw [Finset.prod_const]
    congr
    exact AlgHom.card L F E

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

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 S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
⊢ p.inertiaDeg' I = p.inertiaDeg' P * P.inertiaDeg' I

Tactic:
simp only [inertiaDeg', dif_pos h₁.symm, dif_pos h₂.symm, dif_pos h₃.symm]

Goal state after:
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 S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
⊢ finrank (R ⧸ p) (T ⧸ I) = finrank (R ⧸ p) (S ⧸ P) * finrank (S ⧸ P) (T ⧸ I)
Module: Mathlib.RingTheory.Finiteness.NilpotentKer

Goal state before:
pp: case succ.refine_2
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✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this : Module.Finite R (S ⧸ I)
n : ℕ
IH : Module.Finite R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective ⇑φ
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
⊢ (⊤ ⊓ (↑R φ.toLinearMap).ker).FG

Tactic:
have : Module.Finite R ((S ⧸ I) ⊗[S] ↑(I ^ n)) := by
        have : Module.Finite S ↑(I ^ n) := .of_fg (.pow hf₃ _)
        exact .trans (S ⧸ I) _
      let ψ : (S ⧸ I) ⊗[S] ↑(I ^ n) →ₗ[S] (S ⧸ I ^ (n + 1)) := by
        refine ?_ ∘ₗ (TensorProduct.quotTensorEquivQuotSMul _ I).toLinearMap
        refine Submodule.liftQ _ ((Submodule.mkQ _).comp (I ^ n).subtype) ?_
        rw [LinearMap.ker_comp, ← Submodule.map_le_map_iff_of_injective (I ^ n).subtype_injective,
          Submodule.map_smul'', Submodule.map_comap_eq]
        simpa [pow_succ'] using Ideal.mul_le_right (I := I) (J := I ^ n)
      convert! Module.Finite.fg_top.map (ψ.restrictScalars R) using 1
      suffices LinearMap.ker φ.toLinearMap = Submodule.map (I ^ (n + 1)).mkQ (I ^ n) by
        simpa [LinearMap.range_restrictScalars, ψ, LinearMap.range_comp, Submodule.range_liftQ]
      apply Submodule.comap_injective_of_surjective (I ^ (n + 1)).mkQ_surjective
      simpa [← LinearMap.ker_comp, hφ'] using Ideal.pow_le_pow_right n.le_succ

Goal state after:
Module: Mathlib.RingTheory.Localization.InvSubmonoid

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG ↥M
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
⊢ Algebra.FiniteType R S

Tactic:
refine ⟨⟨s, ?_⟩⟩

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG ↥M
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
⊢ Algebra.adjoin R ↑s = ⊤
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
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M].TFAE

Tactic:
by
  tfae_have 2 ↔ 3 := IsSemiprimaryRing.isNoetherian_iff_isArtinian
  tfae_have 2 → 1 := fun _ ↦ inferInstance
  tfae_have 1 → 3 := fun _ ↦ inferInstance
  rw [isFiniteLength_iff_isNoetherian_isArtinian]
  tfae_have 4 → 2 := And.left
  tfae_have 2 → 4 := fun h ↦ ⟨h, tfae_2_iff_3.mp h⟩
  tfae_finish

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

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
p q : Submodule B M
h : p ⋖ q
f : ↥p →ₗ[B] ↥q := inclusion ⋯
key : IsSimpleModule B (↥q ⧸ f.range)
m : Ideal B
hm : m.IsMaximal
e : (↥q ⧸ f.range) ≃ₗ[B] B ⧸ maximalIdeal B
g : ↥q →ₗ[B] ResidueField B := ↑e ∘ₗ f.range.mkQ
this✝¹ : Function.Injective ⇑f
this✝ : Function.Surjective ⇑g
this : Function.Exact ⇑f ⇑g
⊢ length A ↥p + length A (ResidueField B) = length A ↥p + length (ResidueField A) (ResidueField B)

Tactic:
Module.length_eq_of_surjective (M := ResidueField B)
      (residue_surjective (R := A)),

Goal state after:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
p q : Submodule B M
h : p ⋖ q
f : ↥p →ₗ[B] ↥q := inclusion ⋯
key : IsSimpleModule B (↥q ⧸ f.range)
m : Ideal B
hm : m.IsMaximal
e : (↥q ⧸ f.range) ≃ₗ[B] B ⧸ maximalIdeal B
g : ↥q →ₗ[B] ResidueField B := ↑e ∘ₗ f.range.mkQ
this✝¹ : Function.Injective ⇑f
this✝ : Function.Surjective ⇑g
this : Function.Exact ⇑f ⇑g
⊢ length A ↥p + length (ResidueField A) (ResidueField B) = length A ↥p + length (ResidueField A) (ResidueField B)
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
hp : map f p ≤ P
⊢ p.ramificationIdx' P ≠ 1 ↔ map f p ≤ P ^ 2

Tactic:
classical
  by_cases! H : ∀ n : ℕ, ∃ k, p.map f ≤ P ^ k ∧ n < k
  · obtain ⟨k, hk, h2k⟩ := H 2
    simp [Ideal.ramificationIdx'_eq_zero H, hk.trans (Ideal.pow_le_pow_right h2k.le)]
  rw [Ideal.ramificationIdx'_eq_find H]
  constructor
  · intro he
    have : 1 ≤ Nat.find H := Nat.find_spec H 1 (by simpa)
    have := Nat.find_min H (m := 1) (by lia)
    push Not at this
    obtain ⟨k, hk, h1k⟩ := this
    exact hk.trans (Ideal.pow_le_pow_right (Nat.succ_le_iff.mpr h1k))
  · intro he
    have := Nat.find_spec H 2 he
    lia

Goal state after:
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
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Ideal T
hp : p = comap f P
h : ¬sSup {n | map (algebraMap R T) p ≤ Q ^ n} = 0
n : ℕ
hn : n ∈ {n | map (algebraMap S T) P ≤ Q ^ n}
⊢ n ∈ {n | comap f P ≤ comap f (comap (algebraMap S T) (Q ^ n))}

Tactic:
exact comap_mono <| by rwa [← map_le_iff_le_comap]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective ⇑f
⊢ FormallyUnramified R B

Tactic:
by
  rw [iff_comp_injective]
  intro Q _ _ I hI f₁ f₂ e
  ext x
  obtain ⟨x, rfl⟩ := H x
  rw [← AlgHom.comp_apply, ← AlgHom.comp_apply]
  congr 1
  apply FormallyUnramified.comp_injective I hI
  ext x; exact DFunLike.congr_fun e (f x)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsArtinianRing R
p : PrimeSpectrum S
inst✝ : FiniteType R S
H : IsOpen {p}
⊢ QuasiFiniteAt R p.asIdeal

Tactic:
have : IsNoetherianRing S := Algebra.FiniteType.isNoetherianRing R S
  have : IsJacobsonRing S := isJacobsonRing_of_finiteType (A := R)
  rw [(PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing p).out
    0 1 rfl rfl] at H
  obtain ⟨e, he, H⟩ := PrimeSpectrum.isClopen_iff.mp H
  have hep : e ∉ p.asIdeal := H.le rfl
  let f : Localization.Away e →ₐ[S] Localization.AtPrime p.asIdeal :=
    IsLocalization.Away.liftAlgHom e (f := Algebra.ofId _ _)
      (IsLocalization.map_units (M := p.asIdeal.primeCompl) _ ⟨e, hep⟩)
  have h₁ := (PrimeSpectrum.localization_away_comap_range (Localization.Away e) e).trans H.symm
  have : Subsingleton (PrimeSpectrum (Localization.Away e)) :=
    Function.Injective.subsingleton
    (f := Set.codRestrict (PrimeSpectrum.comap (algebraMap S (Localization.Away e))) {p} fun x ↦
      h₁.le ⟨x, rfl⟩)
    ((Set.injective_codRestrict ..).mpr (PrimeSpectrum.localization_comap_injective _ (.powers e)))
  have hf : Function.Surjective f := by
    intro x
    obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq p.asIdeal.primeCompl x
    suffices IsUnit (algebraMap _ (Localization.Away e) s.1) by
      refine ⟨algebraMap _ _ x * this.unit⁻¹, (this.map f).mul_right_cancel ?_⟩
      simp only [← map_mul, mul_assoc, IsUnit.val_inv_mul]
      simp
    by_contra H
    obtain ⟨M, hM, H⟩ :=
      Ideal.exists_le_maximal (.span {algebraMap _ (Localization.Away e) s.1}) (by simpa)
    have := Subsingleton.elim ((IsLocalRing.closedPoint _).comap f.toRingHom) ⟨M, inferInstance⟩
    have := congr(($this).1).ge (H (Ideal.mem_span_singleton_self _))
    simp [IsLocalRing.closedPoint, IsLocalization.AtPrime.isUnit_to_map_iff _ p.asIdeal] at this
  have : Algebra.FiniteType R (Localization.AtPrime p.asIdeal) :=
    .of_surjective (f.restrictScalars R) hf
  have := (PrimeSpectrum.comap_injective_of_surjective f.toRingHom hf).subsingleton
  exact QuasiFinite.iff_finite_comap_preimage_singleton.mpr fun _ ↦
    Set.subsingleton_of_subsingleton.finite

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R q
e : ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) ≃ₜ
  PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S { asIdeal := p, isPrime := ⋯ }
⊢ ∃ s ∉ q, ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'

Tactic:
let qF : PrimeSpectrum (p.Fiber S) := e ⟨⟨q, ‹_›⟩, PrimeSpectrum.ext (q.over_def p).symm⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R q
e : ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) ≃ₜ
  PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S { asIdeal := p, isPrime := ⋯ }
qF : PrimeSpectrum (p.Fiber S) := e ⟨{ asIdeal := q, isPrime := inst✝³ }, ⋯⟩
⊢ ∃ s ∉ q, ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case h₂
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type u_1
inst✝¹ : CommRing B
inst✝ : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ [inst_1 : Algebra R S], Function.Surjective (Ideal.Quotient.mkₐ R I).comp) →
        (∀ [inst_1 : Algebra R (S ⧸ I)],
            Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
          ∀ [inst_1 : Algebra R S], Function.Surjective (Ideal.Quotient.mkₐ R J).comp

Tactic:
intro B _ I J hIJ h₁ h₂ _ g
    let : ((B ⧸ I) ⧸ J.map (Ideal.Quotient.mk I)) ≃ₐ[R] B ⧸ J :=
      { (DoubleQuot.quotQuotEquivQuotSup I J).trans
          (Ideal.quotEquivOfEq (sup_eq_right.mpr hIJ)) with
        commutes' := fun x => rfl }
    obtain ⟨g', e⟩ := h₂ (this.symm.toAlgHom.comp g)
    obtain ⟨g', rfl⟩ := h₁ g'
    replace e := congr_arg this.toAlgHom.comp e
    conv_rhs at e =>
      rw [← AlgHom.comp_assoc, AlgEquiv.comp_symm, AlgHom.id_comp]
    exact ⟨g', e⟩

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

Goal state before:
pp: R : Type u_4
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
M : Submonoid R
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : IsScalarTower R Rₘ Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : FormallySmooth R Sₘ
Q : Type (max u_6 u_7)
x✝¹ : CommRing Q
x✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
⊢ Sₘ →ₐ[Rₘ] Q

Tactic:
by
    refine { FormallySmooth.lift I ⟨2, e⟩ (f.restrictScalars R) with commutes' := ?_ }
    intro r
    change
      (RingHom.comp (FormallySmooth.lift I ⟨2, e⟩ (f.restrictScalars R) : Sₘ →+* Q)
            (algebraMap _ _))
          r =
        algebraMap _ _ r
    congr 1
    refine IsLocalization.ringHom_ext M ?_
    rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq,
      AlgHom.comp_algebraMap]

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

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
⊢ IsNilpotent (IsLocalRing.maximalIdeal A)

Tactic:
← IsLocalRing.jacobson_eq_maximalIdeal ⊥

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
⊢ IsNilpotent ⊥.jacobson

K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
⊢ ⊥ ≠ ⊤
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case refine_1.refine_1
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
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
this : Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) ≤ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker →
  P ⧸ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) →ₗ[R] S ⊗[P] Ω[P⁄R] :=
  (Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2)).liftQ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P))
x : P
hx : x ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)
⊢ ∀ r ∈ RingHom.ker (algebraMap P S), ∀ n ∈ RingHom.ker (algebraMap P S), 1 ⊗ₜ[P] (D R P) (r • n) = 0

pp: case refine_1.refine_2
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
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
this : Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) ≤ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker →
  P ⧸ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) →ₗ[R] S ⊗[P] Ω[P⁄R] :=
  (Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2)).liftQ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P))
x : P
hx : x ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)
⊢ ∀ (x y : P), 1 ⊗ₜ[P] (D R P) x = 0 → 1 ⊗ₜ[P] (D R P) y = 0 → 1 ⊗ₜ[P] (D R P) (x + y) = 0

Tactic:
· intro x hx y hy
      simp only [smul_eq_mul, Derivation.leibniz, tmul_add, ← smul_tmul, Algebra.smul_def,
        mul_one, RingHom.mem_ker.mp hx, RingHom.mem_ker.mp hy, zero_tmul, zero_add]

Goal state after:
case refine_1.refine_2
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
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
this : Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) ≤ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker →
  P ⧸ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) →ₗ[R] S ⊗[P] Ω[P⁄R] :=
  (Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2)).liftQ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P))
x : P
hx : x ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)
⊢ ∀ (x y : P), 1 ⊗ₜ[P] (D R P) x = 0 → 1 ⊗ₜ[P] (D R P) y = 0 → 1 ⊗ₜ[P] (D R P) (x + y) = 0
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
hq : p.primesOver S = {q}
inst✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
x : R
s : ↥p.primeCompl
hx : (localRingHom p q (algebraMap R S) ⋯) (IsLocalization.mk' (Localization.AtPrime p) x s) = 0
a : S
haq : a ∉ q
e : a * (algebraMap R S) x = 0
⊢ IsLocalization.mk' (Localization.AtPrime p) x s = 0

Tactic:
obtain ⟨r, hrp, t, e'⟩ := Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton hq _ haq

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
hq : p.primesOver S = {q}
inst✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
x : R
s : ↥p.primeCompl
hx : (localRingHom p q (algebraMap R S) ⋯) (IsLocalization.mk' (Localization.AtPrime p) x s) = 0
a : S
haq : a ∉ q
e : a * (algebraMap R S) x = 0
r : R
hrp : r ∉ p
t : S
e' : (algebraMap R S) r = a * t
⊢ IsLocalization.mk' (Localization.AtPrime p) x s = 0
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: S : Type u_1
inst✝⁵ : CommRing S
q : Ideal S
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R S
inst✝² : q.IsPrime
inst✝¹ : Algebra.EssFiniteType R S
inst✝ : Algebra.IsUnramifiedAt R q
p : Ideal R := under R q
Rp : Type u_2 := Localization.AtPrime p
Sq : Type u_1 := Localization.AtPrime q
this✝ : Algebra Rp Sq := Localization.AtPrime.algebraOfLiesOver p q
this : Algebra.EssFiniteType Rp Sq
⊢ Module.length (Localization.AtPrime q)
      (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q)) =
    ↑1

Tactic:
Nat.cast_one,

Goal state after:
S : Type u_1
inst✝⁵ : CommRing S
q : Ideal S
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R S
inst✝² : q.IsPrime
inst✝¹ : Algebra.EssFiniteType R S
inst✝ : Algebra.IsUnramifiedAt R q
p : Ideal R := under R q
Rp : Type u_2 := Localization.AtPrime p
Sq : Type u_1 := Localization.AtPrime q
this✝ : Algebra Rp Sq := Localization.AtPrime.algebraOfLiesOver p q
this : Algebra.EssFiniteType Rp Sq
⊢ Module.length (Localization.AtPrime q)
      (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q)) =
    1
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: S : Type u_1
inst✝⁶ : CommRing S
q : Ideal S
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
inst✝³ : q.IsPrime
inst✝² : Algebra.EssFiniteType R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : PerfectField (under R q).ResidueField
h :
  Module.length (Localization.AtPrime q)
      (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q)) =
    ↑1
⊢ Algebra.IsUnramifiedAt R q

Tactic:
Nat.cast_one,

Goal state after:
S : Type u_1
inst✝⁶ : CommRing S
q : Ideal S
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
inst✝³ : q.IsPrime
inst✝² : Algebra.EssFiniteType R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : PerfectField (under R q).ResidueField
h :
  Module.length (Localization.AtPrime q)
      (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q)) =
    1
⊢ Algebra.IsUnramifiedAt R q