awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
⊢ (f.prod g).range ≤ f.range.prod g.range
have simp : ∀ ⦃x : M₂ × M₃⦄ (x_1 : M),
  Function.prod (α := fun (a : M) ↦ M₂) (β := fun (a : M) ↦ M₃) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₃) x_1 = x →
    (∃ (y : M), (f : (a : M) → M₂) y = x.1) ∧ ∃ (y : M), (g : (a : M) → M₃) y = x.2
Tactic: simp only [SetLike.le_def, prod_apply, mem_range, mem_prod, exists_imp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M₂ : Type u_3
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
M₃ : Type u_4
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
⊢ (f.coprod g).ker = f.ker.prod g.ker
have apply : (f.coprod g).ker ≤ f.ker.prod g.ker
Tactic: apply le_antisymm _ (ker_prod_ker_le_ker_coprod f g)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M₂ : Type u_3
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
M₃ : Type u_4
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : (y, z) ∈ (f.coprod g).ker
⊢ (y, z) ∈ f.ker.prod g.ker
have simp : ∀ (h : HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) y : M₃) ((g : (a : M₂) → M₃) z : M₃) = 0),
  Eq.{u_4 + 1} (α := M₃) ((f : (a : M) → M₃) y : M₃) (0 : M₃) ∧
    Eq.{u_4 + 1} (α := M₃) ((g : (a : M₂) → M₃) z : M₃) (0 : M₃)
Tactic: simp only [mem_ker, mem_prod, coprod_apply] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M₂ : Type u_3
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
M₃ : Type u_4
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) y : M₃) ((g : (a : M₂) → M₃) z : M₃) = 0
⊢ Membership.mem (α := M₃) (f.range ⊓ g.range) ((f : (a : M) → M₃) y : M₃)
have simp : ∃ (y_1 : M₂), Eq.{u_4 + 1} (α := M₃) ((g : (a : M₂) → M₃) y_1 : M₃) ((f : (a : M) → M₃) y : M₃)
Tactic: simp only [true_and, mem_range, mem_inf, exists_apply_eq_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M₂ : Type u_3
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
M₃ : Type u_4
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) y : M₃) ((g : (a : M₂) → M₃) z : M₃) = 0
⊢ ∃ (y_1 : M₂), Eq.{u_4 + 1} (α := M₃) ((g : (a : M₂) → M₃) y_1 : M₃) ((f : (a : M) → M₃) y : M₃)
have h₁ : Eq.{u_4 + 1} (α := M₃) ((g : (a : M₂) → M₃) (-z) : M₃) ((f : (a : M) → M₃) y : M₃)
Tactic: use -z
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M₂ : Type u_3
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
M₃ : Type u_4
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) y : M₃) ((g : (a : M₂) → M₃) z : M₃) = 0
⊢ Eq.{u_4 + 1} (α := M₃) ((g : (a : M₂) → M₃) (-z) : M₃) ((f : (a : M) → M₃) y : M₃)
have h₁ : Eq.{u_4 + 1} (α := M₃) ((f : (a : M) → M₃) y : M₃) ((g : (a : M₂) → M₃) (-z) : M₃)
Tactic: rwa [eq_comm, map_neg, ← sub_eq_zero, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M₂ : Type u_3
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
M₃ : Type u_4
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) y : M₃) ((g : (a : M₂) → M₃) z : M₃) = 0
h₁ : Eq.{u_4 + 1} (α := M₃) ((f : (a : M) → M₃) y : M₃) ((g : (a : M₂) → M₃) (-z) : M₃)
⊢ Eq.{u_4 + 1} (α := M₃) ((g : (a : M₂) → M₃) (-z) : M₃) ((f : (a : M) → M₃) y : M₃)
have h₂ : Eq.{u_4 + 1} (α := M₃) ((f : (a : M) → M₃) y : M₃) (-(g : (a : M₂) → M₃) z : M₃)
Tactic: rwa [eq_comm, map_neg, ← sub_eq_zero, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M₂ : Type u_3
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
M₃ : Type u_4
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) y : M₃) ((g : (a : M₂) → M₃) z : M₃) = 0
h₁ : Eq.{u_4 + 1} (α := M₃) ((f : (a : M) → M₃) y : M₃) ((g : (a : M₂) → M₃) (-z) : M₃)
h₂ : Eq.{u_4 + 1} (α := M₃) ((f : (a : M) → M₃) y : M₃) (-(g : (a : M₂) → M₃) z : M₃)
⊢ Eq.{u_4 + 1} (α := M₃) ((g : (a : M₂) → M₃) (-z) : M₃) ((f : (a : M) → M₃) y : M₃)
have h₃ : HSub.hSub (α := M₃) (β := M₃) ((f : (a : M) → M₃) y : M₃) (-(g : (a : M₂) → M₃) z : M₃) = 0
Tactic: rwa [eq_comm, map_neg, ← sub_eq_zero, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M₂ : Type u_3
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
M₃ : Type u_4
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) y : M₃) ((g : (a : M₂) → M₃) z : M₃) = 0
⊢ Eq.{u_4 + 1} (α := M₃) ((f : (a : M) → M₃) y : M₃) (0 : M₃) ∧
    Eq.{u_4 + 1} (α := M₃) ((g : (a : M₂) → M₃) z : M₃) (0 : M₃)
have this : Membership.mem (α := M₃) (f.range ⊓ g.range) ((f : (a : M) → M₃) y : M₃)
Tactic: have : f y ∈ (range f) ⊓ (range g) := by
    simp only [true_and, mem_range, mem_inf, exists_apply_eq_apply]
    use -z
    rwa [eq_comm, map_neg, ← sub_eq_zero, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M₂ : Type u_3
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
M₃ : Type u_4
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) y : M₃) ((g : (a : M₂) → M₃) z : M₃) = 0
this : Membership.mem (α := M₃) (f.range ⊓ g.range) ((f : (a : M) → M₃) y : M₃)
⊢ Eq.{u_4 + 1} (α := M₃) ((f : (a : M) → M₃) y : M₃) (0 : M₃) ∧
    Eq.{u_4 + 1} (α := M₃) ((g : (a : M₂) → M₃) z : M₃) (0 : M₃)
have this₁ : Eq.{u_4 + 1} (α := M₃) ((f : (a : M) → M₃) y : M₃) (0 : M₃)
Tactic: rw [hd.eq_bot, mem_bot] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M₂ : Type u_3
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
M₃ : Type u_4
inst_5 : AddCommGroup M₃
inst_6 : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) y : M₃) ((g : (a : M₂) → M₃) z : M₃) = 0
this : Eq.{u_4 + 1} (α := M₃) ((f : (a : M) → M₃) y : M₃) (0 : M₃)
⊢ Eq.{u_4 + 1} (α := M₃) ((f : (a : M) → M₃) y : M₃) (0 : M₃) ∧
    Eq.{u_4 + 1} (α := M₃) ((g : (a : M₂) → M₃) z : M₃) (0 : M₃)
have h₁ : HAdd.hAdd (α := M₃) (β := M₃) (0 : M₃) ((g : (a : M₂) → M₃) z : M₃) = 0
Tactic: rw [this] at h
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R_1 : Type u
K : Type u'
M_1 : Type v
V : Type v'
M₂_1 : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : Module R_1 M_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M₃
inst_8 : Module R_1 M₄
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst_9 : Ring R
inst_10 : AddCommGroup M
inst_11 : AddCommGroup M₂
inst_12 : Module R M
inst_13 : Module R M₂
f : M →ₗ[R] M₂
C : Submodule R M
h : IsCompl C f.ker
x : M
⊢ ∃ (a : ↥C),
    Eq.{u_5 + 1} (α := ↥f.range) ((codRestrict f.range f ⋯ ∘ₗ C.subtype : (a : ↥C) → ↥f.range) a : ↥f.range)
      (Subtype.mk (p := fun (x : M₂) ↦ x ∈ f.range) ((f : (a : M) → M₂) x) ⋯ : ↥f.range)
have obtain : ∀ (y z : M) (hy : y ∈ C) (hz : z ∈ f.ker),
  ∃ (a : ↥C),
    Eq.{u_5 + 1} (α := ↥f.range) ((codRestrict f.range f sorry ∘ₗ C.subtype : (a : ↥C) → ↥f.range) a : ↥f.range)
      (Subtype.mk (p := fun (x : M₂) ↦ x ∈ f.range) ((f : (a : M) → M₂) (y + z)) sorry : ↥f.range)
Tactic: obtain ⟨y, z, hy, hz, rfl⟩ := codisjoint_iff_exists_add_eq.mp h.codisjoint x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R_1 : Type u
K : Type u'
M_1 : Type v
V : Type v'
M₂_1 : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : Module R_1 M_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M₃
inst_8 : Module R_1 M₄
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst_9 : Ring R
inst_10 : AddCommGroup M
inst_11 : AddCommGroup M₂
inst_12 : Module R M
inst_13 : Module R M₂
f : M →ₗ[R] M₂
C : Submodule R M
h : IsCompl C f.ker
y z : M
hy : y ∈ C
hz : z ∈ f.ker
⊢ ∃ (a : ↥C),
    Eq.{u_5 + 1} (α := ↥f.range) ((codRestrict f.range f ⋯ ∘ₗ C.subtype : (a : ↥C) → ↥f.range) a : ↥f.range)
      (Subtype.mk (p := fun (x : M₂) ↦ x ∈ f.range) ((f : (a : M) → M₂) (y + z)) ⋯ : ↥f.range)
have h₁ : Eq.{u_5 + 1} (α := ↥f.range)
  ((codRestrict f.range f sorry ∘ₗ C.subtype : (a : ↥C) → ↥f.range) (Subtype.mk (p := fun (x : M) ↦ x ∈ C) y hy) : ↥f.range)
  (Subtype.mk (p := fun (x : M₂) ↦ x ∈ f.range) ((f : (a : M) → M₂) (y + z)) sorry : ↥f.range)
Tactic: use ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
p : Submodule R M
⊢ Eq (α := Submodule R (M × M₂)) (map (inl R M M₂) p) (p.prod ⊥)
have h : ∀ (x : M) (y : M₂),
  Membership.mem (γ := Submodule R (M × M₂)) (map (inl R M M₂) p) (x, y) ↔
    Membership.mem (γ := Submodule R (M × M₂)) (p.prod ⊥) (x, y)
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
q : Submodule R M₂
⊢ Eq (α := Submodule R (M × M₂)) (map (inr R M M₂) q) (prod ⊥ q)
have h : ∀ (x : M) (y : M₂),
  Membership.mem (γ := Submodule R (M × M₂)) (map (inr R M M₂) q) (x, y) ↔
    Membership.mem (γ := Submodule R (M × M₂)) (prod ⊥ q) (x, y)
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
p : Submodule R M
⊢ Eq (α := Submodule R (M × M₂)) (comap (fst R M M₂) p) (p.prod ⊤)
have h : ∀ (x : M) (y : M₂),
  Membership.mem (γ := Submodule R (M × M₂)) (comap (fst R M M₂) p) (x, y) ↔
    Membership.mem (γ := Submodule R (M × M₂)) (p.prod ⊤) (x, y)
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
q : Submodule R M₂
⊢ Eq (α := Submodule R (M × M₂)) (comap (snd R M M₂) q) (prod ⊤ q)
have h : ∀ (x : M) (y : M₂),
  Membership.mem (γ := Submodule R (M × M₂)) (comap (snd R M M₂) q) (x, y) ↔
    Membership.mem (γ := Submodule R (M × M₂)) (prod ⊤ q) (x, y)
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
p : Submodule R M
q : Submodule R M₂
⊢ comap (inl R M M₂) (p.prod q) = p
have h : ∀ (x : M), x ∈ comap (inl R M M₂) (p.prod q) ↔ x ∈ p
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
p : Submodule R M
q : Submodule R M₂
⊢ comap (inr R M M₂) (p.prod q) = q
have h : ∀ (x : M₂), x ∈ comap (inr R M M₂) (p.prod q) ↔ x ∈ q
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
p : Submodule R M
q : Submodule R M₂
⊢ map (fst R M M₂) (p.prod q) = p
have h : ∀ (x : M), x ∈ map (fst R M M₂) (p.prod q) ↔ x ∈ p
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
p : Submodule R M
q : Submodule R M₂
⊢ map (snd R M M₂) (p.prod q) = q
have h : ∀ (x : M₂), x ∈ map (snd R M M₂) (p.prod q) ↔ x ∈ q
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
⊢ Eq (α := Submodule R M) (ker (inl R M M₂)) ⊥
have rw : Eq (α := Submodule R M) (comap (inl R M M₂) ⊥) ⊥
Tactic: rw [ker, ← prod_bot, prod_comap_inl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
rw : Eq (α := Submodule R M) (comap (inl R M M₂) ⊥) ⊥
⊢ Eq (α := Submodule R M) (ker (inl R M M₂)) ⊥
have rw₁ : Eq (α := Submodule R M) (comap (inl R M M₂) (prod ⊥ ⊥)) ⊥
Tactic: rw [ker, ← prod_bot, prod_comap_inl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
rw : Eq (α := Submodule R M) (comap (inl R M M₂) ⊥) ⊥
rw₁ : Eq (α := Submodule R M) (comap (inl R M M₂) (prod ⊥ ⊥)) ⊥
⊢ Eq (α := Submodule R M) (ker (inl R M M₂)) ⊥
have rw₂ : Eq.{v + 1} (α := Submodule R M) ⊥ ⊥
Tactic: rw [ker, ← prod_bot, prod_comap_inl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
⊢ Eq (α := Submodule R M₂) (ker (inr R M M₂)) ⊥
have rw : Eq (α := Submodule R M₂) (comap (inr R M M₂) ⊥) ⊥
Tactic: rw [ker, ← prod_bot, prod_comap_inr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
rw : Eq (α := Submodule R M₂) (comap (inr R M M₂) ⊥) ⊥
⊢ Eq (α := Submodule R M₂) (ker (inr R M M₂)) ⊥
have rw₁ : Eq (α := Submodule R M₂) (comap (inr R M M₂) (prod ⊥ ⊥)) ⊥
Tactic: rw [ker, ← prod_bot, prod_comap_inr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
rw : Eq (α := Submodule R M₂) (comap (inr R M M₂) ⊥) ⊥
rw₁ : Eq (α := Submodule R M₂) (comap (inr R M M₂) (prod ⊥ ⊥)) ⊥
⊢ Eq (α := Submodule R M₂) (ker (inr R M M₂)) ⊥
have rw₂ : Eq.{w + 1} (α := Submodule R M₂) ⊥ ⊥
Tactic: rw [ker, ← prod_bot, prod_comap_inr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
⊢ Eq (α := Submodule R M) (range (fst R M M₂)) ⊤
have rw : Eq (α := Submodule R M) (map (fst R M M₂) ⊤) ⊤
Tactic: rw [range_eq_map, ← prod_top, prod_map_fst]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
rw : Eq (α := Submodule R M) (map (fst R M M₂) ⊤) ⊤
⊢ Eq (α := Submodule R M) (range (fst R M M₂)) ⊤
have rw₁ : Eq (α := Submodule R M) (map (fst R M M₂) (prod ⊤ ⊤)) ⊤
Tactic: rw [range_eq_map, ← prod_top, prod_map_fst]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
rw : Eq (α := Submodule R M) (map (fst R M M₂) ⊤) ⊤
rw₁ : Eq (α := Submodule R M) (map (fst R M M₂) (prod ⊤ ⊤)) ⊤
⊢ Eq (α := Submodule R M) (range (fst R M M₂)) ⊤
have rw₂ : Eq.{v + 1} (α := Submodule R M) ⊤ ⊤
Tactic: rw [range_eq_map, ← prod_top, prod_map_fst]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
⊢ Eq (α := Submodule R M₂) (range (snd R M M₂)) ⊤
have rw : Eq (α := Submodule R M₂) (map (snd R M M₂) ⊤) ⊤
Tactic: rw [range_eq_map, ← prod_top, prod_map_snd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
rw : Eq (α := Submodule R M₂) (map (snd R M M₂) ⊤) ⊤
⊢ Eq (α := Submodule R M₂) (range (snd R M M₂)) ⊤
have rw₁ : Eq (α := Submodule R M₂) (map (snd R M M₂) (prod ⊤ ⊤)) ⊤
Tactic: rw [range_eq_map, ← prod_top, prod_map_snd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
rw : Eq (α := Submodule R M₂) (map (snd R M M₂) ⊤) ⊤
rw₁ : Eq (α := Submodule R M₂) (map (snd R M M₂) (prod ⊤ ⊤)) ⊤
⊢ Eq (α := Submodule R M₂) (range (snd R M M₂)) ⊤
have rw₂ : Eq.{w + 1} (α := Submodule R M₂) ⊤ ⊤
Tactic: rw [range_eq_map, ← prod_top, prod_map_snd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
⊢ Eq (α := Submodule R (M × M₂)) (fst R M M₂ ⊔ snd R M M₂) ⊤
have rw : LE.le (α := Submodule R (M × M₂)) ⊤ (fst R M M₂ ⊔ snd R M M₂)
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
m : M
n : M₂
⊢ Membership.mem (γ := Submodule R (M × M₂)) (fst R M M₂ ⊔ snd R M M₂) (m, n)
have rw : Membership.mem (γ := Submodule R (M × M₂)) (fst R M M₂ ⊔ snd R M M₂) ((m, 0) + (0, n))
Tactic: rw [show (m, n) = (m, 0) + (0, n) by simp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
m : M
n : M₂
⊢ Membership.mem (γ := Submodule R (M × M₂)) (fst R M M₂ ⊔ snd R M M₂) ((m, 0) + (0, n))
have h₁ : Membership.mem (γ := Submodule R (M × M₂)) (fst R M M₂ ⊔ snd R M M₂) (m, 0)
Tactic: apply Submodule.add_mem (Submodule.fst R M M₂ ⊔ Submodule.snd R M M₂)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
m : M
n : M₂
h₁ : Membership.mem (γ := Submodule R (M × M₂)) (fst R M M₂ ⊔ snd R M M₂) (m, 0)
⊢ Membership.mem (γ := Submodule R (M × M₂)) (fst R M M₂ ⊔ snd R M M₂) ((m, 0) + (0, n))
have h₂ : Membership.mem (γ := Submodule R (M × M₂)) (fst R M M₂ ⊔ snd R M M₂) (0, n)
Tactic: apply Submodule.add_mem (Submodule.fst R M M₂ ⊔ Submodule.snd R M M₂)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
⊢ q ≤ p₁.prod p₂ ↔ map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂
have mp : q ≤ p₁.prod p₂ → map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
mp : q ≤ p₁.prod p₂ → map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂
⊢ q ≤ p₁.prod p₂ ↔ map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂
have mpr : map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂ → q ≤ p₁.prod p₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
⊢ map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂
have mp : map (LinearMap.fst R M M₂) q ≤ p₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
mp : map (LinearMap.fst R M M₂) q ≤ p₁
⊢ map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂
have mp₁ : map (LinearMap.snd R M M₂) q ≤ p₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
⊢ p₁.prod p₂ ≤ q ↔ map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q
have mp : p₁.prod p₂ ≤ q → map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
mp : p₁.prod p₂ ≤ q → map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q
⊢ p₁.prod p₂ ≤ q ↔ map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q
have mpr : map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q → p₁.prod p₂ ≤ q
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : p₁.prod p₂ ≤ q
⊢ map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q
have mp : map (inl R M M₂) p₁ ≤ q
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : p₁.prod p₂ ≤ q
mp : map (inl R M M₂) p₁ ≤ q
⊢ map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q
have mp₁ : map (inr R M M₂) p₂ ≤ q
Tactic: constructor