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

Goal state before:
pp: case inr.succ
K : Type u_1
g : GenContFract K
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? (n' + 1) = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt (n' + 1)
s_nth_eq : g.s.get? (n' + 1) = some { a := a, b := b }
pa pb : K
s_n'th_eq : g.s.get? n' = some { a := pa, b := pb }
g' : GenContFract K := g.squashGCF (n' + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
succ_n'th_contsAux_eq : pred_conts = g.contsAux (n' + 1)
ppred_conts : Pair K := g.contsAux n'
n'th_contsAux_eq : ppred_conts = g.contsAux n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
⊢ g.convs (n' + 1 + 1) = (g.squashGCF (n' + 1)).convs (n' + 1)

Tactic:
set pred_conts' := g'.contsAux (n' + 1) with succ_n'th_contsAux_eq'

Goal state after:
case inr.succ
K : Type u_1
g : GenContFract K
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? (n' + 1) = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt (n' + 1)
s_nth_eq : g.s.get? (n' + 1) = some { a := a, b := b }
pa pb : K
s_n'th_eq : g.s.get? n' = some { a := pa, b := pb }
g' : GenContFract K := g.squashGCF (n' + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
succ_n'th_contsAux_eq : pred_conts = g.contsAux (n' + 1)
ppred_conts : Pair K := g.contsAux n'
n'th_contsAux_eq : ppred_conts = g.contsAux n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := g'.contsAux (n' + 1)
succ_n'th_contsAux_eq' : pred_conts' = g'.contsAux (n' + 1)
⊢ g.convs (n' + 1 + 1) = (g.squashGCF (n' + 1)).convs (n' + 1)
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
a : K
nth_partNum_eq : (of v).partNums.get? n = some a
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
gp_a_eq_a_n : gp.a = a
this : gp.a = 1
⊢ a = 1

Tactic:
gp_a_eq_a_n

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
a : K
nth_partNum_eq : (of v).partNums.get? n = some a
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
gp_a_eq_a_n : gp.a = a
this : a = 1
⊢ a = 1
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: 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

Tactic:
obtain ⟨n, hn⟩ := h 1 (Subsingleton.elim _ _)

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
n : ℕ
hn : 1 ^ n = 0
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mp
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
⊢ (∀ (i j : n), M i j = 0) → M = 0

Tactic:
intro H

Goal state after:
case mp
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
H : ∀ (i j : n), M i j = 0
⊢ M = 0
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
⊢ M = 0 → ∀ (i j : n), M i j = 0

Tactic:
intro H

Goal state after:
case mpr
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
H : M = 0
⊢ ∀ (i j : n), M i j = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : OrthogonalIdempotents e
he' : 1 = ∑ i, e i
__spread✝⁻⁰ : OrthogonalIdempotents e := he
⊢ ∑ i, e i = 1

Tactic:
eq_comm

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : OrthogonalIdempotents e
he' : ∑ i, e i = 1
__spread✝⁻⁰ : OrthogonalIdempotents e := he
⊢ ∑ i, e i = 1
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
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:
rintro ⟨n, hn, rfl⟩

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✝
n : Matrix n✝ n✝ R
hn : n ∈ I
⊢ n i j ∈ ↑(equivMatrix.symm I)
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
f : End R M
μ : R
x : ↥(f.eigenspace μ)
⊢ ↑((LinearMap.restrict f ⋯) x) = ↑((μ • LinearMap.id) x)

Tactic:
exact mem_eigenspace_iff.mp x.2

Goal state after:
Module: Mathlib.Algebra.Divisibility.Prod

Goal state before:
pp: ι : Type u_1
G₁ : Type u_2
G₂ : Type u_3
G : ι → Type u_4
inst✝³ : Semigroup G₁
inst✝² : Semigroup G₂
inst✝¹ : (i : ι) → Semigroup (G i)
inst✝ : ∀ (i : ι), DecompositionMonoid (G i)
a b c : (i : ι) → G i
h : ∀ (i : ι), a i ∣ (b * c) i
⊢ ∃ a₁ a₂, (∀ (i : ι), a₁ i ∣ b i) ∧ (∀ (i : ι), a₂ i ∣ c i) ∧ a = a₁ * a₂

Tactic:
choose a₁ a₂ h₁ h₂ eq using fun i ↦ DecompositionMonoid.primal _ (h i)

Goal state after:
ι : Type u_1
G₁ : Type u_2
G₂ : Type u_3
G : ι → Type u_4
inst✝³ : Semigroup G₁
inst✝² : Semigroup G₂
inst✝¹ : (i : ι) → Semigroup (G i)
inst✝ : ∀ (i : ι), DecompositionMonoid (G i)
a b c : (i : ι) → G i
h : ∀ (i : ι), a i ∣ (b * c) i
a₁ a₂ : (i : ι) → G i
h₁ : ∀ (i : ι), a₁ i ∣ b i
h₂ : ∀ (i : ι), a₂ i ∣ c i
eq : ∀ (i : ι), a i = a₁ i * a₂ i
⊢ ∃ a₁ a₂, (∀ (i : ι), a₁ i ∣ b i) ∧ (∀ (i : ι), a₂ i ∣ c i) ∧ a = a₁ * a₂
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ ε ^ 2 = 0

Tactic:
by
  simp [pow_two]

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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
⊢ IsNilpotent (LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ⋯)

pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
⊢ MapsTo ⇑(f - (algebraMap R (End R M)) μ₁) ↑((f.genEigenspace μ₁) ↑k) ↑((f.genEigenspace μ₁) ↑k)

pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
⊢ IsNilpotent (LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ?m.275)

Tactic:
· apply isNilpotent_restrict_genEigenspace_nat

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
⊢ MapsTo ⇑(f - (algebraMap R (End R M)) μ₁) ↑((f.genEigenspace μ₁) ↑k) ↑((f.genEigenspace μ₁) ↑k)

R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
⊢ IsNilpotent (LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ?m.275)
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
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
h : Commute f₁ f₂
⊢ (f₁.genEigenspace μ₁) k₁ ⊓ (f₂.genEigenspace μ₂) k₂ ≤ ((f₁ + f₂).genEigenspace (μ₁ + μ₂)) (k₁ + k₂)

Tactic:
intro m hm
  simp only [Submodule.mem_inf, mem_genEigenspace, LinearMap.mem_ker] at hm ⊢
  obtain ⟨⟨l₁, hlk₁, hl₁⟩, ⟨l₂, hlk₂, hl₂⟩⟩ := hm
  use l₁ + l₂
  have : f₁ + f₂ - (μ₁ + μ₂) • 1 = (f₁ - μ₁ • 1) + (f₂ - μ₂ • 1) := by
    rw [add_smul]; exact add_sub_add_comm f₁ f₂ (μ₁ • 1) (μ₂ • 1)
  replace h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1) :=
    (h.sub_right <| Algebra.commute_algebraMap_right μ₂ f₁).sub_left
      (Algebra.commute_algebraMap_left μ₁ _)
  rw [this, h.add_pow', LinearMap.coe_sum, Finset.sum_apply]
  constructor
  · simpa only [Nat.cast_add] using add_le_add hlk₁ hlk₂
  refine Finset.sum_eq_zero fun ⟨i, j⟩ hij ↦ ?_
  suffices (((f₁ - μ₁ • 1) ^ i) * ((f₂ - μ₂ • 1) ^ j)) m = 0 by
    rw [LinearMap.smul_apply, this, smul_zero]
  rw [Finset.mem_antidiagonal] at hij
  obtain hi | hj : l₁ ≤ i ∨ l₂ ≤ j := by lia
  · rw [(h.pow_pow i j).eq, Module.End.mul_apply, Module.End.pow_map_zero_of_le hi hl₁, map_zero]
  · rw [Module.End.mul_apply, Module.End.pow_map_zero_of_le hj hl₂, map_zero]

Goal state after:
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
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ (x⁻¹ ^ n - 1) / (x⁻¹ - 1) = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)

Tactic:
div_eq_iff_mul_eq h₂,

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
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ (x - 1)⁻¹ * (x - x⁻¹ ^ n * x) * (x⁻¹ - 1) = x⁻¹ ^ n - 1
Module: Mathlib.Algebra.Field.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝² : AddCommMonoid α
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Periodic f c
a : γ
x : α
⊢ (fun x ↦ f (a • x)) (x + a⁻¹ • c) = (fun x ↦ f (a • x)) x

Tactic:
by_cases ha : a = 0
  · simp only [ha, zero_smul]
  · simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)

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

Goal state before:
pp: case pos
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2
⊢ Red (hd1 :: tl1) tl2

Tactic:
cases hd1
        cases hd2
        cases h
        dsimp at *
        subst_vars
        apply Red.trans (Red.cons_cons ih)
        exact Red.Step.cons_not_rev.to_red

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hg₂ : Function.MulExact ⇑g₂ ⇑g₃
hi₁ : Function.Surjective ⇑i₁
hi₃ : Function.Surjective ⇑i₃
hi₄ : Function.Injective ⇑i₄
x : N₂
⊢ ∃ a, i₂ a = x

Tactic:
obtain ⟨y, hy⟩ := hi₃ (g₂ x)

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hg₂ : Function.MulExact ⇑g₂ ⇑g₃
hi₁ : Function.Surjective ⇑i₁
hi₃ : Function.Surjective ⇑i₃
hi₄ : Function.Injective ⇑i₄
x : N₂
y : M₃
hy : i₃ y = g₂ x
⊢ ∃ a, i₂ a = x
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : x = y ∧ b = !c
⊢ tail = L2 ++ (x', b') :: (x', !b') :: L3 → p

Tactic:
intro H

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : x = y ∧ b = !c
H : tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ p
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
⊢ (x, b) :: (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3 → p

Tactic:
intro H

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
H : (x, b) :: (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ p
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case neg.cons
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
H : (x, b) :: (y, c) :: tail = a :: L2 ++ (x', b') :: (x', !b') :: L3
⊢ reduce L1 = L2 ++ (x', b') :: (x', !b') :: L3

Tactic:
rw [List.cons_append] at H

Goal state after:
case neg.cons
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
H : (x, b) :: (y, c) :: tail = a :: (L2 ++ (x', b') :: (x', !b') :: L3)
⊢ reduce L1 = L2 ++ (x', b') :: (x', !b') :: L3
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
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ ↑((algebraMap S R) 1) = 1

Tactic:
simp only [map_one, coe_one]

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 = ↑(2 * a.re + c₂ * a.imI)

Tactic:
add_comm,

Goal state after:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ a + star a = ↑(2 * a.re + c₂ * a.imI)
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 = 2 * ↑a.re + ↑c₂ * ↑a.imI

Tactic:
add_comm,

Goal state after:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ a + star a = 2 * ↑a.re + ↑c₂ * ↑a.imI
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
⊢ a = star a ∨ a = 0 ↔ star a = a

Tactic:
eq_comm

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
⊢ star a = a ∨ a = 0 ↔ star a = a
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
hq0 : a ≠ 0
⊢ -a = star a ↔ star a = -a

Tactic:
eq_comm

Goal state after:
case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
hq0 : a ≠ 0
⊢ star a = -a ↔ star a = -a
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
j : ℕ
hP : P.natDegree < P.natDegree + j + 1
⊢ Δ_[1]^[P.natDegree + (j + 1)] (fun x ↦ eval x P) x = 0 x

Tactic:
add_comm,

Goal state after:
R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
j : ℕ
hP : P.natDegree < P.natDegree + j + 1
⊢ Δ_[1]^[j + 1 + P.natDegree] (fun x ↦ eval x P) x = 0 x
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
⊢ (∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2) → x ∈ closure (Set.range f)

Tactic:
rintro ⟨a, rfl⟩

Goal state after:
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
a : ι →₀ ℤ
⊢ (a.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: A : Type u_4
inst✝ : AddGroupWithOne A
a : A
⊢ (∃ x, ↑x = a) ↔ a ∈ zmultiples 1

Tactic:
AddSubgroup.mem_zmultiples_iff,

Goal state after:
A : Type u_4
inst✝ : AddGroupWithOne A
a : A
⊢ (∃ x, ↑x = a) ↔ ∃ k, k • 1 = a
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
⊢ (∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2) → x ∈ closure (Set.range f)

Tactic:
rintro ⟨a, rfl⟩

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
a : ι →₀ ℕ
⊢ (a.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
⊢ τ (a + b) f = τ b (τ a f)

Tactic:
add_comm,

Goal state after:
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
⊢ τ (b + a) f = τ b (τ a f)
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a : G
f : G → α
⊢ τ a f = DomAddAct.mk (-a) +ᵥ f

Tactic:
ext; simp [DomAddAct.vadd_apply, sub_eq_neg_add]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
⊢ closure (v '' IsMulIndecomposable.baseOf v f) = closure (v '' {i | 1 < f (v i)})

Tactic:
refine le_antisymm (closure_mono (image_mono <| IsMulIndecomposable.baseOf_subset_one_lt v f))
    (closure_le.mpr ?_)

Goal state after:
ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
⊢ v '' {i | 1 < f (v i)} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f))
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
r₁ s₁ r₂ s₂ : A
hr₁ : f r₁ ≠ 0
hs₁ : f s₁ ≠ 0
hr₂ : f r₂ ≠ 0
hs₂ : f s₂ ≠ 0
⊢ Units.mk0 (f s₁) hs₁ * Units.mk0 (f r₂) hr₂ = Units.mk0 (f s₂) hs₂ * Units.mk0 (f r₁) hr₁ ↔ f r₁ * f s₂ = f r₂ * f s₁

Tactic:
eq_comm

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
r₁ s₁ r₂ s₂ : A
hr₁ : f r₁ ≠ 0
hs₁ : f s₁ ≠ 0
hr₂ : f r₂ ≠ 0
hs₂ : f s₂ ≠ 0
⊢ Units.mk0 (f s₂) hs₂ * Units.mk0 (f r₁) hr₁ = Units.mk0 (f s₁) hs₁ * Units.mk0 (f r₂) hr₂ ↔ f r₁ * f s₂ = f r₂ * f s₁
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → IsIdempotentComplete C

Tactic:
intro h
    refine ⟨?_⟩
    intro X p hp
    have : HasEqualizer (𝟙 X) p := h X p hp
    refine ⟨equalizer (𝟙 X) p, equalizer.ι (𝟙 X) p,
      equalizer.lift p (show p ≫ 𝟙 X = p ≫ p by rw [hp, comp_id]), ?_, equalizer.lift_ι _ _⟩
    ext
    simp only [assoc, limit.lift_π,
      Fork.ofι_π_app, id_comp]
    rw [← equalizer.condition, comp_id]

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

Goal state before:
pp: n : SimplexCategory
f : n ⟶ ⦋0⦌
⊢ f = n.const ⦋0⦌ 0

Tactic:
ext : 3
  apply @Subsingleton.elim (Fin 1)

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

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ ∃ i e, i ≫ e = 𝟙 { X := P.X, p := p.f, idem := hp } ∧ e ≫ i = p

Tactic:
use ⟨p.f, by rw [comp_p p, hp]⟩

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ ∃ e, { f := p.f, comm := ⋯ } ≫ e = 𝟙 { X := P.X, p := p.f, idem := hp } ∧ e ≫ { f := p.f, comm := ⋯ } = p
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case cast.succ.inl
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ j.predAbove (k.succ.castSucc.pred ⋯) = i.predAbove (j.succ.predAbove k.succ.castSucc)

Tactic:
← Fin.succ_castSucc,

Goal state after:
case cast.succ.inl
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ j.predAbove (k.castSucc.succ.pred ⋯) = i.predAbove (j.succ.predAbove k.castSucc.succ)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case cast.succ.inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
⊢ j.predAbove k.succ = i.predAbove (j.succ.predAbove k.succ.castSucc)

Tactic:
← Fin.succ_castSucc,

Goal state after:
case cast.succ.inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
⊢ j.predAbove k.succ = i.predAbove (j.succ.predAbove k.castSucc.succ)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝³ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst✝² : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
inst✝¹ :
  ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C),
    (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F
inst✝ :
  ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F
⊢ (Truncated.cosk n).FullyFaithful

Tactic:
by
  apply Adjunction.fullyFaithfulROfIsIsoCounit (coskAdj n)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X _⦋0⦌ ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
i j : SimplexCategoryᵒᵖ
g : i ⟶ j
⊢ X.map g ≫ X.map (⦋0⦌.const (unop j) 0).op ≫ f = (X.map (⦋0⦌.const (unop i) 0).op ≫ f) ≫ 𝟙 X₀

Tactic:
← g.op_unop

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X _⦋0⦌ ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
i j : SimplexCategoryᵒᵖ
g : i ⟶ j
⊢ X.map g.unop.op ≫ X.map (⦋0⦌.const (unop j) 0).op ≫ f = (X.map (⦋0⦌.const (unop i) 0).op ≫ f) ≫ 𝟙 X₀
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : SimplexCategory
f : n ⟶ n
hf : Function.Surjective ⇑(Hom.toOrderHom f)
h : n.len = n.len
⊢ Function.Injective (Hom.toOrderHom f).toFun

Tactic:
rwa [Finite.injective_iff_surjective]

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

Goal state before:
pp: X Y : SSet
A : Y.Subcomplex
f : X ⟶ Y
inst✝ : IsIso f
⊢ A.image (inv f) = A.preimage f

Tactic:
by
  simp [← preimage_inv]

Goal state after: