awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Rat
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Module ℚ M
n : ℕ
hn : n ≠ 0
x y : M
hxy : Eq.{u_1 + 1} (α := M) ((fun (a : M) ↦ n • a) x) ((fun (a : M) ↦ n • a) y)
⊢ x = y

Tactic:
simpa [← Nat.cast_smul_eq_nsmul ℚ n, *] using congr((n⁻¹ : ℚ) • $hxy)

Premises used: Rat, Nat.cast, Inv.inv, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Algebra.Module.SnakeLemma
Goal:
R : Type u_1
inst : CommRing R
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 N₁
inst_6 : Module R N₁
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
inst_9 : AddCommGroup N₃
inst_10 : Module R N₃
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₂ : M₂ →ₗ[R] 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₂
σ : M₃ → M₂
hσ : (⇑f₂ : (a : M₂) → M₃) ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₃ : Type u_9
inst_11 : AddCommGroup K₃
inst_12 : Module R K₃
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact.{u_9, u_4, u_7} (M := K₃) (N := M₃) (P := N₃) (⇑ι₃ : (a : K₃) → M₃) (⇑i₃ : (a : M₃) → N₃)
x : K₃
rw : Membership.mem (α := N₂) g₂.ker ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)
rw₁ :
  Eq.{u_7 + 1} (α := N₃) ((g₂ : (a : N₂) → N₃) ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂) : N₃) (0 : N₃)
rw₂ :
  Eq.{u_7 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) (σ ((ι₃ : (a : K₃) → M₃) x)) : M₃) : N₃) (0 : N₃)
rw₃ : Eq.{u_7 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) (((⇑f₂ : (a : M₂) → M₃) ∘ σ) ((ι₃ : (a : K₃) → M₃) x)) : N₃) (0 : N₃)
rw₄ : Eq.{u_7 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) (id ((ι₃ : (a : K₃) → M₃) x) : M₃) : N₃) (0 : N₃)
rw₅ : Eq.{u_7 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((ι₃ : (a : K₃) → M₃) x : M₃) : N₃) (0 : N₃)
rw₆ : Eq.{u_7 + 1} (α := N₃) ((i₃ ∘ₗ ι₃ : (a : K₃) → N₃) x : N₃) (0 : N₃)
rw₇ : Eq.{u_7 + 1} (α := N₃) ((0 : (a : K₃) → N₃) x : N₃) (0 : N₃)
rw₈ rw₉ : Eq.{u_7 + 1} (α := N₃) 0 0
⊢ Membership.mem (α := N₂) g₁.range ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)

Tactic:
rw [← hg.linearMap_ker_eq, mem_ker, show g₂ (i₂ _) = i₃ (f₂ _) from DFunLike.congr_fun h₂ _,
      ← @comp_apply _ _ _ f₂ σ, hσ, id_eq, ← i₃.comp_apply,
      hι₃.linearMap_comp_eq_zero, zero_apply]

Premises used: LinearMap.zero_apply, DFunLike.congr_fun, Function.Exact.linearMap_ker_eq, LinearMap.comp_apply, LinearMap.mem_ker, Function.Exact.linearMap_comp_eq_zero, Function.comp_apply, id_eq
-- Module: Mathlib.Algebra.Module.SnakeLemma
Goal:
R : Type u_1
inst : CommRing R
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 N₁
inst_6 : Module R N₁
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
inst_9 : AddCommGroup N₃
inst_10 : Module R N₃
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₂ : M₂ →ₗ[R] 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₂
σ : M₃ → M₂
hσ : (⇑f₂ : (a : M₂) → M₃) ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₃ : Type u_9
inst_11 : AddCommGroup K₃
inst_12 : Module R K₃
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact.{u_9, u_4, u_7} (M := K₃) (N := M₃) (P := N₃) (⇑ι₃ : (a : K₃) → M₃) (⇑i₃ : (a : M₃) → N₃)
x : K₃
obtain :
  ∀ (d : N₁)
    (hd :
      Eq.{u_6 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) d : N₂) ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)),
    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₂)
⊢ 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:
obtain ⟨d, hd⟩ : i₂ (σ (ι₃ x)) ∈ range g₁ := by
    rw [← hg.linearMap_ker_eq, mem_ker, show g₂ (i₂ _) = i₃ (f₂ _) from DFunLike.congr_fun h₂ _,
      ← @comp_apply _ _ _ f₂ σ, hσ, id_eq, ← i₃.comp_apply,
      hι₃.linearMap_comp_eq_zero, zero_apply]

Premises used: LinearMap.range, DFunLike.coe
-- Module: Mathlib.Algebra.Module.SnakeLemma
Goal:
R : Type u_1
inst : CommRing R
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 N₁
inst_6 : Module R N₁
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
inst_9 : AddCommGroup N₃
inst_10 : Module R N₃
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₂ : M₂ →ₗ[R] 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₂
σ : M₃ → M₂
hσ : (⇑f₂ : (a : M₂) → M₃) ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₃ : Type u_9
inst_11 : AddCommGroup K₃
inst_12 : Module R K₃
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact.{u_9, u_4, u_7} (M := K₃) (N := M₃) (P := N₃) (⇑ι₃ : (a : K₃) → M₃) (⇑i₃ : (a : M₃) → N₃)
x : K₃
d : N₁
hd : Eq.{u_6 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) d : N₂) ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)
rw : Eq.{u_6 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) (ρ ((g₁ : (a : N₁) → N₂) d)) : N₂) ((g₁ : (a : N₁) → N₂) d : N₂)
rw₁ : Eq.{u_6 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) ((ρ ∘ (⇑g₁ : (a : N₁) → N₂)) d) : N₂) ((g₁ : (a : N₁) → N₂) d : N₂)
rw₂ : Eq.{u_6 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) (id d) : N₂) ((g₁ : (a : N₁) → N₂) d : N₂)
rw₃ rw₄ : Eq.{u_6 + 1} (α := N₂) ((g₁ : (a : N₁) → N₂) d : N₂) ((g₁ : (a : N₁) → N₂) d : N₂)
⊢ 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:
rw [← hd, ← ρ.comp_apply, hρ, id_eq]

Premises used: Function.comp_apply, id_eq
-- 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
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₂
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₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₃ : Type u_9
C₁ : Type u_10
inst_11 : AddCommGroup K₃
inst_12 : Module R K₃
inst_13 : AddCommGroup C₁
inst_14 : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : 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₂)
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₂)
⊢ HSub.hSub (α := M₃) (β := M₃) ((f₂ : (a : M₂) → M₃) y₁ : M₃) ((f₂ : (a : M₂) → M₃) y₂ : M₃) = 0

Tactic:
have := sub_eq_zero.mpr (hy₁.trans 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
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₂
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₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₃ : Type u_9
C₁ : Type u_10
inst_11 : AddCommGroup K₃
inst_12 : Module R K₃
inst_13 : AddCommGroup C₁
inst_14 : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : 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₂)
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₂)
this : HSub.hSub (α := M₃) (β := M₃) ((f₂ : (a : M₂) → M₃) y₁ : M₃) ((f₂ : (a : M₂) → M₃) y₂ : M₃) = 0
⊢ Membership.mem (γ := Set M₂) (Set.range.{u_3, u_2 + 1} (ι := M₁) (⇑f₁ : (a : M₁) → M₂)) (y₁ - y₂)

Tactic:
rw [← map_sub, hf] at this

Premises used: map_sub
-- 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
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₂
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₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₃ : Type u_9
C₁ : Type u_10
inst_11 : AddCommGroup K₃
inst_12 : Module R K₃
inst_13 : AddCommGroup C₁
inst_14 : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : 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₂)
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₂)
this : Membership.mem (γ := Set M₂) (Set.range.{u_3, u_2 + 1} (ι := M₁) (⇑f₁ : (a : M₁) → M₂)) (y₁ - y₂)
obtain :
  ∀ (d : M₁) (hd : (f₁ : (a : M₁) → M₂) d = y₁ - y₂),
    Eq.{u_10 + 1} (α := C₁) ((π₁ : (a : N₁) → C₁) z₁ : C₁) ((π₁ : (a : N₁) → C₁) z₂ : C₁)
⊢ Eq.{u_10 + 1} (α := C₁) ((π₁ : (a : N₁) → C₁) z₁ : C₁) ((π₁ : (a : N₁) → C₁) z₂ : C₁)

Tactic:
obtain ⟨d, hd⟩ := this
-- 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
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₂
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₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₃ : Type u_9
C₁ : Type u_10
inst_11 : AddCommGroup K₃
inst_12 : Module R K₃
inst_13 : AddCommGroup C₁
inst_14 : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : 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₂)
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₂)
d : M₁
hd : (f₁ : (a : M₁) → M₂) d = y₁ - y₂
⊢ z₁ - z₂ = (i₁ : (a : M₁) → N₁) d

Tactic:
rw [← eq_sub_iff_add_eq.mp hd, map_add, ← hz₂, ← sub_eq_iff_eq_add, ← map_sub,
    ← i₂.comp_apply, ← h₁, LinearMap.comp_apply,
    (HasLeftInverse.injective ⟨ρ, congr_fun hρ⟩).eq_iff] at hz₁

Premises used: map_sub, Function.HasLeftInverse.injective, Function.Injective.eq_iff, eq_sub_iff_add_eq, LinearMap.comp_apply, map_add, sub_eq_iff_eq_add, Exists.intro, Iff.mp, congr_fun
-- 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
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₂
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₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₃ : Type u_9
C₁ : Type u_10
inst_11 : AddCommGroup K₃
inst_12 : Module R K₃
inst_13 : AddCommGroup C₁
inst_14 : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : 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₂)
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₂)
d : M₁
hd : (f₁ : (a : M₁) → M₂) d = y₁ - y₂
hz₃ : z₁ - z₂ = (i₁ : (a : M₁) → N₁) d
⊢ (f₁ : (a : M₁) → M₂) d = y₁ - y₂

Tactic:
rw [← eq_sub_iff_add_eq.mp hd, map_add, ← hz₂, ← sub_eq_iff_eq_add, ← map_sub,
    ← i₂.comp_apply, ← h₁, LinearMap.comp_apply,
    (HasLeftInverse.injective ⟨ρ, congr_fun hρ⟩).eq_iff] at hz₁

Premises used: map_sub, Function.HasLeftInverse.injective, Function.Injective.eq_iff, eq_sub_iff_add_eq, LinearMap.comp_apply, map_add, sub_eq_iff_eq_add, Exists.intro, Iff.mp, congr_fun
-- 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
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₂
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₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₃ : Type u_9
C₁ : Type u_10
inst_11 : AddCommGroup K₃
inst_12 : Module R K₃
inst_13 : AddCommGroup C₁
inst_14 : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : 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₁
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₂)
d : M₁
hz₁ : z₁ - z₂ = (i₁ : (a : M₁) → N₁) d
hd : (f₁ : (a : M₁) → M₂) d = y₁ - y₂
rw :
  Membership.mem.{u_5, u_5} (α := N₁) (γ := Set N₁) (Set.range.{u_5, u_2 + 1} (ι := M₁) (⇑i₁ : (a : M₁) → N₁))
    ((i₁ : (a : M₁) → N₁) d : N₁)
⊢ Eq.{u_10 + 1} (α := C₁) ((π₁ : (a : N₁) → C₁) z₁ : C₁) ((π₁ : (a : N₁) → C₁) z₂ : C₁)

Tactic:
rw [← sub_eq_zero, ← map_sub, hz₁, hπ₁]

Premises used: map_sub, sub_eq_zero
-- 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
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₂
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₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₃ : Type u_9
C₁ : Type u_10
inst_11 : AddCommGroup K₃
inst_12 : Module R K₃
inst_13 : AddCommGroup C₁
inst_14 : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : 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₁
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₂)
d : M₁
hz₁ : z₁ - z₂ = (i₁ : (a : M₁) → N₁) d
hd : (f₁ : (a : M₁) → M₂) d = y₁ - y₂
⊢ Membership.mem.{u_5, u_5} (α := N₁) (γ := Set N₁) (Set.range.{u_5, u_2 + 1} (ι := M₁) (⇑i₁ : (a : M₁) → N₁))
    ((i₁ : (a : M₁) → N₁) d : N₁)

Tactic:
⟨_, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, 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
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₂
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₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ (⇑g₁ : (a : N₁) → N₂) = id
K₃ : Type u_9
C₁ : Type u_10
inst_11 : AddCommGroup K₃
inst_12 : Module R K₃
inst_13 : AddCommGroup C₁
inst_14 : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : 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₁
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₂)
d : M₁
hz₁ : z₁ - z₂ = (i₁ : (a : M₁) → N₁) d
hd : (f₁ : (a : M₁) → M₂) d = y₁ - y₂
⊢ Membership.mem.{u_5, u_5} (α := N₁) (γ := Set N₁) (Set.range.{u_5, u_2 + 1} (ι := M₁) (⇑i₁ : (a : M₁) → N₁))
    ((i₁ : (a : M₁) → N₁) d : N₁)

Tactic:
exact ⟨_, 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_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₃
rw :
  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₁)
⊢ (π₁ : (a : N₁) → C₁) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) (x + y))))) =
    HAdd.hAdd (α := C₁) (β := C₁) ((π₁ : (a : N₁) → C₁) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)))) : C₁)
      ((π₁ : (a : N₁) → C₁) (ρ ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) y)))) : C₁)

Tactic:
rw [← map_add]

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_4 + 1} (α := M₃) ((f₂ : (a : M₂) → M₃) (σ ((ι₃ : (a : K₃) → M₃) x) + σ ((ι₃ : (a : K₃) → M₃) y)) : M₃)
    ((ι₃ : (a : K₃) → M₃) (x + y) : M₃)

Tactic:
simp only [map_add, H₁]

Premises used: map_add