mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f' i j h)
inst✝ : IsDirectedOrder ι
i : ι
x : G i
this : Nonempty ι
hix : ⟦⟨i, x⟩⟧ = 0
⊢ ∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0

Tactic:
DirectLimit.exists_eq_zero

Goal state after:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f' i j h)
inst✝ : IsDirectedOrder ι
i : ι
x : G i
this : Nonempty ι
hix : ∃ i_1, ∃ (h : ⟨i, x⟩.fst ≤ i_1), (f' ⟨i, x⟩.fst i_1 h) ⟨i, x⟩.snd = 0
⊢ ∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst✝ : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
e : (i : ι) → G i ≃+* G' i
he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i)
i : ι
g : G' i
⊢ (congr e he).symm ((of G' (fun x x_1 h ↦ ⇑(f' x x_1 h)) i) g) = (of G (fun x x_1 h ↦ ⇑(f x x_1 h)) i) ((e i).symm g)

Tactic:
simp only [congr, RingEquiv.ofRingHom_symm_apply, map_apply_of, RingHom.coe_coe]

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

Goal state before:
pp: case succ.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
s_nth_eq : g.s.get? n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr

Tactic:
let ppB := ppconts.b

Goal state after:
case succ.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
s_nth_eq : g.s.get? n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
Module: Mathlib.Data.Seq.Basic

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

Tactic:
induction s using recOn with | nil => ?_ | cons x s_1 => ?_ <;>
  induction S using recOn with | nil => simp | cons x_1 s_2 => ?_

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

case cons.cons
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a x : γ
s_1 : Seq γ
x_1 : Seq1 γ
s_2 : Seq (Seq1 γ)
⊢ (join (((a, Seq.cons x s_1), Seq.cons x_1 s_2), SS)).join =
    join (join ((a, Seq.cons x s_1), Seq.cons x_1 s_2), Seq.map join SS)
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case succ.succ.some
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : (of v).contsAux n = Pair.map Rat.cast ppred_conts
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = ↑z
⊢ ∃ conts,
    { a := ↑z * (Pair.map Rat.cast pred_conts).a + 1 * (Pair.map Rat.cast ppred_conts).a,
        b := ↑z * (Pair.map Rat.cast pred_conts).b + 1 * (Pair.map Rat.cast ppred_conts).b } =
      Pair.map Rat.cast conts

Tactic:
use nextConts 1 (z : ℚ) ppred_conts pred_conts

Goal state after:
case h
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := ⋯
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : (of v).contsAux n = Pair.map Rat.cast ppred_conts
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = ↑z
⊢ { a := ↑z * (Pair.map Rat.cast pred_conts).a + 1 * (Pair.map Rat.cast ppred_conts).a,
      b := ↑z * (Pair.map Rat.cast pred_conts).b + 1 * (Pair.map Rat.cast ppred_conts).b } =
    Pair.map Rat.cast (nextConts 1 (↑z) ppred_conts pred_conts)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
g : GenContFract K
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? 0 = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt 0
s_nth_eq : g.s.get? 0 = some { a := a, b := b }
this : (b * g.h + a) / b = g.h + a / b
⊢ g.convs (0 + 1) = (g.squashGCF 0).convs 0

Tactic:
simpa [squashGCF, s_nth_eq, conv_eq_conts_a_div_conts_b,
          conts_recurrenceAux s_nth_eq zeroth_contAux_eq_one_zero first_contAux_eq_h_one]

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

Goal state before:
pp: case succ
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
⊢ ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q (n + 1) = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑(n + 1)

Tactic:
intro ifp_succ_n stream_succ_nth_eq
    suffices ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - n by
      rw [Int.natCast_succ, sub_add_eq_sub_sub]
      solve_by_elim [le_sub_right_of_add_le]
    rcases succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq with ⟨ifp_n, stream_nth_eq, -⟩
    have : ifp_succ_n.fr.num < ifp_n.fr.num :=
      stream_succ_nth_fr_num_lt_nth_fr_num_rat stream_nth_eq stream_succ_nth_eq
    exact le_trans this (IH stream_nth_eq)

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:
LinearMap.ker_smul _ b hb

Goal state after:
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 = LinearMap.ker (f - b⁻¹ • a • 1)
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ (∃ y, e * e * y = r) ↔ ∃ y, e * y = r

Tactic:
idem.eq

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : NonUnitalSemiring R
idem : IsIdempotentElem e
⊢ e * e * e = e

Tactic:
idem.eq

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e r : R
he : IsIdempotentElem e
I : Ideal R
⊢ (Quotient.mk (span {e})) r ∈ map (Quotient.mk (span {e})) I ↔ (1 - e) * r ∈ I

Tactic:
simp only [Ideal.mem_map_iff_of_surjective _ Ideal.Quotient.mk_surjective,
    Ideal.Quotient.mk_eq_mk_iff_sub_mem, Ideal.mem_span_singleton]
  refine ⟨?_, fun H ↦ ⟨_, H, by simp [sub_mul]⟩⟩
  intro ⟨s, hs, t, hrst⟩
  convert I.mul_mem_left (1 - e) hs using 1
  linear_combination he.eq * t - (1 - e) * hrst

Goal state after:
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
inst✝¹ : Free R M
inst✝ : Module.Finite R M
x : Dual R M ⊗[R] M
⊢ (trace R M) ((dualTensorHom R M M) x) = (contractLeft R M) x

Tactic:
by
  rw [← comp_apply, trace_eq_contract]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β α✝ : Type u
x✝ x y : FreeMagma α✝
ih1 : id <$> x = x
ih2 : id <$> y = y
⊢ id <$> (x * y) = x * y

Tactic:
map_mul',

Goal state after:
α β α✝ : Type u
x✝ x y : FreeMagma α✝
ih1 : id <$> x = x
ih2 : id <$> y = y
⊢ id <$> x * id <$> y = x * y
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ β✝ : Type u
f : α✝ → β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (pure ∘ f) x = pure (f <$> x)
ih2 : traverse (pure ∘ f) y = pure (f <$> y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure (f <$> x) <*> pure (f <$> y) = pure (f <$> (x * y))

Tactic:
map_mul',

Goal state after:
α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ β✝ : Type u
f : α✝ → β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (pure ∘ f) x = pure (f <$> x)
ih2 : traverse (pure ∘ f) y = pure (f <$> y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure (f <$> x) <*> pure (f <$> y) = pure (f <$> x * f <$> y)
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β α✝ : Type u
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : id <$> pure x = pure x
ih2 : id <$> y = y
⊢ id <$> (pure x * y) = pure x * y

Tactic:
map_mul',

Goal state after:
α β α✝ : Type u
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : id <$> pure x = pure x
ih2 : id <$> y = y
⊢ id <$> pure x * id <$> y = pure x * y
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ β✝ : Type u
f : α✝ → β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (pure ∘ f) (of x) = pure (f <$> of x)
ih2 : traverse (pure ∘ f) y = pure (f <$> y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure (f <$> of x) <*> pure (f <$> y) = pure (f <$> (of x * y))

Tactic:
map_mul',

Goal state after:
α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ β✝ : Type u
f : α✝ → β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (pure ∘ f) (of x) = pure (f <$> of x)
ih2 : traverse (pure ∘ f) y = pure (f <$> y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure (f <$> of x) <*> pure (f <$> y) = pure (f <$> of x * f <$> y)
Module: Mathlib.Algebra.Group.Action.Option

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
a₁ a₂ : M
b : Option α
⊢ (a₁ * a₂) • b = a₁ • a₂ • b

Tactic:
by
    cases b
    exacts [rfl, congr_arg some (mul_smul _ _ _)]

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✝ : ℚ≥0
⊢ ↑x✝ = ↑x✝.num / ↑x✝.den

Tactic:
by rw [← coe_nnratCast, NNRat.cast_def, coe_div, coe_natCast, coe_natCast]

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

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
s : Set M
⊢ ↑(closure s) = s ∪ univ * s

Tactic:
let I : SemigroupIdeal M :=
    { carrier := s ∪ univ * s
      smul_mem' x y := by
        rintro (hy | ⟨y, -, z, hz, rfl⟩)
        · exact .inr <| mul_mem_mul (mem_univ _) hy
        · simpa [← mul_assoc] using .inr <| mul_mem_mul (mem_univ _) hz }
  suffices closure s = I by rw [this]; rfl
  refine (closure_le.2 fun x => Or.inl).antisymm fun x hx => hx.elim mem_closure_of_mem ?_
  rintro ⟨y, -, z, hz, rfl⟩
  exact SemigroupIdeal.mul_mem _ _ (mem_closure_of_mem hz)

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

Goal state before:
pp: case e'_3.e_f
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝¹ : fwdDiffₗ M G h = shiftₗ M G h - 1
this✝ : Commute (shiftₗ M G h) (-1)
k : ℕ
this : (-1) ^ (n - k) * ↑(n.choose k) = ↑((-1) ^ (n - k) * ↑(n.choose k))
⊢ ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) = (((-1) ^ (n - k) * ↑(n.choose k)) • (shiftₗ M G h ^ k) f) y

Tactic:
Pi.smul_apply,

Goal state after:
case e'_3.e_f
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝¹ : fwdDiffₗ M G h = shiftₗ M G h - 1
this✝ : Commute (shiftₗ M G h) (-1)
k : ℕ
this : (-1) ^ (n - k) * ↑(n.choose k) = ↑((-1) ^ (n - k) * ↑(n.choose k))
⊢ ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) = ((-1) ^ (n - k) * ↑(n.choose k)) • (shiftₗ M G h ^ k) f y
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: case succ
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
a b : R
k : ℕ
ih : (-1) ^ k * a * b = (-1) ^ k * (a * b)
⊢ -(-1) ^ k * a * b = -(-1) ^ k * (a * b)

Tactic:
simp only [neg_mul, ih]

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
P : ℕ → R
⊢ (Δ_[1]^[n] fun r ↦ ∑ k ∈ range n, P k * r ^ k) = 0

Tactic:
← sum_apply _ _ (fun i x ↦ P i * x ^ i),

Goal state after:
R : Type u_3
inst✝ : CommRing R
n : ℕ
P : ℕ → R
⊢ (Δ_[1]^[n] fun r ↦ (∑ c ∈ range n, fun x ↦ P c * x ^ c) r) = 0
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : Monoid α
inst✝¹ : AddGroup β
inst✝ : DistribMulAction α β
s : Finset α
t : Finset β
⊢ s • -t = -(s • t)

Tactic:
← image_neg_eq_neg

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : Monoid α
inst✝¹ : AddGroup β
inst✝ : DistribMulAction α β
s : Finset α
t : Finset β
⊢ s • image (fun x ↦ -x) t = image (fun x ↦ -x) (s • t)
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
⊢ CommMonoidWithZero α

Tactic:
by
  let _ := e.monoidWithZero
  apply e.injective.commMonoidWithZero _ <;> intros <;> exact e.apply_symm_apply _

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
u : Mˣ
hxy : ↑(u ^ n) = 1
hu : x * ↑u = y
hx : IsLeftRegular (x ^ n)
⊢ x = y

Tactic:
Units.val_eq_one,

Goal state after:
M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
u : Mˣ
hxy : u ^ n = 1
hu : x * ↑u = y
hx : IsLeftRegular (x ^ n)
⊢ x = y
Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
h : n + (i + 1) = m
⊢ X.map (SimplexCategory.δ₀Iter (i + 1) h).op = X.map (SimplexCategory.δ₀Iter i ⋯).op ≫ X.map (SimplexCategory.δ 0).op

Tactic:
rw [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_succ' _ h]

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

Goal state before:
pp: x : SimplexCategory
e : x ≅ x
h : Finset.univ.card = x.len + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.univ.orderEmbOfFin h
eq₂ : RelIso.toRelEmbedding (orderIsoOfIso (Iso.refl x)) = Finset.univ.orderEmbOfFin h
⊢ e = Iso.refl x

Tactic:
ext : 4

Goal state after:
x : SimplexCategory
e : x ≅ x
h : Finset.univ.card = x.len + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.univ.orderEmbOfFin h
eq₂ : RelIso.toRelEmbedding (orderIsoOfIso (Iso.refl x)) = Finset.univ.orderEmbOfFin h
x✝ : Fin (x.len + 1)
⊢ (Hom.toOrderHom e.hom) x✝ = (Hom.toOrderHom (Iso.refl x).hom) x✝
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h' : x ≤ i.castSucc
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) (i.predAbove x))

Tactic:
rw [Fin.predAbove_of_le_castSucc i x h']

Goal state after:
case pos
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h' : x ≤ i.castSucc
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) (x.castPred ⋯))
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case pos
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : i < ↑k
⊢ ↑((ConcreteCategory.hom (σ₀Iter i ⋯)) (j.predAbove k)) = ↑((ConcreteCategory.hom (σ₀Iter (i + 1) ⋯)) k)

Tactic:
σ₀Iter_coe_eq_of_ge (i + 1) ..,

Goal state after:
case pos
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : i < ↑k
⊢ ↑((ConcreteCategory.hom (σ₀Iter i ⋯)) (j.predAbove k)) = ↑k - (i + 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
S T : X.Subcomplex
h : S ≤ T
⊢ S ≤ ((fun S ↦ S.image f) T).preimage f

Tactic:
exact h.trans (by rw [← image_le_iff])

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

Goal state before:
pp: X : SSet
n m : ℕ
x : X _⦋n⦌
y : X _⦋m⦌
hx : x ∈ X.nonDegenerate n
hy : y ∈ X.nonDegenerate m
⊢ N.mk x hx = N.mk y hy ↔ Subcomplex.ofSimplex x = Subcomplex.ofSimplex y

Tactic:
· simp only [le_antisymm_iff]
    rfl

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

Goal state before:
pp: n : ℕ
⊢ face univ = ⊤

Tactic:
ext
  simp only [Subfunctor.top_obj, Set.top_eq_univ, Set.mem_univ, iff_true]
  apply Finset.subset_univ

Goal state after:
Module: Mathlib.Algebra.Homology.ComplexShapeSigns

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst✝ : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁, i₂) * 1 = -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')

Tactic:
by
    rw [← Int.units_mul_self (ComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂')), mul_assoc]
    conv_lhs =>
      arg 2
      rw [← mul_assoc, ε₂_ε₁ c₁₂ h₁ h₂]
    rw [neg_mul, neg_mul, neg_mul, mul_neg, neg_inj, ← mul_assoc, ← mul_assoc,
      Int.units_mul_self, one_mul]

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: 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 : I₁ × I₂
h : c₁.π c₂ c₁₂ i = i₁₂
⊢ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h ≫ K.D₁ c₁₂ i₁₂ i₁₂' = K.d₁ c₁₂ i.1 i.2 i₁₂'

Tactic:
by
  simp [D₁]

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
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 i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
· rw [K.d₂_eq_zero c₁₂ _ _ _ h₄, zero_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_5
C₄ : Type u_6
inst✝²⁰ : Category.{v_1, u_1} C₁
inst✝¹⁹ : Category.{v_2, u_2} C₂
inst✝¹⁸ : Category.{v_3, u_5} C₃
inst✝¹⁷ : Category.{v_4, u_6} C₄
inst✝¹⁶ : Category.{v_5, u_3} C₁₂
inst✝¹⁵ : HasZeroMorphisms C₁
inst✝¹⁴ : HasZeroMorphisms C₂
inst✝¹³ : HasZeroMorphisms C₃
inst✝¹² : Preadditive C₁₂
inst✝¹¹ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝¹⁰ : F₁₂.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁸ : G.Additive
inst✝⁷ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁶ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁵ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁴ : TotalComplexShape c₁₂ c₃ c₄
inst✝³ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝² : DecidableEq ι₁₂
inst✝¹ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
⊢ ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h ≫ D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' = d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'

Tactic:
by
  simp [D₁]

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
⊢ total.map ((shiftFunctor₁ C x).map f) (up ℤ) ≫ (L.totalShift₁Iso x).hom =
    (K.totalShift₁Iso x).hom ≫ (shiftFunctor (HomologicalComplex C (up ℤ)) x).map (total.map f (up ℤ))

Tactic:
ext n i₁ i₂ h
  dsimp at h ⊢
  rw [ιTotal_map_assoc, L.ι_totalShift₁Iso_hom_f x i₁ i₂ n h _ rfl _ rfl,
    K.ι_totalShift₁Iso_hom_f_assoc x i₁ i₂ n h _ rfl _ rfl]
  dsimp
  rw [id_comp, id_comp, id_comp, comp_id, ιTotal_map]

Goal state after: