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

Goal state before:
pp: case nil
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a : γ
⊢ (join (((a, nil), S), SS)).join = join (join ((a, nil), S), Seq.map join SS)

Tactic:
| nil =>

Goal state after:
case nil
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a : γ
⊢ (join (((a, nil), S), SS)).join = join (join ((a, nil), S), Seq.map join SS)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil.nil
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
⊢ (join (((a, nil), nil), SS)).join = join (join ((a, nil), nil), Seq.map join SS)

Tactic:
| nil =>

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

Goal state before:
pp: case cons.nil
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a x : γ
s_1 : Seq γ
⊢ (join (((a, Seq.cons x s_1), nil), SS)).join = join (join ((a, Seq.cons x s_1), nil), Seq.map join SS)

Tactic:
| nil =>

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

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

Tactic:
IH

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
⊢ ∃ conts, (of v).contsAux n = Pair.map Rat.cast conts
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case some.succ
K : Type u_1
inst✝ : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    s.get? (m + 1) = some gp_succ_n → convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = some gp_succ_n
⊢ convs'Aux s (m + 1 + 2) = convs'Aux (squashSeq s (m + 1)) (m + 1 + 1)

Tactic:
obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
        s.ge_stable (m + 2).zero_le s_succ_nth_eq

Goal state after:
case some.succ
K : Type u_1
inst✝ : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    s.get? (m + 1) = some gp_succ_n → convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ convs'Aux s (m + 1 + 2) = convs'Aux (squashSeq s (m + 1)) (m + 1 + 1)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
m : ℕ
⊢ (∀ m_1 < m, m_1 ≤ n → g.contsAux m_1 = (g.squashGCF n).contsAux m_1) →
    m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m

Tactic:
IH

Goal state after:
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
m : ℕ
IH : ∀ m_1 < m, m_1 ≤ n → g.contsAux m_1 = (g.squashGCF n).contsAux m_1
⊢ m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m
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
n : ℕ
⊢ (∀ m < n, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b) →
    n ≤ 1 ∨ ¬(of v).TerminatedAt (n - 2) → ↑(fib n) ≤ ((of v).contsAux n).b

Tactic:
IH

Goal state after:
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
⊢ n ≤ 1 ∨ ¬(of v).TerminatedAt (n - 2) → ↑(fib n) ≤ ((of v).contsAux n).b
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case none.some
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
j : I
ne : none ≠ some j
⊢ none.elim x e * (some j).elim x e = 0

pp: case some.none
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
i : I
ne : some i ≠ none
⊢ (some i).elim x e * none.elim x e = 0

pp: case some.some
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
i j : I
ne : some i ≠ some j
⊢ (some i).elim x e * (some j).elim x e = 0

Tactic:
· simpa only [mul_assoc, Finset.sum_mul, he.mul_eq, Finset.sum_ite_eq', Finset.mem_univ,
        ↓reduceIte, zero_mul] using! congr_arg (· * e j) hx₁

Goal state after:
case some.none
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
i : I
ne : some i ≠ none
⊢ (some i).elim x e * none.elim x e = 0

case some.some
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
i j : I
ne : some i ≠ some j
⊢ (some i).elim x e * (some j).elim x e = 0
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: case nil
ι : Type u_1
M : Type u_2
inst✝ : MulOneClass M
c : Con M
f g : ι → M
h : ∀ x ∈ [], c (f x) (g x)
⊢ c (List.map f []).prod (List.map g []).prod

Tactic:
| nil =>

Goal state after:
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 : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i, single i q (if i = q then 1 - z else M i p * x * z)
⊢ ∃ z, z * M * single p q x + z - 1 ∈ matrix n I

Tactic:
use N

Goal state after:
case h
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := ⋯
⊢ N * M * single p q x + N - 1 ∈ matrix n 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
⊢ ((f - μ • 1) ^ 1).ker = (f - μ • 1).ker

Tactic:
pow_one

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ LinearMap.ker (f - μ • 1) = (f - μ • 1).ker
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
k : ℕ∞
x : M
h : f.HasUnifEigenvector μ k x
⊢ f.HasUnifEigenvalue μ k

