awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.SnakeLemma
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact.{u_2, u_3, u_4} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact.{u_5, u_6, u_7} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : (⇑f₂ : (a : M₂) → M₃) ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst_13 : AddCommGroup K₂
inst_14 : Module R K₂
inst_15 : AddCommGroup K₃
inst_16 : Module R K₃
inst_17 : AddCommGroup C₁
inst_18 : Module R C₁
inst_19 : AddCommGroup C₂
inst_20 : Module R C₂
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact.{u_8, u_3, u_6} (M := K₂) (N := M₂) (P := N₂) (⇑ι₂ : (a : K₂) → M₂) (⇑i₂ : (a : M₂) → N₂)
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact.{u_9, u_4, u_7} (M := K₃) (N := M₃) (P := N₃) (⇑ι₃ : (a : K₃) → M₃) (⇑i₃ : (a : M₃) → N₃)
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact.{u_2, u_5, u_10} (M := M₁) (N := N₁) (P := C₁) (⇑i₁ : (a : M₁) → N₁) (⇑π₁ : (a : N₁) → C₁)
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact.{u_3, u_6, u_11} (M := M₂) (N := N₂) (P := C₂) (⇑i₂ : (a : M₂) → N₂) (⇑π₂ : (a : N₂) → C₂)
H₁ : ∀ (x : M₃), (f₂ : (a : M₂) → M₃) (σ x) = x
H₂ :
  ∀ (x : K₃),
    Eq.{u_6 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : N₂)
      ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)
x y : K₃
⊢ Eq.{u_6 + 1} (α := N₂)
    ((g₁ : (a : N₁) → N₂)
        (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x))) +
          ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) y)))) :
      N₂)
    ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x) + σ ((ι₃ : (a : K₃) → M₃) y)) : N₂)

Tactic:
simp only [map_add, H₂]

Premises used: map_add
-- Module: Mathlib.Algebra.Module.SnakeLemma
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact.{u_2, u_3, u_4} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact.{u_5, u_6, u_7} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : (⇑f₂ : (a : M₂) → M₃) ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst_13 : AddCommGroup K₂
inst_14 : Module R K₂
inst_15 : AddCommGroup K₃
inst_16 : Module R K₃
inst_17 : AddCommGroup C₁
inst_18 : Module R C₁
inst_19 : AddCommGroup C₂
inst_20 : Module R C₂
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact.{u_8, u_3, u_6} (M := K₂) (N := M₂) (P := N₂) (⇑ι₂ : (a : K₂) → M₂) (⇑i₂ : (a : M₂) → N₂)
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact.{u_9, u_4, u_7} (M := K₃) (N := M₃) (P := N₃) (⇑ι₃ : (a : K₃) → M₃) (⇑i₃ : (a : M₃) → N₃)
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact.{u_2, u_5, u_10} (M := M₁) (N := N₁) (P := C₁) (⇑i₁ : (a : M₁) → N₁) (⇑π₁ : (a : N₁) → C₁)
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact.{u_3, u_6, u_11} (M := M₂) (N := N₂) (P := C₂) (⇑i₂ : (a : M₂) → N₂) (⇑π₂ : (a : N₂) → C₂)
H₁ : ∀ (x : M₃), (f₂ : (a : M₂) → M₃) (σ x) = x
H₂ :
  ∀ (x : K₃),
    Eq.{u_6 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : N₂)
      ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)
x y : K₃
⊢ Eq.{u_10 + 1} (α := C₁) ((π₁ : (a : N₁) → C₁) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) (x + y))))) : C₁)
    ((π₁ : (a : N₁) → C₁)
        (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x))) +
          ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) y)))) :
      C₁)

Tactic:
exact eq_of_eq i₁ i₂ f₁ f₂ hf g₁ h₁ ρ hρ ι₃ π₁ hπ₁ (x + y) _ (H₁ _) _ (H₂ _)
        (σ (ι₃ x) + σ (ι₃ y)) (by simp only [map_add, H₁]) _ (by simp only [map_add, H₂])

Premises used: SnakeLemma.eq_of_eq, HAdd.hAdd, DFunLike.coe
-- Module: Mathlib.Algebra.Module.SnakeLemma
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact.{u_2, u_3, u_4} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact.{u_5, u_6, u_7} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : (⇑f₂ : (a : M₂) → M₃) ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst_13 : AddCommGroup K₂
inst_14 : Module R K₂
inst_15 : AddCommGroup K₃
inst_16 : Module R K₃
inst_17 : AddCommGroup C₁
inst_18 : Module R C₁
inst_19 : AddCommGroup C₂
inst_20 : Module R C₂
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact.{u_8, u_3, u_6} (M := K₂) (N := M₂) (P := N₂) (⇑ι₂ : (a : K₂) → M₂) (⇑i₂ : (a : M₂) → N₂)
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact.{u_9, u_4, u_7} (M := K₃) (N := M₃) (P := N₃) (⇑ι₃ : (a : K₃) → M₃) (⇑i₃ : (a : M₃) → N₃)
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact.{u_2, u_5, u_10} (M := M₁) (N := N₁) (P := C₁) (⇑i₁ : (a : M₁) → N₁) (⇑π₁ : (a : N₁) → C₁)
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact.{u_3, u_6, u_11} (M := M₂) (N := N₂) (P := C₂) (⇑i₂ : (a : M₂) → N₂) (⇑π₂ : (a : N₂) → C₂)
H₁ : ∀ (x : M₃), (f₂ : (a : M₂) → M₃) (σ x) = x
H₂ :
  ∀ (x : K₃),
    Eq.{u_6 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : N₂)
      ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)
r : R
x : K₃
simp :
  Eq.{u_10 + 1} (α := C₁) ((π₁ : (a : N₁) → C₁) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) (r • x))))) : C₁)
    ((π₁ : (a : N₁) → C₁) (r • ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : C₁)
⊢ (π₁ : (a : N₁) → C₁) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) (r • x))))) =
    HSMul.hSMul (α := R) (β := C₁) ((RingHom.id R : (a : R) → R) r : R)
      ((π₁ : (a : N₁) → C₁) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : C₁)

Tactic:
simp only [← map_smul, RingHom.id_apply]

Premises used: RingHom.id_apply, map_smul
-- Module: Mathlib.Algebra.Module.SnakeLemma
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact.{u_2, u_3, u_4} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact.{u_5, u_6, u_7} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : (⇑f₂ : (a : M₂) → M₃) ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst_13 : AddCommGroup K₂
inst_14 : Module R K₂
inst_15 : AddCommGroup K₃
inst_16 : Module R K₃
inst_17 : AddCommGroup C₁
inst_18 : Module R C₁
inst_19 : AddCommGroup C₂
inst_20 : Module R C₂
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact.{u_8, u_3, u_6} (M := K₂) (N := M₂) (P := N₂) (⇑ι₂ : (a : K₂) → M₂) (⇑i₂ : (a : M₂) → N₂)
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact.{u_9, u_4, u_7} (M := K₃) (N := M₃) (P := N₃) (⇑ι₃ : (a : K₃) → M₃) (⇑i₃ : (a : M₃) → N₃)
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact.{u_2, u_5, u_10} (M := M₁) (N := N₁) (P := C₁) (⇑i₁ : (a : M₁) → N₁) (⇑π₁ : (a : N₁) → C₁)
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact.{u_3, u_6, u_11} (M := M₂) (N := N₂) (P := C₂) (⇑i₂ : (a : M₂) → N₂) (⇑π₂ : (a : N₂) → C₂)
H₁ : ∀ (x : M₃), (f₂ : (a : M₂) → M₃) (σ x) = x
H₂ :
  ∀ (x : K₃),
    Eq.{u_6 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : N₂)
      ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)
r : R
x : K₃
⊢ Eq.{u_4 + 1} (α := M₃) ((f₂ : (a : M₂) → M₃) (r • σ ((ι₃ : (a : K₃) → M₃) x)) : M₃)
    ((ι₃ : (a : K₃) → M₃) (r • x) : M₃)

Tactic:
simp only [map_smul, H₁]

Premises used: map_smul
-- Module: Mathlib.Algebra.Module.SnakeLemma
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact.{u_2, u_3, u_4} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact.{u_5, u_6, u_7} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : (⇑f₂ : (a : M₂) → M₃) ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst_13 : AddCommGroup K₂
inst_14 : Module R K₂
inst_15 : AddCommGroup K₃
inst_16 : Module R K₃
inst_17 : AddCommGroup C₁
inst_18 : Module R C₁
inst_19 : AddCommGroup C₂
inst_20 : Module R C₂
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact.{u_8, u_3, u_6} (M := K₂) (N := M₂) (P := N₂) (⇑ι₂ : (a : K₂) → M₂) (⇑i₂ : (a : M₂) → N₂)
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact.{u_9, u_4, u_7} (M := K₃) (N := M₃) (P := N₃) (⇑ι₃ : (a : K₃) → M₃) (⇑i₃ : (a : M₃) → N₃)
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact.{u_2, u_5, u_10} (M := M₁) (N := N₁) (P := C₁) (⇑i₁ : (a : M₁) → N₁) (⇑π₁ : (a : N₁) → C₁)
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact.{u_3, u_6, u_11} (M := M₂) (N := N₂) (P := C₂) (⇑i₂ : (a : M₂) → N₂) (⇑π₂ : (a : N₂) → C₂)
H₁ : ∀ (x : M₃), (f₂ : (a : M₂) → M₃) (σ x) = x
H₂ :
  ∀ (x : K₃),
    Eq.{u_6 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : N₂)
      ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)
r : R
x : K₃
⊢ Eq.{u_6 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) (r • ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : N₂)
    ((i₂ : (a : M₂) → N₂) (r • σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)

Tactic:
simp only [map_smul, H₂]

Premises used: map_smul
-- Module: Mathlib.Algebra.Module.SnakeLemma
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact.{u_2, u_3, u_4} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact.{u_5, u_6, u_7} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : (⇑f₂ : (a : M₂) → M₃) ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst_13 : AddCommGroup K₂
inst_14 : Module R K₂
inst_15 : AddCommGroup K₃
inst_16 : Module R K₃
inst_17 : AddCommGroup C₁
inst_18 : Module R C₁
inst_19 : AddCommGroup C₂
inst_20 : Module R C₂
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact.{u_8, u_3, u_6} (M := K₂) (N := M₂) (P := N₂) (⇑ι₂ : (a : K₂) → M₂) (⇑i₂ : (a : M₂) → N₂)
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact.{u_9, u_4, u_7} (M := K₃) (N := M₃) (P := N₃) (⇑ι₃ : (a : K₃) → M₃) (⇑i₃ : (a : M₃) → N₃)
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact.{u_2, u_5, u_10} (M := M₁) (N := N₁) (P := C₁) (⇑i₁ : (a : M₁) → N₁) (⇑π₁ : (a : N₁) → C₁)
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact.{u_3, u_6, u_11} (M := M₂) (N := N₂) (P := C₂) (⇑i₂ : (a : M₂) → N₂) (⇑π₂ : (a : N₂) → C₂)
H₁ : ∀ (x : M₃), (f₂ : (a : M₂) → M₃) (σ x) = x
H₂ :
  ∀ (x : K₃),
    Eq.{u_6 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : N₂)
      ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)
r : R
x : K₃
⊢ Eq.{u_10 + 1} (α := C₁) ((π₁ : (a : N₁) → C₁) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) (r • x))))) : C₁)
    ((π₁ : (a : N₁) → C₁) (r • ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : C₁)

Tactic:
apply eq_of_eq i₁ i₂ f₁ f₂ hf g₁ h₁ ρ hρ ι₃ π₁ hπ₁ (r • x) _ (H₁ _) _ (H₂ _)
        (r • σ (ι₃ x)) (by simp only [map_smul, H₁]) _ (by simp only [map_smul, H₂])

Premises used: SnakeLemma.eq_of_eq, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.Algebra.Module.SnakeLemma
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact.{u_2, u_3, u_4} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact.{u_5, u_6, u_7} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : (⇑f₂ : (a : M₂) → M₃) ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₃ : Type u_9
C₁ : Type u_10
inst_13 : AddCommGroup K₃
inst_14 : Module R K₃
inst_15 : AddCommGroup C₁
inst_16 : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact.{u_9, u_4, u_7} (M := K₃) (N := M₃) (P := N₃) (⇑ι₃ : (a : K₃) → M₃) (⇑i₃ : (a : M₃) → N₃)
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact.{u_2, u_5, u_10} (M := M₁) (N := N₁) (P := C₁) (⇑i₁ : (a : M₁) → N₁) (⇑π₁ : (a : N₁) → C₁)
x : K₃
y : M₂
hy : Eq.{u_4 + 1} (α := M₃) ((f₂ : (a : M₂) → M₃) y : M₃) ((ι₃ : (a : K₃) → M₃) x : M₃)
z : N₁
hz : Eq.{u_6 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) z : N₂) ((i₂ : (a : M₂) → N₂) y : N₂)
⊢ Eq.{u_10 + 1} (α := C₁) ((δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁ : (a : K₃) → C₁) x : C₁)
    ((π₁ : (a : N₁) → C₁) z : C₁)

Tactic:
eq_of_eq i₁ i₂ f₁ f₂ hf g₁ h₁ ρ hρ ι₃ π₁ hπ₁ x _ (congr_fun hσ _) _
    (δ_aux i₂ i₃ f₂ g₁ g₂ hg h₂ σ hσ ρ hρ ι₃ hι₃ _) y hy z hz

Premises used: SnakeLemma.eq_of_eq, congr_fun, SnakeLemma.δ_aux
-- Module: Mathlib.Algebra.Module.SnakeLemma
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact.{u_2, u_3, u_4} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact.{u_5, u_6, u_7} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : (⇑f₂ : (a : M₂) → M₃) ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
inst_13 : AddCommGroup K₂
inst_14 : Module R K₂
inst_15 : AddCommGroup K₃
inst_16 : Module R K₃
inst_17 : AddCommGroup C₁
inst_18 : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact.{u_8, u_3, u_6} (M := K₂) (N := M₂) (P := N₂) (⇑ι₂ : (a : K₂) → M₂) (⇑i₂ : (a : M₂) → N₂)
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact.{u_9, u_4, u_7} (M := K₃) (N := M₃) (P := N₃) (⇑ι₃ : (a : K₃) → M₃) (⇑i₃ : (a : M₃) → N₃)
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact.{u_2, u_5, u_10} (M := M₁) (N := N₁) (P := C₁) (⇑i₁ : (a : M₁) → N₁) (⇑π₁ : (a : N₁) → C₁)
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective.{u_9 + 1, u_4 + 1} (α := K₃) (β := M₃) (⇑ι₃ : (a : K₃) → M₃)
⊢ ∀ (x : M₃), (f₂ : (a : M₂) → M₃) (σ x) = x

Tactic:
haveI H₁ : ∀ x, f₂ (σ x) = x := congr_fun hσ
-- Module: Mathlib.Algebra.Module.SnakeLemma
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact.{u_2, u_3, u_4} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact.{u_5, u_6, u_7} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : (⇑f₂ : (a : M₂) → M₃) ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
inst_13 : AddCommGroup K₂
inst_14 : Module R K₂
inst_15 : AddCommGroup K₃
inst_16 : Module R K₃
inst_17 : AddCommGroup C₁
inst_18 : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact.{u_8, u_3, u_6} (M := K₂) (N := M₂) (P := N₂) (⇑ι₂ : (a : K₂) → M₂) (⇑i₂ : (a : M₂) → N₂)
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact.{u_9, u_4, u_7} (M := K₃) (N := M₃) (P := N₃) (⇑ι₃ : (a : K₃) → M₃) (⇑i₃ : (a : M₃) → N₃)
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact.{u_2, u_5, u_10} (M := M₁) (N := N₁) (P := C₁) (⇑i₁ : (a : M₁) → N₁) (⇑π₁ : (a : N₁) → C₁)
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective.{u_9 + 1, u_4 + 1} (α := K₃) (β := M₃) (⇑ι₃ : (a : K₃) → M₃)
H₁ : ∀ (x : M₃), (f₂ : (a : M₂) → M₃) (σ x) = x
⊢ ∀ (x : K₃),
    Eq.{u_6 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : N₂)
      ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)

Tactic:
haveI H₂ := δ_aux i₂ i₃ f₂ g₁ g₂ hg h₂ σ hσ ρ hρ ι₃ hι₃
-- Module: Mathlib.Algebra.Module.SnakeLemma
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact.{u_2, u_3, u_4} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact.{u_5, u_6, u_7} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : (⇑f₂ : (a : M₂) → M₃) ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
inst_13 : AddCommGroup K₂
inst_14 : Module R K₂
inst_15 : AddCommGroup K₃
inst_16 : Module R K₃
inst_17 : AddCommGroup C₁
inst_18 : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact.{u_8, u_3, u_6} (M := K₂) (N := M₂) (P := N₂) (⇑ι₂ : (a : K₂) → M₂) (⇑i₂ : (a : M₂) → N₂)
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact.{u_9, u_4, u_7} (M := K₃) (N := M₃) (P := N₃) (⇑ι₃ : (a : K₃) → M₃) (⇑i₃ : (a : M₃) → N₃)
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact.{u_2, u_5, u_10} (M := M₁) (N := N₁) (P := C₁) (⇑i₁ : (a : M₁) → N₁) (⇑π₁ : (a : N₁) → C₁)
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective.{u_9 + 1, u_4 + 1} (α := K₃) (β := M₃) (⇑ι₃ : (a : K₃) → M₃)
H₁ : ∀ (x : M₃), (f₂ : (a : M₂) → M₃) (σ x) = x
H₂ :
  ∀ (x : K₃),
    Eq.{u_6 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : N₂)
      ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)
x : K₃
mp :
  Eq.{u_10 + 1} (α := C₁) ((δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁ : (a : K₃) → C₁) x : C₁)
      (0 : C₁) →
    Membership.mem (γ := Set K₃) (Set.range.{u_9, u_8 + 1} (ι := K₂) (⇑F : (a : K₂) → K₃)) x
mpr :
  Membership.mem (γ := Set K₃) (Set.range.{u_9, u_8 + 1} (ι := K₂) (⇑F : (a : K₂) → K₃)) x →
    Eq.{u_10 + 1} (α := C₁) ((δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁ : (a : K₃) → C₁) x : C₁)
      (0 : C₁)
⊢ Eq.{u_10 + 1} (α := C₁) ((δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁ : (a : K₃) → C₁) x : C₁)
      (0 : C₁) ↔
    Membership.mem (γ := Set K₃) (Set.range.{u_9, u_8 + 1} (ι := K₂) (⇑F : (a : K₂) → K₃)) x

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.SnakeLemma
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup N₂
inst_10 : Module R N₂
inst_11 : AddCommGroup N₃
inst_12 : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact.{u_2, u_3, u_4} (M := M₁) (N := M₂) (P := M₃) (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₂) → M₃)
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact.{u_5, u_6, u_7} (M := N₁) (N := N₂) (P := N₃) (⇑g₁ : (a : N₁) → N₂) (⇑g₂ : (a : N₂) → N₃)
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : (⇑f₂ : (a : M₂) → M₃) ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
inst_13 : AddCommGroup K₂
inst_14 : Module R K₂
inst_15 : AddCommGroup K₃
inst_16 : Module R K₃
inst_17 : AddCommGroup C₁
inst_18 : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact.{u_8, u_3, u_6} (M := K₂) (N := M₂) (P := N₂) (⇑ι₂ : (a : K₂) → M₂) (⇑i₂ : (a : M₂) → N₂)
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact.{u_9, u_4, u_7} (M := K₃) (N := M₃) (P := N₃) (⇑ι₃ : (a : K₃) → M₃) (⇑i₃ : (a : M₃) → N₃)
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact.{u_2, u_5, u_10} (M := M₁) (N := N₁) (P := C₁) (⇑i₁ : (a : M₁) → N₁) (⇑π₁ : (a : N₁) → C₁)
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective.{u_9 + 1, u_4 + 1} (α := K₃) (β := M₃) (⇑ι₃ : (a : K₃) → M₃)
H₁ : ∀ (x : M₃), (f₂ : (a : M₂) → M₃) (σ x) = x
H₂ :
  ∀ (x : K₃),
    Eq.{u_6 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : N₂)
      ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)
x : K₃
H :
  Eq.{u_10 + 1} (α := C₁) ((δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁ : (a : K₃) → C₁) x : C₁) (0 : C₁)
mp :
  ∀ (y : M₁) (hy : (i₁ : (a : M₁) → N₁) y = ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))),
    Membership.mem (γ := Set K₃) (Set.range.{u_9, u_8 + 1} (ι := K₂) (⇑F : (a : K₂) → K₃)) x
⊢ Membership.mem (γ := Set K₃) (Set.range.{u_9, u_8 + 1} (ι := K₂) (⇑F : (a : K₂) → K₃)) x

Tactic:
obtain ⟨y, hy⟩ := (hπ₁ _).mp H

Premises used: Iff.mp