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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : PowerBasis R S
⊢ (LinearMap.BilinForm.toMatrix h.basis) (traceForm R S) = of fun i j ↦ (trace R S) (h.gen ^ (↑i + ↑j))

Tactic:
ext; rw [traceForm_toMatrix, of_apply, pow_add, h.basis_eq_pow, h.basis_eq_pow]

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 L) x = finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x)

Tactic:
rw [← trace_trace (S := 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) x) =
    finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x)
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case inr.refine_2
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -↑n < -a.valMinAbs * 2

Tactic:
rw [neg_mul, neg_lt_neg_iff]

Goal state after:
case inr.refine_2
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ a.valMinAbs * 2 < ↑n
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case e_f.e_f
κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
α β x y : κ
⊢ (trace A B) (b y * (algebraMap A B) (P y α) * (b x * P.map (⇑(algebraMap A B)) x β)) =
    Pᵀ α y * traceMatrix A b y x * P x β

Tactic:
mul_comm (b y),

Goal state after:
case e_f.e_f
κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
α β x y : κ
⊢ (trace A B) ((algebraMap A B) (P y α) * b y * (b x * P.map (⇑(algebraMap A B)) x β)) =
    Pᵀ α y * traceMatrix A b y x * P x β
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: case refine_2
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁴ : Group G
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup (↥H) (↥F) L
x : L
hx : x ∈ F
⊢ x ∈ FixedPoints.intermediateField ↥H

Tactic:
have := congr_arg (restrictScalars K) <| IsGaloisGroup.fixedPoints_eq_bot H F L
    rw [restrictScalars_bot_eq_self] at this
    rwa [← this] at hx

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

Goal state before:
pp: case refine_2
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
⊢ (vandermonde fun i ↦ (e i) pb.gen)ᵀ.det * (vandermonde fun i ↦ (e i) pb.gen)ᵀᵀ.det ≠ 0

Tactic:
det_transpose

Goal state after:
case refine_2
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
⊢ (vandermonde fun i ↦ (e i) pb.gen).det * (vandermonde fun i ↦ (e i) pb.gen)ᵀᵀ.det ≠ 0
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: case e_6
G : Type u_1
G' : Type u_2
inst✝¹⁹ : Group G
inst✝¹⁸ : Group G'
A : Type u_5
B : Type u_6
C : Type u_7
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : CommRing C
inst✝¹⁴ : IsDomain C
inst✝¹³ : Algebra A B
inst✝¹² : Algebra A C
inst✝¹¹ : Algebra B C
inst✝¹⁰ : FaithfulSMul A B
inst✝⁹ : FaithfulSMul B C
inst✝⁸ : IsScalarTower A B C
inst✝⁷ : Finite G
inst✝⁶ : Finite G'
N : Subgroup G
inst✝⁵ : N.Normal
inst✝⁴ : MulSemiringAction G C
inst✝³ : IsGaloisGroup G A C
inst✝² : IsGaloisGroup (↥N) B C
inst✝¹ : MulSemiringAction G' B
inst✝ : IsGaloisGroup G' A B
g : G
x : B
this✝³ : IsDomain B
this✝² : MulSemiringAction G B := ⋯
this✝¹ : MulSemiringAction (G ⧸ N) B := ⋯
this✝ : SMulCommClass (G ⧸ N) A B
this : IsGaloisGroup (G ⧸ N) A B
⊢ (quotientMulEquiv G G' A B C N) ↑g • x = g • x

Tactic:
apply mulEquivCongr_apply_smul

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : Fintype K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this : Fintype L
m : ℕ
lt : m < Module.finrank K L
pos : 0 < m
eq : frobeniusAlgHom K L ^ m = 1
x : L
x✝ : x ∈ univ.val
⊢ x ∈ (X ^ q ^ m - X).roots

Tactic:
by
      simp_rw [mem_roots', IsRoot, eval_sub, eval_pow, eval_X]
      have := DFunLike.congr_fun eq x
      rw [AlgHom.coe_pow, coe_frobeniusAlgHom, pow_iterate, AlgHom.one_apply, ← sub_eq_zero] at this
      refine ⟨fun h ↦ ?_, this⟩
      simpa [Fintype.one_lt_card.ne, pos.ne, eqComm] using congr_arg (coeff · 1) h

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

Goal state before:
pp: K : Type u_1
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : DivisionRing K
inst✝ : CharP K p
⊢ (castHom ⋯ K).fieldRange = ⊥

Tactic:
RingHom.fieldRange_eq_map,

Goal state after:
K : Type u_1
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : DivisionRing K
inst✝ : CharP K p
⊢ Subfield.map (castHom ⋯ K) ⊤ = ⊥
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case succ
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ ∑ k ∈ range p, (p ^ m * d) ^ (k + 1) * 1 ^ (p - (k + 1)) * ↑(p.choose (k + 1)) + ↑(p.choose 0) ≡ 1 [MOD p ^ m * p]

Tactic:
Nat.choose_zero_right,

Goal state after:
case succ
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ ∑ k ∈ range p, (p ^ m * d) ^ (k + 1) * 1 ^ (p - (k + 1)) * ↑(p.choose (k + 1)) + ↑1 ≡ 1 [MOD p ^ m * p]
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: p m a : ℕ
⊢ (1 + p * a) ^ p ^ m ≡ 1 [MOD p ^ m]

Tactic:
by
  induction m with
  | zero => exact Nat.modEq_one
  | succ m hm =>
    rw [Nat.ModEq.comm, add_comm, Nat.modEq_iff_dvd' (Nat.one_le_pow' _ _)] at hm
    obtain ⟨d, hd⟩ := hm
    rw [tsub_eq_iff_eq_add_of_le (Nat.one_le_pow' _ _), add_comm] at hd
    rw [pow_succ, pow_mul, hd, add_pow, Finset.sum_range_succ', pow_zero, one_mul, one_pow,
      one_mul, Nat.choose_zero_right, Nat.cast_one]
    refine Nat.ModEq.add_right 1 (Nat.modEq_zero_iff_dvd.mpr ?_)
    simp_rw [one_pow, mul_one, pow_succ', mul_assoc, ← Finset.mul_sum]
    refine mul_dvd_mul_left (p ^ m) (dvd_mul_of_dvd_right (Finset.dvd_sum fun k hk ↦ ?_) d)
    cases m
    · rw [pow_zero, pow_one, one_mul, add_comm, add_left_inj] at hd
      cases k <;> simp [← hd, mul_assoc, pow_succ']
    · cases k <;> simp [mul_assoc, pow_succ']

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

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this✝¹ : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
ha0 : ¬a = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
⊢ ∀ p ∈ normalizedFactors a, Prime p

pp: case neg.refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this✝¹ : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
ha0 : ¬a = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
⊢ ∀ p ∈ normalizedFactors a, ∀ q ∈ normalizedFactors a, p ∣ q → p = q

Tactic:
· apply prime_of_normalized_factor

Goal state after:
case neg.refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this✝¹ : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
ha0 : ¬a = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
⊢ ∀ p ∈ normalizedFactors a, ∀ q ∈ normalizedFactors a, p ∣ q → p = q
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: A₁ : Type u_8
B₁ : Type u_9
A₂ : Type u_10
B₂ : Type u_11
inst✝⁵ : CommRing A₁
inst✝⁴ : Ring B₁
inst✝³ : CommRing A₂
inst✝² : Ring B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x : B₁
⊢ (norm A₁) x = e₁.symm ((norm A₂) (e₂ x))

Tactic:
by
  let := (RingHom.comp (e₂ : B₁ →+* B₂) (algebraMap A₁ B₁)).toAlgebra' ?_
  · let e' : B₁ ≃ₐ[A₁] B₂ := { e₂ with commutes' := fun _ ↦ rfl }
    rw [← Algebra.norm_eq_of_ringEquiv e₁ he, ← Algebra.norm_eq_of_algEquiv e']
    simp [e']
  intro c x
  apply e₂.symm.injective
  simp only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, map_mul,
    RingEquiv.symm_apply_apply, commutes]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.NilpotentKer

Goal state before:
pp: case succ.refine_1
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)
⊢ (Submodule.map (↑R φ.toLinearMap) ⊤).FG

Tactic:
simpa [LinearMap.range_eq_top_of_surjective (φ.toLinearMap.restrictScalars R) hφ] using
        Module.Finite.fg_top

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

Goal state before:
pp: case refine_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
⊢ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q

Tactic:
intro q hq e

Goal state after:
case refine_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
q : Ideal R
hq : q.IsPrime
e : q ≠ p
⊢ r ∈ q
Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian

Goal state before:
pp: case refine_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this✝ : (algebraMap R (Localization p.primeCompl)) r = 1
q : Ideal R
hq : q.IsPrime
e : q ≠ p
this : { asIdeal := q, isPrime := ⋯ } ≠ { asIdeal := p, isPrime := ⋯ }
⊢ r ∈ q

Tactic:
have : (algebraMap R (Localization.AtPrime q)) r = 0 := by
      simpa [PrimeSpectrum.toPiLocalization, this,
        -FaithfulSMul.algebraMap_eq_zero_iff] using funext_iff.mp hr ⟨q, inferInstance⟩

Goal state after:
case refine_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this✝¹ : (algebraMap R (Localization p.primeCompl)) r = 1
q : Ideal R
hq : q.IsPrime
e : q ≠ p
this✝ : { asIdeal := q, isPrime := ⋯ } ≠ { asIdeal := p, isPrime := ⋯ }
this : (algebraMap R (Localization.AtPrime q)) r = 0
⊢ r ∈ q
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Function.Injective f
hf' : Continuous[inst✝¹, inst✝] f
x : X
hx : x ∈ f ⁻¹' closedPoints Y
⊢ {x} = f ⁻¹' {f x}

Tactic:
← Set.image_singleton,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Function.Injective f
hf' : Continuous[inst✝¹, inst✝] f
x : X
hx : x ∈ f ⁻¹' closedPoints Y
⊢ {x} = f ⁻¹' f '' {x}
Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
tfae_2_to_3 : IsClopen {x} → IsClosed {x} ∧ StableUnderGeneralization {x}
h₁ : IsMax x
h₂ : StableUnderGeneralization {x}
this : {x} = (⋃ p ∈ {p | IsMin p ∧ p ≠ x}, closure {p})ᶜ
⊢ IsOpen {x}

Tactic:
by
      rw [this, isOpen_compl_iff]
      refine Set.Finite.isClosed_biUnion ?_ (fun _ _ ↦ isClosed_closure)
      exact (finite_setOfPred_isMin R).subset fun x h ↦ h.1

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsOpenEmbedding f
⊢ JacobsonSpace X

Tactic:
rw [jacobsonSpace_iff_locallyClosed, ← hf.preimage_closedPoints]

Goal state after:
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsOpenEmbedding f
⊢ ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ f ⁻¹' closedPoints Y).Nonempty
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsClosedEmbedding f
⊢ JacobsonSpace X

Tactic:
rw [jacobsonSpace_iff_locallyClosed, ← hf.preimage_closedPoints]

Goal state after:
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsClosedEmbedding f
⊢ ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ f ⁻¹' closedPoints Y).Nonempty
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 : ℕ
hn : n ≤ p.ramificationIdx' P
⊢ map f p ≤ P ^ n

Tactic:
contrapose! hn

Goal state after:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
n : ℕ
hn : ¬map f p ≤ P ^ n
⊢ p.ramificationIdx' P < n
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
g₁ g₂ : A →ₐ[R] B
h : (Ideal.Quotient.mkₐ R I).comp g₁ = (Ideal.Quotient.mkₐ R I).comp g₂
⊢ g₁ = g₂

Tactic:
revert g₁ g₂

Goal state after:
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ (g₁ g₂ : A →ₐ[R] B), (Ideal.Quotient.mkₐ R I).comp g₁ = (Ideal.Quotient.mkₐ R I).comp g₂ → g₁ = g₂
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
B : Type u_3
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : FormallyUnramified R B
⊢ ∀ ⦃B_1 : Type u_3⦄ [inst : CommRing B_1] [inst_1 : Algebra A B_1] (I : Ideal B_1),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ A I).comp

Tactic:
intro Q _ _ I e f₁ f₂ e'

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp f₂
⊢ f₁ = f₂
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j ↦ b.repr (x * f j)) ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun i ↦ (a i).support) (fun j ↦ b.repr (f.sum fun i y ↦ (a i) j • y)) ⋯
this✝ : F = G
this : ∀ (j : I), x * f j = f.sum fun i y ↦ (a i) j • y
i : I
hi : i ∈ f.support
j : I
hj : j ∈ f.support
⊢ (a j) i • (f j * b i) ∈ Submodule.span R (Set.image2 (fun i j ↦ f i * b j) ↑f.support ↑f.support)

Tactic:
apply Submodule.smul_mem

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := ⋯
b : Basis I R S := ⋯
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := ⋯
F : I →₀ I →₀ R := ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R := ⋯
this✝ : F = G
this : ∀ (j : I), x * f j = f.sum fun i y ↦ (a i) j • y
i : I
hi : i ∈ f.support
j : I
hj : j ∈ f.support
⊢ f j * b i ∈ Submodule.span R (Set.image2 (fun i j ↦ f i * b j) ↑f.support ↑f.support)
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 = (map (P₂.toInfinitesimal.comp f)) x

Tactic:
map_eq

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 ?g) x = (map (P₂.toInfinitesimal.comp f)) x

case g
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
⊢ P₁.Hom P₂.infinitesimal
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
⊢ RingHom.ker f.kerSquareLift.toRingHom ^ 2 = ⊥

Tactic:
rw [AlgHom.ker_kerSquareLift, Ideal.cotangentIdeal_square]

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
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g✝ : S →ₐ[R] P
f : P →ₐ[R] S
hf' : RingHom.ker f ^ 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
a b : P
this : (a - g (f a)) * (b - g (f b)) = 0
⊢ ↑({ toFun := fun x ↦ ⟨x - g (f x), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } (a * b)) -
      ↑(a • { toFun := fun x ↦ ⟨x - g (f x), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } b +
          b • { toFun := fun x ↦ ⟨x - g (f x), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } a) =
    -((a - g (f a)) * (b - g (f b)))

Tactic:
simp only [LinearMap.coe_mk, AddHom.coe_mk, map_mul, SetLike.mk_smul_mk, smul_eq_mul, mul_sub,
      AddMemClass.mk_add_mk, sub_mul, neg_sub]

Goal state after:
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
g✝ : S →ₐ[R] P
f : P →ₐ[R] S
hf' : RingHom.ker f ^ 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
a b : P
this : (a - g (f a)) * (b - g (f b)) = 0
⊢ a * b - g (f a) * g (f b) - (a * b - a * g (f b) + (b * a - b * g (f a))) =
    a * g (f b) - g (f a) * g (f b) - (a * b - g (f a) * b)
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case hF
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 σ
i : σ
⊢ (D R T) ((algebraMap S T) (P.val i)) =
    (Q.comp P).toExtension.toKaehler
      ((algebraMap S T) 1 ⊗ₜ[(Q.comp P).toExtension.Ring]
        (D R (Q.comp P).toExtension.Ring) ((Q.toComp P).toExtensionHom.toAlgHom (X i)))

Tactic:
simp only [map_one, mapBaseChange_tmul, map_D, one_smul]

Goal state after:
case hF
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 σ
i : σ
⊢ (D R T) ((algebraMap S T) (P.val i)) =
    (D R T) ((algebraMap (Q.comp P).toExtension.Ring T) ((Q.toComp P).toExtensionHom.toAlgHom (X i)))
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
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
mR : Ideal S := Ideal.map (algebraMap R S) (maximalIdeal R)
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))

Tactic:
have hmR : mR ≤ maximalIdeal S := ((local_hom_TFAE (algebraMap R S)).out 0 2 rfl rfl).mp ‹_›

Goal state after:
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✝ : FormallyUnramified R S
mR : Ideal S := Ideal.map (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))