mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
⊢ (kerCotangentToTensor R A B).range = Submodule.restrictScalars A (mapBaseChange R A B).ker

Tactic:
ext x
  constructor
  · rintro ⟨x, rfl⟩
    obtain ⟨x, rfl⟩ := Ideal.toCotangent_surjective _ x
    simp only [kerCotangentToTensor_toCotangent, Submodule.restrictScalars_mem, LinearMap.mem_ker,
      mapBaseChange_tmul, map_D, RingHom.mem_ker.mp x.2, map_zero, smul_zero]
  · intro hx
    obtain ⟨x, rfl⟩ := LinearMap.rTensor_surjective Ω[A⁄R] (g := Algebra.linearMap A B) h x
    obtain ⟨x, rfl⟩ := (TensorProduct.lid _ _).symm.surjective x
    replace hx : x ∈ LinearMap.ker (KaehlerDifferential.map R R A B) := by simpa using hx
    rw [KaehlerDifferential.ker_map_of_surjective R A B h] at hx
    obtain ⟨x, hx, rfl⟩ := hx
    simp only [TensorProduct.lid_symm_apply, LinearMap.rTensor_tmul,
      Algebra.linearMap_apply, map_one]
    rw [← Finsupp.sum_single x, Finsupp.sum, ← Finset.sum_fiberwise_of_maps_to
      (fun _ ↦ Finset.mem_image_of_mem (algebraMap A B))]
    simp only [map_sum (s := x.support.image (algebraMap A B)),
      TensorProduct.tmul_sum]
    apply sum_mem
    intro c _
    simp only [LinearMap.mem_range]
    simp only [map_sum, Finsupp.linearCombination_single]
    have : ∑ i ∈ x.support with algebraMap A B i = c, x i ∈ RingHom.ker (algebraMap A B) := by
      simpa [Finsupp.mapDomain, Finsupp.sum, Finsupp.finsetSum_apply, RingHom.mem_ker,
        Finsupp.single_apply, ← Finset.sum_filter] using DFunLike.congr_fun hx c
    obtain ⟨a, ha⟩ := h c
    use ∑ i ∈ {i ∈ x.support | algebraMap A B i = c}.attach, x i • Ideal.toCotangent _ ⟨i - a, ?_⟩
    · simp only [map_sum, LinearMapClass.map_smul, kerCotangentToTensor_toCotangent, map_sub]
      simp_rw [← TensorProduct.tmul_smul]
      -- TODO: was `simp [kerCotangentToTensor_toCotangent, RingHom.mem_ker.mp x.2]` and very slow
      -- (https://github.com/leanprover-community/mathlib4/issues/19751)
      simp only [smul_sub, TensorProduct.tmul_sub, Finset.sum_sub_distrib, ← TensorProduct.tmul_sum,
        ← Finset.sum_smul, Finset.sum_attach, sub_eq_self,
        Finset.sum_attach (f := fun i ↦ x i • KaehlerDifferential.D R A i)]
      rw [← TensorProduct.smul_tmul, ← Algebra.algebraMap_eq_smul_one, RingHom.mem_ker.mp this,
        TensorProduct.zero_tmul]
    · have : x i ≠ 0 ∧ algebraMap A B i = c := by
        convert! i.prop
        simp_rw [Finset.mem_filter, Finsupp.mem_support_iff]
      simp [RingHom.mem_ker, ha, this.2]

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

Goal state before:
pp: 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 : ι
hi : ¬c.Rel i (c.next i)
A : C
f g : A ⟶ X φ i
h : f ≫ sndX φ i = g ≫ sndX φ i
⊢ f ≫ (XIso φ i hi).hom = g ≫ (XIso φ i hi).hom

Tactic:
simpa only [sndX, dif_neg hi] using h

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ z₁' : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ (z₁ + z₁').comp z₂ h = z₁.comp z₂ h + z₁'.comp z₂ h

Tactic:
by
  ext p q hpq
  simp only [comp_v _ _ h p _ q rfl (by lia), add_v, add_comp]

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

Goal state before:
pp: 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 : ι
⊢ inrX φ i ≫ d φ i j = G.d i j ≫ inrX φ j

Tactic:
by
  by_cases hij : c.Rel i j
  · by_cases hj : c.Rel j (c.next j)
    · apply ext_to_X _ _ _ hj
      · simp [d_fstX φ _ _ _ hij]
      · simp [d_sndX φ _ _ hij]
    · apply ext_to_X' _ _ hj
      simp [d_sndX φ _ _ hij]
  · rw [shape φ _ _ hij, G.shape _ _ hij, zero_comp, comp_zero]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v, u_1} C
inst✝³ : Category.{v', u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + -1 = q
⊢ (ComplexShape.up ℤ).Rel q p

Tactic:
dsimp; lia

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

Goal state before:
pp: case pos
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
hc : ∀ (j : ι), ∃ i, c.Rel i j
i j : ι
hij : c.Rel j i
⊢ (inrCompHomotopy φ hc).hom i j ≫ (desc φ α hα).f j = hα.hom i j

Tactic:
dsimp
    simp only [inrCompHomotopy_hom φ hc i j hij, desc_f φ α hα _ _ hij,
      comp_add, inlX_fstX_assoc, inlX_sndX_assoc, zero_comp, add_zero]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
m₁ m₂ m₁₂ : ℤ
h₁₂ : n₁₂ + 1 = m₁₂
h₁ : n₁ + 1 = m₁
h₂ : n₂ + 1 = m₂
⊢ δ n₁₂ m₁₂ (z₁.comp z₂ h) = z₁.comp (δ n₂ m₂ z₂) ⋯ + n₂.negOnePow • (δ n₁ m₁ z₁).comp z₂ ⋯

Tactic:
subst h₁₂ h₁ h₂ h
  ext p q hpq
  dsimp
  rw [z₁.comp_v _ (add_assoc n₁ n₂ 1).symm p _ q rfl (by lia),
    Cochain.comp_v _ _ (show n₁ + 1 + n₂ = n₁ + n₂ + 1 by lia) p (p + n₁ + 1) q
      (by lia) (by lia),
    δ_v (n₁ + n₂) _ rfl (z₁.comp z₂ rfl) p q hpq (p + n₁ + n₂) _ (by lia) rfl,
    z₁.comp_v z₂ rfl p _ _ rfl rfl,
    z₁.comp_v z₂ rfl (p + 1) (p + n₁ + 1) q (by lia) (by lia),
    δ_v n₂ (n₂ + 1) rfl z₂ (p + n₁) q (by lia) (p + n₁ + n₂) _ (by lia) rfl,
    δ_v n₁ (n₁ + 1) rfl z₁ p (p + n₁ + 1) (by lia) (p + n₁) _ (by lia) rfl]
  simp only [assoc, comp_add, add_comp, Int.negOnePow_succ, Int.negOnePow_add n₁ n₂,
    Units.neg_smul, comp_neg, neg_comp, smul_neg, smul_smul, Linear.units_smul_comp,
    mul_comm n₁.negOnePow n₂.negOnePow, Linear.comp_units_smul, smul_add]
  abel

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

Goal state before:
pp: case mpr
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
K : HomologicalComplex C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₂ : Homotopy (φ ≫ ⟨x₁, x₂⟩.fst) 0
h : ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = ⟨⟨x₁, x₂⟩.fst, y₂⟩.snd.hom i j
⊢ ⟨x₁, x₂⟩ = ⟨⟨x₁, x₂⟩.fst, y₂⟩

Tactic:
simp only [Sigma.mk.inj_iff, heq_eq_eq, true_and]

Goal state after:
case mpr
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
K : HomologicalComplex C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₂ : Homotopy (φ ≫ ⟨x₁, x₂⟩.fst) 0
h : ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = ⟨⟨x₁, x₂⟩.fst, y₂⟩.snd.hom i j
⊢ x₂ = y₂
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ (ComplexShape.up ℤ).Rel j i

Tactic:
dsimp; lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ (ComplexShape.up ℤ).Rel i k

Tactic:
dsimp; lia

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

Goal state before:
pp: case pos
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
K : HomologicalComplex C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₂ : Homotopy (φ ≫ ⟨x₁, x₂⟩.fst) 0
h : ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = ⟨⟨x₁, x₂⟩.fst, y₂⟩.snd.hom i j
i j : ι
hij : c.Rel j i
⊢ x₂.hom i j = y₂.hom i j

pp: case neg
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
K : HomologicalComplex C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₂ : Homotopy (φ ≫ ⟨x₁, x₂⟩.fst) 0
h : ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = ⟨⟨x₁, x₂⟩.fst, y₂⟩.snd.hom i j
i j : ι
hij : ¬c.Rel j i
⊢ x₂.hom i j = y₂.hom i j

Tactic:
· exact h _ _ hij

Goal state after:
case neg
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
K : HomologicalComplex C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₂ : Homotopy (φ ≫ ⟨x₁, x₂⟩.fst) 0
h : ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = ⟨⟨x₁, x₂⟩.fst, y₂⟩.snd.hom i j
i j : ι
hij : ¬c.Rel j i
⊢ x₂.hom i j = y₂.hom i j
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K✝ : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
K : HomologicalComplex C c
hc : ∀ (j : ι), ∃ i, c.Rel i j
x✝ : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
⊢ (fun f ↦ ⟨inr φ ≫ f, (Homotopy.ofEq ⋯).trans (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ⋯))⟩)
      ((fun x ↦
          match x with
          | ⟨α, hα⟩ => desc φ α hα)
        ⟨α, hα⟩) =
    ⟨α, hα⟩

Tactic:
descSigma_ext_iff

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K✝ : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
K : HomologicalComplex C c
hc : ∀ (j : ι), ∃ i, c.Rel i j
x✝ : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
⊢ ((fun f ↦ ⟨inr φ ≫ f, (Homotopy.ofEq ⋯).trans (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ⋯))⟩)
          ((fun x ↦
              match x with
              | ⟨α, hα⟩ => desc φ α hα)
            ⟨α, hα⟩)).fst =
      ⟨α, hα⟩.fst ∧
    ∀ (i j : ι),
      c.Rel j i →
        ((fun f ↦ ⟨inr φ ≫ f, (Homotopy.ofEq ⋯).trans (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ⋯))⟩)
                  ((fun x ↦
                      match x with
                      | ⟨α, hα⟩ => desc φ α hα)
                    ⟨α, hα⟩)).snd.hom
            i j =
          ⟨α, hα⟩.snd.hom i j
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: case e_a.e_a
ι : 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)
i : ℕ
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    (toPrev i) fun i j ↦
      if h : i + 1 = j then (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom else 0

Tactic:
· dsimp [toPrev]
      rw [dif_pos (by simp only [ChainComplex.prev])]
      simp [xPrevIso, comp_id]

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

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n : ℤ
z₁ : Cochain F G n
z₂ : Cocycle G K 0
m : ℤ
hnm : ¬n + 1 = m
⊢ δ n m (z₁.comp ↑z₂ ⋯) = (δ n m z₁).comp ↑z₂ ⋯

Tactic:
· simp [δ_shape _ _ hnm]

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

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n : ℤ
z₁ : Cocycle F G 0
z₂ : Cochain G K n
m : ℤ
hnm : ¬n + 1 = m
⊢ δ n m ((↑z₁).comp z₂ ⋯) = (↑z₁).comp (δ n m z₂) ⋯

Tactic:
· simp [δ_shape _ _ hnm]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
p q : ℤ
hpq : p + 1 = q
⊢ (lift φ α β eq).f p = (↑α).v p q hpq ≫ (inl φ).v q p ⋯ + β.v p p ⋯ ≫ (inr φ).f p

Tactic:
simp [ext_to_iff _ _ _ hpq]

Goal state after:
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
X Y : C
smul : SMul R ((functor r).obj X ⟶ (functor r).obj Y) := Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
a : R
⊢ a • (functor r).map 0 = (functor r).map 0

Tactic:
smul_eq,

Goal state after:
R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
X Y : C
smul : SMul R ((functor r).obj X ⟶ (functor r).obj Y) := Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
a : R
⊢ (functor r).map (a • 0) = (functor r).map 0
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
X Y : C
smul : SMul R ((functor r).obj X ⟶ (functor r).obj Y) := Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
a : R
f g : X ⟶ Y
⊢ a • (functor r).map (f + g) = (functor r).map (a • f) + (functor r).map (a • g)

Tactic:
smul_eq,

Goal state after:
R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
X Y : C
smul : SMul R ((functor r).obj X ⟶ (functor r).obj Y) := Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
a : R
f g : X ⟶ Y
⊢ (functor r).map (a • (f + g)) = (functor r).map (a • f) + (functor r).map (a • g)
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F₁ F₂ : Quotient r ⥤ D
h : functor r ⋙ F₁ = functor r ⋙ F₂
⊢ F₁ = F₂

Tactic:
lift_unique r (functor r ⋙ F₂) _ F₂ rfl

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F₁ F₂ : Quotient r ⥤ D
h : functor r ⋙ F₁ = functor r ⋙ F₂
⊢ F₁ = lift r (functor r ⋙ F₂) ?m.62

C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F₁ F₂ : Quotient r ⥤ D
h : functor r ⋙ F₁ = functor r ⋙ F₂
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ F₂).map f₁ = (functor r ⋙ F₂).map f₂
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
this : (X Y : Quotient r) → Module R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (a • (functor r).map f) ≫ (functor r).map g = a • (functor r).map f ≫ (functor r).map g

Tactic:
Linear.smul_eq,

Goal state after:
R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
this : (X Y : Quotient r) → Module R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (functor r).map (a • f) ≫ (functor r).map g = a • (functor r).map f ≫ (functor r).map g
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
this : (X Y : Quotient r) → Module R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (functor r).map ((a • f) ≫ g) = a • (functor r).map (f ≫ g)

Tactic:
Linear.smul_eq,

Goal state after:
R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
this : (X Y : Quotient r) → Module R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (functor r).map ((a • f) ≫ g) = (functor r).map (a • f ≫ g)
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
this : (X Y : Quotient r) → Module R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (functor r).map f ≫ (a • (functor r).map g) = a • (functor r).map f ≫ (functor r).map g

Tactic:
Linear.smul_eq,

Goal state after:
R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
this : (X Y : Quotient r) → Module R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (functor r).map f ≫ (functor r).map (a • g) = a • (functor r).map f ≫ (functor r).map g
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
this : (X Y : Quotient r) → Module R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (functor r).map (f ≫ (a • g)) = a • (functor r).map (f ≫ g)

Tactic:
Linear.smul_eq,

Goal state after:
R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
this : (X Y : Quotient r) → Module R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (functor r).map (f ≫ (a • g)) = (functor r).map (a • f ≫ g)
Module: Mathlib.CategoryTheory.Shift.Quotient

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ (lift r F hF).map
        ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X) ≫
          (functor r).map ((shiftFunctorZero C A).inv.app X)) ≫
      (Functor.commShiftIso F 0).hom.app X =
    (lift r F hF).map ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
      (shiftFunctorZero D A).inv.app ((lift r F hF).obj ((functor r).obj X))

Tactic:
Functor.map_comp,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ ((lift r F hF).map ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
        (lift r F hF).map ((functor r).map ((shiftFunctorZero C A).inv.app X))) ≫
      (Functor.commShiftIso F 0).hom.app X =
    (lift r F hF).map ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
      (shiftFunctorZero D A).inv.app ((lift r F hF).obj ((functor r).obj X))
Module: Mathlib.CategoryTheory.Shift.Quotient

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
X : C
⊢ (lift r F hF).map
        ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X) ≫
          (shiftFunctor (Quotient r) b).map ((Functor.commShiftIso (functor r) a).inv.app X) ≫
            (Functor.commShiftIso (functor r) b).inv.app ((shiftFunctor C a).obj X) ≫
              (functor r).map ((shiftFunctorAdd C a b).inv.app X)) ≫
      F.map ((shiftFunctorAdd C a b).hom.app X) ≫
        (Functor.commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
          (shiftFunctor D b).map ((Functor.commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X) =
    (lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
      (LiftCommShift.iso F r hF b).hom.app ((shiftFunctor (Quotient r) a).obj ((functor r).obj X)) ≫
        (shiftFunctor D b).map ((LiftCommShift.iso F r hF a).hom.app ((functor r).obj X)) ≫
          (shiftFunctorAdd D a b).inv.app ((lift r F hF).obj ((functor r).obj X))

Tactic:
Functor.map_comp,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
X : C
⊢ ((lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
        (lift r F hF).map
          ((shiftFunctor (Quotient r) b).map ((Functor.commShiftIso (functor r) a).inv.app X) ≫
            (Functor.commShiftIso (functor r) b).inv.app ((shiftFunctor C a).obj X) ≫
              (functor r).map ((shiftFunctorAdd C a b).inv.app X))) ≫
      F.map ((shiftFunctorAdd C a b).hom.app X) ≫
        (Functor.commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
          (shiftFunctor D b).map ((Functor.commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X) =
    (lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
      (LiftCommShift.iso F r hF b).hom.app ((shiftFunctor (Quotient r) a).obj ((functor r).obj X)) ≫
        (shiftFunctor D b).map ((LiftCommShift.iso F r hF a).hom.app ((functor r).obj X)) ≫
          (shiftFunctorAdd D a b).inv.app ((lift r F hF).obj ((functor r).obj X))