mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case succ.succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts

Tactic:
rcases s_ppred_nth_eq : g.s.get? n with gp_n | gp_n

Goal state after:
case succ.succ.none
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
s_ppred_nth_eq : g.s.get? n = none
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts

case succ.succ.some
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case some
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : s.get? (n + 1) = some val✝
⊢ (squashSeq s n).get? m = s.get? m

Tactic:
| some =>

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
ha : P.a ≠ 0
⊢ (Polynomial.map φ P.toPoly).Splits ↔ ∃ x y z, (map φ P).roots = {x, y, z}

Tactic:
splits_iff_card_roots ha,

Goal state after:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
ha : P.a ≠ 0
⊢ (map φ P).roots.card = 3 ↔ ∃ x y z, (map φ P).roots = {x, y, z}
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this : 1 / den' ≤ 1 / den
⊢ |(-1) ^ n / den'| = 1 / den'

Tactic:
suffices 1 / |den'| = 1 / den' by rwa [abs_div, abs_neg_one_pow n]

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this : 1 / den' ≤ 1 / den
⊢ 1 / |den'| = 1 / den'
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ (x - x ^ 2) ^ n ∣
    (x ^ n * ∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) *
      ((1 - x) * ∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1)) ^ n

Tactic:
rw [Commute.mul_pow, Commute.mul_mul_mul_comm, ← Commute.mul_pow, mul_one_sub, ← pow_two]

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ (x - x ^ 2) ^ n ∣
    (x - x ^ 2) ^ n *
      ((∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) * (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1)) ^ n)

case h
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute x (1 - x)

case hbc
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute (∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) ((1 - x) ^ n)

case h
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute (1 - x) (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1))
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case hbc
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute (∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) ((1 - x) ^ n)

pp: case h
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute (1 - x) (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1))

Tactic:
· refine .pow_right (.sub_right (.one_right _) (.sum_left _ _ _ fun _ _ ↦ .pow_left ?_ _)) _
      simp

Goal state after:
case h
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute (1 - x) (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1))
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
e : Fin n → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), e i ∈ f.range
h✝ : Nontrivial R
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
cases subsingleton_or_nontrivial S

Goal state after:
case inr.inl
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
e : Fin n → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), e i ∈ f.range
h✝¹ : Nontrivial R
h✝ : Subsingleton S
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

case inr.inr
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
e : Fin n → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin n), e i ∈ f.range
h✝¹ : Nontrivial R
h✝ : Nontrivial S
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
⊢ ∀ x ∈ I.jacobson, ∀ (i j : n), single i j x ∈ (matrix n I).jacobson

Tactic:
simp_rw [Ideal.mem_jacobson_iff]

Goal state after:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
⊢ ∀ (x : R),
    (∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I) →
      ∀ (i j : n) (y : Matrix n n R), ∃ z, z * y * single i j x + z - 1 ∈ matrix n I
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
r : R
⊢ r ∈ ↑(equivMatrix.symm I) → r ∈ {x | ∃ N ∈ I, N i j = x}

pp: case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
r : R
⊢ r ∈ {x | ∃ N ∈ I, N i j = x} → r ∈ ↑(equivMatrix.symm I)

Tactic:
· intro h
    exact ⟨single i j r, by simpa using! h i j, by simp⟩

Goal state after:
case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
r : R
⊢ r ∈ {x | ∃ N ∈ I, N i j = x} → r ∈ ↑(equivMatrix.symm I)
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
s : Finset M
b : Basis (↥s) R M
⊢ IsNilpotent ((toMatrix b b) f).trace

Tactic:
apply Matrix.isNilpotent_trace_of_isNilpotent

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
s : Finset M
b : Basis (↥s) R M
⊢ IsNilpotent ((toMatrix b b) f)
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
hμ : g = (algebraMap R (End R M)) μ + n
this : f ∘ₗ (algebraMap R (M →ₗ[R] M)) μ = μ • f
⊢ (trace R M) (μ • f) = μ * (trace R M) f

Tactic:
map_smul,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
hμ : g = (algebraMap R (End R M)) μ + n
this : f ∘ₗ (algebraMap R (M →ₗ[R] M)) μ = μ • f
⊢ μ • (trace R M) f = μ * (trace R M) f
Module: Mathlib.Algebra.Field.GeomSum

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n✝ : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ x * (x * x ^ n)⁻¹ = (x * x ^ n)⁻¹ * x

Tactic:
mul_inv_rev,

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n✝ : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ x * ((x ^ n)⁻¹ * x⁻¹) = (x ^ n)⁻¹ * x⁻¹ * x
Module: Mathlib.Algebra.Free

Goal state before:
pp: case refine_1
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
⊢ ∀ (a b₁ b₂ : α), AssocRel α b₁ b₂ → Quot.mk (AssocRel α) (a * b₁) = Quot.mk (AssocRel α) (a * b₂)

pp: case refine_2
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
⊢ ∀ (a₁ a₂ b : α), AssocRel α a₁ a₂ → Quot.mk (AssocRel α) (a₁ * b) = Quot.mk (AssocRel α) (a₂ * b)

Tactic:
· rintro a b₁ b₂ (⟨c, d, e⟩ | ⟨c, d, e, f⟩)
      · exact quot_mk_assoc_left _ _ _ _
      · rw [← quot_mk_assoc, quot_mk_assoc_left, quot_mk_assoc]

Goal state after:
case refine_2
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
⊢ ∀ (a₁ a₂ b : α), AssocRel α a₁ a₂ → Quot.mk (AssocRel α) (a₁ * b) = Quot.mk (AssocRel α) (a₂ * b)
Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas

Goal state before:
pp: case insert
ι : Type u_3
f : ι → ℚ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (∑ i ∈ s✝, f i).den ∣ s✝.lcm fun i ↦ (f i).den
⊢ (∑ i ∈ insert a✝ s✝, f i).den ∣ (insert a✝ s✝).lcm fun i ↦ (f i).den

Tactic:
rw [Finset.sum_insert has, Finset.lcm_insert]

Goal state after:
case insert
ι : Type u_3
f : ι → ℚ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (∑ i ∈ s✝, f i).den ∣ s✝.lcm fun i ↦ (f i).den
⊢ (f a✝ + ∑ x ∈ s✝, f x).den ∣ GCDMonoid.lcm (f a✝).den (s✝.lcm fun i ↦ (f i).den)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : AddZeroClass R
⊢ ↑(x + y) = ↑x + ↑y

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : AddGroup R
⊢ ↑(-x) = -↑x

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ 1 * x✝ = x✝

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ x✝ * 1 = x✝

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ 0 * x✝ = 0

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ x✝ * 0 = 0

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : CommRing R
⊢ ↑(x * y) = ↑x * ↑y

Tactic:
by ext <;> simp

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

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
ha : ¬a = 0
K : Type u_1 := FractionRing R
⊢ a ∣ b

Tactic:
replace ha : algebraMap R K a ≠ 0 := fun h ↦
    ha <| (injective_iff_map_eq_zero _).1 (IsFractionRing.injective R K) _ h

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : (algebraMap R K) a ≠ 0
⊢ a ∣ b
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : (algebraMap R K) a ≠ 0
y : K := (algebraMap R K) b / (algebraMap R K) a
hy : IsIntegral R y
⊢ a ∣ b

Tactic:
obtain ⟨k, hk⟩ := algebraMap_eq_of_integral hy

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : (algebraMap R K) a ≠ 0
y : K := (algebraMap R K) b / (algebraMap R K) a
hy : IsIntegral R y
k : R
hk : (algebraMap R K) k = y
⊢ a ∣ b
Module: Mathlib.Algebra.GCDMonoid.PUnit

Goal state before:
pp: ⊢ ∀ {a b : PUnit.{?u.2 + 1}}, a ≠ 0 → b ≠ 0 → 1 = 1 * 1

Tactic:
subsingleton

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.PUnit

Goal state before:
pp: ⊢ ∀ (u : PUnit.{?u.2 + 1}ˣ), 1 = u⁻¹

Tactic:
subsingleton

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.PUnit

Goal state before:
pp: x✝¹ x✝ : PUnit.{?u.2 + 1}
⊢ x✝¹ = unit * unit

Tactic:
subsingleton

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.PUnit

Goal state before:
pp: x✝¹ x✝ : PUnit.{?u.2 + 1}
⊢ x✝ = unit * unit

Tactic:
subsingleton

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.PUnit

Goal state before:
pp: x✝⁴ x✝³ x✝² : PUnit.{?u.2 + 1}
x✝¹ : x✝⁴ ∣ x✝²
x✝ : x✝⁴ ∣ x✝³
⊢ unit = x✝⁴ * unit

Tactic:
subsingleton

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.PUnit

Goal state before:
pp: x✝¹ x✝ : PUnit.{?u.2 + 1}
⊢ unit * unit * ↑1 = x✝¹ * x✝

Tactic:
subsingleton

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.PUnit

Goal state before:
pp: ⊢ ∀ (a : PUnit.{?u.2 + 1}), unit = 0

Tactic:
subsingleton

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.PUnit

Goal state before:
pp: ⊢ ∀ (a b : PUnit.{?u.2 + 1}), normalize unit = unit

Tactic:
subsingleton

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this : Algebra S K := g.toAlgebra
⊢ algebraMap R K = g.comp (algebraMap R S)

Tactic:
IsLocalization.map_comp,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this : Algebra S K := g.toAlgebra
⊢ algebraMap R K = (algebraMap R K).comp (RingHom.id R)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : CommRing R
⊢ star ↑x = ↑x

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ star a.im = -a.im + ↑c₂ * ↑a.imI

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₃ : R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
c₁ : R
a : ℍ[R,c₁,c₃]
⊢ star a = -a ↔ a.re = 0

Tactic:
by
  simp [QuaternionAlgebra.ext_iff, eq_neg_iff_add_eq_zero]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ star a.im = -a.im

Tactic:
by ext <;> simp

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

Goal state before:
pp: case hfmodP
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ map (algebraMap R (FractionRing (R ⧸ P))) f =
    C ((algebraMap R (FractionRing (R ⧸ P))) f.leadingCoeff) * map (algebraMap R (FractionRing (R ⧸ P))) X ^ f.natDegree

Tactic:
rw [← map_C, ← Polynomial.map_pow, ← Polynomial.map_mul]

Goal state after:
case hfmodP
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ map (algebraMap R (FractionRing (R ⧸ P))) f =
    map (algebraMap R (FractionRing (R ⧸ P))) (C f.leadingCoeff * X ^ f.natDegree)
Module: Mathlib.Algebra.Group.PNatPowAssoc

Goal state before:
pp: M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m n : ℕ+
⊢ x ^ (n * m) = (x ^ n) ^ m

Tactic:
exact ppow_mul x n m

Goal state after:
Module: Mathlib.Algebra.Group.PNatPowAssoc

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁵ : Mul M
inst✝⁴ : Pow M ℕ+
inst✝³ : PNatPowAssoc M
inst✝² : Mul N
inst✝¹ : Pow N ℕ+
inst✝ : PNatPowAssoc N
x✝ : M × N
⊢ x✝ ^ 1 = x✝

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: case e'_3.e_f
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝¹ : fwdDiffₗ M G h = shiftₗ M G h - 1
this✝ : Commute (shiftₗ M G h) (-1)
k : ℕ
this : (-1) ^ (n - k) * ↑(n.choose k) = ↑((-1) ^ (n - k) * ↑(n.choose k))
⊢ ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) = (shiftₗ M G h ^ k) (((-1) ^ (n - k) * ↑(n.choose k)) • f) y

Tactic:
map_smul,

Goal state after:
case e'_3.e_f
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝¹ : fwdDiffₗ M G h = shiftₗ M G h - 1
this✝ : Commute (shiftₗ M G h) (-1)
k : ℕ
this : (-1) ^ (n - k) * ↑(n.choose k) = ↑((-1) ^ (n - k) * ↑(n.choose k))
⊢ ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) = (((-1) ^ (n - k) * ↑(n.choose k)) • (shiftₗ M G h ^ k) f) y
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁵ : MulOneClass M
inst✝⁴ : Pow M ℕ
inst✝³ : NatPowAssoc M
inst✝² : MulOneClass N
inst✝¹ : Pow N ℕ
inst✝ : NatPowAssoc N
x✝ : M × N
⊢ x✝ ^ 0 = 1

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁵ : MulOneClass M
inst✝⁴ : Pow M ℕ
inst✝³ : NatPowAssoc M
inst✝² : MulOneClass N
inst✝¹ : Pow N ℕ
inst✝ : NatPowAssoc N
x✝ : M × N
⊢ x✝ ^ 1 = x✝

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: case succ
R : Type u_3
inst✝ : CommRing R
n : ℕ
ih : ∀ {j : ℕ}, j < n → (Δ_[1]^[n] fun r ↦ r ^ j) = 0
j : ℕ
h : j < n + 1
this : (Δ_[1] fun r ↦ r ^ j) = ∑ i ∈ range j, j.choose i • fun r ↦ r ^ i
⊢ (Δ_[1]^[n + 1] fun r ↦ r ^ j) = 0

Tactic:
rw [iterate_succ_apply, this, fwdDiff_iter_finsetSum]

Goal state after:
case succ
R : Type u_3
inst✝ : CommRing R
n : ℕ
ih : ∀ {j : ℕ}, j < n → (Δ_[1]^[n] fun r ↦ r ^ j) = 0
j : ℕ
h : j < n + 1
this : (Δ_[1] fun r ↦ r ^ j) = ∑ i ∈ range j, j.choose i • fun r ↦ r ^ i
⊢ ∑ k ∈ range j, Δ_[1]^[n] (j.choose k • fun r ↦ r ^ k) = 0
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
s t : Set M
⊢ #↑(s * t) ≤ #↑s * #↑t

Tactic:
rw [← image2_mul]

Goal state after:
M : Type u_2
inst✝ : Mul M
s t : Set M
⊢ #↑(image2 (fun x1 x2 ↦ x1 * x2) s t) ≤ #↑s * #↑t
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Set G
⊢ Nat.card ↑(s * t⁻¹) ≤ Nat.card ↑s * Nat.card ↑t⁻¹

Tactic:
exact natCard_mul_le

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x✝ : M
hx : x✝ ∈ s
⊢ x✝ * 1 ∈ s

Tactic:
by simpa

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: M : Type u_2
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x : M
hx : x ≠ 1
h : IsMulIndecomposable id univ x
⊢ ¬IsUnit x

Tactic:
by simpa

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

Goal state before:
pp: G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
x : H₀
hx : x ≠ 0
⊢ (fst G₀ H₀) ((inr G₀ H₀) x) = 1

Tactic:
rw [← comp_apply, fst_comp_inr, one_apply_of_ne_zero hx]

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
i : ι
hi : f (v i) ≠ 1
hi' : v i⁻¹ = (v i)⁻¹
hj : 1 < f (v i)
⊢ i ∈ {i | 1 < f (v i)} ∧ v i = v i

Tactic:
by simpa

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
⊢ Function.Injective ⇑embedding

Tactic:
simp [embedding, WithZero.map'_injective_iff]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ X.σ j ≫ X.δ i = X.δ (i.pred ⋯) ≫ X.σ (j.castLT ⋯)

Tactic:
dsimp [δ, σ]
  simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_gt' H]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case «1»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
· simp only [δ, len_mk, Nat.reduceAdd, mkHom, comp_toOrderHom, Hom.toOrderHom_mk, Fin.mk_one,
      OrderHom.comp_coe, OrderEmbedding.toOrderHom_coe, Function.comp_apply,
      mkOfSucc_homToOrderHom_one, Fin.succAboveOrderEmb_apply]
    subst h
    rw [Fin.succAbove_castSucc_self]
    rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
x✝¹ x✝ : Augmented C
f : x✝¹ ⟶ x✝
⊢ (whiskeringObj C D X✝).map f ≫ { left := η.app (point.obj x✝), right := whiskerLeft (drop.obj x✝) η, w := ⋯ } =
    { left := η.app (point.obj x✝¹), right := whiskerLeft (drop.obj x✝¹) η, w := ⋯ } ≫ (whiskeringObj C D Y✝).map f

Tactic:
by ext <;> simp

Goal state after: