awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
x : (WithZero (Multiplicative G))ˣ
none :
  ∀ (hab hba : HMul.hMul (α := WithZero (Multiplicative G)) Option.none Option.none = 1),
    (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G)
        { val := Option.none, inv := Option.none, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } =
      (↑{ val := Option.none, inv := Option.none, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } :
          WithZero (Multiplicative G)).log
none₁ :
  ∀ (b : Multiplicative G) (hab : Option.none * Option.some b = 1) (hba : Option.some b * Option.none = 1),
    (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G)
        { val := Option.none, inv := Option.some b, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } =
      (↑{ val := Option.none, inv := Option.some b, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } :
          WithZero (Multiplicative G)).log
some :
  ∀ (a : Multiplicative G) (hab : Option.some a * Option.none = 1) (hba : Option.none * Option.some a = 1),
    (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G)
        { val := Option.some a, inv := Option.none, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } =
      (↑{ val := Option.some a, inv := Option.none, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } :
          WithZero (Multiplicative G)).log
some₁ :
  ∀ (a b : Multiplicative G) (hab : Option.some a * Option.some b = 1) (hba : Option.some b * Option.some a = 1),
    (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G)
        { val := Option.some a, inv := Option.some b, val_inv := hab, inv_val := hba :
          (WithZero (Multiplicative G))ˣ } =
      (↑{ val := Option.some a, inv := Option.some b, val_inv := hab, inv_val := hba :
              (WithZero (Multiplicative G))ˣ } :
          WithZero (Multiplicative G)).log
⊢ (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G) x = (↑x : WithZero (Multiplicative G)).log

Tactic:
obtain ⟨_ | a, _ | b, hab, hba⟩ := x
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
hab hba : HMul.hMul (α := WithZero (Multiplicative G)) none none = 1
⊢ (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G)
      { val := none, inv := none, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } =
    (↑{ val := none, inv := none, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } :
        WithZero (Multiplicative G)).log

Tactic:
cases hab
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
b : Multiplicative G
hab : none * some b = 1
hba : some b * none = 1
⊢ (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G)
      { val := none, inv := some b, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } =
    (↑{ val := none, inv := some b, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } :
        WithZero (Multiplicative G)).log

Tactic:
cases hab
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
a : Multiplicative G
hab : some a * none = 1
hba : none * some a = 1
⊢ (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G)
      { val := some a, inv := none, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } =
    (↑{ val := some a, inv := none, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } :
        WithZero (Multiplicative G)).log

Tactic:
cases hab
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
a b : Multiplicative G
hab : some a * some b = 1
hba : some b * some a = 1
⊢ (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G)
      { val := some a, inv := some b, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } =
    (↑{ val := some a, inv := some b, val_inv := hab, inv_val := hba : (WithZero (Multiplicative G))ˣ } :
        WithZero (Multiplicative G)).log

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ (logEquiv : (a : (WithZero (Multiplicative G))ˣ) → G) (Units.mk0 x hx) = x.log

Tactic:
logEquiv_apply _

Premises used: WithZero.logEquiv_apply
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
a b : G
⊢ exp (a - b) = exp a / exp b

Tactic:
rfl

Premises used: WithZero.coe, WithZero.exp, rfl, Option.map₂
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
x y : WithZero (Multiplicative G)
hx : x ≠ 0
hy : y ≠ 0
⊢ x ≠ 0

Tactic:
hx
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
x y : WithZero (Multiplicative G)
hx : x ≠ 0
hy : y ≠ 0
lift :
  ∀ (x : Multiplicative G),
    ((↑x : WithZero (Multiplicative G)) / y).log = (↑x : WithZero (Multiplicative G)).log - y.log
⊢ (x / y).log = x.log - y.log

Tactic:
lift x to Multiplicative G using hx

Premises used: Multiplicative
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
y : WithZero (Multiplicative G)
hy : y ≠ 0
x : Multiplicative G
⊢ y ≠ 0

Tactic:
hy
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
y : WithZero (Multiplicative G)
hy : y ≠ 0
x : Multiplicative G
lift :
  ∀ (y : Multiplicative G),
    ((↑x : WithZero (Multiplicative G)) / (↑y : WithZero (Multiplicative G))).log =
      (↑x : WithZero (Multiplicative G)).log - (↑y : WithZero (Multiplicative G)).log
⊢ ((↑x : WithZero (Multiplicative G)) / y).log = (↑x : WithZero (Multiplicative G)).log - y.log

Tactic:
lift y to Multiplicative G using hy

Premises used: Multiplicative
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
x y : Multiplicative G
⊢ ((↑x : WithZero (Multiplicative G)) / (↑y : WithZero (Multiplicative G))).log =
    (↑x : WithZero (Multiplicative G)).log - (↑y : WithZero (Multiplicative G)).log

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
a : G
⊢ exp (-a) = (exp a)⁻¹

Tactic:
rfl

Premises used: WithZero.coe, WithZero.exp, rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
⊢ Eq.{u_5 + 1} (α := G) (log 0⁻¹) (-log 0)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
n : ℤ
a : G
⊢ exp (n • a) = exp a ^ n

Tactic:
rfl

Premises used: WithZero.exp, rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
x : WithZero (Multiplicative G)
n : ℤ
ofNat : ∀ (a : ℕ), (x ^ Int.ofNat a).log = Int.ofNat a • x.log
negSucc : ∀ (a : ℕ), (x ^ Int.negSucc a).log = Int.negSucc a • x.log
⊢ (x ^ n).log = n • x.log

Tactic:
cases n
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
x : WithZero (Multiplicative G)
a : ℕ
⊢ (x ^ Int.ofNat a).log = Int.ofNat a • x.log

Tactic:
simp [log_pow, log_inv]

Premises used: WithZero.log_inv, WithZero.log_pow
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
x : WithZero (Multiplicative G)
a : ℕ
⊢ (x ^ Int.negSucc a).log = Int.negSucc a • x.log

Tactic:
simp [log_pow, log_inv]

Premises used: WithZero.log_inv, WithZero.log_pow
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G₀ : Type u_1
M₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀
inst_2 : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀
⊢ x = 0 → Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) x : M₀) (0 : M₀)

Tactic:
simp +contextual
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G₀ : Type u_1
M₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀
inst_2 : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀
refine : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) x : M₀) (0 : M₀) → x = 0
⊢ Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) x : M₀) (0 : M₀) ↔ x = 0

Tactic:
refine ⟨?_, by simp +contextual⟩
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G₀ : Type u_1
M₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀
inst_2 : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀
contrapose! : x ≠ 0 → Ne.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) x : M₀) (0 : M₀)
⊢ Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) x : M₀) (0 : M₀) → x = 0

Tactic:
contrapose!
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G₀ : Type u_1
M₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀
inst_2 : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀
hx : x ≠ 0
H : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) x : M₀) (0 : M₀)
⊢ IsUnit x

Tactic:
isUnit_iff_ne_zero.mpr hx

Premises used: Iff.mpr, isUnit_iff_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G₀ : Type u_1
M₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀
inst_2 : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀
hx : x ≠ 0
H : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) x : M₀) (0 : M₀)
lift :
  ∀ (x : G₀ˣ) (hx : (↑x : G₀) ≠ 0) (H : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) (↑x : G₀) : M₀) (0 : M₀)), False
⊢ False

Tactic:
lift x to G₀ˣ using isUnit_iff_ne_zero.mpr hx

Premises used: Iff.mpr, isUnit_iff_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G₀ : Type u_1
M₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀
inst_2 : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : (↑x : G₀) ≠ 0
H : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) (↑x : G₀) : M₀) (0 : M₀)
apply : Eq.{u_2 + 1} (α := M₀) 1 0
⊢ False

Tactic:
apply one_ne_zero (α := M₀)

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G₀ : Type u_1
M₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MulZeroOneClass M₀
inst_2 : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : (↑x : G₀) ≠ 0
H : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) (↑x : G₀) : M₀) (0 : M₀)
rw : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) 1 : M₀) (0 : M₀)
rw₁ : Eq.{u_2 + 1} (α := M₀) ((f : (a : G₀) → M₀) ((↑x : G₀) * (↑x⁻¹ : G₀)) : M₀) (0 : M₀)
rw₂ : HMul.hMul (α := M₀) (β := M₀) ((f : (a : G₀) → M₀) (↑x : G₀) : M₀) ((f : (a : G₀) → M₀) (↑x⁻¹ : G₀) : M₀) = 0
rw₃ : HMul.hMul (α := M₀) (β := M₀) (0 : M₀) ((f : (a : G₀) → M₀) (↑x⁻¹ : G₀) : M₀) = 0
rw₄ rw₅ : Eq.{u_2 + 1} (α := M₀) 0 0
⊢ Eq.{u_2 + 1} (α := M₀) 1 0

Tactic:
rw [← map_one f, ← Units.mul_inv x, map_mul, H, zero_mul]

Premises used: MulZeroClass.zero_mul, Units.mul_inv, map_mul, map_one
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : MulZeroOneClass N₀
inst_2 : DecidablePred fun (x : M₀) ↦ x = 0
inst_3 : Nontrivial M₀
inst_4 : NoZeroDivisors M₀
x : M₀ˣ
⊢ Eq.{u_2 + 1} (α := N₀) ((1 : (a : M₀) → N₀) (↑x : M₀) : N₀) (1 : N₀)

Tactic:
one_apply_of_ne_zero x.ne_zero

Premises used: Units.ne_zero, MonoidWithZeroHom.one_apply_of_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
inst_3 : MulZeroOneClass N₀
inst_4 : MulZeroOneClass G₀
inst_5 : DecidablePred fun (x : M₀) ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
inl : Eq.{u_3 + 1} (α := G₀) ((f : (a : N₀) → G₀) ((1 : (a : M₀) → N₀) 0 : N₀) : G₀) ((1 : (a : M₀) → G₀) 0 : G₀)
inr :
  ∀ (hx : x ≠ 0),
    Eq.{u_3 + 1} (α := G₀) ((f : (a : N₀) → G₀) ((1 : (a : M₀) → N₀) x : N₀) : G₀) ((1 : (a : M₀) → G₀) x : G₀)
⊢ Eq.{u_3 + 1} (α := G₀) ((f : (a : N₀) → G₀) ((1 : (a : M₀) → N₀) x : N₀) : G₀) ((1 : (a : M₀) → G₀) x : G₀)

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
inst_3 : MulZeroOneClass N₀
inst_4 : MulZeroOneClass G₀
inst_5 : DecidablePred fun (x : M₀) ↦ x = 0
f : N₀ →*₀ G₀
⊢ Eq.{u_3 + 1} (α := G₀) ((f : (a : N₀) → G₀) ((1 : (a : M₀) → N₀) 0 : N₀) : G₀) ((1 : (a : M₀) → G₀) 0 : G₀)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
inst_3 : MulZeroOneClass N₀
inst_4 : MulZeroOneClass G₀
inst_5 : DecidablePred fun (x : M₀) ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
hx : x ≠ 0
inr : Eq.{u_3 + 1} (α := G₀) ((f : (a : N₀) → G₀) 1 : G₀) ((1 : (a : M₀) → G₀) x : G₀)
inr₁ : Eq.{u_3 + 1} (α := G₀) ((f : (a : N₀) → G₀) 1 : G₀) (1 : G₀)
inr₂ inr₃ : Eq.{u_3 + 1} (α := G₀) 1 1
⊢ Eq.{u_3 + 1} (α := G₀) ((f : (a : N₀) → G₀) ((1 : (a : M₀) → N₀) x : N₀) : G₀) ((1 : (a : M₀) → G₀) x : G₀)

Tactic:
rw [one_apply_of_ne_zero hx, one_apply_of_ne_zero hx, map_one]

Premises used: MonoidWithZeroHom.one_apply_of_ne_zero, map_one
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
inst_3 : MulZeroOneClass N₀
inst_4 : MulZeroOneClass G₀
inst_5 : DecidablePred fun (x : M₀) ↦ x = 0
f : N₀ →*₀ G₀
⊢ Eq (α := M₀ →*₀ G₀) (f.comp 1) 1

Tactic:
ext <| apply_one_apply_eq _

Premises used: MonoidWithZeroHom.ext, MonoidWithZeroHom.apply_one_apply_eq
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f_1 : C ⟶ D
i_1 : ι
n : ℕ
f : C ⟶ D
i j : ι
h : c.Rel i j
⊢ (n • f.f i) ≫ D.d i j = C.d i j ≫ (n • f.f j)

Tactic:
simp [Preadditive.nsmul_comp, Preadditive.comp_nsmul]

Premises used: CategoryTheory.Preadditive.nsmul_comp, CategoryTheory.Preadditive.comp_nsmul
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f_1 : C ⟶ D
i_1 : ι
n : ℤ
f : C ⟶ D
i j : ι
h : c.Rel i j
⊢ (n • f.f i) ≫ D.d i j = C.d i j ≫ (n • f.f j)

Tactic:
simp [Preadditive.zsmul_comp, Preadditive.comp_zsmul]

Premises used: CategoryTheory.Preadditive.comp_zsmul, CategoryTheory.Preadditive.zsmul_comp
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
i : ι
⊢ Eq.{v + 1} (α := C.X i ⟶ D.X i) (Hom.f 0 i) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
i : ι
⊢ (f + g).f i = f.f i + g.f i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
i : ι
⊢ (-f).f i = -f.f i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
i : ι
⊢ (f - g).f i = f.f i - g.f i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
n : ℕ
f : C ⟶ D
i : ι
⊢ (n • f).f i = n • f.f i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
n : ℤ
f : C ⟶ D
i : ι
⊢ (n • f).f i = n • f.f i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
i : ι
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : Eq (α := (i : ι) → C.X i ⟶ D.X i) (Hom.f 0) 0
⊢ Eq (α := (i : ι) → C.X i ⟶ D.X i) (Hom.f 0) 0

Tactic:
cat_disch
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
i : ι
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : ∀ (x y : C ⟶ D), (x + y).f = x.f + y.f
⊢ ∀ (x y : C ⟶ D), (x + y).f = x.f + y.f

Tactic:
cat_disch
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
i : ι
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : ∀ (x : C ⟶ D), (-x).f = -x.f
⊢ ∀ (x : C ⟶ D), (-x).f = -x.f

Tactic:
cat_disch
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
i : ι
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : ∀ (x y : C ⟶ D), (x - y).f = x.f - y.f
⊢ ∀ (x y : C ⟶ D), (x - y).f = x.f - y.f

Tactic:
cat_disch
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
i : ι
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : ∀ (x : C ⟶ D) (n : ℕ), (n • x).f = n • x.f
⊢ ∀ (x : C ⟶ D) (n : ℕ), (n • x).f = n • x.f

Tactic:
cat_disch
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
i : ι
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : ∀ (x : C ⟶ D) (n : ℤ), (n • x).f = n • x.f
⊢ ∀ (x : C ⟶ D) (n : ℤ), (n • x).f = n • x.f

Tactic:
cat_disch
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C_1 D : HomologicalComplex.{v, u, u_1} V c_1
f : C_1 ⟶ D
i_1 : ι
F : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
c : ComplexShape ι
C : HomologicalComplex.{v_2, u_3, u_1} W₁ c
i j : ι
w : ¬c.Rel i j
rw : Eq (α := F.obj (C.X i) ⟶ F.obj (C.X j)) (F.map 0) 0
rw₁ rw₂ : Eq.{v_3 + 1} (α := F.obj (C.X i) ⟶ F.obj (C.X j)) 0 0
⊢ F.map (C.d i j) = 0

Tactic:
rw [C.shape _ _ w, F.map_zero]

Premises used: CategoryTheory.Functor.map_zero, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C_1 D : HomologicalComplex.{v, u, u_1} V c_1
f : C_1 ⟶ D
i_1 : ι
F : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
c : ComplexShape ι
C : HomologicalComplex.{v_2, u_3, u_1} W₁ c
i j k : ι
h : c.Rel i j
h_1 : c.Rel j k
rw : F.map (C.d i j ≫ C.d j k) = 0
rw₁ : Eq (α := F.obj (C.X i) ⟶ F.obj (C.X k)) (F.map 0) 0
rw₂ rw₃ : Eq.{v_3 + 1} (α := F.obj (C.X i) ⟶ F.obj (C.X k)) 0 0
⊢ F.map (C.d i j) ≫ F.map (C.d j k) = 0

Tactic:
rw [← F.map_comp, C.d_comp_d, F.map_zero]

Premises used: CategoryTheory.Functor.map_zero, HomologicalComplex.d_comp_d, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f_1 : C ⟶ D
i_1 : ι
F : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
c : ComplexShape ι
X Y : HomologicalComplex.{v_2, u_3, u_1} W₁ c
f : X ⟶ Y
i j : ι
h : c.Rel i j
dsimp : F.map (f.f i) ≫ F.map (Y.d i j) = F.map (X.d i j) ≫ F.map (f.f j)
⊢ Eq (α :=
    Quiver.Hom.{v_3, u_4} (V := W₂)
      (HomologicalComplex.X.{v_3, u_4, u_1} (c := c)
        { X := fun (i : ι) ↦ F.obj (X.X i), d := fun (i j : ι) ↦ F.map (X.d i j), shape := ⋯, d_comp_d' := ⋯ } i)
      (HomologicalComplex.X.{v_3, u_4, u_1} (c := c)
        { X := fun (i : ι) ↦ F.obj (Y.X i), d := fun (i j : ι) ↦ F.map (Y.d i j), shape := ⋯, d_comp_d' := ⋯ } j))
    (F.map (f.f i) ≫
      d { X := fun (i : ι) ↦ F.obj (Y.X i), d := fun (i j : ι) ↦ F.map (Y.d i j), shape := ⋯, d_comp_d' := ⋯ } i j)
    (d { X := fun (i : ι) ↦ F.obj (X.X i), d := fun (i j : ι) ↦ F.map (X.d i j), shape := ⋯, d_comp_d' := ⋯ } i j ≫
      F.map (f.f j))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f_1 : C ⟶ D
i_1 : ι
F : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
c : ComplexShape ι
X Y : HomologicalComplex.{v_2, u_3, u_1} W₁ c
f : X ⟶ Y
i j : ι
h : c.Rel i j
rw : F.map (f.f i ≫ Y.d i j) = F.map (X.d i j) ≫ F.map (f.f j)
rw₁ : F.map (f.f i ≫ Y.d i j) = F.map (X.d i j ≫ f.f j)
rw₂ rw₃ : F.map (X.d i j ≫ f.f j) = F.map (X.d i j ≫ f.f j)
⊢ F.map (f.f i) ≫ F.map (Y.d i j) = F.map (X.d i j) ≫ F.map (f.f j)

Tactic:
rw [← F.map_comp, ← F.map_comp, f.comm]

Premises used: CategoryTheory.Functor.map_comp, HomologicalComplex.Hom.comm