mathlib-initiative/mathlib-tactics huggingface dataset:
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
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_eq_zero : ifp.fr = 0
⊢ v = g.convs n

Tactic:
simpa [GenContFract.compExactValue, ifp_fr_eq_zero] using! g_finite_correctness

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case inr
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
⊢ let g := of v;
  let B := (g.contsAux (n + 1)).b;
  let pB := (g.contsAux n).b;
  v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
suffices v - A / B = (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB)) by simpa [ifp_fr_ne_zero]

Goal state after:
case inr
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
⊢ v - A / B = (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))
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
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ y ∉ {z} ∧ {z}.Nodup

Tactic:
mem_singleton

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
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ {z}.Nodup
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
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ {z}.Nodup

Tactic:
simp only [nodup_singleton]

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
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
⊢ f e₁ - f (e₁ * e₂) = f e₁

Tactic:
map_mul,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
⊢ f e₁ - f e₁ * f e₂ = f e₁
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ f ((1 - e₂) * e') = f e'

Tactic:
map_mul,

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ f (1 - e₂) * f e' = f e'
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝¹ : ∀ (i : ι), Free R ↥(N i)
h : IsInternal N
inst✝ : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : {i | N i ≠ ⊥}.Finite
⊢ (trace R M) f = 0

Tactic:
let s := hN.toFinset

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝¹ : ∀ (i : ι), Free R ↥(N i)
h : IsInternal N
inst✝ : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : {i | N i ≠ ⊥}.Finite
s : Finset ι := hN.toFinset
⊢ (trace R M) f = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r₁ r₂ : R
i : I
⊢ ↑⟨(fun x ↦ e i * x * e i) (r₁ + r₂), ⋯⟩ =
    ↑(((fun i ↦ ⟨(fun x ↦ e i * x * e i) r₁, ⋯⟩) + fun i ↦ ⟨(fun x ↦ e i * x * e i) r₂, ⋯⟩) i)

Tactic:
simpa [mul_add] using! add_mul ..

Goal state after:
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }
r x : A
⊢ (↑fe).1 (r * x) * (↑fe).2 = (↑fe).1 r * ((↑fe).1 x * (↑fe).2)

Tactic:
map_mul,

Goal state after:
R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }
r x : A
⊢ (↑fe).1 r * (↑fe).1 x * (↑fe).2 = (↑fe).1 r * ((↑fe).1 x * (↑fe).2)
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }
r x : A
⊢ (↑fe).1 (x * r) * (↑fe).2 = (↑fe).1 x * (↑fe).2 * (↑fe).1 r

Tactic:
map_mul,

Goal state after:
R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }
r x : A
⊢ (↑fe).1 x * (↑fe).1 r * (↑fe).2 = (↑fe).1 x * (↑fe).2 * (↑fe).1 r
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { _fe // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 (_fe.1 a) }
a : A
ad : A[ε]
⊢ (lift fe) (inl a * ad) = (↑fe).1 a * (lift fe) ad

Tactic:
map_mul,

Goal state after:
R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { _fe // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 (_fe.1 a) }
a : A
ad : A[ε]
⊢ (lift fe) (inl a) * (lift fe) ad = (↑fe).1 a * (lift fe) ad
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { _fe // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 (_fe.1 a) }
a : A
ad : A[ε]
⊢ (lift fe) (ad * inl a) = (lift fe) ad * (↑fe).1 a

Tactic:
map_mul,

Goal state after:
R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { _fe // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 (_fe.1 a) }
a : A
ad : A[ε]
⊢ (lift fe) ad * (lift fe) (inl a) = (lift fe) ad * (↑fe).1 a
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Semigroup β
f : α → β
x : α
y : FreeSemigroup α
⊢ (lift f) (of x * y) = f x * (lift f) y

Tactic:
map_mul,

Goal state after:
α : Type u
β : Type v
inst✝ : Semigroup β
f : α → β
x : α
y : FreeSemigroup α
⊢ (lift f) (of x) * (lift f) y = f x * (lift f) y
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
h : reduce L = L
x₁ : α
x₂ y₂ : Bool
l₁ l₂ : List (α × Bool)
hl : L = l₁ ++ (x₁, x₂) :: ((x₁, x₂).1, y₂) :: l₂
⊢ ((x₁, x₂).1, y₂).2 = (x₁, x₂).2

Tactic:
← Bool.ne_not

Goal state after:
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
h : reduce L = L
x₁ : α
x₂ y₂ : Bool
l₁ l₂ : List (α × Bool)
hl : L = l₁ ++ (x₁, x₂) :: ((x₁, x₂).1, y₂) :: l₂
⊢ ((x₁, x₂).1, y₂).2 ≠ !(x₁, x₂).2
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
x✝ x y : FreeMagma α
hx : (toFreeSemigroup x).length = x.length
hy : (toFreeSemigroup y).length = y.length
⊢ (toFreeSemigroup (x * y)).length = (x * y).length

Tactic:
map_mul,

Goal state after:
α : Type u
x✝ x y : FreeMagma α
hx : (toFreeSemigroup x).length = x.length
hy : (toFreeSemigroup y).length = y.length
⊢ (toFreeSemigroup x * toFreeSemigroup y).length = (x * y).length
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: case a.f
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
i : Fin (Polynomial.map (algebraMap R S) f).natDegree
| (algebraMap R S) (p * φ ↑i) * x ^ ↑i

Tactic:
map_mul,

Goal state after:
case a.f
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
i : Fin (Polynomial.map (algebraMap R S) f).natDegree
| (algebraMap R S) p * (algebraMap R S) (φ ↑i) * x ^ ↑i
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case right
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 : ∀ (r : R), C r ∣ f → IsUnit r
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 + r
hr : map (algebraMap R K) r = 0
hm : m = 0
hg' : ¬g.natDegree = 0
⊢ coeff 0 g.natDegree = 0

Tactic:
coeff_zero

Goal state after:
case right
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 : ∀ (r : R), C r ∣ f → IsUnit r
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 + r
hr : map (algebraMap R K) r = 0
hm : m = 0
hg' : ¬g.natDegree = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case hr
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n✝ : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n✝ + s
hs : map (algebraMap R K) s = 0
hn0 : n✝ = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n✝ = 0
this : f %ₘ q = r * s %ₘ q
n : ℕ
x : ℕ × ℕ
⊢ coeff 0 x.1 = 0

Tactic:
coeff_zero

Goal state after:
case hr
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n✝ : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n✝ + s
hs : map (algebraMap R K) s = 0
hn0 : n✝ = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n✝ = 0
this : f %ₘ q = r * s %ₘ q
n : ℕ
x : ℕ × ℕ
⊢ 0 = 0
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case hs
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n✝ : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n✝ + s
hs : map (algebraMap R K) s = 0
hn0 : n✝ = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n✝ = 0
this : f %ₘ q = r * s %ₘ q
n : ℕ
x : ℕ × ℕ
⊢ coeff 0 x.2 = 0

Tactic:
coeff_zero

Goal state after:
case hs
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n✝ : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n✝ + s
hs : map (algebraMap R K) s = 0
hn0 : n✝ = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n✝ = 0
this : f %ₘ q = r * s %ₘ q
n : ℕ
x : ℕ × ℕ
⊢ 0 = 0
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
k : R
hk : (algebraMap R K) k = y
⊢ (algebraMap R K) b = (algebraMap R K) (a * k)

Tactic:
map_mul,

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
⊢ (algebraMap R K) b = (algebraMap R K) a * (algebraMap R K) k
Module: Mathlib.Algebra.Group.Action.Equidecomp

Goal state before:
pp: case right
X : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
f g : X → X
A : Set X
S : Finset G
hf : IsDecompOn f A S
h : LeftInvOn g f A
a : X
ha : a ∈ A
γ : G
γ_mem : γ ∈ S
hγ : f a = γ • a
⊢ g (f a) = γ⁻¹ • f a

Tactic:
hγ,

Goal state after:
case right
X : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
f g : X → X
A : Set X
S : Finset G
hf : IsDecompOn f A S
h : LeftInvOn g f A
a : X
ha : a ∈ A
γ : G
γ_mem : γ ∈ S
hγ : f a = γ • a
⊢ g (γ • a) = γ⁻¹ • γ • a
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝¹ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a✝ b a : ℍ[R]
ha : a ≠ 0
⊢ ↑((normSq a)⁻¹ * normSq a) = 1

Tactic:
inv_mul_cancel₀ (normSq_ne_zero.2 ha),

Goal state after:
R : Type u_1
inst✝² : Field R
a✝¹ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a✝ b a : ℍ[R]
ha : a ≠ 0
⊢ ↑1 = 1
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: case a
a b : ℤ
⊢ zmultiples ↑(a.gcd b) ≤ closure {a, b}

Tactic:
· simp [zmultiples_le, mem_closure_pair, gcd_eq_gcd_ab, mul_comm]

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✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
this : ⇑invMonoidHom '' v '' baseOf v f ⊆ ⇑(MonoidHom.id G) '' v '' baseOf v (invMonoidHom.comp f)
⊢ ⇑invMonoidHom ∘ v '' baseOf v f ⊆ v '' baseOf v (invMonoidHom.comp f)

Tactic:
← image_comp

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
this : ⇑invMonoidHom ∘ v '' baseOf v f ⊆ ⇑(MonoidHom.id G) '' v '' baseOf v (invMonoidHom.comp f)
⊢ ⇑invMonoidHom ∘ v '' baseOf v f ⊆ v '' baseOf v (invMonoidHom.comp f)
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
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
⊢ ⇑invMonoidHom '' ⇑invMonoidHom '' v '' IsMulIndecomposable.baseOf v f = v '' IsMulIndecomposable.baseOf v f

Tactic:
← image_comp

Goal state after:
ι : 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
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
⊢ ⇑invMonoidHom ∘ ⇑invMonoidHom '' v '' IsMulIndecomposable.baseOf v f = v '' IsMulIndecomposable.baseOf v f
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 : G₀
⊢ ((snd G₀ H₀).comp (inl G₀ H₀)) x = 1 x

Tactic:
obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x <;>
  simp_all [WithZero.withZeroUnitsEquiv, snd, inl]

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

Goal state before:
pp: case h
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : MonoidWithZero B
f : A →*₀ B
a✝ b✝ : Bˣ
y : A
hy : f y = ↑a✝
y' : A
hy' : f y' = ↑b✝
⊢ f (y * y') = ↑(a✝ * b✝)

Tactic:
map_mul,

Goal state after:
case h
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : MonoidWithZero B
f : A →*₀ B
a✝ b✝ : Bˣ
y : A
hy : f y = ↑a✝
y' : A
hy' : f y' = ↑b✝
⊢ f y * f y' = ↑(a✝ * b✝)
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case a.a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| p ≫ φ.hom

pp: case a.a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.inv

pp: case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.symm.hom

Tactic:
hpp'

Goal state after:
case a.a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.hom ≫ p'

case a.a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.inv

case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| φ.symm.hom
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
h : f.f = g.f
⊢ f = g

Tactic:
simpa [hom_ext_iff] using h

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h.e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (-1) ^ ↑i * (-1) ^ ↑j = -((-1) ^ ↑(φ (i, j) hij).1 * (-1) ^ ↑(φ (i, j) hij).2)

Tactic:
simp only [φ, Fin.val_succ, pow_add, pow_one, mul_neg, neg_neg, mul_one]

Goal state after:
case h.e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (-1) ^ ↑i * (-1) ^ ↑j = (-1) ^ ↑(j.castLT ⋯) * (-1) ^ ↑i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
⊢ Fin (X.len + 1) ≃ Fin (Y.len + 1)

Tactic:
exact ((skeletalFunctor ⋙ forget NonemptyFinLinOrd).mapIso I).toEquiv

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
⊢ X.δ j ≫ X.δ₀Iter i hi = X.δ₀Iter (i + 1) ⋯

Tactic:
dsimp [δ, δ₀Iter]
  rw [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_δ ..]

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

Goal state before:
pp: A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
⊢ f ≫ Hom.mk { toFun := ⇑(ConcreteCategory.hom (inv ((forget SimplexCategory).map f))), monotone' := ⋯ } = 𝟙 A✝

Tactic:
ext x : 3
          exact Iso.hom_inv_id_apply (asIso ((forget _).map f)) x

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

Goal state before:
pp: i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m),
    ↑j = ↑j' + i → δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
m : ℕ
j : Fin (m + 1 + 1)
hi' : n + (i + 1) = m + 1
hj' : ↑j = ↑j' + (i + 1)
⊢ j ≠ 0

Tactic:
rintro rfl; dsimp at hj'; lia

Goal state after: