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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_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
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
⊢ pA * (g.contsAux (n + 2)).b - pB * (g.contsAux (n + 2)).a = (ppA * pB - ppB * pA) * -gp.a

Tactic:
contsAux_recurrence s_nth_eq ppred_conts_eq pred_conts_eq

Goal state after:
K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_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
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
⊢ pA *
        { a := gp.b * (g.contsAux (n + 1)).a + gp.a * (g.contsAux n).a,
            b := gp.b * (g.contsAux (n + 1)).b + gp.a * (g.contsAux n).b }.b -
      pB *
        { a := gp.b * (g.contsAux (n + 1)).a + gp.a * (g.contsAux n).a,
            b := gp.b * (g.contsAux (n + 1)).b + gp.a * (g.contsAux n).b }.a =
    (ppA * pB - ppB * pA) * -gp.a
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
o : Option α
om : o ∈ g
oe : Option.map f o = some b
⊢ ∃ a ∈ ⟨g, al⟩, f a = b

Tactic:
rcases o with - | a

Goal state after:
case none
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
om : none ∈ g
oe : Option.map f none = some b
⊢ ∃ a ∈ ⟨g, al⟩, f a = b

case some
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
a : α
om : some a ∈ g
oe : Option.map f (some a) = some b
⊢ ∃ a ∈ ⟨g, al⟩, f a = b
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim
α : Type u
S T : Seq (Seq1 α)
⊢ IsBisimulation fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)

Tactic:
rintro s1 s2 ⟨s, S, T, rfl, rfl⟩
    cases s with
    | nil =>
      cases S with
      | nil =>
        cases T with
        | nil => simp
        | cons s T =>
          obtain ⟨a, s⟩ := s
          simpa using ⟨s, nil, T, by simp, by simp⟩
      | cons s S =>
        obtain ⟨a, s⟩ := s
        simpa using ⟨s, S, T, rfl, rfl⟩
    | cons _ s => simpa using ⟨s, S, T, rfl, rfl⟩

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : α
s : Seq α
x' : β
s' : Seq β
n : ℕ
⊢ (zipWith f (cons x s) (cons x' s')).get? n = (cons (f x x') (zipWith f s s')).get? n

Tactic:
cases n

Goal state after:
case zero
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : α
s : Seq α
x' : β
s' : Seq β
⊢ (zipWith f (cons x s) (cons x' s')).get? 0 = (cons (f x x') (zipWith f s s')).get? 0

case succ
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : α
s : Seq α
x' : β
s' : Seq β
n✝ : ℕ
⊢ (zipWith f (cons x s) (cons x' s')).get? (n✝ + 1) = (cons (f x x') (zipWith f s s')).get? (n✝ + 1)
Module: Mathlib.Data.Seq.Basic

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

Tactic:
cases n

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

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)
Module: Mathlib.Data.Seq.Basic

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

Tactic:
cases n

Goal state after:
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

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)
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ fib n ≤ fib (n + 1)

Tactic:
cases n

Goal state after:
case zero
⊢ fib 0 ≤ fib (0 + 1)

case succ
n✝ : ℕ
⊢ fib (n✝ + 1) ≤ fib (n✝ + 1 + 1)
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ fib (2 * n) = fib n * (2 * fib (n + 1) - fib n)

Tactic:
cases n

Goal state after:
case zero
⊢ fib (2 * 0) = fib 0 * (2 * fib (0 + 1) - fib 0)

case succ
n✝ : ℕ
⊢ fib (2 * (n✝ + 1)) = fib (n✝ + 1) * (2 * fib (n✝ + 1 + 1) - fib (n✝ + 1))
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
⊢ P.toPoly.natDegree ≤ 2

Tactic:
simpa only [of_a_eq_zero ha] using natDegree_quadratic_le

Goal state after:
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
I : Type u_3
e : I → R
inst✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents (⇑f ∘ e)
e' : I → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = ⇑f ∘ e
⊢ e = e'

Tactic:
ext i
    refine eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute
      (he _) (h₁.idem _) (h _ ?_) ((he' i).comm _)
    simpa [RingHom.mem_ker, sub_eq_zero] using congr_fun h₂.symm i

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
f : End R M
μ : R
h : f.HasUnifEigenvalue μ 1
n : ℕ
m : M
hm : f.HasUnifEigenvector μ 1 m
⊢ ∃ x ∈ ((f ^ n).genEigenspace (μ ^ n)) 1, x ≠ 0

Tactic:
exact ⟨m, by simpa [mem_genEigenspace_one] using hm.pow_apply n, hm.2⟩

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_1
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
⊢ Pairwise fun x1 x2 ↦ Option.rec e₀ ((1 - e₀) • e') x1 * Option.rec e₀ ((1 - e₀) • e') x2 = 0

Tactic:
rintro (_|i) (_|j) h
    · simp at h
    · dsimp; linear_combination - he₀.eq * e' j
    · dsimp; linear_combination - he₀.eq * e' i
    · 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.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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
⊢ p ⊓ (f.genEigenspace μ) k = Submodule.map p.subtype ((genEigenspace (LinearMap.restrict f hfp) μ) k)

Tactic:
f.genEigenspace_restrict _ _ _ hfp,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
⊢ p ⊓ (f.genEigenspace μ) k = Submodule.map p.subtype (Submodule.comap p.subtype ((f.genEigenspace μ) k))
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h :
  Submodule.comap ((f - μ • 1) ^ finrank K V) ((f.genEigenspace μ) ↑(finrank K V)) = (f.genEigenspace μ) ↑(finrank K V)
⊢ f.genEigenrange μ ↑(finrank K V) ⊓ (f.genEigenspace μ) ↑(finrank K V) ≤ ⊥

Tactic:
genEigenrange_nat,

Goal state after:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h :
  Submodule.comap ((f - μ • 1) ^ finrank K V) ((f.genEigenspace μ) ↑(finrank K V)) = (f.genEigenspace μ) ↑(finrank K V)
⊢ ((f - μ • 1) ^ finrank K V).range ⊓ (f.genEigenspace μ) ↑(finrank K V) ≤ ⊥
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
L : Type u_1
F : Type u_2
inst✝² : SMul R L
inst✝¹ : FunLike F L (End R M)
inst✝ : MulActionHomClass F R L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
t : R
x : L
⊢ μ (t • x) = t • μ x

Tactic:
by
  by_contra contra
  let g : L → Submodule R M := fun x ↦ (f x).genEigenspace (μ x) k
  have : ⨅ x, g x ≤ g x ⊓ g (t • x) := le_inf_iff.mpr ⟨iInf_le g x, iInf_le g (t • x)⟩
  refine h_ne <| eq_bot_iff.mpr (le_trans this (disjoint_iff_inf_le.mp ?_))
  apply Disjoint.mono_left (genEigenspace_le_smul (f x) (μ x) t k)
  simp only [g, map_smul]
  exact disjoint_genEigenspace (t • f x) (Ne.symm contra) k k

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
f : End R M
μ ρ : R
⊢ (f - ρ • LinearMap.id).HasEigenvalue μ ↔ f.HasEigenvalue (μ + ρ)

Tactic:
by
  rw [sub_eq_add_neg, ← neg_smul, hasEigenvalue_add_iff, sub_neg_eq_add]

Goal state after:
Module: Mathlib.Algebra.Field.GeomSum

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x : K
h : x ≠ 1
n : ℕ
this : x - 1 ≠ 0
⊢ ∑ i ∈ range n, x ^ i = (x ^ n - 1) / (x - 1)

Tactic:
rw [← geom_sum_mul, mul_div_cancel_right₀ _ this]

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

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

Tactic:
cases r : reduce L1 with

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

Goal state before:
pp: A : Type u_2
inst✝³ : CommRing A
C : Type u_5
inst✝² : SetLike C A
inst✝¹ : SubringClass C A
S : C
T : Subring A
inst✝ : IsIntegrallyClosedIn (↥T) A
⊢ (integralClosure (↥S) A).toSubring ≤ T ↔ ofClass S ≤ T

Tactic:
by
  rw [integralClosure_le_iff, Subtype.forall, SetLike.le_def]; rfl

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

Goal state before:
pp: 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 : ℕ × ℕ
⊢ r.coeff x.1 * s.coeff x.2 ∈ P * P

Tactic:
apply mul_mem_mul

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 := ⋯
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 : ℕ × ℕ
⊢ r.coeff x.1 ∈ P

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
Module: Mathlib.Algebra.Group.Action.Equidecomp

Goal state before:
pp: X : Type u_1
G : Type u_2
A B C : Set X
inst✝¹ : Group G
inst✝ : MulAction G X
f : Equidecomp X G
⊢ f.symm.source = f.target

Tactic:
symm_source

Goal state after:
X : Type u_1
G : Type u_2
A B C : Set X
inst✝¹ : Group G
inst✝ : MulAction G X
f : Equidecomp X G
⊢ f.target = f.target
Module: Mathlib.Algebra.Group.Action.Sum

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
m : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
x : α ⊕ β
⊢ 1 • x = x

Tactic:
cases x
    exacts [congr_arg inl (one_smul _ _), congr_arg inr (one_smul _ _)]

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

Goal state before:
pp: case succ
M : Type u_3
R : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Ring R
φ : AddChar M R
h : M
n : ℕ
IH : ∀ (x : M), Δ_[h]^[n] (⇑φ) x = (φ h - 1) ^ n * φ x
x : M
⊢ (φ h - 1) ^ n * (φ (x + h) - φ x) = (φ h - 1) ^ n * (φ (h + x) - 1 * φ x)

Tactic:
add_comm h x,

Goal state after:
case succ
M : Type u_3
R : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Ring R
φ : AddChar M R
h : M
n : ℕ
IH : ∀ (x : M), Δ_[h]^[n] (⇑φ) x = (φ h - 1) ^ n * φ x
x : M
⊢ (φ h - 1) ^ n * (φ (x + h) - φ x) = (φ h - 1) ^ n * (φ (x + h) - 1 * φ x)
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: case inl
M : Type u_2
inst✝¹ : Mul M
s t : Set M
inst✝ : IsCancelMul M
h : (s * t).Infinite
⊢ Nat.card ↑(s * t) ≤ Nat.card ↑s * Nat.card ↑t

Tactic:
simp [Set.Infinite.card_eq_zero h]

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

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

Tactic:
obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_lt hP
  rw [add_assoc, add_comm, Function.iterate_add_apply, Function.iterate_succ_apply,
    P.fwdDiff_iter_degree_eq_factorial, Pi.smul_def]
  simp [fwdDiff_iter_eq_sum_shift]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommGroup M
x : M
s : Set M
inst✝ : Fintype ↑s
| x ∈ closure s

Tactic:
rw [← Subtype.range_coe (s := s)]

Goal state after:
M : Type u_1
inst✝¹ : CommGroup M
x : M
s : Set M
inst✝ : Fintype ↑s
| x ∈ closure (Set.range Subtype.val)
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
x : M
s : Set M
inst✝ : Fintype ↑s
| x ∈ closure s

Tactic:
rw [← Subtype.range_coe (s := s)]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
x : M
s : Set M
inst✝ : Fintype ↑s
| x ∈ closure (Set.range Subtype.val)
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 (invMonoidHom.comp (invMonoidHom.comp f)) ⊆
    ⇑invMonoidHom '' ⇑invMonoidHom ∘ v '' baseOf v (invMonoidHom.comp f)
⊢ ⇑invMonoidHom ∘ v '' baseOf v f ⊆ v '' baseOf v (invMonoidHom.comp f)

Tactic:
rw [← MonoidHom.comp_assoc, invMonoidHom_comp_invMonoidHom, MonoidHom.id_comp, image_comp,
      ← image_comp invMonoidHom invMonoidHom, ← MonoidHom.coe_comp, invMonoidHom_comp_invMonoidHom,
      ← image_comp] at this

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✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
s : Set ι
hst : s ⊆ {j | IsMulIndecomposable v {i | 1 < f (v i)} j}
i : ι
hf : v i = 1
⊢ ∃ i, f (v i) = 1

Tactic:
exact ⟨i, by simp [hf]⟩

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

Goal state before:
pp: case refine_2.a
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
x✝ : ∃ a, ¬f a = 0 ∧ ∃ x, f a * ↑y = f x
a : A
ha : f a ≠ 0
x : A
hv : f x ≠ 0
v : Bˣ := ⋯
hv₀ : f x = ↑v
u : Bˣ := ⋯
ha₀ : f a = ↑u
hy : u⁻¹ * v = y
⊢ u⁻¹ ∈ f.valueGroup

Tactic:
apply inv_mem_valueGroup

Goal state after:
case refine_2.a
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
x✝ : ∃ a, ¬f a = 0 ∧ ∃ x, f a * ↑y = f x
a : A
ha : f a ≠ 0
x : A
hv : f x ≠ 0
v : Bˣ := ⋯
hv₀ : f x = ↑v
u : Bˣ := ⋯
ha₀ : f a = ↑u
hy : u⁻¹ * v = y
⊢ ↑u ∈ range ⇑f
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case a
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
x✝ : ∃ a, ¬f a = 0 ∧ ∃ x, f a * ↑y = f x
a : A
ha : f a ≠ 0
x : A
hv : f x ≠ 0
v : Bˣ := ⋯
hv₀ : f x = ↑v
u : Bˣ := ⋯
ha₀ : f a = ↑u
hy : u⁻¹ * v = y
⊢ v ∈ f.valueGroup

Tactic:
apply mem_valueGroup

Goal state after:
case a
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
x✝ : ∃ a, ¬f a = 0 ∧ ∃ x, f a * ↑y = f x
a : A
ha : f a ≠ 0
x : A
hv : f x ≠ 0
v : Bˣ := ⋯
hv₀ : f x = ↑v
u : Bˣ := ⋯
ha₀ : f a = ↑u
hy : u⁻¹ * v = y
⊢ ↑v ∈ range ⇑f
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: n : ℕ
⊢ Fintype.card (ULift.{u_1, 0} (Fin n)) = Fintype.card (Fin n)

Tactic:
convert! (Fintype.ofEquiv_card Equiv.ulift).symm

Goal state after:
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n : ℕ
⊢ (objX Y n).Factors ((objX X n).arrow ≫ f.app (op ⦋n⦌))

Tactic:
cases n

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
⊢ (objX Y 0).Factors ((objX X 0).arrow ≫ f.app (op ⦋0⦌))

case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
⊢ (objX Y (n✝ + 1)).Factors ((objX X (n✝ + 1)).arrow ≫ f.app (op ⦋n✝ + 1⦌))
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n : ℕ
⊢ (objX Y (n + 1)).factorThru ((objX X (n + 1)).arrow ≫ f.app (op ⦋n + 1⦌)) ⋯ ≫ (obj Y).d (n + 1) n =
    (obj X).d (n + 1) n ≫ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯

Tactic:
cases n

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
⊢ (objX Y (0 + 1)).factorThru ((objX X (0 + 1)).arrow ≫ f.app (op ⦋0 + 1⦌)) ⋯ ≫ (obj Y).d (0 + 1) 0 =
    (obj X).d (0 + 1) 0 ≫ (objX Y 0).factorThru ((objX X 0).arrow ≫ f.app (op ⦋0⦌)) ⋯

case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
⊢ (objX Y (n✝ + 1 + 1)).factorThru ((objX X (n✝ + 1 + 1)).arrow ≫ f.app (op ⦋n✝ + 1 + 1⦌)) ⋯ ≫
      (obj Y).d (n✝ + 1 + 1) (n✝ + 1) =
    (obj X).d (n✝ + 1 + 1) (n✝ + 1) ≫ (objX Y (n✝ + 1)).factorThru ((objX X (n✝ + 1)).arrow ≫ f.app (op ⦋n✝ + 1⦌)) ⋯
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : j = i.castSucc
⊢ δ i ≫ δ j = δ i ≫ δ i.succ

Tactic:
subst H
  rw [δ_comp_δ_self]

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

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

Tactic:
subst H
  rw [δ_comp_δ_self]

Goal state after:
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 = i.predAbove (j.predAbove k.castSucc).succ

Tactic:
Fin.predAbove_of_castSucc_lt i _ (Fin.castSucc_lt_succ_iff.mpr _),

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 = (j.predAbove k.castSucc).succ.pred ⋯

n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ i ≤ j.predAbove k.castSucc
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ mkOfSucc i ≫ δ j = mkOfSucc i.succ

Tactic:
ext x
  simp only [δ, len_mk, mkHom, comp_toOrderHom, Hom.toOrderHom_mk, OrderHom.comp_coe,
    OrderEmbedding.toOrderHom_coe, Function.comp_apply, Fin.succAboveOrderEmb_apply]
  fin_cases x <;> rw [Fin.succAbove_of_le_castSucc]
  · rfl
  · exact Nat.le_of_lt_succ h
  · rfl
  · exact Nat.le_of_lt h

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

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

Tactic:
subst H
  rw [δ_comp_δ_self]

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

Goal state before:
pp: X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
⊢ X = Y

Tactic:
suffices Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1)) by
    ext
    simpa
  apply Fintype.card_congr
  exact ((skeletalFunctor ⋙ forget NonemptyFinLinOrd).mapIso I).toEquiv

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

Goal state before:
pp: X : NonemptyFinLinOrd
aux : Fintype.card ↑X.toLinOrd = Fintype.card ↑X.toLinOrd - 1 + 1
f : Fin (Fintype.card ↑X.toLinOrd - 1 + 1) ≃o ↑X.toLinOrd := monoEquivOfFin (↑X.toLinOrd) aux
hf : StrictMono ⇑(Finset.univ.orderEmbOfFin aux)
i j : ↑X.1
h : i ≤ j
⊢ f.symm i ≤ f.symm j

Tactic:
← hf.le_iff_le

Goal state after:
X : NonemptyFinLinOrd
aux : Fintype.card ↑X.toLinOrd = Fintype.card ↑X.toLinOrd - 1 + 1
f : Fin (Fintype.card ↑X.toLinOrd - 1 + 1) ≃o ↑X.toLinOrd := monoEquivOfFin (↑X.toLinOrd) aux
hf : StrictMono ⇑(Finset.univ.orderEmbOfFin aux)
i j : ↑X.1
h : i ≤ j
⊢ (Finset.univ.orderEmbOfFin aux) (f.symm i) ≤ (Finset.univ.orderEmbOfFin aux) (f.symm j)