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

Goal state before:
pp: case pos.succ.zero
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
H : ¬Algebra.IsSeparable K L
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
n : ℕ
inst✝ : CharZero K
this : 1 ≠ 0
hn : finrank (↥(separableClosure K L)) L = 1 ^ (n + 1)
⊢ (trace K ↥(separableClosure K L)) (finrank (↥(separableClosure K L)) L • x) =
    0 ((algebraMap (↥(separableClosure K L)) L) x)

Tactic:
rw [one_pow, IntermediateField.finrank_eq_one_iff_eq_top, separableClosure.eq_top_iff] at hn

Goal state after:
case pos.succ.zero
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
H : ¬Algebra.IsSeparable K L
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
n : ℕ
inst✝ : CharZero K
this : 1 ≠ 0
hn : Algebra.IsSeparable K L
⊢ (trace K ↥(separableClosure K L)) (finrank (↥(separableClosure K L)) L • x) =
    0 ((algebraMap (↥(separableClosure K L)) L) x)
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case refine_2
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
h : G
⊢ (algebraMap B (B ⧸ Q)) (h • (a - eval b r)) = (algebraMap B (B ⧸ Q)) (if h • Q = Q then a else 0)

Tactic:
← sub_eq_zero,

Goal state after:
case refine_2
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
h : G
⊢ (algebraMap B (B ⧸ Q)) (h • (a - eval b r)) - (algebraMap B (B ⧸ Q)) (if h • Q = Q then a else 0) = 0
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case neg.succ.hnc
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this✝ : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
h : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - 1
this : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - (g.natDegree * p ^ (n + 1) - 1)
⊢ False

Tactic:
rw [tsub_tsub_cancel_of_le, Nat.dvd_one] at this

Goal state after:
case neg.succ.hnc
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this✝ : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
h : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - 1
this : p ^ (n + 1) = 1
⊢ False

case neg.succ.hnc
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this✝ : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
h : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - 1
this : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - (g.natDegree * p ^ (n + 1) - 1)
⊢ 1 ≤ g.natDegree * p ^ (n + 1)
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : f.degree = 2
hg2 : g.degree = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
hd : Disjoint (image (fun x ↦ eval x f) univ) (image (fun x ↦ eval x (-g)) univ)
⊢ 0 < f.degree

Tactic:
hf2

Goal state after:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : f.degree = 2
hg2 : g.degree = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
hd : Disjoint (image (fun x ↦ eval x f) univ) (image (fun x ↦ eval x (-g)) univ)
⊢ 0 < 2
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 * (embeddingsMatrix K E b)ᵀ =
    (reindex (Equiv.refl κ) e.symm) (embeddingsMatrix K E b) *
      ((reindex (Equiv.refl κ) e.symm) (embeddingsMatrix K E b))ᵀ

Tactic:
reindex_apply,

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 * (embeddingsMatrix K E b)ᵀ =
    (embeddingsMatrix K E b).submatrix ⇑(Equiv.refl κ).symm ⇑e.symm.symm *
      ((embeddingsMatrix K E b).submatrix ⇑(Equiv.refl κ).symm ⇑e.symm.symm)ᵀ
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
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'
inst✝³ : MulSemiringAction G C
inst✝² : IsGaloisGroup G A C
inst✝¹ : MulSemiringAction G' B
inst✝ : IsGaloisGroup G' A B
g : G
x : B
this✝³ : IsDomain B
this✝² : IsDomain A
this✝¹ : FaithfulSMul A C
this✝ : MulSemiringAction G (FractionRing C) := IsFractionRing.mulSemiringAction G C (FractionRing C)
this : MulSemiringAction G' (FractionRing B) := IsFractionRing.mulSemiringAction G' B (FractionRing B)
⊢ (algebraMap (FractionRing B) (FractionRing C))
      ((algebraMap B (FractionRing B))
        ((quotientMulEquiv G G' (FractionRing A) (FractionRing B) (FractionRing C)
              (fixingSubgroup G (Set.range ⇑(algebraMap (FractionRing B) (FractionRing C)))))
            ↑g •
          x)) =
    (algebraMap C (FractionRing C)) (g • (algebraMap B C) x)

Tactic:
algebraMap.smul',

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
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'
inst✝³ : MulSemiringAction G C
inst✝² : IsGaloisGroup G A C
inst✝¹ : MulSemiringAction G' B
inst✝ : IsGaloisGroup G' A B
g : G
x : B
this✝³ : IsDomain B
this✝² : IsDomain A
this✝¹ : FaithfulSMul A C
this✝ : MulSemiringAction G (FractionRing C) := IsFractionRing.mulSemiringAction G C (FractionRing C)
this : MulSemiringAction G' (FractionRing B) := IsFractionRing.mulSemiringAction G' B (FractionRing B)
⊢ (algebraMap (FractionRing B) (FractionRing C))
      ((quotientMulEquiv G G' (FractionRing A) (FractionRing B) (FractionRing C)
            (fixingSubgroup G (Set.range ⇑(algebraMap (FractionRing B) (FractionRing C)))))
          ↑g •
        (algebraMap B (FractionRing B)) x) =
    (algebraMap C (FractionRing C)) (g • (algebraMap B C) x)
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
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'
inst✝³ : MulSemiringAction G C
inst✝² : IsGaloisGroup G A C
inst✝¹ : MulSemiringAction G' B
inst✝ : IsGaloisGroup G' A B
g : G
x : B
this✝³ : IsDomain B
this✝² : IsDomain A
this✝¹ : FaithfulSMul A C
this✝ : MulSemiringAction G (FractionRing C) := IsFractionRing.mulSemiringAction G C (FractionRing C)
this : MulSemiringAction G' (FractionRing B) := IsFractionRing.mulSemiringAction G' B (FractionRing B)
⊢ g • (algebraMap B (FractionRing C)) x = (algebraMap C (FractionRing C)) (g • (algebraMap B C) x)

Tactic:
algebraMap.smul',

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
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'
inst✝³ : MulSemiringAction G C
inst✝² : IsGaloisGroup G A C
inst✝¹ : MulSemiringAction G' B
inst✝ : IsGaloisGroup G' A B
g : G
x : B
this✝³ : IsDomain B
this✝² : IsDomain A
this✝¹ : FaithfulSMul A C
this✝ : MulSemiringAction G (FractionRing C) := IsFractionRing.mulSemiringAction G C (FractionRing C)
this : MulSemiringAction G' (FractionRing B) := IsFractionRing.mulSemiringAction G' B (FractionRing B)
⊢ g • (algebraMap B (FractionRing C)) x = g • (algebraMap C (FractionRing C)) ((algebraMap B C) x)
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ a ^ (p - 1) = 1

Tactic:
have h := FiniteField.pow_card_sub_one_eq_one a ha
  rwa [ZMod.card p] at h

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

Goal state before:
pp: F : Type u_3
inst✝² : Field F
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP F p
⊢ (X ^ p - X).Splits

Tactic:
let _ := Subfield.fintypeBot F p
  rw [splits_iff_card_roots, roots_X_pow_char_sub_X_bot, ← Finset.card_def, Finset.card_univ,
    FiniteField.X_pow_card_sub_X_natDegree_eq _ (Fact.out (p := p.Prime)).one_lt,
    Fintype.card_eq_nat_card, card_bot F p]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Goal state before:
pp: case refine_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Free ℤ M
inst✝ : Module.Finite ℤ M
N : Submodule ℤ M
h : Finite (M ⧸ N)
⊢ Function.Injective ⇑(LinearMap.codRestrict N ((LinearMap.lsmul ℤ M) ↑(Nat.card (M ⧸ N))) ⋯)

Tactic:
refine (LinearMap.lsmul_injective ?_).codRestrict _

Goal state after:
case refine_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Free ℤ M
inst✝ : Module.Finite ℤ M
N : Submodule ℤ M
h : Finite (M ⧸ N)
⊢ ↑(Nat.card (M ⧸ N)) ≠ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case neg
α : 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).prod

Tactic:
← (normalizedFactors a).map_id,

Goal state after:
case neg
α : 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 (Multiset.map id (normalizedFactors a)).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case e_a.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
⊢ f ((normalizedFactors a).prod * (normalizedFactors b).prod) =
    f (normalizedFactors a).prod * f (normalizedFactors b).prod

Tactic:
← (normalizedFactors a).map_id,

Goal state after:
case e_a.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
⊢ f ((Multiset.map id (normalizedFactors a)).prod * (normalizedFactors b).prod) =
    f (Multiset.map id (normalizedFactors a)).prod * f (normalizedFactors b).prod
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:
let := (RingHom.comp (e₂ : B₁ →+* B₂) (algebraMap A₁ B₁)).toAlgebra' ?_

Goal state after:
case refine_2
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₁
this : Algebra A₁ B₂ := ((↑e₂).comp (algebraMap A₁ B₁)).toAlgebra' ?refine_1
⊢ (norm A₁) x = e₁.symm ((norm A₂) (e₂ x))

