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

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K L : IntermediateField F E
inst✝¹ : IsGalois F ↥K
inst✝ : FiniteDimensional F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ : Polynomial.IsSplittingField F (↥K) T
⊢ IsGalois (↥L) E

Tactic:
let T' := T.map (algebraMap F L)

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K L : IntermediateField F E
inst✝¹ : IsGalois F ↥K
inst✝ : FiniteDimensional F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ : Polynomial.IsSplittingField F (↥K) T
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
⊢ IsGalois (↥L) E
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : ↑H ∈ galGroupBasis K L
W : Set Gal(L/K)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : ∀ x ∈ E, φ x = x
⊢ False

Tactic:
specialize h_in_H x

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : ↑H ∈ galGroupBasis K L
W : Set Gal(L/K)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : x ∈ E → φ x = x
⊢ False
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
x : S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
y : S
hy : (aeval y) (minpoly R x) = 0
⊢ eval₂ (RingHom.id S) y (minpolyDiv R x) = if x = y then (aeval x) (derivative (minpoly R x)) else 0

Tactic:
eval₂_minpolyDiv_of_eval₂_eq_zero,

Goal state after:
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
x : S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
y : S
hy : (aeval y) (minpoly R x) = 0
⊢ (if (RingHom.id S) x = y then (RingHom.id S) ((aeval x) (derivative (minpoly R x))) else 0) =
    if x = y then (aeval x) (derivative (minpoly R x)) else 0

case hy
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
x : S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
y : S
hy : (aeval y) (minpoly R x) = 0
⊢ eval₂ ((RingHom.id S).comp (algebraMap R S)) y (minpoly R x) = 0
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
x : S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
y : S
hy : (aeval y) (minpoly R x) = 0
⊢ (if (RingHom.id S) x = y then (RingHom.id S) ((aeval x) (derivative (minpoly R x))) else 0) =
    if x = y then (aeval x) (derivative (minpoly R x)) else 0

pp: case hy
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
x : S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
y : S
hy : (aeval y) (minpoly R x) = 0
⊢ eval₂ ((RingHom.id S).comp (algebraMap R S)) y (minpoly R x) = 0

Tactic:
RingHom.id_apply,

Goal state after:
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
x : S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
y : S
hy : (aeval y) (minpoly R x) = 0
⊢ (if x = y then (RingHom.id S) ((aeval x) (derivative (minpoly R x))) else 0) =
    if x = y then (aeval x) (derivative (minpoly R x)) else 0

case hy
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
x : S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
y : S
hy : (aeval y) (minpoly R x) = 0
⊢ eval₂ ((RingHom.id S).comp (algebraMap R S)) y (minpoly R x) = 0
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
K : Type u_3
inst✝² : Ring K
inst✝¹ : Algebra F K
e : K ≃ₐ[F] E
inst✝ : IsPurelyInseparable F K
⊢ IsPurelyInseparable F E

Tactic:
by
  refine ⟨⟨fun _ ↦ by rw [← isIntegral_algEquiv e.symm]; exact IsPurelyInseparable.isIntegral' F _⟩,
    fun x h ↦ ?_⟩
  rw [IsSeparable, ← minpoly.algEquiv_eq e.symm] at h
  simpa only [RingHom.mem_range, algebraMap_eq_apply] using IsPurelyInseparable.inseparable F _ h

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

Goal state before:
pp: F : Type u
inst✝² : Field F
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
⊢ Algebra.IsSeparable F K ↔ finInsepDegree F K = 1

Tactic:
rw [← separableClosure.eq_top_iff, ← IntermediateField.finrank_eq_one_iff_eq_top, finInsepDegree]

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

Goal state before:
pp: case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
halg : ¬Algebra.IsAlgebraic F E
⊢ finSepDegree F E * finrank (↥(separableClosure F E)) E = 0

Tactic:
finrank_of_infinite_dimensional (K := separableClosure F E) (V := E) fun _ ↦
      halg (.trans _ (separableClosure F E) _),

Goal state after:
case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
halg : ¬Algebra.IsAlgebraic F E
⊢ finSepDegree F E * 0 = 0
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
L : Type u_5
inst✝⁶ : Field L
F : Type u_6
inst✝⁵ : Field F
inst✝⁴ : Algebra R L
inst✝³ : Algebra L F
inst✝² : Algebra R F
inst✝¹ : IsScalarTower R L F
inst✝ : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
⊢ IsIntegral R ((algebraMap L (AlgebraicClosure F)) ((trace L F) x))

Tactic:
trace_eq_sum_roots

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_5
inst✝⁶ : Field L
F : Type u_6
inst✝⁵ : Field F
inst✝⁴ : Algebra R L
inst✝³ : Algebra L F
inst✝² : Algebra R F
inst✝¹ : IsScalarTower R L F
inst✝ : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
⊢ IsIntegral R (finrank (↥L⟮x⟯) F • ((minpoly L x).aroots (AlgebraicClosure F)).sum)

R : Type u_1
inst✝⁷ : CommRing R
L : Type u_5
inst✝⁶ : Field L
F : Type u_6
inst✝⁵ : Field F
inst✝⁴ : Algebra R L
inst✝³ : Algebra L F
inst✝² : Algebra R F
inst✝¹ : IsScalarTower R L F
inst✝ : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
⊢ (Polynomial.map (algebraMap L (AlgebraicClosure F)) (minpoly L x)).Splits
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
L : Type u_5
inst✝⁶ : Field L
F : Type u_6
inst✝⁵ : Field F
inst✝⁴ : Algebra R L
inst✝³ : Algebra L F
inst✝² : Algebra R F
inst✝¹ : IsScalarTower R L F
inst✝ : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
⊢ IsIntegral R (finrank (↥L⟮x⟯) F • ((minpoly L x).aroots (AlgebraicClosure F)).sum)

Tactic:
refine (IsIntegral.multiset_sum ?_).nsmul _

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_5
inst✝⁶ : Field L
F : Type u_6
inst✝⁵ : Field F
inst✝⁴ : Algebra R L
inst✝³ : Algebra L F
inst✝² : Algebra R F
inst✝¹ : IsScalarTower R L F
inst✝ : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
⊢ ∀ x_1 ∈ (minpoly L x).aroots (AlgebraicClosure F), IsIntegral R x_1
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case neg.refine_1
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ -↑n < (↑x.val - ↑n) * 2

Tactic:
linarith only [h]

Goal state after:
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case succ
a n✝ : ℕ
ha : (n✝ + 1) / 2 < a
ha' : a < n✝ + 1
⊢ (↑a).valMinAbs = ↑a - ↑(n✝ + 1)

Tactic:
simp [valMinAbs_def_pos, val_natCast, Nat.mod_eq_of_lt ha', ha.not_ge]

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

Goal state before:
pp: case pos
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
⊢ (trace K L) x = 0 x

Tactic:
by_cases hx : IsSeparable K x

Goal state after:
case pos
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
⊢ (trace K L) x = 0 x

case neg
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
⊢ (trace K L) x = 0 x
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: case inl
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✝ : IsGaloisGroup G K L
val✝ : Fintype G
⊢ Nat.card G = finrank K L

Tactic:
have : FaithfulSMul G L := faithful K

Goal state after:
case inl
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✝ : IsGaloisGroup G K L
val✝ : Fintype G
this : FaithfulSMul G L
⊢ Nat.card G = finrank K L
Module: Mathlib.RingTheory.Trace.Basic

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

Tactic:
rw [RingHom.map_det, RingHom.mapMatrix_apply,
      traceMatrix_eq_embeddingsMatrixReindex_mul_trans K _ _ e,
      embeddingsMatrixReindex_eq_vandermonde, det_mul, det_transpose]
    refine mt mul_self_eq_zero.mp ?_
    simp only [det_vandermonde, Finset.prod_eq_zero_iff, not_exists, sub_eq_zero]
    rintro i ⟨_, j, hij, h⟩
    exact (Finset.mem_Ioi.mp hij).ne' (e.injective <| pb.algHom_ext h)

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

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  ∑ x, x pb.gen ^ ↑j / x ((aeval pb.gen) (derivative (minpoly K pb.gen))) * x ((minpolyDiv K pb.gen).coeff ↑i) =
    if j = i then 1 else 0
⊢ (algebraMap K (AlgebraicClosure K))
      (((traceForm K L) ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen))))
        (pb.basis j)) =
    (algebraMap K (AlgebraicClosure K)) (if j = i then 1 else 0)

Tactic:
rw [PowerBasis.coe_basis]

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  ∑ x, x pb.gen ^ ↑j / x ((aeval pb.gen) (derivative (minpoly K pb.gen))) * x ((minpolyDiv K pb.gen).coeff ↑i) =
    if j = i then 1 else 0
⊢ (algebraMap K (AlgebraicClosure K))
      (((traceForm K L) ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen))))
        ((fun i ↦ pb.gen ^ ↑i) j)) =
    (algebraMap K (AlgebraicClosure K)) (if j = i then 1 else 0)
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
n : ℕ
a : K
⊢ a ^ q ^ n = a

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih => simp [pow_succ, pow_mul, ih, pow_card]

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

Goal state before:
pp: a b : ℤ
⊢ a.gcd b = 1 ↔ a.natAbs.Coprime b.natAbs

Tactic:
Nat.coprime_iff_gcd_eq_one,

Goal state after:
a b : ℤ
⊢ a.gcd b = 1 ↔ a.natAbs.gcd b.natAbs = 1
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : i = 0
⊢ ∑ x, x ^ i = 0

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
⊢ ∑ x, x ^ i = 0

Tactic:
· simp only [hi, nsmul_one, sum_const, pow_zero, card_univ, cast_card_eq_zero]

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
⊢ ∑ x, x ^ i = 0
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
| (RingHom.id K) x

Tactic:
RingHom.id_apply,

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
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
n : ℕ
x : ZMod p
⊢ x ^ p ^ n = x

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih => simp [pow_succ, pow_mul, ih, pow_card]

Goal state after:
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 a

Tactic:
refine P_of_associated (prod_normalizedFactors ha0) ?_

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 (normalizedFactors a).prod
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

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
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
this✝¹ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfLEComap ⋯
this✝ : Algebra (S ⧸ P) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
this : Algebra (R ⧸ p) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
⊢ ∀ (x : R ⧸ p), (algebraMap (R ⧸ p) (T ⧸ I)) x = (algebraMap (S ⧸ P) (T ⧸ I)) ((algebraMap (R ⧸ p) (S ⧸ P)) x)

Tactic:
by
    rintro ⟨x⟩; exact congr_arg _ (IsScalarTower.algebraMap_apply R S T x)

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 d d' e e' : S
a_notMem : a ∉ P ^ (i + 1)
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)
⊢ d - d' ∈ P

Tactic:
have h' : a * (d - d') ∈ P ^ (i + 1) := by
    convert! Ideal.add_mem _ h (Ideal.sub_mem _ e'_mem e_mem) using 1
    ring
  exact Ideal.mem_prime_of_mul_mem_pow hP a_notMem h'

Goal state after:
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
p : α
a✝ : p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset
hpa : p ∉ normalizedFactors a
⊢ id p ^ Multiset.count p (normalizedFactors a) = 1

Tactic:
simp [hpa]

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.leftInv
⊢ ↑((fun x ↦ ⟨↑(IsUnit.unit ⋯)⁻¹, ⋯⟩) ((↑S.fromCommLeftInv).toFun x)) = ↑x

Tactic:
simp [← Units.mul_eq_one_iff_inv_eq]

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

Goal state before:
pp: case inr.refine_2
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
I : Ideal S
hI : I ∈ {I | absNorm I = n}
⊢ ∀ ⦃x₂ : Ideal S⦄, x₂ ∈ {I | absNorm I = n} → f I = f x₂ → I = x₂

Tactic:
J

Goal state after:
case inr.refine_2
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
I : Ideal S
hI : I ∈ {I | absNorm I = n}
J : Ideal S
⊢ J ∈ {I | absNorm I = n} → f I = f J → I = J
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: case succ.succ.refine_1
R₀ : Type u_1
R : Type u_2
inst✝⁷ : Ring R₀
inst✝⁶ : Ring R
inst✝⁵ : Module R₀ R
inst✝⁴ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R₀ M
inst✝¹ : Module R M
inst✝ : IsScalarTower R₀ R M
n : ℕ
ih :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M],
    Jac ^ (n + 1) ≤ Module.annihilator R M → P M
hn : Jac ^ (n + 1 + 1) • ⊤ = ⊥
⊢ Jac ^ (n + 1) ≤ Module.annihilator R ↥(Jac • ⊤)

Tactic:
Jac.pow_succ,

Goal state after:
case succ.succ.refine_1
R₀ : Type u_1
R : Type u_2
inst✝⁷ : Ring R₀
inst✝⁶ : Ring R
inst✝⁵ : Module R₀ R
inst✝⁴ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R₀ M
inst✝¹ : Module R M
inst✝ : IsScalarTower R₀ R M
n : ℕ
ih :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M],
    Jac ^ (n + 1) ≤ Module.annihilator R M → P M
hn : (Jac ^ (n + 1) * Jac) • ⊤ = ⊥
⊢ Jac ^ (n + 1) ≤ Module.annihilator R ↥(Jac • ⊤)
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
⊢ ¬map f p ≤ P * P → map (algebraMap R (Localization.AtPrime P)) p = maximalIdeal (Localization.AtPrime P)

Tactic:
intro H₁

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
⊢ map (algebraMap R (Localization.AtPrime P)) p = maximalIdeal (Localization.AtPrime P)
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case h₂
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B✝ : Type w
inst✝² : CommRing B✝
inst✝¹ : FormallyUnramified R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type w
inst✝ : CommRing B
I : Ideal B
⊢ ∀ (J : Ideal B),
    I ≤ J →
      (∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R I).comp) →
        (∀ [inst : Algebra R (B ⧸ I)],
            Function.Injective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
          ∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R J).comp

Tactic:
J

Goal state after:
case h₂
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B✝ : Type w
inst✝² : CommRing B✝
inst✝¹ : FormallyUnramified R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type w
inst✝ : CommRing B
I J : Ideal B
⊢ I ≤ J →
    (∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R I).comp) →
      (∀ [inst : Algebra R (B ⧸ I)],
          Function.Injective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
        ∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R J).comp