awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Rat (goal)
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_3
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
c : ℚ
x : M
rw :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
rw₁ :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₂ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₃ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
rw₄ :
  (f : (a : M) → M₂)
      (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.num : R) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x)) =
    HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c : R) x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
have rw₅ : (f : (a : M) → M₂)
    (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.num : R) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x)) =
  HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
    (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂))
Tactic: rw [Rat.cast_def, Rat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_intCast_smul f R S, map_inv_natCast_smul f R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Rat (goal)
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_3
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
c : ℚ
x : M
rw :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
rw₁ :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₂ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₃ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
rw₄ :
  (f : (a : M) → M₂)
      (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.num : R) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x)) =
    HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
rw₅ :
  (f : (a : M) → M₂)
      (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.num : R) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x)) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
      (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂))
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c : R) x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
have rw₆ : HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.num : S)
    ((f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x) : M₂) =
  HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
    (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂))
Tactic: rw [Rat.cast_def, Rat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_intCast_smul f R S, map_inv_natCast_smul f R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Rat (goal)
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_3
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
c : ℚ
x : M
rw :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
rw₁ :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₂ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₃ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
rw₄ :
  (f : (a : M) → M₂)
      (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.num : R) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x)) =
    HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
rw₅ :
  (f : (a : M) → M₂)
      (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.num : R) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x)) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
      (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂))
rw₆ :
  HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.num : S)
      ((f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x) : M₂) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
      (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂))
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c : R) x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
have rw₇ : HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
    (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂)) =
  HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
    (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂))
Tactic: rw [Rat.cast_def, Rat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_intCast_smul f R S, map_inv_natCast_smul f R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Rat (goal)
Goal:
M : Type u_1
R : Type u_3
inst : DivisionSemiring R
inst_1 : MulAction R M
inst_2 : MulAction ℚ≥0 M
inst_3 : IsScalarTower ℚ≥0 R M
q : ℚ≥0
x : M
⊢ HSMul.hSMul.{u_3, u_1, u_1} (α := R) (↑q : R) x = q • x
have rw : HSMul.hSMul (α := R) (β := R) (↑q : R) 1 • x = HSMul.hSMul (β := R) q 1 • x
Tactic: rw [← one_smul R x, ← smul_assoc, ← smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.Rat (goal)
Goal:
M : Type u_1
R : Type u_3
inst : DivisionRing R
inst_1 : MulAction R M
inst_2 : MulAction ℚ M
inst_3 : IsScalarTower ℚ R M
q : ℚ
x : M
⊢ HSMul.hSMul.{u_3, u_1, u_1} (α := R) (↑q : R) x = q • x
have rw : HSMul.hSMul (α := R) (β := R) (↑q : R) 1 • x = HSMul.hSMul (β := R) q 1 • x
Tactic: rw [← one_smul R x, ← smul_assoc, ← smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.SnakeLemma (goal)
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₃
⊢ Membership.mem (α := N₂) g₁.range ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)
have rw : Membership.mem (α := N₂) g₂.ker ((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]
-- Lean 4 proof step from Mathlib.Algebra.Module.SnakeLemma (goal)
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₂)
⊢ Membership.mem (α := N₂) g₁.range ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)
have rw₁ : Eq.{u_7 + 1} (α := N₃) ((g₂ : (a : N₂) → N₃) ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂) : N₃) (0 : 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]
-- Lean 4 proof step from Mathlib.Algebra.Module.SnakeLemma (goal)
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₃)
⊢ Membership.mem (α := N₂) g₁.range ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)
have rw₂ : Eq.{u_7 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((f₂ : (a : M₂) → M₃) (σ ((ι₃ : (a : K₃) → M₃) x)) : M₃) : N₃) (0 : 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]
-- Lean 4 proof step from Mathlib.Algebra.Module.SnakeLemma (goal)
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₃)
⊢ Membership.mem (α := N₂) g₁.range ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)
have rw₃ : Eq.{u_7 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) (((⇑f₂ : (a : M₂) → M₃) ∘ σ) ((ι₃ : (a : K₃) → M₃) x)) : N₃) (0 : 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]
-- Lean 4 proof step from Mathlib.Algebra.Module.SnakeLemma (goal)
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₃)
⊢ Membership.mem (α := N₂) g₁.range ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)
have rw₄ : Eq.{u_7 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) (id ((ι₃ : (a : K₃) → M₃) x) : M₃) : N₃) (0 : 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]
-- Lean 4 proof step from Mathlib.Algebra.Module.SnakeLemma (goal)
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₃)
⊢ Membership.mem (α := N₂) g₁.range ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)
have rw₅ : Eq.{u_7 + 1} (α := N₃) ((i₃ : (a : M₃) → N₃) ((ι₃ : (a : K₃) → M₃) x : M₃) : N₃) (0 : 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]
-- Lean 4 proof step from Mathlib.Algebra.Module.SnakeLemma (goal)
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₃)
⊢ Membership.mem (α := N₂) g₁.range ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)
have rw₆ : Eq.{u_7 + 1} (α := N₃) ((i₃ ∘ₗ ι₃ : (a : K₃) → N₃) x : N₃) (0 : 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]
-- Lean 4 proof step from Mathlib.Algebra.Module.SnakeLemma (goal)
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₃)
⊢ Membership.mem (α := N₂) g₁.range ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)
have rw₇ : Eq.{u_7 + 1} (α := N₃) ((0 : (a : K₃) → N₃) x : N₃) (0 : 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]
-- Lean 4 proof step from Mathlib.Algebra.Module.SnakeLemma (goal)
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₃)
⊢ Membership.mem (α := N₂) g₁.range ((i₂ : (a : M₂) → N₂) (σ ((ι₃ : (a : K₃) → M₃) x)) : N₂)
have rw₈ : Eq.{u_7 + 1} (α := N₃) 0 0
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]