mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type u_3
A : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
a : A
inst✝⁵ : Algebra R A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module A M
inst✝² : Module R M
inst✝¹ : IsScalarTower R A M
inst✝ : FaithfulSMul A M
p : R[X]
h : ∀ (m : M), (aeval a) p • m = 0
⊢ ∀ (a_1 : M), (aeval a) p • a_1 = 0 • a_1

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type u_3
A : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
a : A
inst✝⁵ : Algebra R A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module A M
inst✝² : Module R M
inst✝¹ : IsScalarTower R A M
inst✝ : FaithfulSMul A M
p : R[X]
h : (aeval a) p = 0
⊢ ∀ (m : M), (aeval a) p • m = 0

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
p p' : ↥((Algebra.lsmul R R M) a).invtSubmodule
h :
  {
        toFun := fun p ↦
          let __AddSubmonoid := AddSubmonoid.map (of R M a) (↑p).toAddSubmonoid;
          { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
        invFun := fun q ↦ ⟨(Submodule.orderIsoMapComap (of R M a)).symm (Submodule.restrictScalars R q), ⋯⟩,
        left_inv := ⋯, right_inv := ⋯ }
      p ≤
    {
        toFun := fun p ↦
          let __AddSubmonoid := AddSubmonoid.map (of R M a) (↑p).toAddSubmonoid;
          { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
        invFun := fun q ↦ ⟨(Submodule.orderIsoMapComap (of R M a)).symm (Submodule.restrictScalars R q), ⋯⟩,
        left_inv := ⋯, right_inv := ⋯ }
      p'
x : M
hx : x ∈ ↑p
⊢ x ∈ ↑p'

Tactic:
aesop (rule_sets := [SetLike!])

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
y : M
hy : y ∈ I • (R ∙ i)
z : M
hz : z ∈ I • span R s
hyz : y + z = ((LinearMap.lsmul R M) r) i
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s

Tactic:
dsimp at hyz

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
y : M
hy : y ∈ I • (R ∙ i)
z : M
hz : z ∈ I • span R s
hyz : y + z = r • i
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case insert.refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
y : M
hy : y ∈ I • (R ∙ i)
z : M
hz : z ∈ I • span R s
hyz : y + z = ((LinearMap.lsmul R M) r) n
⊢ n ∈ comap ((LinearMap.lsmul R M) (c * r)) (I • span R s)

Tactic:
dsimp at hyz

Goal state after:
case insert.refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
y : M
hy : y ∈ I • (R ∙ i)
z : M
hz : z ∈ I • span R s
hyz : y + z = r • n
⊢ n ∈ comap ((LinearMap.lsmul R M) (c * r)) (I • span R s)
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
hle : map N.mkQ P ≤ I • map N.mkQ P
r : R
hmem : r - 1 ∈ I
hr : ∀ n ∈ map N.mkQ P, r • n = 0
x : M
hx : x ∈ r • P
⊢ x ∈ N

Tactic:
induction hx using Submodule.smul_inductionOn_pointwise with

Goal state after:
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ I.cotangentToQuotientSquare.range = Submodule.restrictScalars R I.cotangentIdeal

Tactic:
trans LinearMap.range (I.cotangentToQuotientSquare.comp I.toCotangent)
  · rw [LinearMap.range_comp, I.toCotangent_range, Submodule.map_top]
  · rw [to_quotient_square_comp_toCotangent, LinearMap.range_comp, I.range_subtype]; ext; rfl

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
⊢ ∀ (x y_1 : S),
    D.tensorProductTo (x ⊗ₜ[R] y_1 * y) =
      (TensorProduct.lmul' R) (x ⊗ₜ[R] y_1) • D.tensorProductTo y +
        (TensorProduct.lmul' R) y • D.tensorProductTo (x ⊗ₜ[R] y_1)

pp: case refine_3
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
⊢ ∀ (x y_1 : S ⊗[R] S),
    D.tensorProductTo (x * y) =
        (TensorProduct.lmul' R) x • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo x →
      D.tensorProductTo (y_1 * y) =
          (TensorProduct.lmul' R) y_1 • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo y_1 →
        D.tensorProductTo ((x + y_1) * y) =
          (TensorProduct.lmul' R) (x + y_1) • D.tensorProductTo y +
            (TensorProduct.lmul' R) y • D.tensorProductTo (x + y_1)

Tactic:
swap

Goal state after:
case refine_3
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
⊢ ∀ (x y_1 : S ⊗[R] S),
    D.tensorProductTo (x * y) =
        (TensorProduct.lmul' R) x • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo x →
      D.tensorProductTo (y_1 * y) =
          (TensorProduct.lmul' R) y_1 • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo y_1 →
        D.tensorProductTo ((x + y_1) * y) =
          (TensorProduct.lmul' R) (x + y_1) • D.tensorProductTo y +
            (TensorProduct.lmul' R) y • D.tensorProductTo (x + y_1)

case refine_2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
⊢ ∀ (x y_1 : S),
    D.tensorProductTo (x ⊗ₜ[R] y_1 * y) =
      (TensorProduct.lmul' R) (x ⊗ₜ[R] y_1) • D.tensorProductTo y +
        (TensorProduct.lmul' R) y • D.tensorProductTo (x ⊗ₜ[R] y_1)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_2.refine_2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁ x₂ : S
⊢ ∀ (x y : S),
    D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * x ⊗ₜ[R] y) =
      (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo (x ⊗ₜ[R] y) +
        (TensorProduct.lmul' R) (x ⊗ₜ[R] y) • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)

pp: case refine_2.refine_3
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁ x₂ : S
⊢ ∀ (x y : S ⊗[R] S),
    D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * x) =
        (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo x +
          (TensorProduct.lmul' R) x • D.tensorProductTo (x₁ ⊗ₜ[R] x₂) →
      D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * y) =
          (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo y +
            (TensorProduct.lmul' R) y • D.tensorProductTo (x₁ ⊗ₜ[R] x₂) →
        D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * (x + y)) =
          (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo (x + y) +
            (TensorProduct.lmul' R) (x + y) • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)

Tactic:
swap

Goal state after:
case refine_2.refine_3
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁ x₂ : S
⊢ ∀ (x y : S ⊗[R] S),
    D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * x) =
        (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo x +
          (TensorProduct.lmul' R) x • D.tensorProductTo (x₁ ⊗ₜ[R] x₂) →
      D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * y) =
          (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo y +
            (TensorProduct.lmul' R) y • D.tensorProductTo (x₁ ⊗ₜ[R] x₂) →
        D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * (x + y)) =
          (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo (x + y) +
            (TensorProduct.lmul' R) (x + y) • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)

case refine_2.refine_2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁ x₂ : S
⊢ ∀ (x y : S),
    D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * x ⊗ₜ[R] y) =
      (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo (x ⊗ₜ[R] y) +
        (TensorProduct.lmul' R) (x ⊗ₜ[R] y) • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i : ι
hi : i ≠ j
⊢ IsZero (((single V c j).obj A).X i)

Tactic:
dsimp [single]
  rw [if_neg hi]
  exact Limits.isZero_zero V

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
⊢ a₁ + a₂₃ = a₁₂₃

Tactic:
← h₂₃,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
⊢ a₁ + (a₂ + a₃) = a₁₂₃
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctorAdd' C a 0 a ⋯).inv.app X = (shiftFunctorZero C A).hom.app ((shiftFunctor C a).obj X)

Tactic:
simpa using NatTrans.congr_app (congr_arg Iso.inv (shiftFunctorAdd'_add_zero C a)) X

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬c.Rel (c.prev j) j
⊢ C.dTo j = 0

Tactic:
simp [h]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ a₁ + a₂₃ = a₁₂₃

Tactic:
← h₂₃,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ a₁ + (a₂ + a₃) = a₁₂₃
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬c.Rel i (c.next i)
⊢ C.dFrom i = 0

Tactic:
simp [h]

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬c.Rel (c.prev j) j
⊢ (C.xPrevIsoSelf h).inv ≫ C.dTo j = 0

Tactic:
simp [h]

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬c.Rel i (c.next i)
⊢ C.dFrom i ≫ (C.xNextIsoSelf h).hom = 0

Tactic:
simp [h]

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i j : ι
hij : c.Rel i j
⊢ (f i).inv ≫ (C₁.d i j ≫ (f j).hom) ≫ (f j).inv = (f i).inv ≫ ((f i).hom ≫ C₂.d i j) ≫ (f j).inv

Tactic:
hf i j hij

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i j : ι
hij : c.Rel i j
⊢ (f i).inv ≫ (C₁.d i j ≫ (f j).hom) ≫ (f j).inv = (f i).inv ≫ (C₁.d i j ≫ (f j).hom) ≫ (f j).inv
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_3
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
hx✝ : x✝ ∈ ideal R S
hx : x✝ ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
x y : S ⊗[R] S
hx₁ : x ∈ ideal R S
hx₂ : (fromIdeal R S) ⟨x, hx₁⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
hy₁ : y ∈ ideal R S
hy₂ : (fromIdeal R S) ⟨y, hy₁⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
⊢ ∃ (hx : x + y ∈ ideal R S), (fromIdeal R S) ⟨x + y, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Tactic:
exact ⟨add_mem hx₁ hy₁, Submodule.add_mem _ hx₂ hy₂⟩

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹¹ : Category.{v, u} V
inst✝¹⁰ : Preadditive V
W : Type u_2
inst✝⁹ : Category.{v_1, u_2} W
inst✝⁸ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f : C ⟶ D
i✝ : ι
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X : W₁
i : ι
h : i = j
⊢ ((single W₁ c j ⋙ F.mapHomologicalComplex c).obj X).X i = ((F ⋙ single W₂ c j).obj X).X i

Tactic:
simp [h]

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹¹ : Category.{v, u} V
inst✝¹⁰ : Preadditive V
W : Type u_2
inst✝⁹ : Category.{v_1, u_2} W
inst✝⁸ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f : C ⟶ D
i✝ : ι
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X : W₁
i : ι
h : i = j
⊢ ((F ⋙ single W₂ c j).obj X).X i = ((single W₁ c j ⋙ F.mapHomologicalComplex c).obj X).X i

Tactic:
simp [h]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
⊢ (shiftFunctorCompIsoId C 0 0 ⋯).hom.app X =
    (shiftFunctor C 0).map ((shiftFunctorZero C A).hom.app X) ≫ (shiftFunctorZero C A).hom.app X

Tactic:
by
  simp [shiftFunctorCompIsoId, shiftFunctorAdd'_zero_add_inv_app]

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
P Q : CochainComplex V ℕ
zero : P.X 0 ⟶ Q.X 0
one : P.X 1 ⟶ Q.X 1
one_zero_comm : zero ≫ Q.d 0 1 = P.d 0 1 ≫ one
succ :
  (n : ℕ) →
    (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f') →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' p.snd.fst ≫ Q.d (n + 1) (n + 2) = P.d (n + 1) (n + 2) ≫ f''
n m : ℕ
⊢ (ComplexShape.up ℕ).Rel n m →
    (P.mkHomAux Q zero one one_zero_comm succ n).fst ≫ Q.d n m =
      P.d n m ≫ (P.mkHomAux Q zero one one_zero_comm succ m).fst

Tactic:
by
    rintro (rfl : n + 1 = m)
    exact (mkHomAux P Q zero one one_zero_comm succ n).2.2

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
inst✝ : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
i j : J
φ : i ⟶ j
⊢ F.map φ ≫ { f := fun n ↦ colimit.ι (F ⋙ eval C c n) j, comm' := ⋯ } =
    { f := fun n ↦ colimit.ι (F ⋙ eval C c n) i, comm' := ⋯ } ≫
      ((Functor.const J).obj
            { X := fun n ↦ colimit (F ⋙ eval C c n),
              d := fun n m ↦ colimMap { app := fun j ↦ (F.obj j).d n m, naturality := ⋯ }, shape := ⋯,
              d_comp_d' := ⋯ }).map
        φ

Tactic:
ext n
        dsimp
        simp only [Category.comp_id]
        rw [← eval_map, ← Functor.comp_map, colimit.w]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.sc' i j k).pOpcycles ≫ (K.opcyclesIsoSc' i j k hi hk).inv = K.pOpcycles j

Tactic:
dsimp [opcyclesIsoSc']
  simp only [ShortComplex.p_opcyclesMap, shortComplexFunctor'_obj_X₂, shortComplexFunctor_obj_X₂,
    natIsoSc'_inv_app_τ₂, id_comp]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
⊢ (isomorphisms C).IsInvertedBy F

Tactic:
intro _ _ _ hf
  simp only [isomorphisms.iff] at hf
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m n₁ n₂ n₃ n₁₂ n₂₃ n₁₂₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
h₁₂ : n₁ + n₂ = n₁₂
h₂₃ : n₂ + n₃ = n₂₃
h₁₂₃ : n₁ + n₂ + n₃ = n₁₂₃
⊢ n₁ + n₂₃ = n₁₂₃

Tactic:
← h₂₃,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m n₁ n₂ n₃ n₁₂ n₂₃ n₁₂₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
h₁₂ : n₁ + n₂ = n₁₂
h₂₃ : n₂ + n₃ = n₂₃
h₁₂₃ : n₁ + n₂ + n₃ = n₁₂₃
⊢ n₁ + (n₂ + n₃) = n₁₂₃
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case h₁
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel j i
A : C
f g : X φ j ⟶ A
h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g
h₂ : inrX φ j ≫ f = inrX φ j ≫ g
this : HasBinaryBiproduct (F.X i) (G.X j)
⊢ biprod.inr ≫ (XIsoBiprod φ j i hij).inv ≫ f = biprod.inr ≫ (XIsoBiprod φ j i hij).inv ≫ g

Tactic:
· obtain rfl := c.next_eq' hij
    simpa [-inr_XIsoBiprod_inv, -inr_XIsoBiprod_inv_assoc, inrX, dif_pos hij] using h₂

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap fun i j ↦ dite (c.Rel j i) (h i j) fun x ↦ 0).f k₀ = 0

Tactic:
apply nullHomotopicMap_f_eq_zero hk₀ hk₀'

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n₀ n₁ n₂ : ℤ
z : Cochain F G n₀
h₁₂ : n₁ + 1 = n₂
⊢ δ n₁ n₂ (δ n₀ n₁ z) = 0

pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n₀ n₁ n₂ : ℤ
z : Cochain F G n₀
h₁₂ : ¬n₁ + 1 = n₂
⊢ δ n₁ n₂ (δ n₀ n₁ z) = 0

Tactic:
swap

Goal state after:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n₀ n₁ n₂ : ℤ
z : Cochain F G n₀
h₁₂ : ¬n₁ + 1 = n₂
⊢ δ n₁ n₂ (δ n₀ n₁ z) = 0

case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n₀ n₁ n₂ : ℤ
z : Cochain F G n₀
h₁₂ : n₁ + 1 = n₂
⊢ δ n₁ n₂ (δ n₀ n₁ z) = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n₀ n₁ n₂ : ℤ
z : Cochain F G n₀
h₁₂ : n₁ + 1 = n₂
h₀₁ : n₀ + 1 = n₁
⊢ δ n₁ n₂ (δ n₀ n₁ z) = 0

pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n₀ n₁ n₂ : ℤ
z : Cochain F G n₀
h₁₂ : n₁ + 1 = n₂
h₀₁ : ¬n₀ + 1 = n₁
⊢ δ n₁ n₂ (δ n₀ n₁ z) = 0

Tactic:
swap

Goal state after:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n₀ n₁ n₂ : ℤ
z : Cochain F G n₀
h₁₂ : n₁ + 1 = n₂
h₀₁ : ¬n₀ + 1 = n₁
⊢ δ n₁ n₂ (δ n₀ n₁ z) = 0

case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n₀ n₁ n₂ : ℤ
z : Cochain F G n₀
h₁₂ : n₁ + 1 = n₂
h₀₁ : n₀ + 1 = n₁
⊢ δ n₁ n₂ (δ n₀ n₁ z) = 0
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: case e_a.succ
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = P.d (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ Q.d (n + 3) (n + 2)
n✝ : ℕ
⊢ (xNextIso P ⋯).hom ≫ (mkInductiveAux₁ e zero one comm_one succ n✝).fst =
    (xNextIso P ⋯).inv ≫ (mkInductiveAux₂ e zero comm_zero one comm_one succ (n✝ + 1)).fst

Tactic:
dsimp [xNextIso]

Goal state after:
case e_a.succ
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = P.d (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ Q.d (n + 3) (n + 2)
n✝ : ℕ
⊢ eqToHom ⋯ ≫ (mkInductiveAux₁ e zero one comm_one succ n✝).fst =
    𝟙 (xNext P (n✝ + 1)) ≫ eqToHom ⋯ ≫ (mkInductiveAux₁ e zero one comm_one succ n✝).fst