mathlib-initiative/mathlib-tactics huggingface dataset:
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
κ : Type w
E : Type z
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Module.Finite K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsAlgClosed E
b : κ → L
inst✝ : Fintype κ
e : κ ≃ (L →ₐ[K] E)
⊢ (embeddingsMatrix K E b).submatrix _root_.id ⇑?e * (embeddingsMatrix K E b)ᵀ.submatrix (⇑?e) _root_.id =
    (embeddingsMatrix K E b).submatrix ⇑(Equiv.refl κ).symm ⇑e.symm.symm *
      (embeddingsMatrix K E b)ᵀ.submatrix ⇑e.symm.symm ⇑(Equiv.refl κ).symm

pp: case e
K : Type u_4
L : Type u_5
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
κ : Type w
E : Type z
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Module.Finite K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsAlgClosed E
b : κ → L
inst✝ : Fintype κ
e : κ ≃ (L →ₐ[K] E)
⊢ κ ≃ (L →ₐ[K] E)

Tactic:
← Equiv.coe_refl,

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
κ : Type w
E : Type z
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Module.Finite K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsAlgClosed E
b : κ → L
inst✝ : Fintype κ
e : κ ≃ (L →ₐ[K] E)
⊢ (embeddingsMatrix K E b).submatrix ⇑(Equiv.refl κ) ⇑?e * (embeddingsMatrix K E b)ᵀ.submatrix ⇑?e ⇑(Equiv.refl κ) =
    (embeddingsMatrix K E b).submatrix ⇑(Equiv.refl κ).symm ⇑e.symm.symm *
      (embeddingsMatrix K E b)ᵀ.submatrix ⇑e.symm.symm ⇑(Equiv.refl κ).symm

case e
K : Type u_4
L : Type u_5
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
κ : Type w
E : Type z
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Module.Finite K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsAlgClosed E
b : κ → L
inst✝ : Fintype κ
e : κ ≃ (L →ₐ[K] E)
⊢ κ ≃ (L →ₐ[K] E)
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
a_mul_emb : ↥G ↪ ↥G := ⋯
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x, ↑↑x = ↑↑a * ∑ x, ↑↑x
hzero : ↑↑a - 1 = 0 ∨ ∑ x, ↑↑x = 0
ha : ↑↑a - 1 = 0
⊢ ↑↑a = ↑↑1

Tactic:
← sub_eq_zero

Goal state after:
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x, ↑↑x = ↑↑a * ∑ x, ↑↑x
hzero : ↑↑a - 1 = 0 ∨ ∑ x, ↑↑x = 0
ha : ↑↑a - 1 = 0
⊢ ↑↑a - ↑↑1 = 0
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✝ : Module.IsTorsionFree (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((Ideal.Quotient.stabilizerHom Q P G) g) ((Ideal.Quotient.mk Q) b₀) = (Ideal.Quotient.mk Q) b₀
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb : ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a * b₀ else 0)
M : A[X]
key : map (algebraMap (A ⧸ P) (B ⧸ Q)) (map (algebraMap A (A ⧸ P)) M) = ∏ i, map (algebraMap B (B ⧸ Q)) (X - C (i • b))
⊢ ∀ (g : G),
    map (algebraMap B (B ⧸ Q)) (X - C (g • b)) = if g • Q = Q then X - C ((algebraMap B (B ⧸ Q)) (a * b₀)) else X

Tactic:
intro g

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✝ : Module.IsTorsionFree (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((Ideal.Quotient.stabilizerHom Q P G) g) ((Ideal.Quotient.mk Q) b₀) = (Ideal.Quotient.mk Q) b₀
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb : ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a * b₀ else 0)
M : A[X]
key : map (algebraMap (A ⧸ P) (B ⧸ Q)) (map (algebraMap A (A ⧸ P)) M) = ∏ i, map (algebraMap B (B ⧸ Q)) (X - C (i • b))
g : G
⊢ map (algebraMap B (B ⧸ Q)) (X - C (g • b)) = if g • Q = Q then X - C ((algebraMap B (B ⧸ Q)) (a * b₀)) else 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
ι : Type w
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ (pb.basis.toMatrix ⇑b * (pb.basis.toMatrix ⇑b)ᵀ).det * ((b.toMatrix ⇑pb.basis)ᵀ * b.toMatrix ⇑pb.basis).det =
    (pb.basis.toMatrix ⇑b * (b.toMatrix ⇑pb.basis * pb.basis.toMatrix ⇑b)ᵀ * b.toMatrix ⇑pb.basis).det

Tactic:
by
        simp only [← det_mul, Matrix.mul_assoc, Matrix.transpose_mul]

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

Goal state before:
pp: K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card ↥G
a✝ : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map : Multiset.map (fun x ↦ ↑↑x ^ k) univ.val = Multiset.map (fun x ↦ ↑↑x ^ k * ↑↑a ^ k) univ.val
h_multiset_map_sum :
  (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum = (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum * ↑↑a ^ k
hzero : ↑↑a ^ k - 1 = 0 ∨ (Multiset.map (fun i ↦ ↑↑i ^ k) univ.val).sum = 0
h : ↑↑a ^ k - 1 = 0
⊢ ↑↑(a ^ k) = ↑↑1

Tactic:
← sub_eq_zero

Goal state after:
K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card ↥G
a✝ : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map : Multiset.map (fun x ↦ ↑↑x ^ k) univ.val = Multiset.map (fun x ↦ ↑↑x ^ k * ↑↑a ^ k) univ.val
h_multiset_map_sum :
  (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum = (Multiset.map (fun x ↦ ↑↑x ^ k) univ.val).sum * ↑↑a ^ k
hzero : ↑↑a ^ k - 1 = 0 ∨ (Multiset.map (fun i ↦ ↑↑i ^ k) univ.val).sum = 0
h : ↑↑a ^ k - 1 = 0
⊢ ↑↑(a ^ k) - ↑↑1 = 0
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ orderOf x ∣ i

Tactic:
orderOf_dvd_iff_pow_eq_one

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ x ^ i = 1
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
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
N : Subgroup G
inst✝⁷ : N.Normal
inst✝⁶ : MulSemiringAction G C
hG : IsGaloisGroup G A C
inst✝⁵ : MulSemiringAction G B
inst✝⁴ : MulSemiringAction (G ⧸ N) B
inst✝³ : SMulCommClass (G ⧸ N) A B
inst✝² : SMulDistribClass G B C
inst✝¹ : IsScalarTower G (G ⧸ N) B
inst✝ : IsGaloisGroup (↥N) B C
x : B
h : ∀ (g : G ⧸ N), g • x = x
⊢ ∀ (g : G), g • (algebraMap B C) x = (algebraMap B C) x

Tactic:
intro g

Goal state after:
G : Type u_1
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
N : Subgroup G
inst✝⁷ : N.Normal
inst✝⁶ : MulSemiringAction G C
hG : IsGaloisGroup G A C
inst✝⁵ : MulSemiringAction G B
inst✝⁴ : MulSemiringAction (G ⧸ N) B
inst✝³ : SMulCommClass (G ⧸ N) A B
inst✝² : SMulDistribClass G B C
inst✝¹ : IsScalarTower G (G ⧸ N) B
inst✝ : IsGaloisGroup (↥N) B C
x : B
h : ∀ (g : G ⧸ N), g • x = x
g : G
⊢ g • (algebraMap B C) x = (algebraMap B C) x
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
this : (fun x ↦ x ^ q ^ m) x = x
⊢ X ^ q ^ m - X ≠ 0 ∧ x ^ q ^ m - x = 0

Tactic:
← sub_eq_zero

Goal state after:
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
this : (fun x ↦ x ^ q ^ m) x - x = 0
⊢ X ^ q ^ m - X ≠ 0 ∧ x ^ q ^ m - x = 0
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: 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
N : Subgroup G
inst✝³ : N.Normal
inst✝² : IsGaloisGroup (↥N) (↥F) L
E : IntermediateField K L
hE : IsGaloisGroup (↥H) (↥E) L
inst✝¹ : Finite G
inst✝ : IsGaloisGroup G K L
h✝ : E ≤ F
this✝³ : Algebra ↥E ↥F := (IntermediateField.inclusion h✝).toAlgebra
this✝² : SMul G ↥F := smulOfNormal G (↥F) L N
this✝¹ : SMulDistribClass G (↥F) L
this✝ : MulSemiringAction G ↥F := mulSemiringActionOfSmulDistribClass (↥F) L G
this : IsScalarTower (↥E) (↥F) L
x : ↥F
h : ∀ (g : ↥(Subgroup.map (QuotientGroup.mk' N) H)), g • x = x
⊢ ∀ (g : ↥H), g • (algebraMap (↥F) L) x = (algebraMap (↥F) L) x

Tactic:
by
        rintro ⟨g, hg⟩
        rw [MulAction.subgroup_smul_def, ← algebraMap.smul']
        exact congr_arg (algebraMap F L) <| h ⟨g, ⟨g, hg, rfl⟩⟩

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
⊢ (frobenius K p ^ n) x = x ^ p ^ n

Tactic:
clear hcard

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ (frobenius K p ^ n) x = x ^ p ^ n
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
g : (ZMod p)[X] := X ^ 2 - C x
a b : ZMod p
hab : eval a f + eval b g = 0
⊢ a ^ 2 + b ^ 2 = x

Tactic:
← sub_eq_zero

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
g : (ZMod p)[X] := X ^ 2 - C x
a b : ZMod p
hab : eval a f + eval b g = 0
⊢ a ^ 2 + b ^ 2 - x = 0
Module: Mathlib.LinearAlgebra.Quotient.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
Ms : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommGroup (Ms i)
inst✝⁴ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
x : (i : ι) → Ms i
⊢ ((piQuotientLift p q f hf) fun i ↦ Quotient.mk (x i)) = Quotient.mk (((lsum R Ms R) f) x)

Tactic:
rw [piQuotientLift, lsum_apply, sum_apply, ← mkQ_apply, lsum_apply, sum_apply, _root_.map_sum]

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
Ms : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommGroup (Ms i)
inst✝⁴ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
x : (i : ι) → Ms i
⊢ (∑ d, ((p d).mapQ q (f d) ⋯ ∘ₗ proj d) fun i ↦ Quotient.mk (x i)) = ∑ x_1, q.mkQ ((f x_1 ∘ₗ proj x_1) x)
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
F : Type u_4
inst✝⁷ : CommRing F
inst✝⁶ : Algebra F R
inst✝⁵ : Module F M
inst✝⁴ : IsScalarTower F R M
N : Submodule R M
ι : Type u_5
inst✝³ : Fintype ι
b : Basis ι R M
inst✝² : Nontrivial F
h : finrank R ↥N = finrank R M
inst✝¹ : ∀ (i : ι), Free F (R ⧸ Ideal.span {smithNormalFormCoeffs b h i})
inst✝ : ∀ (i : ι), Module.Finite F (R ⧸ Ideal.span {smithNormalFormCoeffs b h i})
⊢ finrank F (M ⧸ N) = ∑ i, finrank F (R ⧸ Ideal.span {smithNormalFormCoeffs b h i})

Tactic:
LinearEquiv.finrank_eq <| quotientEquivDirectSum F b h,

Goal state after:
R : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
F : Type u_4
inst✝⁷ : CommRing F
inst✝⁶ : Algebra F R
inst✝⁵ : Module F M
inst✝⁴ : IsScalarTower F R M
N : Submodule R M
ι : Type u_5
inst✝³ : Fintype ι
b : Basis ι R M
inst✝² : Nontrivial F
h : finrank R ↥N = finrank R M
inst✝¹ : ∀ (i : ι), Free F (R ⧸ Ideal.span {smithNormalFormCoeffs b h i})
inst✝ : ∀ (i : ι), Module.Finite F (R ⧸ Ideal.span {smithNormalFormCoeffs b h i})
⊢ finrank F (⨁ (i : ι), R ⧸ Ideal.span {smithNormalFormCoeffs b h i}) =
    ∑ i, finrank F (R ⧸ Ideal.span {smithNormalFormCoeffs b h i})
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case insert
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
i : α → ℕ
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 : α
f' : Finset α
hpf' : p ∉ f'
ih : (∀ p ∈ f', Prime p) → (∀ p ∈ f', ∀ q ∈ f', p ∣ q → p = q) → P (∏ p ∈ f', p ^ i p)
is_prime : ∀ p_1 ∈ insert p f', Prime p_1
is_coprime : ∀ p_1 ∈ insert p f', ∀ q ∈ insert p f', p_1 ∣ q → p_1 = q
⊢ P (∏ p ∈ insert p f', p ^ i p)

Tactic:
rw [Finset.prod_insert hpf']

Goal state after:
case insert
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
i : α → ℕ
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 : α
f' : Finset α
hpf' : p ∉ f'
ih : (∀ p ∈ f', Prime p) → (∀ p ∈ f', ∀ q ∈ f', p ∣ q → p = q) → P (∏ p ∈ f', p ^ i p)
is_prime : ∀ p_1 ∈ insert p f', Prime p_1
is_coprime : ∀ p_1 ∈ insert p f', ∀ q ∈ insert p f', p_1 ∣ q → p_1 = q
⊢ P (p ^ i p * ∏ x ∈ f', x ^ i x)
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
    have : PrimeSpectrum.mk q inferInstance ≠ ⟨p, inferInstance⟩ := ne_of_apply_ne (·.1) e
    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⟩
    rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff (Localization.AtPrime q) q, this]
    simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
this : s ≠ ∅
⊢ ∃ x, ¬↑I ⊆ ↑x.asIdeal ∧ x.asIdeal.IsMaximal

Tactic:
contrapose! this

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
this : ∀ (x : PrimeSpectrum R), ¬↑I ⊆ ↑x.asIdeal → ¬x.asIdeal.IsMaximal
⊢ s = ∅
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: case refine_1
R₀ : Type u_1
R : Type u_2
M✝ : Type u
inst✝⁹ : Ring R₀
inst✝⁸ : Ring R
inst✝⁷ : Module R₀ R
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R₀ M✝
inst✝⁴ : Module R M✝
inst✝³ : IsScalarTower R₀ R M✝
inst✝² : IsSemiprimaryRing R
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝⁴ : AddCommGroup M
x✝³ : Module R₀ M
x✝² : Module R M
x✝¹ : IsScalarTower R₀ R M
x✝ : IsSemisimpleModule R M
hJ : Module.IsTorsionBySet R M ↑(Ring.jacobson R)
h : IsNoetherian R M ∨ IsArtinian R M
⊢ Module.Finite R₀ M

Tactic:
let _ := hJ.module
    have := IsSemisimpleModule.finite_tfae (R := R) (M := M)
    simp_rw [this.out 1 0, this.out 2 0, or_self,
      hJ.semilinearMap.finite_iff_of_bijective Function.bijective_id] at h
    exact .trans (R ⧸ Ring.jacobson R) M

Goal state after:
Module: Mathlib.RingTheory.HopkinsLevitzki

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

Tactic:
tfae_have 2 → 1 := fun _ ↦ inferInstance

Goal state after:
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : IsNoetherian R M → Module.Finite R M
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M].TFAE
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : Ring.KrullDimLE 0 R
eq : Ring.jacobson R = nilradical R
Spec : Set (Ideal R) := {I | I.IsPrime}
this✝¹ : Finite ↑Spec
this✝ : ∀ (I : ↑Spec), (↑I).IsPrime
this : ∀ (I : ↑Spec), IsSemisimpleRing (R ⧸ ↑I)
⊢ IsSemisimpleRing (R ⧸ sInf {J | J.IsPrime})

Tactic:
sInf_eq_iInf'

Goal state after:
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : Ring.KrullDimLE 0 R
eq : Ring.jacobson R = nilradical R
Spec : Set (Ideal R) := {I | I.IsPrime}
this✝¹ : Finite ↑Spec
this✝ : ∀ (I : ↑Spec), (↑I).IsPrime
this : ∀ (I : ↑Spec), IsSemisimpleRing (R ⧸ ↑I)
⊢ IsSemisimpleRing (R ⧸ ⨅ a, ↑a)
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : Q.toExtension.Cotangent
⊢ ∃ a, (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) a = x

Tactic:
obtain ⟨⟨x, hx⟩, rfl⟩ := Extension.Cotangent.mk_surjective x

Goal state after:
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : Q.toExtension.Ring
hx : x ∈ Q.toExtension.ker
⊢ ∃ a, (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) a = Extension.Cotangent.mk ⟨x, hx⟩
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h1
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Cotangent
⊢ ((Extension.Cotangent.map ((Q.ofComp P).toExtensionHom.comp (Q.toComp P).toExtensionHom)) x).val = (0 x).val

Tactic:
obtain ⟨⟨x, hx⟩, rfl⟩ := Extension.Cotangent.mk_surjective x

Goal state after:
case h1
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
⊢ ((Extension.Cotangent.map ((Q.ofComp P).toExtensionHom.comp (Q.toComp P).toExtensionHom))
        (Extension.Cotangent.mk ⟨x, hx⟩)).val =
    (0 (Extension.Cotangent.mk ⟨x, hx⟩)).val
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)

Tactic:
← sub_eq_zero

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
⊢ ↑({ 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) =
    0
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
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
this : Algebra S P := ⋯
⊢ ∀ (x : P) (y : S) (z : ↥(RingHom.ker (algebraMap P S))), (x • y) • z = x • y • z

Tactic:
intro p s m

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
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
this : Algebra S P := g.toAlgebra
p : P
s : S
m : ↥(RingHom.ker (algebraMap P S))
⊢ (p • s) • m = p • s • m
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
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
g : { g // (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S }
⊢ (fun l ↦ ⟨sectionOfRetractionKerToTensor ↑l ⋯ hf' hf, ⋯⟩)
      ((fun g ↦ ⟨retractionOfSectionOfKerSqZero (↑g) hf' ⋯, ⋯⟩) g) =
    g

Tactic:
ext s

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
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
g : { g // (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S }
s : S
⊢ ↑((fun l ↦ ⟨sectionOfRetractionKerToTensor ↑l ⋯ hf' hf, ⋯⟩)
          ((fun g ↦ ⟨retractionOfSectionOfKerSqZero (↑g) hf' ⋯, ⋯⟩) g))
      s =
    ↑g s