Tactic:
rw [HasUnifEigenvalue, Submodule.ne_bot_iff]

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
h : f.HasUnifEigenvector μ k x
⊢ ∃ x ∈ (f.genEigenspace μ) k, x ≠ 0
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
h : f.HasUnifEigenvalue μ 1
n : ℕ
⊢ (f ^ n).HasUnifEigenvalue (μ ^ n) 1

Tactic:
rw [HasUnifEigenvalue, Submodule.ne_bot_iff]

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
h : f.HasUnifEigenvalue μ 1
n : ℕ
⊢ ∃ x ∈ ((f ^ n).genEigenspace (μ ^ n)) 1, x ≠ 0
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✝ : IsNoetherian R M
f : End R M
μ : R
k : ℕ∞
⊢ (f.genEigenspace μ) k ≤ (f.genEigenspace μ) ⊤

Tactic:
exact (f.genEigenspace μ).monotone le_top

Goal state after:
Module: Mathlib.Algebra.Ring.MinimalAxioms

Goal state before:
pp: R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
a : R
⊢ 0 * a = 0

Tactic:
have : 0 * a = 0 * a + 0 * a :=
      calc 0 * a = (0 + 0) * a := by rw [zero_add]
      _ = 0 * a + 0 * a := by rw [right_distrib]

Goal state after:
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this✝ : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
a : R
this : 0 * a = 0 * a + 0 * a
⊢ 0 * a = 0
Module: Mathlib.Algebra.Field.NegOnePow

Goal state before:
pp: case inr
K : Type u_1
inst✝ : DivisionRing K
k : ℤ
⊢ ↑↑(2 * k + 1).negOnePow = ((-1) ^ 2) ^ k * -1

Tactic:
zpow_ofNat

Goal state after:
case inr
K : Type u_1
inst✝ : DivisionRing K
k : ℤ
⊢ ↑↑(2 * k + 1).negOnePow = ((-1) ^ 2) ^ k * -1
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case nil
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
⊢ Red [] (reduce [])

Tactic:
| nil =>

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

Goal state before:
pp: case cons.nil
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
htl : reduce tl1 = []
ih : Red tl1 []
⊢ Red (hd1 :: tl1)
    (List.rec [hd1] (fun head tail tail_ih ↦ if hd1.1 = head.1 ∧ hd1.2 = !head.2 then tail else hd1 :: head :: tail) [])

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
r : reduce L1 = []
⊢ List.rec [(x, b)] (fun head tail tail_ih ↦ if x = head.1 ∧ b = !head.2 then tail else (x, b) :: head :: tail) [] =
      L2 ++ (x', b') :: (x', !b') :: L3 →
    p

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ (x * y).toWord = reduce (x.toWord ++ y.toWord)

Tactic:
← mk_toWord (x := x),

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ (mk x.toWord * y).toWord = reduce ((mk x.toWord).toWord ++ y.toWord)
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:
rw [map_mul, FreeSemigroup.length_mul, hx, hy]; rfl

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case inr
α : Type u
inst✝ : Nonempty α
hR : Infinite α
⊢ Nonempty (CommRing α)

Tactic:
have ⟨e⟩ : Nonempty (α ≃ FreeCommRing α) := by simp [← Cardinal.eq]
    exact ⟨e.commRing⟩

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ (countP p) (of x) = if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0

Tactic:
rw [countP_apply, toList_of, List.countP_singleton, apply_ite (Multiplicative.ofAdd)]
  simp only [decide_eq_true_eq]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
B : Type u_3
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ⇑f
inj : Function.Injective ⇑(algebraMap R B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ y, (algebraMap R B) y = x
x✝ : A
hx : IsIntegral R x✝
⊢ ∃ y, (algebraMap R A) y = x✝

Tactic:
obtain ⟨y, fx_eq⟩ := cl.mp ((isIntegral_algHom_iff f hf).mpr hx)
    aesop

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
B : Type u_3
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ⇑f
inj : Function.Injective ⇑(algebraMap R B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ y, (algebraMap R B) y = x
x✝ : A
hx : IsIntegral R x✝
⊢ ∃ y, (algebraMap R A) y = x✝

pp: case refine_3
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
B : Type u_3
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ⇑f
inj : Function.Injective ⇑(algebraMap R B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ y, (algebraMap R B) y = x
x✝ : A
⊢ (∃ y, (algebraMap R A) y = x✝) → IsIntegral R x✝

Tactic:
· obtain ⟨y, fx_eq⟩ := cl.mp ((isIntegral_algHom_iff f hf).mpr hx)
    aesop

Goal state after:
case refine_3
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
B : Type u_3
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ⇑f
inj : Function.Injective ⇑(algebraMap R B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ y, (algebraMap R B) y = x
x✝ : A
⊢ (∃ y, (algebraMap R A) y = x✝) → IsIntegral R x✝
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case refine_2.refine_2
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : CommRing U
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra S T
inst✝⁶ : Algebra R U
inst✝⁵ : Algebra S U
inst✝⁴ : Algebra T U
inst✝³ : IsScalarTower S T U
inst✝² : IsScalarTower R T U
inst✝¹ : IsIntegralClosure S R T
inst✝ : IsIntegrallyClosedIn T U
x : S
⊢ IsIntegral R ((algebraMap S U) x)

Tactic:
IsScalarTower.algebraMap_apply S T U

Goal state after:
case refine_2.refine_2
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : CommRing U
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra S T
inst✝⁶ : Algebra R U
inst✝⁵ : Algebra S U
inst✝⁴ : Algebra T U
inst✝³ : IsScalarTower S T U
inst✝² : IsScalarTower R T U
inst✝¹ : IsIntegralClosure S R T
inst✝ : IsIntegrallyClosedIn T U
x : S
⊢ IsIntegral R ((algebraMap T U) ((algebraMap S T) x))
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 := ⋯
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 : ℕ × ℕ
⊢ s.coeff x.2 ∈ P

Tactic:
rw [mem_ker, ← coeff_map, hs, coeff_zero]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq γ
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
b : β
s : Finset γ
⊢ (a • b) • s = a • b • s

Tactic:
by simp only [← image_smul, image_image, smul_assoc, Function.comp_def]

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

Goal state before:
pp: case one
M : Type u_1
inst✝² : Monoid M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
⊢ x = x ^ 1

Tactic:
pow_one

Goal state after:
case one
M : Type u_1
inst✝² : Monoid M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
⊢ x = x
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: C : Type u_1
inst✝ : CommGroup C
x y z : Subgroup C
xz : x ≤ z
a : C
ha : a ∈ x ⊔ y ∧ a ∈ z
⊢ a ∈ x ⊔ y ⊓ z

Tactic:
mem_sup

Goal state after:
C : Type u_1
inst✝ : CommGroup C
x y z : Subgroup C
xz : x ≤ z
a : C
ha : (∃ y_1 ∈ x, ∃ z ∈ y, y_1 * z = a) ∧ a ∈ z
⊢ a ∈ x ⊔ y ⊓ z
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: C : Type u_1
inst✝ : CommGroup C
x y z : Subgroup C
xz : x ≤ z
b : C
hb : b ∈ x
c : C
hc : c ∈ y
haz : b * c ∈ z
⊢ b * c ∈ x ⊔ y ⊓ z

Tactic:
mem_sup

Goal state after:
C : Type u_1
inst✝ : CommGroup C
x y z : Subgroup C
xz : x ≤ z
b : C
hb : b ∈ x
c : C
hc : c ∈ y
haz : b * c ∈ z
⊢ ∃ y_1 ∈ x, ∃ z_1 ∈ y ⊓ z, y_1 * z_1 = b * c
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
simp only [Functor.id_obj] at φ

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : i < k
hjk : j.castSucc < k
⊢ k.succ.pred ⋯ = i.succAbove (k.pred ⋯)

Tactic:
Fin.pred_succ,

Goal state after:
case inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : i < k
hjk : j.castSucc < k
⊢ k = i.succAbove (k.pred ⋯)
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.castSucc.succ.pred ⋯) = i.predAbove (j.succ.predAbove k.castSucc.succ)

Tactic:
Fin.pred_succ,

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 = 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.predAbove k.castSucc).succ

Tactic:
rw [Fin.predAbove_of_le_castSucc _ k.castSucc
        (Fin.castSucc_le_castSucc_iff.mpr (h.le.trans H)),
        Fin.castPred_castSucc, Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr (H.trans_lt' h)), Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr h)]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
n✝ : ℕ
j : Fin (n✝ + 1)
⊢ F.map (H.h j.succ) ≫ (((whiskering C D).obj F).obj Y).δ j.castSucc.succ =
    F.map (H.h j.castSucc) ≫ (((whiskering C D).obj F).obj Y).δ j.castSucc.succ

Tactic:
simpa [SimplicialObject.δ] using!
      congrArg (fun k => F.map k) (H.h_succ_comp_δ_castSucc_succ j)

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

Goal state before:
pp: case h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
x : Fin (Δ.len + 1)
⊢ ∀ (j : Fin (n + 2)), j ≠ i → i.succAbove (((Fin.last n).predAbove i).predAbove j) = j

Tactic:
intro j hj

Goal state after:
case h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
x : Fin (Δ.len + 1)
j : Fin (n + 2)
hj : j ≠ i
⊢ i.succAbove (((Fin.last n).predAbove i).predAbove j) = j
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j m : ℕ
i' : Fin (m + 2)
h : m + j = n
hi' : j < ↑i
hi'' : ↑i = ↑i' + j
⊢ δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'

Tactic:
induction j generalizing n m with
  | zero =>
    obtain rfl : n = m := by lia
    obtain rfl : i = i' := by lia
    simp
  | succ j hj =>
    rw [σ₀Iter_succ _, σ₀Iter_succ_assoc _,
      reassoc_of% hj _ i'.succ (by lia) (by lia) (by grind),
      dsimp% δ_comp_σ_of_gt (i := i') (j := 0)
        (by rw [Fin.lt_def]; dsimp; lia)]

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

Goal state before:
pp: X : SSet
s : X.S
⊢ ∃ (h : s.dim = s.dim), (s.cast h).simplex = s.simplex

Tactic:
exact ⟨rfl, rfl⟩

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
S : X.Subcomplex
⊢ ∀ ⦃b : X.Subcomplex⦄, S ≤ b → (fun S ↦ S.image f) S ≤ (fun S ↦ S.image f) b

Tactic:
T

Goal state after:
X Y : SSet
f : X ⟶ Y
S T : X.Subcomplex
⊢ S ≤ T → (fun S ↦ S.image f) S ≤ (fun S ↦ S.image f) T
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: case pos
X : SSet
inst✝ : X.Finite
this : Fintype X.N
φ : X.N → ℕ := fun x ↦ x.dim
h : (Finset.image φ ⊤).Nonempty
⊢ ∃ d, ∀ s ∈ Finset.image φ ⊤, s < d

pp: case neg
X : SSet
inst✝ : X.Finite
this : Fintype X.N
φ : X.N → ℕ := fun x ↦ x.dim
h : ¬(Finset.image φ ⊤).Nonempty
⊢ ∃ d, ∀ s ∈ Finset.image φ ⊤, s < d

Tactic:
· obtain ⟨d, hd⟩ := Finset.max_of_nonempty h
      exact ⟨d + 1, fun _ _ ↦ by grind [WithBot.coe_le_coe, → Finset.le_max]⟩

Goal state after:
case neg
X : SSet
inst✝ : X.Finite
this : Fintype X.N
φ : X.N → ℕ := fun x ↦ x.dim
h : ¬(Finset.image φ ⊤).Nonempty
⊢ ∃ d, ∀ s ∈ Finset.image φ ⊤, s < d
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate

Goal state before:
pp: case pos
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin (n + 1)
h₁ : i.castSucc < j.succ
⊢ s.obj (i.castSucc.succAbove (j.succ.pred ⋯)) = s.obj j.succ

Tactic:
Fin.pred_succ,

Goal state after:
case pos
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin (n + 1)
h₁ : i.castSucc < j.succ
⊢ s.obj (i.castSucc.succAbove j) = s.obj j.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate

Goal state before:
pp: case pos
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin (n + 1)
h₁ : i.castSucc < j.succ
⊢ s.obj (i.castSucc.succAbove j) = s.obj j.succ

Tactic:
Fin.succAbove_of_le_castSucc _ _ (Fin.le_castSucc_iff.2 h₁)

Goal state after:
case pos
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin (n + 1)
h₁ : i.castSucc < j.succ
⊢ s.obj j.succ = s.obj j.succ
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i j : ℕ
w : ¬(ComplexShape.up ℕ).Rel i j
⊢ C.d (i + 1) (j + 1) = 0

Tactic:
by
        apply C.shape
        simpa

Goal state after: