mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ (fun o ↦ Option.rec none (fun val ↦ some (g (f val))) o) =
    (fun o ↦ Option.rec none (fun val ↦ some (g val)) o) ∘ fun o ↦ Option.rec none (fun val ↦ some (f val)) o

Tactic:
ext ⟨⟩

Goal state after:
case none
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
a✝ : γ
⊢ Option.rec none (fun val ↦ some (g (f val))) none = some a✝ ↔
    ((fun o ↦ Option.rec none (fun val ↦ some (g val)) o) ∘ fun o ↦ Option.rec none (fun val ↦ some (f val)) o) none =
      some a✝

case some
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
val✝ : α
a✝ : γ
⊢ Option.rec none (fun val ↦ some (g (f val))) (some val✝) = some a✝ ↔
    ((fun o ↦ Option.rec none (fun val ↦ some (g val)) o) ∘ fun o ↦ Option.rec none (fun val ↦ some (f val)) o)
        (some val✝) =
      some a✝
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ}, k < n → s.get? k = some x → x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
y : α
hy : s.get? 0 = some y
⊢ s.tail.get? k = some x

Tactic:
get?_tail

Goal state after:
case succ
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ}, k < n → s.get? k = some x → x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
y : α
hy : s.get? 0 = some y
⊢ s.get? (k + 1) = some x
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
⊢ Option.map (g ∘ f) = Option.map g ∘ Option.map f

Tactic:
ext ⟨⟩

Goal state after:
case none
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
a✝ : γ
⊢ Option.map (g ∘ f) none = some a✝ ↔ (Option.map g ∘ Option.map f) none = some a✝

case some
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
val✝ : α
a✝ : γ
⊢ Option.map (g ∘ f) (some val✝) = some a✝ ↔ (Option.map g ∘ Option.map f) (some val✝) = some a✝
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι) (a : G i), (g i) a = 0 → a = 0
z : DirectLimit G f
⊢ (lift G f P g Hg) z = 0 → z = 0

Tactic:
hz

Goal state after:
ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι) (a : G i), (g i) a = 0 → a = 0
z : DirectLimit G f
hz : (lift G f P g Hg) z = 0
⊢ z = 0
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: case zero
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
stream_zero_eq : IntFractPair.stream v 0 = some (IntFractPair.of v)
x✝ : Int.fract v = 0 ∨ Int.fract v ≠ 0
⊢ v = compExactValue ((of v).contsAux 0) ((of v).contsAux (0 + 1)) (IntFractPair.of v).fr

Tactic:
cases eq_or_ne (Int.fract v) 0 with

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

Goal state before:
pp: case zero
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
n : ℕ
inst✝ : IsStrictOrderedRing K
a : ℤ
⊢ (of ↑a).convs' 0 = ↑a

Tactic:
simp only [zeroth_conv'_eq_h, of_h_eq_floor, floor_intCast]

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
f : α → α
n m : ℕ
⊢ (nil.update n f).get? m = nil.get? m

Tactic:
simp [get?_update]

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case zero
α : Type u
hd : α
tl : Seq α
f : α → α
⊢ ((cons hd tl).update 0 f).get? 0 = (cons (f hd) tl).get? 0

Tactic:
simp [get?_update]

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
hd : α
tl : Seq α
f : α → α
n✝ : ℕ
⊢ ((cons hd tl).update 0 f).get? (n✝ + 1) = (cons (f hd) tl).get? (n✝ + 1)

Tactic:
simp [get?_update]

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case zero
α : Type u
hd : α
tl : Seq α
f : α → α
n : ℕ
⊢ ((cons hd tl).update (n + 1) f).get? 0 = (cons hd (tl.update n f)).get? 0

Tactic:
simp [get?_update]

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
hd : α
tl : Seq α
f : α → α
n n✝ : ℕ
⊢ ((cons hd tl).update (n + 1) f).get? (n✝ + 1) = (cons hd (tl.update n f)).get? (n✝ + 1)

Tactic:
simp [get?_update]

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case inl
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
hy : some y = (s.set n x).get? n
⊢ p y

pp: case inr
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
m : ℕ
hy : some y = (s.set n x).get? m
h_nm : n ≠ m
⊢ p y

Tactic:
· by_cases h_term : s.TerminatedAt n
    · simp [get?_set_of_terminatedAt _ h_term] at hy
    · simp_all [get?_set_of_not_terminatedAt _ h_term]

Goal state after:
case inr
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
m : ℕ
hy : some y = (s.set n x).get? m
h_nm : n ≠ m
⊢ p y
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case zero
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
IH : ∀ m < 0, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
⊢ ∃ conts, (of v).contsAux 0 = Pair.map Rat.cast conts

Tactic:
suffices ∃ gp : Pair ℚ, Pair.mk (1 : K) 0 = gp.map (↑) by simpa [contsAux]

Goal state after:
case zero
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
IH : ∀ m < 0, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
⊢ ∃ gp, { a := 1, b := 0 } = Pair.map Rat.cast gp
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case refl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GenContFract K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < m.succ → g.s.get? m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      g.convs m.succ = g.convs' m.succ
s_pos : ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < m.succ + 1 → g.s.get? m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF m.succ
not_terminatedAt_n : ¬g.TerminatedAt m.succ
this✝ : g.convs (m.succ + 1) = g'.convs m.succ
s_mth_eq' : g'.s.get? m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : g.s.get? (m + 1) = some gp_succ_m
gp_m : Pair K
mth_s_eq : g.s.get? m = some gp_m
m_lt_n : m < m.succ
this : 0 < gp_succ_m.a ∧ 0 < gp_succ_m.b
⊢ 0 < gp_succ_m.a / gp_succ_m.b

Tactic:
exact div_pos this.left this.right

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
hd : P.d = 1
⊢ P.toPoly.Monic

Tactic:
by
  rw [Monic, leadingCoeff_of_c_eq_zero ha hb hc, hd]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝¹ : CommRing R
inst✝ : IsDomain R
h0 : P.toPoly ≠ 0
x : R
⊢ x ∈ P.roots ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0

Tactic:
rw [roots, mem_roots h0, IsRoot, toPoly]
  simp only [eval_C, eval_X, eval_add, eval_mul, eval_pow]

Goal state after:
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 ∣ (1 ^ n - (1 - x ^ n) ^ n) * (1 ^ n - x ^ n) ^ n

Tactic:
rw [← (Commute.one_left x).mul_geom_sum₂, ← (Commute.one_left (1 - x ^ n)).mul_geom_sum₂]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Type u_3
e : I → R
inst✝ : Fintype I
he : OrthogonalIdempotents e
⊢ (∑ i, e i) * (1 - ∑ i, e i) = 0

Tactic:
simp [mul_sub, he.isIdempotentElem_sum.eq]

Goal state after:
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : (i : ι) → AddCommMonoid (β i)
c : AddCon M
h h' : (i : ι) → β i →+ M
f g : Π₀ (i : ι), β i
H : ∀ (i : ι), c ((h i) (f i)) ((h' i) (g i))
⊢ c ((DFinsupp.sumAddHom h) f) ((DFinsupp.sumAddHom h') g)

Tactic:
simp_rw [DFinsupp.sumAddHom_apply]

Goal state after:
ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : (i : ι) → AddCommMonoid (β i)
c : AddCon M
h h' : (i : ι) → β i →+ M
f g : Π₀ (i : ι), β i
H : ∀ (i : ι), c ((h i) (f i)) ((h' i) (g i))
⊢ c (f.sum fun x ↦ ⇑(h x)) (g.sum fun x ↦ ⇑(h' x))
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : (i : ι) → AddCommMonoid (β i)
c : AddCon M
h : (i : ι) → β i →+ M
f : Π₀ (i : ι), β i
⊢ ↑((DFinsupp.sumAddHom h) f) = (DFinsupp.sumAddHom fun i ↦ c.mk'.comp (h i)) f

Tactic:
simp_rw [← AddCon.coe_mk', DFinsupp.sumAddHom_apply, map_dfinsuppSum]

Goal state after:
ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : (i : ι) → AddCommMonoid (β i)
c : AddCon M
h : (i : ι) → β i →+ M
f : Π₀ (i : ι), β i
⊢ (f.sum fun a b ↦ c.mk' ((h a) b)) = f.sum fun x ↦ ⇑(c.mk'.comp (h x))
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_1.some.some
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k : I → R
hk : ∀ (i : I), e' i * e' i - e' i = e₀ * k i
i j : I
h : some i ≠ some j
⊢ Option.rec e₀ ((1 - e₀) • e') (some i) * Option.rec e₀ ((1 - e₀) • e') (some j) = 0

Tactic:
obtain ⟨k, hk⟩ := Ideal.mem_span_singleton.mp
        (hfe₀.le (show f (e' i * e' j) = 0 by simp [he', he.1.2 (by simpa using h)]))
      dsimp
      rw [mul_mul_mul_comm, hk, he₀.one_sub.eq, ← mul_assoc, he₀.one_sub_mul_self, zero_mul]

Goal state after:
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
R' : Type u_5
inst✝ : CommSemiring R'
f g : R[ε] →+* R'
h₀ : f.comp (algebraMap R R[ε]) = g.comp (algebraMap R R[ε])
hε : f ε = g ε
⊢ f = g

Tactic:
let : Algebra R R' := by
    letI := f.toAlgebra
    exact Algebra.compHom _ (algebraMap R R[ε])
  let f' : R[ε] →ₐ[R] R' :=
    { toRingHom := f
      commutes' _ := rfl }
  let g' : R[ε] →ₐ[R] R' :=
    { toRingHom := g
      commutes' r := (DFunLike.congr_fun h₀ r).symm }
  exact congr_arg AlgHom.toRingHom (show f' = g' from algHom_ext hε)

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f g : End R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
μ₁ μ₂ : R
h : MapsTo ⇑f ↑(g.maxGenEigenspace μ₁) ↑(g.maxGenEigenspace μ₂)
⊢ MapsTo ⇑(LinearMap.restrict f hf) ↑(maxGenEigenspace (LinearMap.restrict g hg) μ₁)
    ↑(maxGenEigenspace (LinearMap.restrict g hg) μ₂)

Tactic:
by
  intro x hx
  simp_rw [SetLike.mem_coe, mem_maxGenEigenspace, ← LinearMap.restrict_smul_one _,
    LinearMap.restrict_sub _, Module.End.pow_restrict _, LinearMap.restrict_apply,
    Submodule.mk_eq_zero, ← mem_maxGenEigenspace] at hx ⊢
  exact h hx

Goal state after:
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
V₁ : Type u₁
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
V₂ : Type u₂
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
V₃ : Type u₃
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
V₄ : Type u₄
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
V₅ : Type u₅
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
⊢ ↑(finrank k V₀) - ↑(finrank k V₁) + ↑(finrank k V₂) - ↑(finrank k V₃) + ↑(finrank k V₄) - ↑(finrank k V₅) = 0

Tactic:
let W₀ := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅} V₀

Goal state after:
k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
V₁ : Type u₁
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
V₂ : Type u₂
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
V₃ : Type u₃
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
V₄ : Type u₄
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
V₅ : Type u₅
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
W₀ : Type (max u₀ u₁ u₂ u₃ u₄ u₅) := ULift.{max u₀ u₁ u₂ u₃ u₄ u₅, u₀} V₀
⊢ ↑(finrank k V₀) - ↑(finrank k V₁) + ↑(finrank k V₂) - ↑(finrank k V₃) + ↑(finrank k V₄) - ↑(finrank k V₅) = 0
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
⊢ reduce (reduce L₁ ++ reduce L₂) = reduce (L₁ ++ L₂)

Tactic:
by
  rw [← toWord_mk (L₁ := L₁ ++ L₂), ← mul_mk, toWord_mul, toWord_mk, toWord_mk]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
⊢ IsReduced x.toWord

Tactic:
simp [isReduced_iff_reduce_eq]

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.Count

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ (countP fun x_1 ↦ x_1 = x) (of y) = Pi.single x 1 y

Tactic:
rw [countP_of]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ (if y = x then 1 else 0) = Pi.single x 1 y
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✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ x✝² * x✝¹ * x✝ = x✝² * (x✝¹ * x✝)

Tactic:
by ext <;> simp <;> ring

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✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ x✝² * (x✝¹ + x✝) = x✝² * x✝¹ + x✝² * x✝

Tactic:
by ext <;> simp <;> ring

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

Goal state before:
pp: R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
⊢ (p.scaleRoots x).IsRoot y

Tactic:
injective_iff_map_eq_zero'

Goal state after:
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), f a = 0 ↔ a = 0
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
⊢ (p.scaleRoots x).IsRoot y
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✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² + x✝¹) * x✝ = x✝² * x✝ + x✝¹ * x✝

Tactic:
by ext <;> simp <;> ring

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✝¹ x✝ : ℍ[R,c₁,c₃]
⊢ { re := (x✝¹ * x✝).re, imI := (x✝¹ * x✝).imJ, imJ := (x✝¹ * x✝).imI, imK := -(x✝¹ * x✝).imK } =
    { re := x✝¹.re, imI := x✝¹.imJ, imJ := x✝¹.imI, imK := -x✝¹.imK } *
      { re := x✝.re, imI := x✝.imJ, imJ := x✝.imI, imK := -x✝.imK }

Tactic:
by ext <;> simp <;> ring

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
a b : ℍ[R,c₁,c₂,c₃]
⊢ star (a * b) = star b * star a

Tactic:
by ext <;> simp <;> ring

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 * a = ↑(star a * a).re

Tactic:
by ext <;> simp <;> ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ star a = ↑(2 * a.re) - a

Tactic:
simpa using! QuaternionAlgebra.star_eq_two_re_sub a

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

Goal state before:
pp: 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
i : ℕ
hi : i ∈ range j
⊢ Δ_[1]^[n] (j.choose i • fun r ↦ r ^ i) = 0

Tactic:
by
      rw [fwdDiff_iter_const_smul, ih (by have := mem_range.1 hi; lia), nsmul_zero]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s : Submonoid M
p : (x : M) → x ∈ s.saturation → Prop
mem : ∀ (x : M) (hx : x ∈ s), p x ⋯
mul : ∀ (x y : M) (hx : x ∈ s.saturation) (hy : y ∈ s.saturation), p x hx → p y hy → p (x * y) ⋯
of_mul : ∀ (x y : M) (hxy : x * y ∈ s.saturation), p (x * y) hxy → p x ⋯ ∧ p y ⋯
x : M
hx : x ∈ s.saturation
⊢ p x hx

Tactic:
by
  let s' : SaturatedSubmonoid M :=
  { carrier := { x | ∃ hx, p x hx }
    one_mem' := ⟨_ , mem 1 <| one_mem s⟩
    mul_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, mul _ _ _ _ hpx hpy⟩
    mulSaturated := fun x y ⟨_, hpxy⟩ ↦ ⟨⟨_, (of_mul _ _ _ hpxy).1⟩, ⟨_, (of_mul _ _ _ hpxy).2⟩⟩ }
  exact SaturatedSubmonoid.mem_sInf.mp hx s' (fun _ h ↦ ⟨_, mem _ h⟩) |>.2

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ { l // l ≫ (Fork.ofι i ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι i ⋯).pt}, m ≫ (Fork.ofι i ⋯).ι = s.ι → m = l }

Tactic:
refine ⟨s.ι ≫ e, ?_⟩

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ (s.ι ≫ e) ≫ (Fork.ofι i ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι i ⋯).pt}, m ≫ (Fork.ofι i ⋯).ι = s.ι → m = s.ι ≫ e
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.castSucc = ↑⟨k, isLt✝⟩.castSucc.castSucc

Tactic:
· simp at * <;> lia

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

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.castSucc = ↑⟨k, isLt✝⟩.castSucc.succ

Tactic:
· simp at * <;> lia

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

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.castSucc = ↑⟨k, isLt✝⟩.succ.castSucc

Tactic:
· simp at * <;> lia

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

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.castSucc = ↑⟨k, isLt✝⟩.succ.succ

Tactic:
· simp at * <;> lia

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

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.succ = ↑⟨k, isLt✝⟩.castSucc.castSucc

Tactic:
· simp at * <;> lia

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

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.succ = ↑⟨k, isLt✝⟩.castSucc.succ

Tactic:
· simp at * <;> lia

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

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.succ = ↑⟨k, isLt✝⟩.succ.castSucc

Tactic:
· simp at * <;> lia

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

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.succ = ↑⟨k, isLt✝⟩.succ.succ

Tactic:
· simp at * <;> lia

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

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ¬⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.succ.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.succ.castSucc = ↑⟨k, isLt✝⟩.castSucc.castSucc

Tactic:
· simp at * <;> lia

Goal state after: