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_9
C₁ : Type u_10
C₂ : Type u_11
inst_13 : AddCommGroup K₃
inst_14 : Module R K₃
inst_15 : AddCommGroup C₁
inst_16 : Module R C₁
inst_17 : AddCommGroup C₂
inst_18 : 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₁)
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact.{u_3, u_6, u_11} (M := M₂) (N := N₂) (P := C₂) (⇑i₂ : (a : M₂) → N₂) (⇑π₂ : (a : N₂) → C₂)
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective.{u_5 + 1, u_10 + 1} (α := N₁) (β := C₁) (⇑π₁ : (a : N₁) → C₁)
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 : C₁
H : Eq.{u_11 + 1} (α := C₂) ((G : (a : C₁) → C₂) x : C₂) (0 : C₂)
mp :
  ∀ (x : N₁) (H : Eq.{u_11 + 1} (α := C₂) ((G : (a : C₁) → C₂) ((π₁ : (a : N₁) → C₁) x : C₁) : C₂) (0 : C₂)),
    Membership.mem.{u_10, u_10} (α := C₁) (γ := Set C₁)
      (Set.range.{u_10, u_9 + 1} (ι := K₃)
        (⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) : (a : K₃) → C₁))
      ((π₁ : (a : N₁) → C₁) x : C₁)
⊢ Membership.mem (γ := Set C₁)
    (Set.range.{u_10, u_9 + 1} (ι := K₃)
      (⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) : (a : K₃) → C₁))
    x

Tactic:
obtain ⟨x, rfl⟩ := h x

Premises used: rfl
-- 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
C₂ : Type u_11
inst_13 : AddCommGroup K₃
inst_14 : Module R K₃
inst_15 : AddCommGroup C₁
inst_16 : Module R C₁
inst_17 : AddCommGroup C₂
inst_18 : 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₁)
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact.{u_3, u_6, u_11} (M := M₂) (N := N₂) (P := C₂) (⇑i₂ : (a : M₂) → N₂) (⇑π₂ : (a : N₂) → C₂)
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective.{u_5 + 1, u_10 + 1} (α := N₁) (β := C₁) (⇑π₁ : (a : N₁) → C₁)
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 : N₁
H : Eq.{u_11 + 1} (α := C₂) ((G : (a : C₁) → C₂) ((π₁ : (a : N₁) → C₁) x : C₁) : C₂) (0 : C₂)
⊢ Eq.{u_11 + 1} (α := C₂) ((π₂ : (a : N₂) → C₂) ((g₁ : (a : N₁) → N₂) x : N₂) : C₂) (0 : C₂)

Tactic:
simpa only [← LinearMap.comp_apply, hF] using H

Premises used: LinearMap.comp_apply
-- 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
C₂ : Type u_11
inst_13 : AddCommGroup K₃
inst_14 : Module R K₃
inst_15 : AddCommGroup C₁
inst_16 : Module R C₁
inst_17 : AddCommGroup C₂
inst_18 : 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₁)
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact.{u_3, u_6, u_11} (M := M₂) (N := N₂) (P := C₂) (⇑i₂ : (a : M₂) → N₂) (⇑π₂ : (a : N₂) → C₂)
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective.{u_5 + 1, u_10 + 1} (α := N₁) (β := C₁) (⇑π₁ : (a : N₁) → C₁)
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 : N₁
H : Eq.{u_11 + 1} (α := C₂) ((G : (a : C₁) → C₂) ((π₁ : (a : N₁) → C₁) x : C₁) : C₂) (0 : C₂)
mp :
  ∀ (y : M₂) (hy : Eq.{u_6 + 1} (α := N₂) ((i₂ : (a : M₂) → N₂) y : N₂) ((g₁ : (a : N₁) → N₂) x : N₂)),
    Membership.mem.{u_10, u_10} (α := C₁) (γ := Set C₁)
      (Set.range.{u_10, u_9 + 1} (ι := K₃)
        (⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) : (a : K₃) → C₁))
      ((π₁ : (a : N₁) → C₁) x : C₁)
⊢ Membership.mem.{u_10, u_10} (α := C₁) (γ := Set C₁)
    (Set.range.{u_10, u_9 + 1} (ι := K₃)
      (⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) : (a : K₃) → C₁))
    ((π₁ : (a : N₁) → C₁) x : C₁)

Tactic:
obtain ⟨y, hy⟩ := (hπ₂ (g₁ x)).mp (by simpa only [← LinearMap.comp_apply, hF] using H)

Premises used: Iff.mp, 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
C₂ : Type u_11
inst_13 : AddCommGroup K₃
inst_14 : Module R K₃
inst_15 : AddCommGroup C₁
inst_16 : Module R C₁
inst_17 : AddCommGroup C₂
inst_18 : 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₁)
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact.{u_3, u_6, u_11} (M := M₂) (N := N₂) (P := C₂) (⇑i₂ : (a : M₂) → N₂) (⇑π₂ : (a : N₂) → C₂)
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective.{u_5 + 1, u_10 + 1} (α := N₁) (β := C₁) (⇑π₁ : (a : N₁) → C₁)
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 : N₁
H : Eq.{u_11 + 1} (α := C₂) ((G : (a : C₁) → C₂) ((π₁ : (a : N₁) → C₁) x : C₁) : C₂) (0 : C₂)
y : M₂
hy : Eq.{u_6 + 1} (α := N₂) ((i₂ : (a : M₂) → N₂) y : N₂) ((g₁ : (a : N₁) → N₂) x : N₂)
rw : Eq.{u_7 + 1} (α := N₃) ((i₃ ∘ₗ f₂ : (a : M₂) → N₃) y : N₃) (0 : N₃)
rw₁ : Eq.{u_7 + 1} (α := N₃) ((g₂ ∘ₗ i₂ : (a : M₂) → N₃) y : N₃) (0 : N₃)
rw₂ : Eq.{u_7 + 1} (α := N₃) ((g₂ : (a : N₂) → N₃) ((i₂ : (a : M₂) → N₂) y : N₂) : N₃) (0 : N₃)
rw₃ : Eq.{u_7 + 1} (α := N₃) ((g₂ : (a : N₂) → N₃) ((g₁ : (a : N₁) → N₂) x : N₂) : N₃) (0 : N₃)
rw₄ rw₅ : Eq.{u_7 + 1} (α := N₃) 0 0
⊢ Eq.{u_7 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) y : M₃) : N₃) (0 : N₃)

Tactic:
rw [← i₃.comp_apply, ← h₂,
      g₂.comp_apply, hy, hg.apply_apply_eq_zero]

Premises used: Function.Exact.apply_apply_eq_zero, LinearMap.comp_apply
-- 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
C₂ : Type u_11
inst_13 : AddCommGroup K₃
inst_14 : Module R K₃
inst_15 : AddCommGroup C₁
inst_16 : Module R C₁
inst_17 : AddCommGroup C₂
inst_18 : 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₁)
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact.{u_3, u_6, u_11} (M := M₂) (N := N₂) (P := C₂) (⇑i₂ : (a : M₂) → N₂) (⇑π₂ : (a : N₂) → C₂)
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective.{u_5 + 1, u_10 + 1} (α := N₁) (β := C₁) (⇑π₁ : (a : N₁) → C₁)
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 : N₁
H : Eq.{u_11 + 1} (α := C₂) ((G : (a : C₁) → C₂) ((π₁ : (a : N₁) → C₁) x : C₁) : C₂) (0 : C₂)
y : M₂
hy : Eq.{u_6 + 1} (α := N₂) ((i₂ : (a : M₂) → N₂) y : N₂) ((g₁ : (a : N₁) → N₂) x : N₂)
mp :
  ∀ (z : K₃) (hz : Eq.{u_4 + 1} (α := M₃) ((ι₃ : (a : K₃) → M₃) z : M₃) ((f₂ : (a : M₂) → M₃) y : M₃)),
    Membership.mem.{u_10, u_10} (α := C₁) (γ := Set C₁)
      (Set.range.{u_10, u_9 + 1} (ι := K₃)
        (⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) : (a : K₃) → C₁))
      ((π₁ : (a : N₁) → C₁) x : C₁)
⊢ Membership.mem.{u_10, u_10} (α := C₁) (γ := Set C₁)
    (Set.range.{u_10, u_9 + 1} (ι := K₃)
      (⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) : (a : K₃) → C₁))
    ((π₁ : (a : N₁) → C₁) x : C₁)

Tactic:
obtain ⟨z, hz⟩ : f₂ y ∈ range ι₃ := (hι₃ (f₂ y)).mp (by rw [← i₃.comp_apply, ← h₂,
      g₂.comp_apply, hy, hg.apply_apply_eq_zero])

Premises used: LinearMap.range, Iff.mp, 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
C₂ : Type u_11
inst_13 : AddCommGroup K₃
inst_14 : Module R K₃
inst_15 : AddCommGroup C₁
inst_16 : Module R C₁
inst_17 : AddCommGroup C₂
inst_18 : 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₁)
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact.{u_3, u_6, u_11} (M := M₂) (N := N₂) (P := C₂) (⇑i₂ : (a : M₂) → N₂) (⇑π₂ : (a : N₂) → C₂)
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective.{u_5 + 1, u_10 + 1} (α := N₁) (β := C₁) (⇑π₁ : (a : N₁) → C₁)
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 : N₁
H : Eq.{u_11 + 1} (α := C₂) ((G : (a : C₁) → C₂) ((π₁ : (a : N₁) → C₁) x : C₁) : C₂) (0 : C₂)
y : M₂
hy : Eq.{u_6 + 1} (α := N₂) ((i₂ : (a : M₂) → N₂) y : N₂) ((g₁ : (a : N₁) → N₂) x : N₂)
z : K₃
hz : Eq.{u_4 + 1} (α := M₃) ((ι₃ : (a : K₃) → M₃) z : M₃) ((f₂ : (a : M₂) → M₃) y : M₃)
⊢ Membership.mem.{u_10, u_10} (α := C₁) (γ := Set C₁)
    (Set.range.{u_10, u_9 + 1} (ι := K₃)
      (⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) : (a : K₃) → C₁))
    ((π₁ : (a : N₁) → C₁) x : C₁)

Tactic:
⟨z, δ_eq i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁ _ _ hz.symm _ hy.symm⟩

Premises used: Set.Mem, setOf, SnakeLemma.δ_eq, Exists.intro, Set.range, Eq.symm
-- 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
C₂ : Type u_11
inst_13 : AddCommGroup K₃
inst_14 : Module R K₃
inst_15 : AddCommGroup C₁
inst_16 : Module R C₁
inst_17 : AddCommGroup C₂
inst_18 : 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₁)
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact.{u_3, u_6, u_11} (M := M₂) (N := N₂) (P := C₂) (⇑i₂ : (a : M₂) → N₂) (⇑π₂ : (a : N₂) → C₂)
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective.{u_5 + 1, u_10 + 1} (α := N₁) (β := C₁) (⇑π₁ : (a : N₁) → C₁)
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 : N₁
H : Eq.{u_11 + 1} (α := C₂) ((G : (a : C₁) → C₂) ((π₁ : (a : N₁) → C₁) x : C₁) : C₂) (0 : C₂)
y : M₂
hy : Eq.{u_6 + 1} (α := N₂) ((i₂ : (a : M₂) → N₂) y : N₂) ((g₁ : (a : N₁) → N₂) x : N₂)
z : K₃
hz : Eq.{u_4 + 1} (α := M₃) ((ι₃ : (a : K₃) → M₃) z : M₃) ((f₂ : (a : M₂) → M₃) y : M₃)
⊢ Membership.mem.{u_10, u_10} (α := C₁) (γ := Set C₁)
    (Set.range.{u_10, u_9 + 1} (ι := K₃)
      (⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) : (a : K₃) → C₁))
    ((π₁ : (a : N₁) → C₁) x : C₁)

Tactic:
exact ⟨z, δ_eq i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁ _ _ hz.symm _ hy.symm⟩
-- 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
C₂ : Type u_11
inst_13 : AddCommGroup K₃
inst_14 : Module R K₃
inst_15 : AddCommGroup C₁
inst_16 : Module R C₁
inst_17 : AddCommGroup C₂
inst_18 : 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₁)
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact.{u_3, u_6, u_11} (M := M₂) (N := N₂) (P := C₂) (⇑i₂ : (a : M₂) → N₂) (⇑π₂ : (a : N₂) → C₂)
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective.{u_5 + 1, u_10 + 1} (α := N₁) (β := C₁) (⇑π₁ : (a : N₁) → C₁)
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₃
mpr :
  Eq.{u_11 + 1} (α := C₂)
    ((G : (a : C₁) → C₂) ((π₁ : (a : N₁) → C₁) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : C₁) : C₂)
    (0 : C₂)
⊢ Eq.{u_11 + 1} (α := C₂)
    ((G : (a : C₁) → C₂) ((δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁ : (a : K₃) → C₁) x : C₁) : C₂)
    (0 : C₂)

Tactic:
simp only [δ, coe_mk, AddHom.coe_mk]

Premises used: LinearMap.coe_mk, SnakeLemma.δ, AddHom.coe_mk
-- 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
C₂ : Type u_11
inst_13 : AddCommGroup K₃
inst_14 : Module R K₃
inst_15 : AddCommGroup C₁
inst_16 : Module R C₁
inst_17 : AddCommGroup C₂
inst_18 : 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₁)
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact.{u_3, u_6, u_11} (M := M₂) (N := N₂) (P := C₂) (⇑i₂ : (a : M₂) → N₂) (⇑π₂ : (a : N₂) → C₂)
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective.{u_5 + 1, u_10 + 1} (α := N₁) (β := C₁) (⇑π₁ : (a : N₁) → C₁)
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₃
mpr :
  Eq.{u_11 + 1} (α := C₂) ((G ∘ₗ π₁ : (a : N₁) → C₂) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : C₂)
    (0 : C₂)
mpr₁ :
  Eq.{u_11 + 1} (α := C₂) ((π₂ ∘ₗ g₁ : (a : N₁) → C₂) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : C₂)
    (0 : C₂)
mpr₂ :
  Eq.{u_11 + 1} (α := C₂)
    ((π₂ : (a : N₂) → C₂) ((g₁ : (a : N₁) → N₂) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : N₂) : C₂)
    (0 : C₂)
mpr₃ :
  Eq.{u_11 + 1} (α := C₂) ((π₂ : (a : N₂) → C₂) ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂) : C₂) (0 : C₂)
mpr₄ mpr₅ : Eq.{u_11 + 1} (α := C₂) 0 0
⊢ Eq.{u_11 + 1} (α := C₂)
    ((G : (a : C₁) → C₂) ((π₁ : (a : N₁) → C₁) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : C₁) : C₂)
    (0 : C₂)

Tactic:
rw [← G.comp_apply, hF, π₂.comp_apply, H₂, hπ₂.apply_apply_eq_zero]

Premises used: Function.Exact.apply_apply_eq_zero, LinearMap.comp_apply
-- 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₂
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₁)
hf₂ : Surjective.{u_3 + 1, u_4 + 1} (α := M₂) (β := M₃) (⇑f₂ : (a : M₂) → M₃)
hg₁ : Injective.{u_5 + 1, u_6 + 1} (α := N₁) (β := N₂) (⇑g₁ : (a : N₁) → N₂)
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π₁ hf₂ hg₁ : (a : K₃) → C₁) x : C₁)
    ((π₁ : (a : N₁) → C₁) z : C₁)

Tactic:
SnakeLemma.δ_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ‹_› ‹_› _ ‹_›

Premises used: SnakeLemma.δ_eq