mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n : M
X Y : C
f : X ⟶ Y
inst✝ : F.OplaxMonoidal
⊢ (δ F m n).app X ≫ (F.obj n).map ((F.obj m).map f) = (F.obj (m ⊗ n)).map f ≫ (δ F m n).app Y

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n m' : M
f : m ⟶ m'
X : C
inst✝ : F.LaxMonoidal
⊢ (F.obj n).map ((F.map f).app X) ≫ (μ F m' n).app X = (μ F m n).app X ≫ (F.map (f ▷ n)).app X

Tactic:
rw [← tensorHom_id, ← μ_naturality₂ F f (𝟙 n) X]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (η F).app ((F.obj n).obj X) = (μ F n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X

Tactic:
rw [map_rightUnitor]
  dsimp
  simp only [Category.comp_id, μ_δ_app_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst✝² : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst✝¹ : X.HasMap p
inst✝ : Y.HasMap p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
k : K
c : (j : J) → q j = k → X.CofanMapObjFun p j
hc : (j : J) → (hj : q j = k) → IsColimit (c j hj)
c' : Cofan fun j ↦ (c ↑j ⋯).pt
hc' : IsColimit c'
s : Cofan (X.mapObjFun r k)
x✝ : ↑(r ⁻¹' {k})
i : I
hi : r i = k
⊢ (Cofan.inj (X.cofanMapObjComp p q r hpqr k c c') ⟨i, hi⟩ ≫
      Cofan.IsColimit.desc hc' fun x ↦
        match x with
        | ⟨j, hj⟩ =>
          Cofan.IsColimit.desc (hc j hj) fun x ↦
            match x with
            | ⟨i, hi⟩ => s.inj ⟨i, ⋯⟩) =
    s.inj ⟨i, hi⟩

Tactic:
by simp

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

Goal state before:
pp: case neg
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✝ : ι
h : ¬i✝ = j
⊢ 0 = 𝟙 (if i✝ = j then A else 0)

Tactic:
convert! (id_zero (C := V)).symm

Goal state after:
case e'_1.e'_3
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✝ : ι
h : ¬i✝ = j
⊢ (if i✝ = j then A else 0) = 0

case e'_1.e'_4
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✝ : ι
h : ¬i✝ = j
⊢ (if i✝ = j then A else 0) = 0

case e'_2.e'_3.e'_2.e'_4
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✝ : ι
h : ¬i✝ = j
e_1✝¹ : ((if i✝ = j then A else 0) ⟶ if i✝ = j then A else 0) = (0 ⟶ 0)
e_1✝ :
  ({ X := fun i ↦ if i = j then A else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i✝ ⟶
      { X := fun i ↦ if i = j then A else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i✝) =
    (0 ⟶ 0)
⊢ { X := fun i ↦ if i = j then A else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i✝ = 0

case e'_2.e'_3.e'_2.e'_5
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✝ : ι
h : ¬i✝ = j
e_1✝¹ : ((if i✝ = j then A else 0) ⟶ if i✝ = j then A else 0) = (0 ⟶ 0)
e_1✝ :
  ({ X := fun i ↦ if i = j then A else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i✝ ⟶
      { X := fun i ↦ if i = j then A else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i✝) =
    (0 ⟶ 0)
⊢ { X := fun i ↦ if i = j then A else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i✝ = 0

case e'_3
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✝ : ι
h : ¬i✝ = j
e_1✝ : ((if i✝ = j then A else 0) ⟶ if i✝ = j then A else 0) = (0 ⟶ 0)
⊢ (if i✝ = j then A else 0) = 0
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: case neg
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✝ : ι
h : ¬i✝ = j
⊢ 0 = 𝟙 (if i✝ = j then A else 0)

Tactic:
#adaptation_note /-- nightly-2024-03-07
      previously was `rw [if_neg h]; simp`, but that fails with "motive not type correct"
      This is because dsimp does not simplify numerals;
      this note should be removable once https://github.com/leanprover/lean4/pull/8433 lands. -/
      convert! (id_zero (C := V)).symm
      all_goals simp [if_neg h]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x y : S
⊢ x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] 1 = x • 1 ⊗ₜ[R] y - x • y ⊗ₜ[R] 1

Tactic:
TensorProduct.smul_tmul',

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x y : S
⊢ x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] 1 = (x • 1) ⊗ₜ[R] y - (x • y) ⊗ₜ[R] 1
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : ChainComplex V ℕ
X : V
f : { f // C.d 1 0 ≫ f = 0 }
⊢ (fun φ ↦ ⟨φ.f 0, ⋯⟩) ((fun f ↦ HomologicalComplex.mkHomToSingle ↑f ⋯) f) = f

Tactic:
by simp

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
X : C
⊢ (shiftFunctor C a₃).map ((shiftFunctorAdd C a₁ a₂).inv.app X) ≫ (shiftFunctorAdd C (a₁ + a₂) a₃).inv.app X =
    (shiftFunctorAdd C a₂ a₃).inv.app ((shiftFunctor C a₁).obj X) ≫
      (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯).inv.app X

Tactic:
simpa using NatTrans.congr_app (congr_arg Iso.inv (shiftFunctorAdd_assoc C a₁ a₂ 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 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 i).inv ≫ (C₁.d i j ≫ (f j).hom) ≫ (f j).inv

Tactic:
by simp

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 ≫ ((f i).hom ≫ C₂.d i j) ≫ (f j).inv = C₂.d i j ≫ (f j).inv

Tactic:
by simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ ⊤ ≤ ⊥

Tactic:
← KaehlerDifferential.span_range_derivation,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ Submodule.span S (Set.range ⇑(D R S)) ≤ ⊥
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 0 = d₀

Tactic:
change ite (1 = 0 + 1) (𝟙 X₁ ≫ d₀) 0 = d₀

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
⊢ (if 1 = 0 + 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
n : ℕ
eq :
  (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).snd.fst =
    eqToHom ⋯ ≫
      (succ
            { X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2), X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1),
              X₃ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X n, f := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1),
              g := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }).snd.fst
⊢ (if h : n + 3 = n + 2 + 1 then eqToHom ⋯ ≫ (mkAux X₀ X₁ X₂ d₀ d₁ s succ (n + 2)).g else 0) =
    (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).snd.fst

Tactic:
dif_pos (by rfl),

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
n : ℕ
eq :
  (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).snd.fst =
    eqToHom ⋯ ≫
      (succ
            { X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2), X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1),
              X₃ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X n, f := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1),
              g := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }).snd.fst
⊢ eqToHom ⋯ ≫ (mkAux X₀ X₁ X₂ d₀ d₁ s succ (n + 2)).g = (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).snd.fst
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
⊢ (mk' X₀ X₁ d₀ fun {X₀ X₁} ↦ succ').d 1 0 = d₀

Tactic:
change ite (1 = 0 + 1) (𝟙 X₁ ≫ d₀) 0 = d₀

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
⊢ (if 1 = 0 + 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀
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
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f f' : Ω[S⁄R] →ₗ[S] M
hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
x : Ω[S⁄R]
this : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))
⊢ ∀ (x y : Ω[S⁄R]),
    x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)) →
      y ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)) → f x = f' x → f y = f' y → f (x + y) = f' (x + y)

pp: case refine_4
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
f f' : Ω[S⁄R] →ₗ[S] M
hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
x : Ω[S⁄R]
this : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))
⊢ ∀ (a : S), ∀ x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)), f x = f' x → f (a • x) = f' (a • x)

Tactic:
· intro x y _ _ hx hy; rw [map_add, map_add, hx, hy]

Goal state after:
case refine_4
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
f f' : Ω[S⁄R] →ₗ[S] M
hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
x : Ω[S⁄R]
this : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))
⊢ ∀ (a : S), ∀ x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)), f x = f' x → f (a • x) = f' (a • x)
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
i j : A
⊢ (shiftComm X i j).symm = shiftComm X j i

Tactic:
by
  ext
  exact NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorComm_symm C i j)) X

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
n : ι
⊢ (F.map φ).f n ≫ colimit.ι (F ⋙ eval C c n) j = colimit.ι (F ⋙ eval C c n) i ≫ 𝟙 (colimit (F ⋙ eval C c n))

Tactic:
simp only [Category.comp_id]

Goal state after:
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
n : ι
⊢ (F.map φ).f n ≫ colimit.ι (F ⋙ eval C c n) j = colimit.ι (F ⋙ eval C c n) i
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 ι
i j k : ι
hi : c.prev j = i
hk : c.next j = k
K : HomologicalComplex C c
⊢ (K.XIsoOfEq hi).hom ≫ ((shortComplexFunctor' C c i j k).obj K).f =
    ((shortComplexFunctor C c j).obj K).f ≫ (Iso.refl ((shortComplexFunctor C c j).obj K).X₂).hom

Tactic:
by simp

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 ι
i j k : ι
hi : c.prev j = i
hk : c.next j = k
K : HomologicalComplex C c
⊢ (Iso.refl ((shortComplexFunctor C c j).obj K).X₂).hom ≫ ((shortComplexFunctor' C c i j k).obj K).g =
    ((shortComplexFunctor C c j).obj K).g ≫ (K.XIsoOfEq hk).hom

Tactic:
by simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A
            (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ''
              Set.range fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ⊔
          Submodule.span A
            (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ''
              Set.range fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ⊔
        Submodule.span A
          (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ''
            Set.range fun x ↦ single ((algebraMap R A) x) 1) ⊔
      Submodule.span A (Set.range fun x ↦ single ((algebraMap S B) x) 1) =
    Submodule.span A (Set.range fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ⊔
        Submodule.span A (Set.range fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ⊔
      Submodule.span A (Set.range fun x ↦ single ((algebraMap S B) x) 1)

Tactic:
← Set.image_univ,

Goal state after:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A
            (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ''
              (fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) '' Set.univ) ⊔
          Submodule.span A
            (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ''
              (fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) '' Set.univ) ⊔
        Submodule.span A
          (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ''
            (fun x ↦ single ((algebraMap R A) x) 1) '' Set.univ) ⊔
      Submodule.span A ((fun x ↦ single ((algebraMap S B) x) 1) '' Set.univ) =
    Submodule.span A ((fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) '' Set.univ) ⊔
        Submodule.span A ((fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) '' Set.univ) ⊔
      Submodule.span A ((fun x ↦ single ((algebraMap S B) x) 1) '' Set.univ)
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 : ι
inst✝ : K.HasHomology j
⊢ K.d i j = 𝟙 (K.X i) ≫ K.d i j

Tactic:
by simp

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 : ι
inst✝ : K.HasHomology i
⊢ K.d i j = K.d i j ≫ 𝟙 (K.X j)

Tactic:
by simp

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 : ι
hj : c.next i = j
h : K.d i j = 0
inst✝ : K.HasHomology i
⊢ IsIso (K.iCycles i)

Tactic:
by
  subst hj
  exact ShortComplex.isIso_iCycles _ h

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
K L : ChainComplex C ℕ
φ : K ⟶ L
inst✝ : HomologicalComplex.HasHomology K 0
⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
by simp

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
K L : ChainComplex C ℕ
φ : K ⟶ L
inst✝ : HomologicalComplex.HasHomology K 0
⊢ K.d 0 0 = 0

Tactic:
by simp

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
K L : ChainComplex C ℕ
φ : K ⟶ L
inst✝ : HomologicalComplex.HasHomology K 0
⊢ K.d 0 ((ComplexShape.down ℕ).next 0) = 0

Tactic:
by simp

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
K L : CochainComplex C ℕ
φ : K ⟶ L
inst✝ : HomologicalComplex.HasHomology K 0
⊢ (ComplexShape.up ℕ).prev 0 = 0

Tactic:
by simp

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
K L : CochainComplex C ℕ
φ : K ⟶ L
inst✝ : HomologicalComplex.HasHomology K 0
⊢ K.d 0 0 = 0

Tactic:
by simp

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
K L : CochainComplex C ℕ
φ : K ⟶ L
inst✝ : HomologicalComplex.HasHomology K 0
⊢ K.d ((ComplexShape.up ℕ).prev 0) 0 = 0

Tactic:
by simp

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✝¹ : Abelian C
K : CochainComplex C ℕ
X : C
φ : X ⟶ K.X 0
inst✝ : HomologicalComplex.HasHomology K 0
hφ : φ ≫ K.d 0 1 = 0
⊢ (ComplexShape.up ℕ).next 0 = 1

Tactic:
by simp

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✝¹ : Abelian C
K : CochainComplex C ℕ
X : C
φ : X ⟶ K.X 0
inst✝ : HomologicalComplex.HasHomology K 0
hφ : φ ≫ K.d 0 1 = 0
this :
  ∀ (i : ℕ) (hx : (ComplexShape.up ℕ).next 0 = i) (hφ : φ ≫ K.d 0 i = 0),
    IsIso (HomologicalComplex.liftCycles K φ i hx hφ) ↔
      { X₁ := X, X₂ := K.X 0, X₃ := K.X i, f := φ, g := K.d 0 i, zero := hφ }.Exact ∧ Mono φ
⊢ (ComplexShape.up ℕ).next 0 = 1

Tactic:
by simp

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✝¹ : Abelian C
K : CochainComplex C ℕ
X : C
φ : X ⟶ K.X 0
inst✝ : HomologicalComplex.HasHomology K 0
hφ✝ : φ ≫ K.d 0 1 = 0
hφ : φ ≫ K.d 0 ((ComplexShape.up ℕ).next 0) = 0
⊢ 0 ≫ 0 = 0

Tactic:
by simp

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✝¹ : Abelian C
K : CochainComplex C ℕ
X : C
φ : X ⟶ K.X 0
inst✝ : HomologicalComplex.HasHomology K 0
hφ✝ : φ ≫ K.d 0 1 = 0
hφ : φ ≫ K.d 0 ((ComplexShape.up ℕ).next 0) = 0
α : { X₁ := X, X₂ := X, X₃ := X, f := 0, g := 0, zero := ⋯ } ⟶ HomologicalComplex.sc K 0 :=
  { τ₁ := 0, τ₂ := φ, τ₃ := 0, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (HomologicalComplex.sc K 0).f = 0

Tactic:
by simp

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✝¹ : Abelian C
K : ChainComplex C ℕ
X : C
φ : K.X 0 ⟶ X
inst✝ : HomologicalComplex.HasHomology K 0
hφ : K.d 1 0 ≫ φ = 0
⊢ (ComplexShape.down ℕ).prev 0 = 1

Tactic:
by simp

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✝¹ : Abelian C
K : ChainComplex C ℕ
X : C
φ : K.X 0 ⟶ X
inst✝ : HomologicalComplex.HasHomology K 0
hφ : K.d 1 0 ≫ φ = 0
this :
  ∀ (i : ℕ) (hx : (ComplexShape.down ℕ).prev 0 = i) (hφ : K.d i 0 ≫ φ = 0),
    IsIso (HomologicalComplex.descOpcycles K φ i hx hφ) ↔
      { X₁ := K.X i, X₂ := K.X 0, X₃ := X, f := K.d i 0, g := φ, zero := hφ }.Exact ∧ Epi φ
⊢ (ComplexShape.down ℕ).prev 0 = 1

Tactic:
by simp

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✝¹ : Abelian C
K : ChainComplex C ℕ
X : C
φ : K.X 0 ⟶ X
inst✝ : HomologicalComplex.HasHomology K 0
hφ✝ : K.d 1 0 ≫ φ = 0
hφ : K.d ((ComplexShape.down ℕ).prev 0) 0 ≫ φ = 0
⊢ 0 ≫ 0 = 0

Tactic:
by simp

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✝¹ : Abelian C
K : ChainComplex C ℕ
X : C
φ : K.X 0 ⟶ X
inst✝ : HomologicalComplex.HasHomology K 0
hφ✝ : K.d 1 0 ≫ φ = 0
hφ : K.d ((ComplexShape.down ℕ).prev 0) 0 ≫ φ = 0
α : HomologicalComplex.sc K 0 ⟶ { X₁ := X, X₂ := X, X₃ := X, f := 0, g := 0, zero := ⋯ } :=
  { τ₁ := 0, τ₂ := φ, τ₃ := 0, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (HomologicalComplex.sc K 0).g = 0

Tactic:
by simp

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
W : MorphismProperty C
F₁ F₂ : W.FunctorsInverting D
h : F₁.obj = F₂.obj
⊢ F₁ = F₂

Tactic:
by
  cases F₁
  cases F₂
  subst h
  rfl

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

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
h : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : W f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ IsIso (F.map f)

Tactic:
simp only [Arrow.iso_w' e, F.map_comp]

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
h : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : W f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ IsIso (F.map (Arrow.Hom.left e.inv) ≫ F.map f' ≫ F.map (Arrow.Hom.right e.hom))