case refine_1
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₁
⊢ ∀ (c : A₁) (x : B₂), ((↑e₂).comp (algebraMap A₁ B₁)) c * x = x * ((↑e₂).comp (algebraMap A₁ B₁)) c
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case inr.refine_1
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I ↦ map (Quotient.mk (span {↑n})) I
⊢ Finite (S ⧸ span {↑n})

Tactic:
rw [← absNorm_ne_zero_iff, absNorm_span_singleton]

Goal state after:
case inr.refine_1
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I ↦ map (Quotient.mk (span {↑n})) I
⊢ ((Algebra.norm ℤ) ↑n).natAbs ≠ 0
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: 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

Tactic:
exact Pi.disjoint_iff.mpr fun I ↦ Prop.disjoint_iff.mpr (by tauto)

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

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
p q : Submodule A M
h : p ⋖ q
⊢ length B (B ⊗[A] ↥q) = length B (B ⊗[A] ↥p) + length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))

Tactic:
let f : p →ₗ[A] q := inclusion h.le

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✝ : Flat A B
p q : Submodule A M
h : p ⋖ q
f : ↥p →ₗ[A] ↥q := inclusion ⋯
⊢ length B (B ⊗[A] ↥q) = length B (B ⊗[A] ↥p) + length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
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✝ : Flat A B
⊢ length B (B ⊗[A] M) = length A M * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))

Tactic:
by_cases h : IsFiniteLength A M

Goal state after:
case pos
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✝ : Flat A B
h : IsFiniteLength A M
⊢ length B (B ⊗[A] M) = length A M * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))

case neg
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✝ : Flat A B
h : ¬IsFiniteLength A M
⊢ length B (B ⊗[A] M) = length A M * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
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
inst✝¹ : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst✝ : P.IsPrime
hp : P ≠ ⊥
hpP : map f p ≤ P
Sₚ : Type v := Localization.AtPrime P
H₁ : ¬map f p ≤ P * P
a : Ideal S
ha : map f p = P * a
ha' : ¬a ≤ P
⊢ map (algebraMap S (Localization.AtPrime P)) P * map (algebraMap S (Localization.AtPrime P)) a =
    maximalIdeal (Localization.AtPrime P)

Tactic:
Localization.AtPrime.map_eq_maximalIdeal

Goal state after:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst✝ : P.IsPrime
hp : P ≠ ⊥
hpP : map f p ≤ P
Sₚ : Type v := Localization.AtPrime P
H₁ : ¬map f p ≤ P * P
a : Ideal S
ha : map f p = P * a
ha' : ¬a ≤ P
⊢ maximalIdeal (Localization P.primeCompl) * map (algebraMap S (Localization.AtPrime P)) a =
    maximalIdeal (Localization.AtPrime 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 ≠ ⊥
⊢ p.ramificationIdx' Q = p.ramificationIdx' P * P.ramificationIdx' Q

Tactic:
have hp0 : P ≠ ⊥ := ne_bot_of_map_ne_bot hg0

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 ≠ ⊥
⊢ p.ramificationIdx' Q = p.ramificationIdx' P * P.ramificationIdx' Q
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case mpr.refine_2
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [Small.{w, u} B] [inst_2 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial Ω[A⁄R]
f₁ f₂ : { f // (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R A }
e : f₁ ≠ f₂
f : Ideal (A ⊗[R] A ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) := ⋯
x : A
⊢ (TensorProduct.lmul' R).kerSquareLift.kerLift
      (((Ideal.Quotient.mkₐ R (RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom)).comp ↑f₁) x) =
    (TensorProduct.lmul' R).kerSquareLift.kerLift
      (((Ideal.Quotient.mkₐ R (RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom)).comp ↑f₂) x)

Tactic:
simpa using DFunLike.congr_fun (f₁.2.trans f₂.2.symm) x

Goal state after:
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
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
this : ∀ (i : ℕ), (Ideal.Quotient.mkₐ R (I ^ i)).comp g₁ = (Ideal.Quotient.mkₐ R (I ^ i)).comp g₂
x : A
⊢ g₁ x = g₂ x

Tactic:
← sub_eq_zero,

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
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
this : ∀ (i : ℕ), (Ideal.Quotient.mkₐ R (I ^ i)).comp g₁ = (Ideal.Quotient.mkₐ R (I ^ i)).comp g₂
x : A
⊢ g₁ x - g₂ x = 0
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
s : S
⊢ 1 ⊗ₜ[R] s * elem R S = s ⊗ₜ[R] 1 * elem R S

Tactic:
← sub_eq_zero,

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
s : S
⊢ 1 ⊗ₜ[R] s * elem R S - s ⊗ₜ[R] 1 * elem R S = 0