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

Goal state before:
pp: a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
⊢ ∃ d, a = d ^ k

Tactic:
obtain ⟨d, hd⟩ := exists_associated_pow_of_mul_eq_pow' hab h
  replace hd := hd.symm
  rw [associated_iff_natAbs, natAbs_eq_natAbs_iff, ← hk.neg_pow] at hd
  obtain rfl | rfl := hd <;> exact ⟨_, rfl⟩

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
e : Fin (Module.finrank K L) ≃ ↥(Submonoid.powers (frobeniusAlgHom K L)) := (finCongr ⋯).symm.trans (finEquivPowers ⋯)
⊢ Module.finrank K L = Nat.card (Fin (Module.finrank K L))

Tactic:
by simp

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Group G
inst✝¹⁵ : Finite G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹² : Q.IsPrime
inst✝¹¹ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra (A ⧸ P) K
inst✝⁷ : Algebra (B ⧸ Q) L
inst✝⁶ : Algebra (A ⧸ P) L
inst✝⁵ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower (A ⧸ P) K L
inst✝² : Algebra.IsInvariant A B G
inst✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
hy : y ∈ nonZeroDivisors (B ⧸ Q)
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y) =
      (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
b : B ⧸ Q
a : A ⧸ P
ha : a ≠ 0
h : a • x = y * b
⊢ ¬(algebraMap (A ⧸ P) K) a = 0

Tactic:
algebraMap_eq_zero_iff

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Group G
inst✝¹⁵ : Finite G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹² : Q.IsPrime
inst✝¹¹ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra (A ⧸ P) K
inst✝⁷ : Algebra (B ⧸ Q) L
inst✝⁶ : Algebra (A ⧸ P) L
inst✝⁵ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower (A ⧸ P) K L
inst✝² : Algebra.IsInvariant A B G
inst✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
hy : y ∈ nonZeroDivisors (B ⧸ Q)
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y) =
      (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
b : B ⧸ Q
a : A ⧸ P
ha : a ≠ 0
h : a • x = y * b
⊢ ¬a = 0
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case inr.inr
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
ha0 : ↑a ≠ 0
h : ¬IsUnit (↑a - 1)
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]

Tactic:
replace ha0 : 1 ≤ a := by
    contrapose! ha0
    rw [Nat.lt_one_iff.mp ha0, Nat.cast_zero]

Goal state after:
case inr.inr
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
h : ¬IsUnit (↑a - 1)
ha0 : 1 ≤ a
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
h : Function.Injective fun x ↦ x * x
⊢ -1 * -1 = 1 * 1

Tactic:
by simp

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

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
h : (fun x ↦ g ^ x) n ^ (Nat.card F / 2) = 1
key : 2 * (Nat.card F / 2) ∣ n * (Nat.card F / 2)
⊢ 0 < 2

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
N : Type u_4
inst✝² : Semiring N
inst✝¹ : Module N S
inst✝ : SMulCommClass R N S
b : Basis ι R S
x : S
hx : x ≠ 0
i : ι
⊢ ((↑(b.constr N)).toFun (Subtype.val ∘ ⇑(basisSpanSingleton b hx))) (b i) = ((Algebra.lmul R S) x) (b i)

Tactic:
by simp

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 R
P : Ideal S
inst✝ : P.LiesOver p
⊢ p.inertiaDeg' P = finrank (R ⧸ p) (S ⧸ P)

Tactic:
by
  rw [inertiaDeg', dif_pos (over_def P p).symm]

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

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
c_mem : c ∈ P ^ i
this : P ^ (i + 1) = span {a} ⊔ P ^ (i + 1)
⊢ 0 ∈ P ^ (i + 1)

Tactic:
by simp

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

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
c_mem : c ∈ P ^ i
this : P ^ (i + 1) = span {a} ⊔ P ^ (i + 1)
⊢ a + 0 = a

Tactic:
by simp

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

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✝ : 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)
this : ∀ (i : ℕ), Module.Finite R (S ⧸ I ^ i)
n : ℕ
hn : I ^ n = ⊥
e : (S ⧸ I ^ n) ≃ₐ[R] S := ⋯ ▸ AlgEquiv.quotientBot R S
⊢ Module.Finite R S

Tactic:
exact .of_surjective e.toLinearMap e.surjective

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

Goal state before:
pp: case IJ
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
I : Ideal S
hI : Nat.Prime (absNorm I)
this : (span {↑(absNorm I)}).IsPrime
⊢ ↑(absNorm I) ∈ I

Tactic:
exact absNorm_mem I

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
⊢ ↑(IsUnit.unit ⋯)⁻¹ * ↑x = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hS' : IsPreirreducible S
hf₁ : Continuous[inst✝², inst✝¹] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
⊢ (f '' closure[inst✝²] S).Subsingleton

Tactic:
replace hS' : IsIrreducible S := ⟨hS'', hS'⟩

Goal state after:
case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst✝², inst✝¹] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
⊢ (f '' closure[inst✝²] S).Subsingleton
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
⊢ length A ↥q = length A ↥p + length (ResidueField A) (ResidueField B)

Tactic:
have : Function.Exact f g := exact_iff.mpr ((e.ker_comp f.range.mkQ).trans f.range.ker_mkQ)

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 ↥q = length A ↥p + length (ResidueField A) (ResidueField B)
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: case pos
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
q : Ideal S
r : Ideal T
inst✝ : r.LiesOver q
hr : r.IsPrime
this✝¹ : q.IsPrime
this✝ : q.LiesOver (under R r)
this : Algebra (Localization.AtPrime (under R r)) (Localization.AtPrime r) :=
  Localization.AtPrime.algebraOfLiesOver (under R r) r
⊢ r.inertiaDeg R = q.inertiaDeg R * r.inertiaDeg S

Tactic:
let := Localization.AtPrime.algebraOfLiesOver (r.under R) q

Goal state after:
case pos
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
q : Ideal S
r : Ideal T
inst✝ : r.LiesOver q
hr : r.IsPrime
this✝² : q.IsPrime
this✝¹ : q.LiesOver (under R r)
this✝ : Algebra (Localization.AtPrime (under R r)) (Localization.AtPrime r) :=
  Localization.AtPrime.algebraOfLiesOver (under R r) r
this : Algebra (Localization.AtPrime (under R r)) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver (under R r) q
⊢ r.inertiaDeg R = q.inertiaDeg R * r.inertiaDeg S
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 S
n : ℕ
hn : ∀ a ∈ {n | map f ⊥ ≤ P ^ n}, a ≤ n
⊢ n.succ ∈ {n | map f ⊥ ≤ P ^ n}

Tactic:
by simp

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
h : ¬map f p ≤ P
⊢ map f p ≤ P ^ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.IdempotentFG

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r * n = n
x : R
hx : x ∈ I
⊢ x ∈ R ∙ r

Tactic:
rw [← hr' x hx]

Goal state after:
case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r * n = n
x : R
hx : x ∈ I
⊢ r * x ∈ R ∙ r
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
inst✝ : IsDedekindDomain S
h₁ : map f p ≠ ⊤
h₂ : map f p ≠ ⊥
⊢ map f p ≤ map f p ^ 1

Tactic:
by simp

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

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
e : S ⊗[R] S
he : IsIdempotentElem e
hsp : KaehlerDifferential.ideal R S = S ⊗[R] S ∙ e
⊢ e + (1 - e) = 1

Tactic:
by simp

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)
h₁ :
  ∀ (k : I),
    ((f.sum fun i y ↦ (b.repr (b i * x)) k • b.repr y).sum fun j z ↦ z • b j ⊗ₜ[R] b k) =
      f.sum fun i y ↦ (b.repr y).sum fun j z ↦ (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
⊢ ∑ i ∈ f.support, ∑ x ∈ (a i).support, ((a i) x • f i) ⊗ₜ[R] b x =
    ∑ y ∈ f.support,
      ∑ x_1 ∈ f.support.biUnion fun i ↦ (b.repr (b i * x)).support,
        ∑ x_2 ∈ (b.repr (f y)).support, (b.repr (b y * x)) x_1 • (b.repr (f y)) x_2 • b x_2 ⊗ₜ[R] b x_1

Tactic:
TensorProduct.smul_tmul',

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)
h₁ :
  ∀ (k : I),
    ((f.sum fun i y ↦ (b.repr (b i * x)) k • b.repr y).sum fun j z ↦ z • b j ⊗ₜ[R] b k) =
      f.sum fun i y ↦ (b.repr y).sum fun j z ↦ (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
⊢ ∑ i ∈ f.support, ∑ x ∈ (a i).support, ((a i) x • f i) ⊗ₜ[R] b x =
    ∑ y ∈ f.support,
      ∑ x_1 ∈ f.support.biUnion fun i ↦ (b.repr (b i * x)).support,
        ∑ x_2 ∈ (b.repr (f y)).support, ((b.repr (b y * x)) x_1 • (b.repr (f y)) x_2 • b x_2) ⊗ₜ[R] b x_1
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✝² : Algebra.IsIntegral R S
inst✝¹ : FiniteType R T
s : S
inst✝ : IsLocalization.Away s T
A : Subalgebra R S := R[s]
⊢ s ∈ {s}

Tactic:
by simp

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✝² : Algebra.IsIntegral R S
inst✝¹ : FiniteType R T
s : S
inst✝ : IsLocalization.Away s T
A : Subalgebra R S := R[s]
sA : ↥A := ⟨s, ⋯⟩
f : Localization.Away sA →+* T := IsLocalization.Away.lift sA ⋯
this✝⁶ : Algebra (Localization.Away sA) T := f.toAlgebra
this✝⁵ : Algebra (↥A) (Localization.Away sA) := OreLocalization.instAlgebra
this✝⁴ : SMul (↥A) (Localization.Away sA) := this✝⁵.toSMul
this✝³ : MulAction (↥A) (Localization.Away sA) := toModule.toMulAction
this✝² : IsScalarTower R (↥A) (Localization.Away sA)
this✝¹ : IsScalarTower (↥A) (Localization.Away sA) T
this✝ : IsScalarTower R (Localization.Away sA) T
x : S
n : ℕ
this : IsIntegral (Localization.Away sA) ((algebraMap S T) x)
⊢ IsIntegral (Localization.Away sA) (IsLocalization.mk' T x ⟨(fun x ↦ s ^ x) n, ⋯⟩)

Tactic:
convert! this.smul (Localization.Away.invSelf sA ^ n)

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 R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra.IsIntegral R S
inst✝¹ : FiniteType R T
s : S
inst✝ : IsLocalization.Away s T
A : Subalgebra R S := R[s]
sA : ↥A := ⟨s, ⋯⟩
f : Localization.Away sA →+* T := IsLocalization.Away.lift sA ⋯
this✝⁶ : Algebra (Localization.Away sA) T := f.toAlgebra
this✝⁵ : Algebra (↥A) (Localization.Away sA) := OreLocalization.instAlgebra
this✝⁴ : SMul (↥A) (Localization.Away sA) := this✝⁵.toSMul
this✝³ : MulAction (↥A) (Localization.Away sA) := toModule.toMulAction
this✝² : IsScalarTower R (↥A) (Localization.Away sA)
this✝¹ : IsScalarTower (↥A) (Localization.Away sA) T
this✝ : IsScalarTower R (Localization.Away sA) T
x : S
n : ℕ
this : IsIntegral (Localization.Away sA) ((algebraMap S T) x)
⊢ IsLocalization.mk' T x ⟨(fun x ↦ s ^ x) n, ⋯⟩ = Localization.Away.invSelf sA ^ n • (algebraMap S T) x
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
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)) ⋯
i : I
⊢ ∑ x_1 ∈ (b.repr (x * f i)).support, (b.repr (x * f i)) x_1 • b x_1 ⊗ₜ[R] b i = (x * f i) ⊗ₜ[R] b i

Tactic:
TensorProduct.smul_tmul',

Goal state after:
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)) ⋯
i : I
⊢ ∑ x_1 ∈ (b.repr (x * f i)).support, ((b.repr (x * f i)) x_1 • b x_1) ⊗ₜ[R] b i = (x * f i) ⊗ₜ[R] b i
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
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B ⧸ I
P : Generators R A A := Generators.self R A
hP : Function.Injective ⇑P.toExtension.cotangentComplex
l : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
⊢ ∀ (x y : P.toExtension.Cotangent), (x + y).val = x.val + y.val

Tactic:
by simp

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 S
inst✝³ : p.IsPrime
inst✝² : IsArtinianRing R
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R p
y : Localization.AtPrime p
⊢ (y, 1).2 • y = LinearMap.id (y, 1).1

Tactic:
by simp

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✝² : IsClopen {p}
this✝² : IsNoetherianRing S
this✝¹ : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H✝¹ : {p} = ↑(PrimeSpectrum.basicOpen e)
hep : e ∉ p.asIdeal
f : Localization.Away e →ₐ[S] Localization.AtPrime p.asIdeal := IsLocalization.Away.liftAlgHom e ⋯
h₁ : Set.range (PrimeSpectrum.comap (algebraMap S (Localization.Away e))) = {p}
this✝ : Subsingleton (PrimeSpectrum (Localization.Away e))
x : S
s : ↥p.asIdeal.primeCompl
H✝ : ¬IsUnit ((algebraMap S (Localization.Away e)) ↑s)
M : Ideal (Localization.Away e)
hM : M.IsMaximal
H : Ideal.span {(algebraMap S (Localization.Away e)) ↑s} ≤ M
this :
  PrimeSpectrum.comap f.toRingHom (IsLocalRing.closedPoint (Localization.AtPrime p.asIdeal)) =
    { asIdeal := M, isPrime := ⋯ }
⊢ False

Tactic:
have := congr(($this).1).ge (H (Ideal.mem_span_singleton_self _))

Goal state after:
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✝² : IsClopen {p}
this✝³ : IsNoetherianRing S
this✝² : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H✝¹ : {p} = ↑(PrimeSpectrum.basicOpen e)
hep : e ∉ p.asIdeal
f : Localization.Away e →ₐ[S] Localization.AtPrime p.asIdeal := IsLocalization.Away.liftAlgHom e ⋯
h₁ : Set.range (PrimeSpectrum.comap (algebraMap S (Localization.Away e))) = {p}
this✝¹ : Subsingleton (PrimeSpectrum (Localization.Away e))
x : S
s : ↥p.asIdeal.primeCompl
H✝ : ¬IsUnit ((algebraMap S (Localization.Away e)) ↑s)
M : Ideal (Localization.Away e)
hM : M.IsMaximal
H : Ideal.span {(algebraMap S (Localization.Away e)) ↑s} ≤ M
this✝ :
  PrimeSpectrum.comap f.toRingHom (IsLocalRing.closedPoint (Localization.AtPrime p.asIdeal)) =
    { asIdeal := M, isPrime := ⋯ }
this :
  (algebraMap S (Localization.Away e)) ↑s ∈
    (PrimeSpectrum.comap f.toRingHom (IsLocalRing.closedPoint (Localization.AtPrime p.asIdeal))).asIdeal
⊢ False
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
B : Type u_1
P : Type u_2
C : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : CommRing C
inst✝³ : Algebra R C
inst✝² : CommRing P
inst✝¹ : Algebra R P
P₁ : Extension R A
P₂ : Extension R A
inst✝ : FormallySmooth R P₁.Ring
lift : P₁.Ring →ₐ[R] P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
⊢ ∀ (x : R),
    (Ideal.Quotient.liftₐ (P₁.ker ^ 2) lift ⋯).toRingHom ((algebraMap R P₁.infinitesimal.Ring) x) =
      (algebraMap R P₂.infinitesimal.Ring) ((algebraMap R R) x)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Function.Surjective ⇑(algebraMap R A)
H : IsIdempotentElem (RingHom.ker (algebraMap R A))
e : (R ⧸ RingHom.ker (algebraMap R A) ^ 2) ≃ₐ[R] A :=
  (Ideal.quotientEquivAlgOfEq R ⋯).trans (Ideal.quotientKerAlgEquivOfSurjective h)
x : R
⊢ ((ofId R A).kerSquareLift.comp ↑e.symm) ((algebraMap R A) x) = (AlgHom.id R A) ((algebraMap R A) x)

Tactic:
by simp

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

Goal state before:
pp: case refine_2
R✝ : Type u
A✝ : Type v
inst✝¹⁴ : CommRing R✝
inst✝¹³ : CommRing A✝
inst✝¹² : Algebra R✝ A✝
B✝ : Type u_1
P : Type u_2
C✝ : Type u_3
inst✝¹¹ : CommRing B✝
inst✝¹⁰ : Algebra R✝ B✝
inst✝⁹ : CommRing C✝
inst✝⁸ : Algebra R✝ C✝
inst✝⁷ : CommRing P
inst✝⁶ : Algebra R✝ P
R : Type u_4
inst✝⁵ : CommRing R
A : Type u_5
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_6
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
C : Type (max u_5 u_6)
x✝¹ : CommRing C
x✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this✝ : Algebra R C := ((algebraMap B C).comp (algebraMap R B)).toAlgebra
this : IsScalarTower R B C
b : B
a : A
⊢ f (b • 1 ⊗ₜ[R] a) = f (b ⊗ₜ[R] a)

Tactic:
TensorProduct.smul_tmul',

Goal state after:
case refine_2
R✝ : Type u
A✝ : Type v
inst✝¹⁴ : CommRing R✝
inst✝¹³ : CommRing A✝
inst✝¹² : Algebra R✝ A✝
B✝ : Type u_1
P : Type u_2
C✝ : Type u_3
inst✝¹¹ : CommRing B✝
inst✝¹⁰ : Algebra R✝ B✝
inst✝⁹ : CommRing C✝
inst✝⁸ : Algebra R✝ C✝
inst✝⁷ : CommRing P
inst✝⁶ : Algebra R✝ P
R : Type u_4
inst✝⁵ : CommRing R
A : Type u_5
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_6
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
C : Type (max u_5 u_6)
x✝¹ : CommRing C
x✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this✝ : Algebra R C := ((algebraMap B C).comp (algebraMap R B)).toAlgebra
this : IsScalarTower R B C
b : B
a : A
⊢ f ((b • 1) ⊗ₜ[R] a) = f (b ⊗ₜ[R] a)