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

Goal state before:
pp: α : Type u
n : ℕ
⊢ take n nil = []

Tactic:
cases n <;> rfl

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
⊢ (s.bind f).bind g = s.bind fun x ↦ (f x).bind g

Tactic:
by
  apply
    eq_of_bisim fun c₁ c₂ =>
      c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x : α => bind (f x) g
  · intro c₁ c₂ h
    match c₁, c₂, h with
    | _, c₂, Or.inl (Eq.refl _) => rcases destruct c₂ with b | cb <;> simp
    | _, _, Or.inr ⟨s, rfl, rfl⟩ =>
      induction s using recOn with
      | pure s =>
        simp only [BisimO, ret_bind]; generalize f s = fs
        induction fs using recOn with
        | pure t => rw [ret_bind]; rcases destruct (g t) with b | cb <;> simp
        | think => simp
      | think s => simpa [BisimO] using Or.inr ⟨s, rfl, rfl⟩
  · exact Or.inr ⟨s, rfl, rfl⟩

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

Goal state before:
pp: case cons
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Tactic:
have := congr_arg destruct e

Goal state after:
case cons
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
p : α → Prop
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → p hd ∧ motive tl
⊢ ∀ x ∈ s, p x

Tactic:
apply all_of_get
  intro n
  have := all_coind_drop_motive motive base (fun hd tl ih ↦ (step hd tl ih).right) n
  rw [← head_dropn]
  generalize s.drop n = s' at this
  cases s' with
  | nil => simp
  | cons hd tl => simp [(step hd tl this).left]

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: m n : ℕ
⊢ fib (m.gcd n) = (fib m).gcd (fib n)

Tactic:
induction m, n using Nat.gcd.induction with

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
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ m < n, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts) →
      ∃ conts, (of v).contsAux n = Pair.map Rat.cast conts

Tactic:
clear n

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
⊢ ∀ (n : ℕ),
    (∀ 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.CubicDiscriminant

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
w x y z : S
⊢ C w * (X - C x) * (X - C y) * (X - C z) =
    { a := w, b := w * -(x + y + z), c := w * (x * y + x * z + y * z), d := w * -(x * y * z) }.toPoly

Tactic:
simp only [toPoly, C_neg, C_add, C_mul]

Goal state after:
S : Type u_2
inst✝ : CommRing S
w x y z : S
⊢ C w * (X - C x) * (X - C y) * (X - C z) =
    C w * X ^ 3 + C w * -(C x + C y + C z) * X ^ 2 + C w * (C x * C y + C x * C z + C y * C z) * X +
      C w * -(C x * C y * C z)
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 :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
i : Fin 2
⊢ IsIdempotentElem (o i)

Tactic:
fin_cases i <;> simpa [o]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
i j : n
x y : R
⊢ Relation.Map (⇑c) (fun x ↦ x i j) (fun x ↦ x i j) x y → c.ofMatrix x y

Tactic:
rintro ⟨X, Y, h, rfl, rfl⟩ i' j'
    simpa using c.mul (c.mul (c.refl <| single i' i 1) h) (c.refl <| single j j' 1)

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)
⊢ LinearMap.restrict (f - μ • 1) h ^ k = 0

Tactic:
ext ⟨x, hx⟩

Goal state after:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)
x : M
hx : x ∈ (f.genEigenspace μ) ↑k
⊢ ↑((LinearMap.restrict (f - μ • 1) h ^ k) ⟨x, hx⟩) = ↑(0 ⟨x, hx⟩)
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, (f.genEigenspace μ) ↑k = (f.genEigenspace μ) ⊤

Tactic:
genEigenspace_top

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

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

Tactic:
obtain ⟨a₂, a₂', h₂, h₂', eq₂⟩ := DecompositionMonoid.primal a.2 h.2

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

Goal state before:
pp: R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }
⊢ ((lift fe).comp (inlAlgHom R A A)).range ⊔ R[(↑fe).2] = Subalgebra.map (↑fe).1 ⊤ ⊔ R[(↑fe).2]

Tactic:
lift_comp_inlHom,

Goal state after:
R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }
⊢ (↑fe).1.range ⊔ R[(↑fe).2] = Subalgebra.map (↑fe).1 ⊤ ⊔ R[(↑fe).2]
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
contra : ¬μ (t • x) = t • μ x
g : L → Submodule R M := fun x ↦ ((f x).genEigenspace (μ x)) k
this : ⨅ x, g x ≤ g x ⊓ g (t • x)
⊢ Disjoint (g x) (g (t • x))

Tactic:
apply Disjoint.mono_left (genEigenspace_le_smul (f x) (μ x) t k)

Goal state after:
R : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : IsDomain R
inst✝³ : IsTorsionFree R M
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
contra : ¬μ (t • x) = t • μ x
g : L → Submodule R M := ⋯
this : ⨅ x, g x ≤ g x ⊓ g (t • x)
⊢ Disjoint (((t • f x).genEigenspace (t * μ x)) k) (g (t • x))
Module: Mathlib.Algebra.DualQuaternion

Goal state before:
pp: case h2
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ { re := TrivSqZeroExt.snd (x✝ * y✝).re, imI := TrivSqZeroExt.snd (x✝ * y✝).imI,
      imJ := TrivSqZeroExt.snd (x✝ * y✝).imJ, imK := TrivSqZeroExt.snd (x✝ * y✝).imK } =
    { re := TrivSqZeroExt.fst x✝.re, imI := TrivSqZeroExt.fst x✝.imI, imJ := TrivSqZeroExt.fst x✝.imJ,
          imK := TrivSqZeroExt.fst x✝.imK } *
        { re := TrivSqZeroExt.snd y✝.re, imI := TrivSqZeroExt.snd y✝.imI, imJ := TrivSqZeroExt.snd y✝.imJ,
          imK := TrivSqZeroExt.snd y✝.imK } +
      { re := TrivSqZeroExt.snd x✝.re, imI := TrivSqZeroExt.snd x✝.imI, imJ := TrivSqZeroExt.snd x✝.imJ,
          imK := TrivSqZeroExt.snd x✝.imK } *
        { re := TrivSqZeroExt.fst y✝.re, imI := TrivSqZeroExt.fst y✝.imI, imJ := TrivSqZeroExt.fst y✝.imJ,
          imK := TrivSqZeroExt.fst y✝.imK }

Tactic:
congr 1 <;> simp <;> ring

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

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
⊢ ∑ i ∈ range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)

Tactic:
have h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x :=
    Nat.recOn n (by simp) fun n h => by
      rw [pow_succ', mul_inv_rev, ← mul_assoc, h, mul_assoc, mul_inv_cancel₀ hx0, mul_assoc,
        inv_mul_cancel₀ hx0]

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ ∑ i ∈ range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
⊢ reduce L = L

Tactic:
rw [← h.red_iff_eq]

Goal state after:
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
⊢ Red L (reduce L)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x : ℍ[R,c₁,c₂,c₃]
⊢ star (star x) = x

Tactic:
simp [Star.star]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ a.re * b.re + -1 * a.imI * b.imI + -1 * a.imJ * b.imJ + 0 * -1 * a.imJ * b.imK - -1 * -1 * a.imK * b.imK =
    a.re * b.re - a.imI * b.imI - a.imJ * b.imJ - a.imK * b.imK

Tactic:
by simp [one_mul, neg_mul, sub_eq_add_neg, neg_neg]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ star a + a = 2 * ↑a.re

Tactic:
by
  simpa using! QuaternionAlgebra.star_add_self a

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
⊢ normSq ↑n = ↑n ^ 2

Tactic:
← coe_natCast,

Goal state after:
R : Type u_3
inst✝ : CommRing R
n : ℕ
⊢ normSq ↑↑n = ↑n ^ 2
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : ((a.re ^ 2 = 0 ∧ a.imI ^ 2 = 0) ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ a = 0

Tactic:
apply ext a 0 <;> apply eq_zero_of_pow_eq_zero
    exacts [h.1.1.1, h.1.1.2, h.1.2, h.2]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : MonoidWithZero B
f : A →*₀ B
a✝ b✝ : Bˣ
y : A
hy : f y = ↑a✝
y' : A
hy' : f y' = ↑b✝
⊢ a✝ * b✝ ∈ Units.val ⁻¹' range ⇑f

Tactic:
use y * y'

Goal state after:
case h
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : MonoidWithZero B
f : A →*₀ B
a✝ b✝ : Bˣ
y : A
hy : f y = ↑a✝
y' : A
hy' : f y' = ↑b✝
⊢ f (y * y') = ↑(a✝ * b✝)
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case refine_1.mem
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y x✝ : Bˣ
h : x✝ ∈ ↑{ carrier := Units.val ⁻¹' range ⇑f, mul_mem' := ⋯, one_mem' := ⋯ }
⊢ ∃ a, f a ≠ 0 ∧ ∃ x, f a * ↑x✝ = f x

Tactic:
obtain ⟨a, ha⟩ := h
      exact ⟨a, ha.symm ▸ Units.ne_zero _, ⟨a * a, by simp [← ha]⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X : FintypeCat
⊢ uSwitch.map
        ((NatIso.ofComponents (fun X ↦ (equivEquivIso ((uSwitch.obj X).uSwitchEquiv.trans X.uSwitchEquiv)).symm)
                @uSwitchEquivalence._proof_2).hom.app
          X) ≫
      (NatIso.ofComponents (fun X ↦ equivEquivIso ((uSwitch.obj X).uSwitchEquiv.trans X.uSwitchEquiv))
              @uSwitchEquivalence._proof_4).hom.app
        (uSwitch.obj X) =
    𝟙 (uSwitch.obj X)

Tactic:
ext x
    simp [← uSwitchEquiv_naturality]

Goal state after:
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case mp
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{?u.19, 0} (Fin 2))
⊢ False

Tactic:
let p₁ : B ⟶ Y := ofHom
      ⟨fun b => if b < m then ULift.up 0 else ULift.up 1, fun x₁ x₂ h => by
        simp only
        split_ifs with h₁ h₂ h₂
        any_goals apply Fin.zero_le
        · exfalso
          exact h₁ (lt_of_le_of_lt h h₂)
        · rfl⟩

Goal state after:
case mp
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
⊢ False
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
P✝ Q : Karoubi (J ⥤ C)
f : P✝ ⟶ Q
X : J
P : Karoubi (J ⥤ C)
j j' : J
φ : j ⟶ j'
h : P.p.app j ≫ P.p.app j = P.p.app j
⊢ P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ

Tactic:
reassoc_of% h

Goal state after:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
P✝ Q : Karoubi (J ⥤ C)
f : P✝ ⟶ Q
X : J
P : Karoubi (J ⥤ C)
j j' : J
φ : j ⟶ j'
h : P.p.app j ≫ P.p.app j = P.p.app j
⊢ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case inl
n : ℕ
⊢ ↑((ConcreteCategory.hom (σ₀Iter 1 ⋯)) 0) = ↑((ConcreteCategory.hom (σ 0)) 0)

Tactic:
rw [σ₀Iter_coe_eq_of_lt _ _ _ (by simp), coe_σ,
      Fin.predAbove_of_le_castSucc _ _ (by simp)]
    dsimp

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

Goal state before:
pp: X : SSet
n k : ℕ
hk : n ≤ k
⊢ ⊥.toSSet.degenerate k = ⊤

Tactic:
ext ⟨x, hx⟩

Goal state after:
X : SSet
n k : ℕ
hk : n ≤ k
x : X _⦋k⦌
hx : x ∈ ⊥.obj (op ⦋k⦌)
⊢ ⟨x, hx⟩ ∈ ⊥.toSSet.degenerate k ↔ ⟨x, hx⟩ ∈ ⊤
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
x : X _⦋0⦌
m : ℕ
hm : m < 0
h✝ : ∃ f, x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))
⊢ False

Tactic:
simp at hm

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

Goal state before:
pp: case mpr
X : SSet
n : ℕ
x : X.op _⦋n⦌
m : ℕ
x✝ : m < n
⊢ (∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.op.map f.op))) →
    ∃ f, ∃ (_ : Epi f), opObjEquiv x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))

Tactic:
rintro ⟨f, _, y, rfl⟩
    exact ⟨SimplexCategory.rev.map f, inferInstance, opObjEquiv y, by simp [op_map]⟩

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

Goal state before:
pp: X : SSet
x y : X.N
⊢ x = y ↔ x.toS = y.toS

Tactic:
grind [cases SSet.N]

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c✝ : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
x✝² x✝¹ x✝ : I
⊢ c.ε₂ c c (x✝², c.π c c (x✝¹, x✝)) * c.ε₁ c c (x✝¹, x✝) = c.ε₁ c c (c.π c c (x✝², x✝¹), x✝) * c.ε₂ c c (x✝², x✝¹)

Tactic:
by dsimp; rw [one_mul, mul_one]

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

Tactic:
totalAux.d₂_eq K c₁₂ i₁ h₄ i₁₂'

Goal state after:
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 i₂ (c₂.next i₂)
⊢ (c₁.ε₂ c₂ c₁₂ (i₁, i₂) •
        (K.X i₁).d i₂ (c₂.next i₂) ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂' ?pos✝) ≫
      K.D₁ c₁₂ i₁₂' i₁₂'' =
    0

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 i₂ (c₂.next i₂)
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
inst✝² : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
j : J
c₂₃ : (i₂₃ : ρ₂₃.I₂₃) → (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).CofanMapObjFun ρ₂₃.p i₂₃ :=
  fun i₂₃ ↦ (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).cofanMapObj ρ₂₃.p i₂₃
h₂₃ : (i₂₃ : ρ₂₃.I₂₃) → IsColimit (c₂₃ i₂₃)
c : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).CofanMapObjFun ρ₂₃.q j :=
  (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).cofanMapObj ρ₂₃.q j
⊢ IsColimit (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)

Tactic:
have hc : IsColimit c := (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
    (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).isColimitCofanMapObj ρ₂₃.q j

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
inst✝² : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
j : J
c₂₃ : (i₂₃ : ρ₂₃.I₂₃) → (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).CofanMapObjFun ρ₂₃.p i₂₃ :=
  fun i₂₃ ↦ (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).cofanMapObj ρ₂₃.p i₂₃
h₂₃ : (i₂₃ : ρ₂₃.I₂₃) → IsColimit (c₂₃ i₂₃)
c : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).CofanMapObjFun ρ₂₃.q j :=
  (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).cofanMapObj ρ₂₃.q j
hc : IsColimit c
⊢ IsColimit (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)
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 L M : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
x✝ : c₁₂.Rel i₁₂ i₁₂'
⊢ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ (L.total c₁₂).d i₁₂ i₁₂' =
    (K.total c₁₂).d i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'

Tactic:
dsimp [total]
    rw [comp_add, add_comp, mapAux.mapMap_D₁, mapAux.mapMap_D₂]

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

Goal state before:
pp: case neg.h₁₂
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : ¬(up ℤ).Rel n₀ n₁
⊢ ¬(up ℤ).Rel n₀' n₁'

Tactic:
simp_all only [up_Rel]

Goal state after:
case neg.h₁₂
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : ¬n₀ + 1 = n₁
⊢ ¬n₀' + 1 = n₁'
Module: Mathlib.Algebra.Homology.CochainComplexOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
m : ℤ
hK : HomologicalComplex.ExactAt K (-m)
hm : -m + m = 0
⊢ (ComplexShape.up ℤ).prev (-m) = -(m + 1)

Tactic:
grind [prev]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Orthogonal

Goal state before:
pp: case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
hh : P.trW h
⊢ Function.Bijective fun f ↦ f ≫ h

Tactic:
rw [trW_iff'] at hh
    obtain ⟨Y₁, f, g, hT, hY₁⟩ := hh
    refine ⟨?_, fun α ↦ ?_⟩
    · suffices ∀ (α : X ⟶ Y₂), α ≫ h = 0 → α = 0 from fun α₁ α₂ hα ↦ by
        simpa [sub_eq_zero] using this (α₁ - α₂) (by simpa [sub_eq_zero])
      intro α hα
      obtain ⟨β, rfl⟩ := Triangle.coyoneda_exact₂ _ hT α hα
      simp [hX β hY₁]
    · obtain ⟨β, rfl⟩ := Triangle.coyoneda_exact₂ _ (rot_of_distTriang _ hT)
        α (hX _ (P.le_shift _ _ hY₁))
      exact ⟨β, rfl⟩

Goal state after: