mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹² : Group G
inst✝¹¹ : Group G'
A : Type u_5
B : Type u_6
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : IsDomain B
inst✝⁷ : Algebra A B
inst✝⁶ : FaithfulSMul A B
inst✝⁵ : MulSemiringAction G B
inst✝⁴ : MulSemiringAction G' B
inst✝³ : IsGaloisGroup G A B
inst✝² : IsGaloisGroup G' A B
inst✝¹ : Finite G
inst✝ : Finite G'
S : Set B
⊢ Subgroup.map (↑(mulEquivCongr G G' A B)) (fixingSubgroup G S) = fixingSubgroup G' S

Tactic:
ext g

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹² : Group G
inst✝¹¹ : Group G'
A : Type u_5
B : Type u_6
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : IsDomain B
inst✝⁷ : Algebra A B
inst✝⁶ : FaithfulSMul A B
inst✝⁵ : MulSemiringAction G B
inst✝⁴ : MulSemiringAction G' B
inst✝³ : IsGaloisGroup G A B
inst✝² : IsGaloisGroup G' A B
inst✝¹ : Finite G
inst✝ : Finite G'
S : Set B
g : G'
⊢ g ∈ Subgroup.map (↑(mulEquivCongr G G' A B)) (fixingSubgroup G S) ↔ g ∈ fixingSubgroup G' S
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
inst✝⁵ : Finite G
inst✝⁴ : IsGaloisGroup G K L
E : Type u_5
inst✝³ : Field E
inst✝² : Algebra K E
inst✝¹ : Algebra E L
inst✝ : IsScalarTower K E L
⊢ IsGaloisGroup (↥(fixingSubgroup G (Set.range ⇑(algebraMap E L)))) E L

Tactic:
rw [← IsScalarTower.toAlgHom_fieldRange K E L]
  refine IsGaloisGroup.of_ringEquiv _ _ _ L
    (AlgHom.equivFieldRange (IsScalarTower.toAlgHom K E L)).toRingEquiv.symm fun ⟨_, ⟨x, rfl⟩⟩ ↦ ?_
  simp [AlgEquiv.symm_apply_eq, Subtype.ext_iff]

Goal state after:
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
hGKL : IsGaloisGroup G K L
⊢ FixedPoints.intermediateField ↥⊤ = ⊥

Tactic:
by
  convert! IsGaloisGroup.fixedPoints_eq_bot G K L
  ext; simp

Goal state after:
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : Finite G
A : Type u_5
B : Type u_6
C : Type u_7
H : Subgroup G
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : CommRing C
inst✝⁵ : IsDomain C
inst✝⁴ : Algebra A C
inst✝³ : FaithfulSMul A C
inst✝² : MulSemiringAction G C
hGAC : IsGaloisGroup G A C
inst✝¹ : Algebra B C
inst✝ : FaithfulSMul B C
hH : IsGaloisGroup (↥H) B C
this✝² : IsDomain B
this✝¹ : IsDomain A
K : Type u_5 := FractionRing A
L : Type u_7 := FractionRing C
this✝ : MulSemiringAction G L := IsFractionRing.mulSemiringAction G C L
this : IsGaloisGroup (↥H) (FractionRing B) L
⊢ fixingSubgroup G (Set.range ⇑(algebraMap B C)) = fixingSubgroup G (Set.range ⇑(algebraMap (FractionRing B) L))

Tactic:
ext g

Goal state after:
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : Finite G
A : Type u_5
B : Type u_6
C : Type u_7
H : Subgroup G
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : CommRing C
inst✝⁵ : IsDomain C
inst✝⁴ : Algebra A C
inst✝³ : FaithfulSMul A C
inst✝² : MulSemiringAction G C
hGAC : IsGaloisGroup G A C
inst✝¹ : Algebra B C
inst✝ : FaithfulSMul B C
hH : IsGaloisGroup (↥H) B C
this✝² : IsDomain B
this✝¹ : IsDomain A
K : Type u_5 := FractionRing A
L : Type u_7 := FractionRing C
this✝ : MulSemiringAction G L := IsFractionRing.mulSemiringAction G C L
this : IsGaloisGroup (↥H) (FractionRing B) L
g : G
⊢ g ∈ fixingSubgroup G (Set.range ⇑(algebraMap B C)) ↔ g ∈ fixingSubgroup G (Set.range ⇑(algebraMap (FractionRing B) L))
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case intro
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₀ :
  ∀ (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
key :
  map (algebraMap (A ⧸ P) L) (map (algebraMap A (A ⧸ P)) M) =
    map (algebraMap (B ⧸ Q) L)
      ((X - C ((algebraMap B (B ⧸ Q)) (a * b₀))) ^ {x | x • Q = Q}.card * X ^ {x | ¬x • Q = Q}.card)
⊢ f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) = (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)

Tactic:
algebraMap_eq (A ⧸ P) K L,

Goal state after:
case intro
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₀ :
  ∀ (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
key :
  map ((algebraMap K L).comp (algebraMap (A ⧸ P) K)) (map (algebraMap A (A ⧸ P)) M) =
    map (algebraMap (B ⧸ Q) L)
      ((X - C ((algebraMap B (B ⧸ Q)) (a * b₀))) ^ {x | x • Q = Q}.card * X ^ {x | ¬x • Q = Q}.card)
⊢ f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) = (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)
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
| x ^ q

Tactic:
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 : ℕ
hcard : q = p ^ n
x : K
| x ^ p ^ n
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
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
h : x * (algebraMap (A ⧸ P) (B ⧸ Q)) a = b * y
ha : (algebraMap (A ⧸ P) L) a ≠ 0
hy : (algebraMap (B ⧸ Q) L) y ≠ 0
⊢ (algebraMap (B ⧸ Q) L) x * (algebraMap (A ⧸ P) L) a =
    (algebraMap (B ⧸ Q) L) x * (algebraMap (B ⧸ Q) L) ((algebraMap (A ⧸ P) (B ⧸ Q)) a)

Tactic:
← algebraMap_apply

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
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
h : x * (algebraMap (A ⧸ P) (B ⧸ Q)) a = b * y
ha : (algebraMap (A ⧸ P) L) a ≠ 0
hy : (algebraMap (B ⧸ Q) L) y ≠ 0
⊢ (algebraMap (B ⧸ Q) L) x * (algebraMap (A ⧸ P) L) a = (algebraMap (B ⧸ Q) L) x * (algebraMap (A ⧸ P) L) a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

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

Tactic:
by
  let := Classical.decEq α
  induction s using Finset.induction_on with
  | empty => simpa using h1 isUnit_one
  | insert p f' hpf' ih =>
    rw [Finset.prod_insert hpf']
    exact
      hcp (prime_pow_coprime_prod_of_coprime_insert i p hpf' is_prime is_coprime)
        (hpr (i p) (is_prime _ (Finset.mem_insert_self _ _)))
        (ih (fun q hq => is_prime _ (Finset.mem_insert_of_mem hq)) fun q hq q' hq' =>
          is_coprime _ (Finset.mem_insert_of_mem hq) _ (Finset.mem_insert_of_mem hq'))

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

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
⊢ { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }

Tactic:
refine (Equiv.subtypeEquivRight ?_).trans (subtypeOrEquiv _ _ ?_)

Goal state after:
case refine_1
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
⊢ ∀ (x : Ideal S), absNorm x ≤ n ↔ x ∈ (Ideal S)⁰ ∧ absNorm x ≤ n ∨ x ∉ (Ideal S)⁰ ∧ absNorm x ≤ n

case refine_2
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
⊢ Disjoint (fun I ↦ I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) fun I ↦ I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case e'_3
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ ↑(U i)
y : ↥(U i)
hy : y ∈ Subtype.val ⁻¹' Z
hy' : y ∈ closedPoints ↥(U i)
j : ι
h : ↑y ∉ U j
⊢ ∀ (x : ↥(U j)), x ∉ Subtype.val ⁻¹' {↑y}

Tactic:
intro z

Goal state after:
case e'_3
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ ↑(U i)
y : ↥(U i)
hy : y ∈ Subtype.val ⁻¹' Z
hy' : y ∈ closedPoints ↥(U i)
j : ι
h : ↑y ∉ U j
z : ↥(U j)
⊢ z ∉ Subtype.val ⁻¹' {↑y}
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 | map (algebraMap R T) (comap f P) ≤ Q ^ n}

Tactic:
IsScalarTower.algebraMap_eq R S T,

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
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 | map ((algebraMap S T).comp f) (comap f P) ≤ Q ^ n}
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

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
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map (algebraMap S T) P ≠ ⊥
hfg : map (algebraMap R T) p ≠ ⊥
hg : map (algebraMap S T) P ≤ Q
⊢ map f p ≠ ⊥

Tactic:
IsScalarTower.algebraMap_eq R S T,

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
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map (algebraMap S T) P ≠ ⊥
hfg : map ((algebraMap S T).comp f) p ≠ ⊥
hg : map (algebraMap S T) P ≤ Q
⊢ map f p ≠ ⊥
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

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
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map (algebraMap S T) P ≠ ⊥
hfg : map (algebraMap R T) p ≠ ⊥
hg : map (algebraMap S T) P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
⊢ Multiset.count Q (normalizedFactors (map (algebraMap R T) p)) =
    Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map (algebraMap S T) P))

Tactic:
IsScalarTower.algebraMap_eq R S T,

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
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map (algebraMap S T) P ≠ ⊥
hfg : map (algebraMap R T) p ≠ ⊥
hg : map (algebraMap S T) P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
⊢ Multiset.count Q (normalizedFactors (map ((algebraMap S T).comp f) p)) =
    Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map (algebraMap S T) P))
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case mpr
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
⊢ (∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
      I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp) →
    FormallyUnramified R A

Tactic:
· intro H
    replace H : ∀ ⦃B : Type u⦄ [CommRing B] [Small.{w} B],
        ∀ [Algebra R B] (I : Ideal B) (_ : I ^ 2 = ⊥),
          Function.Injective ((Ideal.Quotient.mkₐ R I).comp : (A →ₐ[R] B) → A →ₐ[R] B ⧸ I) := by
      intro B _ _ _ I hI f g e
      simpa [DFunLike.ext_iff] using H (B := Shrink B) (I.comap (Shrink.ringEquiv _))
        (by rw [← Ideal.map_symm, ← Ideal.map_pow, hI]; simp)
        (a₁ := (Shrink.algEquiv _ _).symm.toAlgHom.comp f)
        (a₂ := (Shrink.algEquiv _ _).symm.toAlgHom.comp g)
        (by simpa [DFunLike.ext_iff, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Shrink.ringEquiv] using e)
    constructor
    by_contra! h
    obtain ⟨f₁, f₂, e⟩ := (KaehlerDifferential.endEquiv R A).injective.nontrivial
    apply e
    ext1
    let f := RingHom.ker (TensorProduct.lmul' R (S := A)).kerSquareLift.toRingHom
    refine H
      (RingHom.ker (TensorProduct.lmul' R (S := A)).kerSquareLift.toRingHom) ?_ ?_
    · rw [AlgHom.ker_kerSquareLift]
      exact Ideal.cotangentIdeal_square _
    · ext x
      apply RingHom.kerLift_injective (TensorProduct.lmul' R (S := A)).kerSquareLift.toRingHom
      simpa using DFunLike.congr_fun (f₁.2.trans f₂.2.symm) 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
inst✝ : QuasiFinite R S
e : R ≃ₐ[R] PrimeSpectrum.PiLocalization R :=
  AlgEquiv.ofBijective (IsScalarTower.toAlgHom R R (PrimeSpectrum.PiLocalization R)) ⋯
⊢ Module.Finite R S

Tactic:
have : Fintype (PrimeSpectrum R) := .ofFinite _

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsArtinianRing R
inst✝ : QuasiFinite R S
e : R ≃ₐ[R] PrimeSpectrum.PiLocalization R :=
  AlgEquiv.ofBijective (IsScalarTower.toAlgHom R R (PrimeSpectrum.PiLocalization R)) ⋯
this : Fintype (PrimeSpectrum R)
⊢ Module.Finite R S
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
this✝¹ : IsLocalizedModule p.primeCompl LinearMap.id
this✝ : Module.Finite R (Localization.AtPrime p)
this : Module.Finite S (Localization.AtPrime p)
⊢ ∃ f ∉ p, ↑(PrimeSpectrum.basicOpen f) = {{ asIdeal := p, isPrime := inst✝³ }}

Tactic:
have : IsArtinianRing (Localization.AtPrime p) := .of_finite R _

Goal state after:
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
this✝² : IsLocalizedModule p.primeCompl LinearMap.id
this✝¹ : Module.Finite R (Localization.AtPrime p)
this✝ : Module.Finite S (Localization.AtPrime p)
this : IsArtinianRing (Localization.AtPrime p)
⊢ ∃ f ∉ p, ↑(PrimeSpectrum.basicOpen f) = {{ asIdeal := p, isPrime := inst✝³ }}
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✝
σ : Type u_4
P : Generators R (MvPolynomial σ R) σ := Generators.mvPolynomial R σ
this✝ : Subsingleton ↥P.toExtension.ker
this : Subsingleton P.toExtension.Cotangent
⊢ FormallySmooth R (MvPolynomial σ R)

Tactic:
have := P.toExtension.h1Cotangentι_injective.subsingleton

Goal state after:
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✝
σ : Type u_4
P : Generators R (MvPolynomial σ R) σ := Generators.mvPolynomial R σ
this✝¹ : Subsingleton ↥P.toExtension.ker
this✝ : Subsingleton P.toExtension.Cotangent
this : Subsingleton P.toExtension.H1Cotangent
⊢ FormallySmooth R (MvPolynomial σ R)
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h2
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.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
hx : (Q.ofComp P).toAlgHom x ∈ Q.ker * Q.ker
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈
    (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)).range

Tactic:
← map_ofComp_ker (P := P),

Goal state after:
case h2
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.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
hx :
  (Q.ofComp P).toAlgHom x ∈
    Ideal.map (Q.ofComp P).toAlgHom (Q.comp P).ker * Ideal.map (Q.ofComp P).toAlgHom (Q.comp P).ker
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈
    (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)).range
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case monomial.add
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₁
Q : Generators S T ι
n : ι →₀ ℕ
r : S
y₁ y₂ : MvPolynomial ι S
hy₁ : (δAux R Q) ((monomial n) r * y₁) = (monomial n) r • (δAux R Q) y₁ + y₁ • (δAux R Q) ((monomial n) r)
hy₂ : (δAux R Q) ((monomial n) r * y₂) = (monomial n) r • (δAux R Q) y₂ + y₂ • (δAux R Q) ((monomial n) r)
⊢ (δAux R Q) ((monomial n) r * (y₁ + y₂)) =
    (monomial n) r • (δAux R Q) (y₁ + y₂) + (y₁ + y₂) • (δAux R Q) ((monomial n) r)

Tactic:
simp only [map_add, smul_add, hy₁, hy₂, mul_add, add_smul]

Goal state after:
case monomial.add
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₁
Q : Generators S T ι
n : ι →₀ ℕ
r : S
y₁ y₂ : MvPolynomial ι S
hy₁ : (δAux R Q) ((monomial n) r * y₁) = (monomial n) r • (δAux R Q) y₁ + y₁ • (δAux R Q) ((monomial n) r)
hy₂ : (δAux R Q) ((monomial n) r * y₂) = (monomial n) r • (δAux R Q) y₂ + y₂ • (δAux R Q) ((monomial n) r)
⊢ (monomial n) r • (δAux R Q) y₁ + y₁ • (δAux R Q) ((monomial n) r) +
      ((monomial n) r • (δAux R Q) y₂ + y₂ • (δAux R Q) ((monomial n) r)) =
    (monomial n) r • (δAux R Q) y₁ + (monomial n) r • (δAux R Q) y₂ +
      (y₁ • (δAux R Q) ((monomial n) r) + y₂ • (δAux R Q) ((monomial n) r))
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case tmul
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
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
this✝¹ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
y : Q.Ring ⊗[P.Ring] ↥P.ker
a : Q.Ring
b : ↥P.ker
⊢ ↑(e (a ⊗ₜ[P.Ring] b)) •
      (LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk)) y =
    0

Tactic:
induction y with

Goal state after: