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
⊢ g.convs (n' + 1 + 1) = (g.squashGCF (n' + 1)).convs (n' + 1)

Tactic:
let ppB := ppred_conts.b

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
⊢ g.convs (n' + 1 + 1) = (g.squashGCF (n' + 1)).convs (n' + 1)
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case succ.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
⊢ ↑(fib (n + 2)) ≤ ((of v).contsAux (n + 2)).b

Tactic:
suffices (fib n : K) + fib (n + 1) ≤ gp.a * ppconts.b + gp.b * pconts.b by
          simpa [g, fib_add_two, add_comm, contsAux_recurrence s_ppred_nth_eq ppconts_eq pconts_eq]

Goal state after:
case succ.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
⊢ ↑(fib n) + ↑(fib (n + 1)) ≤ gp.a * ppconts.b + gp.b * pconts.b
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
⊢ (fun P ↦ ⟨P.toPoly, ⋯⟩) ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f) =
    f

Tactic:
ext n
    obtain hn | hn := le_or_gt n 3
    · interval_cases n <;> simp only <;> ring_nf <;> try simp only [coeffs]
    · rw [coeff_eq_zero hn, (degree_le_iff_coeff_zero (f : R[X]) 3).mp f.2]
      simpa using hn

Goal state after:
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv

Goal state before:
pp: case pos
K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Subsingleton V
⊢ ∃ T, f = conjAlgEquiv K T

Tactic:
nontriviality W

Goal state after:
K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Subsingleton V
a✝ : Nontrivial W
⊢ ∃ T, f = conjAlgEquiv K T
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : S
he : e ∈ f.range
he' : IsIdempotentElem e
⊢ ∃! e', IsIdempotentElem e' ∧ f e' = e

Tactic:
by
  obtain ⟨e', he₂, rfl⟩ := exists_isIdempotentElem_eq_of_ker_isNilpotent f h e he he'
  exact ⟨e', ⟨he₂, rfl⟩, fun x ⟨hx, hx'⟩ ↦
    eq_of_isNilpotent_sub_of_isIdempotentElem hx he₂
      (h _ (by rw [RingHom.mem_ker, map_sub, hx', sub_self]))⟩

Goal state after:
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
f : End K V
a b : K
hb : b ≠ 0
⊢ (f - b⁻¹ • a • 1).ker = (b • (f - b⁻¹ • a • 1)).ker

Tactic:
rw [LinearMap.ker_smul _ b hb]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case he₁
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R := ⋯
⊢ ∀ (i j : Fin 2), i ≠ j → (1 - o i) * (1 - o j) = 0

pp: case he₂
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R := ⋯
⊢ ∏ i, o i = 0

Tactic:
· intro i j hij
    fin_cases i <;> fin_cases j <;> simp at hij ⊢ <;>
      simp [o, mul_comm, hef₂, ← hef₁]

Goal state after:
case he₂
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R := ⋯
⊢ ∏ i, o i = 0
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Free R ↥(N i)
h : IsInternal N
hN : {i | N i ≠ ⊥}.Finite
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
x✝¹ : Fintype { i // N i ≠ ⊥ } := hN.fintype
x✝ : Fintype ↑{i | N i ≠ ⊥} := hN.fintype
⊢ ∑ i, (trace R ↥(N ↑i)) (f.restrict ⋯) = ∑ i, (trace R ↥(N ↑i)) (f.restrict ⋯)

Tactic:
exact Fintype.sum_equiv hN.subtypeEquivToFinset _ _ (fun i ↦ rfl)

Goal state after:
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
k : R
hk : e' i * e' j = e₀ * k
⊢ (1 - e₀) * e₀ * k = 0

Tactic:
he₀.one_sub_mul_self,

Goal state after:
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
k : R
hk : e' i * e' j = e₀ * k
⊢ 0 * k = 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✝¹ : 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 μ₂) ↑l) ↑((f.genEigenspace μ₂) ↑l)

Tactic:
apply mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f _)

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 := ⋯
⊢ MapsTo ⇑(f - (algebraMap R (End R M)) μ₁) ↑((f.genEigenspace μ₁) ↑k) ↑((f.genEigenspace μ₁) ↑k)

Tactic:
apply mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f _)

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g h : M →ₗ[R] M
⊢ (trace R M) (f * g * h) = (trace R M) (h * (f * g))

Tactic:
LinearMap.trace_mul_comm

Goal state after:
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g h : M →ₗ[R] M
⊢ (trace R M) (h * (f * g)) = (trace R M) (h * (f * g))
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
⊢ trace R M ∘ₗ dualTensorHom R M M = contractLeft R M

Tactic:
cases nonempty_fintype ι
    apply Basis.ext (Basis.tensorProduct (Basis.dualBasis b) b)
    rintro ⟨i, j⟩
    simp only [Function.comp_apply, Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp]
    rw [trace_eq_matrix_trace R b, toMatrix_dualTensorHom]
    obtain rfl | hij := eq_or_ne i j
    · simp
    rw [Matrix.trace_single_eq_of_ne j i (1 : R) hij.symm]
    simp [hij]

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_6
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
M : Type u_7
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
e : M →ₗ[R] M
he : IsIdempotentElem e
inst✝³ : Free R ↥e.range
inst✝² : Module.Finite R ↥e.range
inst✝¹ : Free R ↥e.ker
inst✝ : Module.Finite R ↥e.ker
⊢ e.range = ⊥ ↔ e = 0

Tactic:
range_eq_bot

Goal state after:
R : Type u_6
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
M : Type u_7
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
e : M →ₗ[R] M
he : IsIdempotentElem e
inst✝³ : Free R ↥e.range
inst✝² : Module.Finite R ↥e.range
inst✝¹ : Free R ↥e.ker
inst✝ : Module.Finite R ↥e.ker
⊢ e = 0 ↔ e = 0
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_3
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : IsIntegrallyClosedIn A B
inst✝ : Algebra.IsIntegral R A
⊢ IsIntegralClosure A R B

Tactic:
refine ⟨IsIntegralClosure.algebraMap_injective _ A _, fun {x} ↦
    ⟨fun hx ↦ IsIntegralClosure.isIntegral_iff.mp (IsIntegral.tower_top (A := A) hx), ?_⟩⟩

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_3
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : IsIntegrallyClosedIn A B
inst✝ : Algebra.IsIntegral R A
x : B
⊢ (∃ y, (algebraMap A B) y = x) → IsIntegral R x
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
⊢ Cardinal.toNat (Module.rank R ℍ[R,c₁,c₂,c₃]) = 4

Tactic:
rank_eq_four,

Goal state after:
R : Type u_3
c₁ c₂ c₃ : R
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
⊢ Cardinal.toNat 4 = 4
Module: Mathlib.Algebra.Group.Action.Option

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝³ : SMul M α
inst✝² : SMul N α
a✝ : M
b : α
x✝ : Option α
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
a : M
x : Option α
⊢ MulOpposite.op a • x = a • x

Tactic:
by
    cases x
    exacts [rfl, congr_arg some (op_smul_eq_smul _ _)]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : SMul α β
inst✝¹ : IsLeftCancelSMul α β
inst✝ : DecidableEq β
s : Set α
t : Finset β
⊢ (s.PairwiseDisjoint fun i ↦ i • ↑t) ↔ Set.InjOn (fun p ↦ p.1 • p.2) (s ×ˢ ↑t)

Tactic:
Set.pairwiseDisjoint_smul_iff

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝ : ℚ
⊢ ↑x✝ = ↑x✝.num / ↑x✝.den

Tactic:
by rw [← coe_ratCast, Rat.cast_def, coe_div, coe_intCast, coe_natCast]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : s.Nontrivial
⊢ ↑(s • univ) = ↑univ

Tactic:
by push_cast; exact Set.smul_univ₀' hs

Goal state after:
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
y x✝ : Bˣ
a : A
ha : f a = ↑x✝
⊢ f a * ↑x✝ = f (a * a)

Tactic:
by simp [← ha]

Goal state after:
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
y c : Bˣ
hc : c ∈ Subgroup.closure ↑{ carrier := Units.val ⁻¹' range ⇑f, mul_mem' := ⋯, one_mem' := ⋯ }
u : A
hu : f u ≠ 0
a : A
ha : f u * ↑c = f a
⊢ f a * ↑c⁻¹ = f u

Tactic:
by simp [← ha]

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

Goal state before:
pp: case refine_2
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ˣ := ⋯.unit
hv₀ : f x = ↑v
u : Bˣ := ⋯.unit
ha₀ : f a = ↑u
hy : u⁻¹ * v = y
⊢ y ∈ f.valueGroup

Tactic:
← hy

Goal state after:
case refine_2
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ˣ := ⋯.unit
hv₀ : f x = ↑v
u : Bˣ := ⋯.unit
ha₀ : f a = ↑u
hy : u⁻¹ * v = y
⊢ u⁻¹ * v ∈ f.valueGroup
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case refine_1
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
a b : ↑Y.1
h : φ b < φ a
⊢ b < a

Tactic:
suffices b ≤ a by
        apply lt_of_le_of_ne this
        rintro rfl
        exfalso
        simp at h

Goal state after:
case refine_1
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
a b : ↑Y.1
h : φ b < φ a
⊢ b ≤ a
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

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

Tactic:
Fin.val_castLT

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

Goal state before:
pp: S T : SSet
f : S ⟶ T
n : ℕ
i : Fin (n + 1)
x : S _⦋n⦌
⊢ (ConcreteCategory.hom (f.app (op ⦋n + 1⦌))) ((ConcreteCategory.hom (SimplicialObject.σ S i)) x) =
    (ConcreteCategory.hom (SimplicialObject.σ T i)) ((ConcreteCategory.hom (f.app (op ⦋n⦌))) x)

Tactic:
by
  change (S.σ i ≫ f.app (op ⦋n + 1⦌)) x = (f.app (op ⦋n⦌) ≫ T.σ i) x
  exact congr_hom (SimplicialObject.σ_naturality f i) x

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
d : ℕ
inst✝ : Y.HasDimensionLT d
n : ℕ
hn : d ≤ n
⊢ X.degenerate n = ⊤

Tactic:
ext x
    rw [← degenerate_iff_of_isIso (Subcomplex.toRange f),
      Subcomplex.mem_degenerate_iff, Y.degenerate_eq_univ_of_hasDimensionLT d n hn]
    simp

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

Goal state before:
pp: X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
y : X.obj (op m)
hy : (ConcreteCategory.hom (X.map f.op)) y = ↑x
this : IsIso (factorThruImage f)
⊢ Mono f

Tactic:
rw [← image.fac f]

Goal state after:
X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
y : X.obj (op m)
hy : (ConcreteCategory.hom (X.map f.op)) y = ↑x
this : IsIso (factorThruImage f)
⊢ Mono (factorThruImage f ≫ image.ι f)
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case term
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
j✝ : ι
⊢ (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).map (WidePullbackShape.Hom.term j✝) ≫
      Option.casesOn none (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
        limit.π (Discrete.functor fun x ↦ X) { as := i }) =
    (Option.casesOn (some j✝) (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none))
        fun i ↦ limit.π (Discrete.functor fun x ↦ X) { as := i }) ≫
      (wideCospan ι X).map (WidePullbackShape.Hom.term j✝)

Tactic:
simp only [Functor.const_obj_obj, Functor.const_obj_map, terminal.comp_from]

Goal state after:
case term
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
j✝ : ι
⊢ terminal.from (∏ᶜ fun x ↦ X) =
    limit.π (Discrete.functor fun x ↦ X) { as := j✝ } ≫ (wideCospan ι X).map (WidePullbackShape.Hom.term j✝)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
B : X.Subcomplex
f : Y ⟶ X
⊢ B.preimage f = ⊤ ↔ range f ≤ B

Tactic:
← image_top,

Goal state after:
X Y : SSet
B : X.Subcomplex
f : Y ⟶ X
⊢ B.preimage f = ⊤ ↔ ⊤.image f ≤ B
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case neg
X : SSet
n : ℕ
x✝ : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f₁
y₁ : ↑(X.nonDegenerate m)
hy₁ : x✝ = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : ↑(X.nonDegenerate m)
hy₂ : x✝ = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : Fin (m + 1) → Fin (n + 1) :=
  fun y ↦ if y = (SimplexCategory.Hom.toOrderHom f₁) x then x else (SimplexCategory.Hom.toOrderHom hf.section_) y
y : Fin (m + 1)
hy : ¬y = (SimplexCategory.Hom.toOrderHom f₁) x
⊢ (SimplexCategory.Hom.toOrderHom f₁) ((SimplexCategory.Hom.toOrderHom hf.section_) y) = y

Tactic:
apply SimplexCategory.congr_toOrderHom_apply hf.id

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

Goal state before:
pp: X Y : SSet
x₀ x₁ x₂ y₀ y₁ : X _⦋0⦌
hom : Edge x₀ x₁
hom' : Edge y₀ y₁
I : hom.InvStruct
hhom : hom.edge = hom'.edge
⊢ (ConcreteCategory.hom (SimplicialObject.δ X 0)) hom.edge = y₁

Tactic:
hhom,

Goal state after:
X Y : SSet
x₀ x₁ x₂ y₀ y₁ : X _⦋0⦌
hom : Edge x₀ x₁
hom' : Edge y₀ y₁
I : hom.InvStruct
hhom : hom.edge = hom'.edge
⊢ (ConcreteCategory.hom (SimplicialObject.δ X 0)) hom'.edge = y₁
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct

Goal state before:
pp: X Y : SSet
x₀ x₁ x₂ y₀ y₁ : X _⦋0⦌
hom : Edge x₀ x₁
hom' : Edge y₀ y₁
I : hom.InvStruct
hhom : hom.edge = hom'.edge
⊢ (ConcreteCategory.hom (SimplicialObject.δ X 1)) hom.edge = y₀

Tactic:
hhom,

Goal state after:
X Y : SSet
x₀ x₁ x₂ y₀ y₁ : X _⦋0⦌
hom : Edge x₀ x₁
hom' : Edge y₀ y₁
I : hom.InvStruct
hhom : hom.edge = hom'.edge
⊢ (ConcreteCategory.hom (SimplicialObject.δ X 1)) hom'.edge = y₀
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct

Goal state before:
pp: X Y : SSet
x₀ x₁ x₂ y₀ y₁ : X _⦋0⦌
hom : Edge x₀ x₁
hom' : Edge y₀ y₁
I : hom.InvStruct
hhom : hom.edge = hom'.edge
⊢ (id ((ConcreteCategory.hom (SimplicialObject.δ X 1)) hom.edge)).edge = (id y₀).edge

Tactic:
hhom,

Goal state after:
X Y : SSet
x₀ x₁ x₂ y₀ y₁ : X _⦋0⦌
hom : Edge x₀ x₁
hom' : Edge y₀ y₁
I : hom.InvStruct
hhom : hom.edge = hom'.edge
⊢ (id ((ConcreteCategory.hom (SimplicialObject.δ X 1)) hom'.edge)).edge = (id y₀).edge
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct

Goal state before:
pp: X Y : SSet
x₀ x₁ x₂ y₀ y₁ : X _⦋0⦌
hom : Edge x₀ x₁
hom' : Edge y₀ y₁
I : hom.InvStruct
hhom : hom.edge = hom'.edge
⊢ (id ((ConcreteCategory.hom (SimplicialObject.δ X 0)) hom.edge)).edge = (id y₁).edge

Tactic:
hhom,

Goal state after:
X Y : SSet
x₀ x₁ x₂ y₀ y₁ : X _⦋0⦌
hom : Edge x₀ x₁
hom' : Edge y₀ y₁
I : hom.InvStruct
hhom : hom.edge = hom'.edge
⊢ (id ((ConcreteCategory.hom (SimplicialObject.δ X 0)) hom'.edge)).edge = (id y₁).edge
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case a
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
⊢ face S ≤ Subcomplex.ofSimplex (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom))

Tactic:
rintro ⟨k⟩ x hx

Goal state after:
case a
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
k : SimplexCategory
x : Δ[n].obj (op k)
hx : x ∈ (face S).obj (op k)
⊢ x ∈
    (Subcomplex.ofSimplex (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom))).obj (op k)
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.d₁ c₁₂ (c₁.next i₁) i₂ i₁₂'' = 0

pp: case neg
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : ¬c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.d₁ c₁₂ (c₁.next i₁) i₂ i₁₂'' = 0

Tactic:
· rw [totalAux.d₁_eq K c₁₂ h₄ i₂ i₁₂'', Linear.comp_units_smul,
            d_f_comp_d_f_assoc, zero_comp, smul_zero, smul_zero]
          rw [← ComplexShape.next_π₁ c₂ c₁₂ h₄, ← ComplexShape.next_π₁ c₂ c₁₂ h₃,
            h, c₁₂.next_eq' h₁, c₁₂.next_eq' h₂]

Goal state after:
case neg
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : ¬c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.d₁ c₁₂ (c₁.next i₁) i₂ i₁₂'' = 0