mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case qsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
q✝ : ℚ
x✝ : α
⊢ e (q✝ • x✝) = q✝ • e x✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case npow
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case zpow
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
x✝ : α
n✝ : ℤ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
n✝ : ℕ
⊢ e ↑n✝ = ↑n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case intCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
n✝ : ℤ
⊢ e ↑n✝ = ↑n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case nnratCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
q✝ : ℚ≥0
⊢ e ↑q✝ = ↑q✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case ratCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
q✝ : ℚ
⊢ e ↑q✝ = ↑q✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ e 0 = 0

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case one
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := ⋯
neg : Neg α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
mul : Mul α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
nnratCast : NNRatCast α := ⋯
ratCast : RatCast α := ⋯
nnqsmul : SMul ℚ≥0 α := ⋯
qsmul : SMul ℚ α := ⋯
⊢ e 1 = 1

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
x✝ y✝ : α
⊢ e (x✝ + y✝) = e x✝ + e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
x✝ : α
⊢ e (-x✝) = -e x✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case sub
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
x✝ y✝ : α
⊢ e (x✝ - y✝) = e x✝ - e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case inv
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
x✝ : α
⊢ e x✝⁻¹ = (e x✝)⁻¹

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case div
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
x✝ y✝ : α
⊢ e (x✝ / y✝) = e x✝ / e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
n✝ : ℕ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case zsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
n✝ : ℤ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case nnqsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
q✝ : ℚ≥0
x✝ : α
⊢ e (q✝ • x✝) = q✝ • e x✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case qsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
q✝ : ℚ
x✝ : α
⊢ e (q✝ • x✝) = q✝ • e x✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case npow
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case zpow
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
x✝ : α
n✝ : ℤ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
n✝ : ℕ
⊢ e ↑n✝ = ↑n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case intCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
n✝ : ℤ
⊢ e ↑n✝ = ↑n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case nnratCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
q✝ : ℚ≥0
⊢ e ↑q✝ = ↑q✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: case ratCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
ratCast : RatCast α := e.ratCast
nnqsmul : SMul ℚ≥0 α := Equiv.smul ℚ≥0 e
qsmul : SMul ℚ α := Equiv.smul ℚ e
q✝ : ℚ
⊢ e ↑q✝ = ↑q✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
n : ℕ
⊢ (x ^ n).toWord = reduce (List.replicate n x.toWord).flatten

Tactic:
rw [← mk_toWord (x := x)]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
n : ℕ
⊢ (mk x.toWord ^ n).toWord = reduce (List.replicate n (mk x.toWord).toWord).flatten
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
⊢ Infinite (FreeGroup α)

Tactic:
exact Infinite.of_surjective FreeGroup.norm FreeGroup.norm_surjective

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff * q ^ m + r
⊢ ∃ m r, g = C g.leadingCoeff * q ^ m + r ∧ map (algebraMap R K) r = 0 ∧ (m = 0 → IsUnit g)

Tactic:
have hr : r.map (algebraMap R K) = 0 := by
    obtain ⟨u, hu⟩ := hf.symm
    obtain ⟨a, ha, ha'⟩ := Polynomial.isUnit_iff.mp u.isUnit
    suffices C (algebraMap R K g.leadingCoeff) = u by
      simp [r, ← this, Polynomial.map_sub, ← hu, Polynomial.map_mul, map_C,
        Polynomial.map_pow, mul_comm]
    rw [← leadingCoeff_map_of_leadingCoeff_ne_zero _ hgP, ← hu, ← ha',
      leadingCoeff_mul, leadingCoeff_C, (hq_monic.map _).pow m, one_mul]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
⊢ ∃ m r, g = C g.leadingCoeff * q ^ m + r ∧ map (algebraMap R K) r = 0 ∧ (m = 0 → IsUnit g)
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case mpr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : IsIntegrallyClosedIn R A
x : A
⊢ x ∈ integralClosure R A → x ∈ ⊥

Tactic:
hx

Goal state after:
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : IsIntegrallyClosedIn R A
x : A
hx : x ∈ integralClosure R A
⊢ x ∈ ⊥
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : 0 < p.natDegree - n✝
⊢ p.coeff n✝ * x ^ (p.natDegree - n✝) ∈ P

Tactic:
exact Ideal.mul_mem_left _ _ (Ideal.pow_mem_of_mem P hP _ i)

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_4
K : Type u_5
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : FaithfulSMul R K
inst✝ : IsIntegrallyClosedIn R K
this : IsDomain R
f : FractionRing R →ₐ[R] K := IsFractionRing.liftAlgHom ⋯
x : FractionRing R
⊢ IsIntegral R x → ∃ y, (algebraMap R (FractionRing R)) y = x

Tactic:
hx

Goal state after:
R : Type u_4
K : Type u_5
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : FaithfulSMul R K
inst✝ : IsIntegrallyClosedIn R K
this : IsDomain R
f : FractionRing R →ₐ[R] K := IsFractionRing.liftAlgHom ⋯
x : FractionRing R
hx : IsIntegral R x
⊢ ∃ y, (algebraMap R (FractionRing R)) y = x
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n : ℤ
m : ℕ
⊢ ↑(n ^ m * n) = ↑n ^ (m + 1)

Tactic:
Int.cast_mul,

Goal state after:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n : ℤ
m : ℕ
⊢ ↑(n ^ m) * ↑n = ↑n ^ (m + 1)
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n : ℤ
m : ℕ
⊢ ↑(n ^ (m + 1)) = ↑n ^ (m + 1)

Tactic:
by
    rw [npow_add, npow_one, Int.cast_mul, Int.cast_npow R n m, npow_add, npow_one]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
mul : Mul α := ⋯
zero : Zero α := ⋯
⊢ e 0 = 0

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
mul : Mul α := e.mul
zero : Zero α := e.zero
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
zero : Zero α := ⋯
mul : Mul α := ⋯
⊢ e 0 = 0

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
zero : Zero α := e.zero
mul : Mul α := e.mul
a✝ b✝ : α
⊢ e (a✝ * b✝) = e a✝ * e b✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
⊢ MulZeroClass α

Tactic:
by
  let zero := e.zero
  let mul := e.mul
  apply e.injective.mulZeroClass _ <;> intros <;> exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := ⋯
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 0 = 0

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := ⋯
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 1 = 1

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroOneClass β
zero : Zero α := e.zero
one : One α := e.one
mul : Mul α := e.mul
a✝ b✝ : α
⊢ e (a✝ * b✝) = e a✝ * e b✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ e 0 = 0

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ e 1 = 1

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝² : MulZeroOneClass α := e.mulZeroOneClass
x✝¹ : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case npow
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝² : MulZeroOneClass α := e.mulZeroOneClass
x✝¹ : Pow α ℕ := Equiv.pow ℕ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := ⋯
⊢ e 0 = 0

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝ : MonoidWithZero α := ⋯
⊢ e 1 = 1

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝¹ : MonoidWithZero α := e.monoidWithZero
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case npow
α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
x✝¹ : MonoidWithZero α := e.monoidWithZero
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
a : A
h : f a ≠ 0
⊢ (restrict₀ f) a = ↑⟨Units.mk0 (f a) h, ⋯⟩

Tactic:
by
  simp [h, restrict₀_apply]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case some
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
x : Bˣ
hx : x ∈ f.valueGroup
r : A
hr : f r ≠ 0
s : A
hs : f s ≠ 0
hrs : f r * ↑x = f s
⊢ some ⟨x, hx⟩ = 0 ∨ ∃ r s, ∃ (hr : f r ≠ 0) (hs : f s ≠ 0), some ⟨x, hx⟩ = ↑(valueGroup.mk f r s hr hs)

Tactic:
refine .inr ⟨r, s, hr, hs, Option.some_inj.mpr <| by
      simp only [valueGroup.mk, Subtype.mk.injEq]
      rw [eq_inv_mul_iff_mul_eq]
      simp [← hrs, mul_comm]⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
x✝¹ x✝ : ⊥.toSSet ⟶ Y
⊢ x✝¹ = x✝

Tactic:
ext _ ⟨_, h⟩; tauto

Goal state after: