awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
N : ι ⊕ ι₂ → Type u_12
inst_10 : (i : ι ⊕ ι₂) → AddCommMonoid (N i)
inst_11 : (i : ι ⊕ ι₂) → Module.{u_4, u_12} R (N i)
x : (i : ι ⊕ ι₂) → N i
H :
  ∀ (val : ι),
    Eq (α := N (Sum.inl val))
      (Sum.rec (motive := fun (x : ι ⊕ ι₂) ↦ N x) (fun (i₁ : ι) ↦ x (Sum.inl i₁)) (fun (i₂ : ι₂) ↦ x (Sum.inr i₂))
        (Sum.inl val))
      (x (Sum.inl val))
⊢ (fun (t : ι ⊕ ι₂) ↦
      Sum.rec (motive := fun (x : ι ⊕ ι₂) ↦ N x) (fun (i₁ : ι) ↦ x (Sum.inl i₁)) (fun (i₂ : ι₂) ↦ x (Sum.inr i₂)) t) =
    x
have H₁ : ∀ (val : ι₂),
  Eq (α := N (Sum.inr val))
    (Sum.rec (motive := fun (x : ι ⊕ ι₂) ↦ N x) (fun (i₁ : ι) ↦ x (Sum.inl i₁)) (fun (i₂ : ι₂) ↦ x (Sum.inr i₂))
      (Sum.inr val))
    (x (Sum.inr val))
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₂
⊢ Eq (α := Submodule R (M × M₂)) (range (inl R M M₂)) (ker (snd R M M₂))
have h : ∀ (x : M × M₂),
  Membership.mem (γ := Submodule R (M × M₂)) (range (inl R M M₂)) x ↔
    Membership.mem (γ := Submodule R (M × M₂)) (ker (snd R M M₂)) x
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₂
x : M × M₂
⊢ (∃ (y : M), (inl R M M₂ : (a : M) → M × M₂) y = x) ↔
    Eq.{w + 1} (α := M₂) ((snd R M M₂ : (a : M × M₂) → M₂) x : M₂) (0 : M₂)
have h : (∃ (y : M), (inl R M M₂ : (a : M) → M × M₂) y = x) →
  Eq.{w + 1} (α := M₂) ((snd R M M₂ : (a : M × M₂) → M₂) x : M₂) (0 : M₂)
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₂
x : M × M₂
h :
  (∃ (y : M), (inl R M M₂ : (a : M) → M × M₂) y = x) →
    Eq.{w + 1} (α := M₂) ((snd R M M₂ : (a : M × M₂) → M₂) x : M₂) (0 : M₂)
⊢ (∃ (y : M), (inl R M M₂ : (a : M) → M × M₂) y = x) ↔
    Eq.{w + 1} (α := M₂) ((snd R M M₂ : (a : M × M₂) → M₂) x : M₂) (0 : M₂)
have h₁ : Eq.{w + 1} (α := M₂) ((snd R M M₂ : (a : M × M₂) → M₂) x : M₂) (0 : M₂) →
  ∃ (y : M), (inl R M M₂ : (a : M) → M × M₂) y = x
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₂
⊢ Eq (α := Submodule R (M × M₂)) (range (inr R M M₂)) (ker (fst R M M₂))
have h : ∀ (x : M × M₂),
  Membership.mem (γ := Submodule R (M × M₂)) (range (inr R M M₂)) x ↔
    Membership.mem (γ := Submodule R (M × M₂)) (ker (fst R M M₂)) x
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₂
x : M × M₂
⊢ (∃ (y : M₂), (inr R M M₂ : (a : M₂) → M × M₂) y = x) ↔
    Eq.{v + 1} (α := M) ((fst R M M₂ : (a : M × M₂) → M) x : M) (0 : M)
have h : (∃ (y : M₂), (inr R M M₂ : (a : M₂) → M × M₂) y = x) →
  Eq.{v + 1} (α := M) ((fst R M M₂ : (a : M × M₂) → M) x : M) (0 : M)
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₂
x : M × M₂
h :
  (∃ (y : M₂), (inr R M M₂ : (a : M₂) → M × M₂) y = x) →
    Eq.{v + 1} (α := M) ((fst R M M₂ : (a : M × M₂) → M) x : M) (0 : M)
⊢ (∃ (y : M₂), (inr R M M₂ : (a : M₂) → M × M₂) y = x) ↔
    Eq.{v + 1} (α := M) ((fst R M M₂ : (a : M × M₂) → M) x : M) (0 : M)
have h₁ : Eq.{v + 1} (α := M) ((fst R M M₂ : (a : M × M₂) → M) x : M) (0 : M) → ∃ (y : M₂), (inr R M M₂ : (a : M₂) → M × M₂) y = x
Tactic: constructor
-- 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.coprod g ∘ₗ inl R M M₂ = f
have h : ∀ (x : M), Eq.{y + 1} (α := M₃) ((f.coprod g ∘ₗ inl R M M₂ : (a : M) → M₃) x : M₃) ((f : (a : M) → M₃) x : M₃)
Tactic: ext
-- 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.coprod g ∘ₗ inr R M M₂ = g
have h : ∀ (x : M₂), Eq.{y + 1} (α := M₃) ((f.coprod g ∘ₗ inr R M M₂ : (a : M₂) → M₃) x : M₃) ((g : (a : M₂) → M₃) x : M₃)
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₂
⊢ Eq (α := M × M₂ →ₗ[R] M × M₂) (coprod (inl R M M₂) (inr R M M₂)) id
have h : ∀ (x : M × M₂),
  Eq.{v + 1} (α := M) ((coprod (inl R M M₂) (inr R M M₂) : (a : M × M₂) → M × M₂) x).1
    ((id : (a : M × M₂) → M × M₂) x).1
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₂
h :
  ∀ (x : M × M₂),
    Eq.{v + 1} (α := M) ((coprod (inl R M M₂) (inr R M M₂) : (a : M × M₂) → M × M₂) x).1
      ((id : (a : M × M₂) → M × M₂) x).1
⊢ Eq (α := M × M₂ →ₗ[R] M × M₂) (coprod (inl R M M₂) (inr R M M₂)) id
have h₁ : ∀ (x : M × M₂),
  Eq.{w + 1} (α := M₂) ((coprod (inl R M M₂) (inr R M M₂) : (a : M × M₂) → M × M₂) x).2
    ((id : (a : M × M₂) → M × M₂) x).2
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₂
⊢ Eq (α := M × M₂ →ₗ[R] M) (fst R M M₂) (coprod id 0)
have h : ∀ (x : M × M₂), Eq.{v + 1} (α := M) ((fst R M M₂ : (a : M × M₂) → M) x : M) ((coprod id 0 : (a : M × M₂) → M) x : M)
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₂
⊢ Eq (α := M × M₂ →ₗ[R] M₂) (snd R M M₂) (coprod 0 id)
have h : ∀ (x : M × M₂),
  Eq.{w + 1} (α := M₂) ((snd R M M₂ : (a : M × M₂) → M₂) x : M₂) ((coprod 0 id : (a : M × M₂) → M₂) x : M₂)
Tactic: ext
-- 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₃
S : Submodule R M
S' : Submodule R M₂
⊢ (↑(Submodule.map (f.coprod g) (S.prod S')) : Set M₃) = (↑(Submodule.map f S ⊔ Submodule.map g S') : Set M₃)
have simp : (fun (a : M × M₂) ↦ HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) a.1 : M₃) ((g : (a : M₂) → M₃) a.2 : M₃)) ''
    (↑(S.prod S') : Set (M × M₂)) =
  HAdd.hAdd (α := Set M₃) ((⇑f : (a : M) → M₃) '' (↑S : Set M)) ((⇑g : (a : M₂) → M₃) '' (↑S' : Set M₂))
Tactic: simp only [LinearMap.coprod_apply, Submodule.coe_sup, Submodule.map_coe]
-- 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₃
S : Submodule R M
S' : Submodule R M₂
⊢ (fun (a : M × M₂) ↦ HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) a.1 : M₃) ((g : (a : M₂) → M₃) a.2 : M₃)) ''
      (↑(S.prod S') : Set (M × M₂)) =
    HAdd.hAdd (α := Set M₃) ((⇑f : (a : M) → M₃) '' (↑S : Set M)) ((⇑g : (a : M₂) → M₃) '' (↑S' : Set M₂))
have rw : Eq.{y + 1} (α := Set M₃)
  ((fun (a : M × M₂) ↦ HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) a.1 : M₃) ((g : (a : M₂) → M₃) a.2 : M₃)) ''
    (↑(S.prod S') : Set (M × M₂)))
  (Set.image2
    (fun (a : M) (b : M₂) ↦ HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) a : M₃) ((g : (a : M₂) → M₃) b : M₃))
    (↑S : Set M) (↑S' : Set M₂))
Tactic: rw [← Set.image2_add, Set.image2_image_left, Set.image2_image_right]
-- 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 × M₂ →ₗ[R] M₃
⊢ (f ∘ₗ inl R M M₂).coprod (f ∘ₗ inr R M M₂) = f
have rw : f ∘ₗ coprod (inl R M M₂) (inr R M M₂) = f
Tactic: rw [← comp_coprod, coprod_inl_inr, comp_id]
-- 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 × M₂ →ₗ[R] M₃
rw : f ∘ₗ coprod (inl R M M₂) (inr R M M₂) = f
⊢ (f ∘ₗ inl R M M₂).coprod (f ∘ₗ inr R M M₂) = f
have rw₁ : f ∘ₗ id = f
Tactic: rw [← comp_coprod, coprod_inl_inr, comp_id]
-- 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 × M₂ →ₗ[R] M₃
rw : f ∘ₗ coprod (inl R M M₂) (inr R M M₂) = f
rw₁ : f ∘ₗ id = f
⊢ (f ∘ₗ inl R M M₂).coprod (f ∘ₗ inr R M M₂) = f
have rw₂ : f = f
Tactic: rw [← comp_coprod, coprod_inl_inr, comp_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid M₅
inst_7 : AddCommMonoid M₆
inst_8 : Module R M
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R M₅
inst_13 : Module R M₆
f : M →ₗ[R] M₂
inst_14 : Module S M₃
inst_15 : SMulCommClass R S M₃
a b : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)
⊢ (a + b).1.coprod (a + b).2 = a.1.coprod a.2 + b.1.coprod b.2
have h : ∀ (x : M × M₂),
  Eq.{y + 1} (α := M₃) (((a + b).1.coprod (a + b).2 : (a : M × M₂) → M₃) x : M₃)
    ((a.1.coprod a.2 + b.1.coprod b.2 : (a : M × M₂) → M₃) x : M₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid M₅
inst_7 : AddCommMonoid M₆
inst_8 : Module R M
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R M₅
inst_13 : Module R M₆
f : M →ₗ[R] M₂
inst_14 : Module S M₃
inst_15 : SMulCommClass R S M₃
r : S
a : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)
⊢ (r • a).1.coprod (r • a).2 = HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) r : S) (a.1.coprod a.2)
have dsimp : (r • a.1).coprod (r • a.2) = r • a.1.coprod a.2
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid M₅
inst_7 : AddCommMonoid M₆
inst_8 : Module R M
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R M₅
inst_13 : Module R M₆
f : M →ₗ[R] M₂
inst_14 : Module S M₃
inst_15 : SMulCommClass R S M₃
r : S
a : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)
⊢ (r • a.1).coprod (r • a.2) = r • a.1.coprod a.2
have h : ∀ (x : M × M₂),
  Eq.{y + 1} (α := M₃) (((r • a.1).coprod (r • a.2) : (a : M × M₂) → M₃) x : M₃)
    ((r • a.1.coprod a.2 : (a : M × M₂) → M₃) x : M₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
⊢ Submodule.comap (f.prodMap g) ⊥ = (Submodule.comap f ⊥).prod (Submodule.comap g ⊥)
have rw : Submodule.comap (f.prodMap g) ⊥ = Submodule.comap (f.prodMap g) (Submodule.prod ⊥ ⊥)
Tactic: rw [← prodMap_comap_prod, Submodule.prod_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
rw : Submodule.comap (f.prodMap g) ⊥ = Submodule.comap (f.prodMap g) (Submodule.prod ⊥ ⊥)
⊢ Submodule.comap (f.prodMap g) ⊥ = (Submodule.comap f ⊥).prod (Submodule.comap g ⊥)
have rw₁ : Submodule.comap (f.prodMap g) ⊥ = Submodule.comap (f.prodMap g) ⊥
Tactic: rw [← prodMap_comap_prod, Submodule.prod_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₄
⊢ (f.prodMap g).range = f.range.prod g.range
have h : ∀ (fst : M₃) (snd : M₄), (fst, snd) ∈ (f.prodMap g).range ↔ (fst, snd) ∈ f.range.prod g.range
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₂
⊢ IsCompl (α := Submodule R (M × M₂)) (range (inl R M M₂)) (range (inr R M M₂))
have disjoint : Disjoint (α := Submodule R (M × M₂)) (range (inl R M M₂)) (range (inr R M M₂))
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₂
disjoint : Disjoint (α := Submodule R (M × M₂)) (range (inl R M M₂)) (range (inr R M M₂))
⊢ IsCompl (α := Submodule R (M × M₂)) (range (inl R M M₂)) (range (inr R M M₂))
have codisjoint : Codisjoint (α := Submodule R (M × M₂)) (range (inl R M M₂)) (range (inr R M M₂))
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₂
⊢ Disjoint (α := Submodule R (M × M₂)) (range (inl R M M₂)) (range (inr R M M₂))
have disjoint : ∀ (x : M × M₂),
  Membership.mem (γ := Submodule R (M × M₂)) (range (inl R M M₂)) x →
    Membership.mem (γ := Submodule R (M × M₂)) (range (inr R M M₂)) x → x = 0
Tactic: rw [disjoint_def]
-- 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₂
fst : M
snd : M₂
x : M
hx : (inl R M M₂ : (a : M) → M × M₂) x = (fst, snd)
y : M₂
hy : (inr R M M₂ : (a : M₂) → M × M₂) y = (fst, snd)
⊢ (fst, snd) = 0
have disjoint : ∀ (hx : x = fst ∧ 0 = snd) (hy : 0 = fst ∧ y = snd), fst = 0.1 ∧ snd = 0.2
Tactic: simp only [Prod.ext_iff, inl_apply, inr_apply] at hx hy ⊢
Cleared hypotheses: hx, 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₂
⊢ Codisjoint (α := Submodule R (M × M₂)) (range (inl R M M₂)) (range (inr R M M₂))
have codisjoint : LE.le (α := Submodule R (M × M₂)) ⊤ (range (inl R M M₂) ⊔ range (inr R M M₂))
Tactic: rw [codisjoint_iff_le_sup]
-- 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₂
x : M
y : M₂
⊢ Membership.mem (γ := Submodule R (M × M₂)) (range (inl R M M₂) ⊔ range (inr R M M₂)) (x, y)
have codisjoint : ∃ (y_1 : M × M₂),
  (∃ (y : M), (inl R M M₂ : (a : M) → M × M₂) y = y_1) ∧
    ∃ (z : M × M₂), (∃ (y : M₂), (inr R M M₂ : (a : M₂) → M × M₂) y = z) ∧ y_1 + z = (x, y)
Tactic: simp only [mem_sup, mem_range]
-- 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₂
x : M
y : M₂
⊢ ∃ (y_1 : M × M₂),
    (∃ (y : M), (inl R M M₂ : (a : M) → M × M₂) y = y_1) ∧
      ∃ (z : M × M₂), (∃ (y : M₂), (inr R M M₂ : (a : M₂) → M × M₂) y = z) ∧ y_1 + z = (x, y)
have codisjoint : (x, 0) + (0, y) = (x, y)
Tactic: refine ⟨(x, 0), ⟨x, rfl⟩, (0, y), ⟨y, rfl⟩, ?_⟩
-- 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₂
⊢ p.prod q = map (inl R M M₂) p ⊔ map (inr R M M₂) q
have rw : p.prod q = map (coprod (inl R M M₂) (inr R M M₂)) (p.prod q)
Tactic: rw [← map_coprod_prod, coprod_inl_inr, map_id]
-- 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₂
rw : p.prod q = map (coprod (inl R M M₂) (inr R M M₂)) (p.prod q)
⊢ p.prod q = map (inl R M M₂) p ⊔ map (inr R M M₂) q
have rw₁ : p.prod q = map id (p.prod q)
Tactic: rw [← map_coprod_prod, coprod_inl_inr, map_id]
-- 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₂
rw : p.prod q = map (coprod (inl R M M₂) (inr R M M₂)) (p.prod q)
rw₁ : p.prod q = map id (p.prod q)
⊢ p.prod q = map (inl R M M₂) p ⊔ map (inr R M M₂) q
have rw₂ : p.prod q = p.prod q
Tactic: rw [← map_coprod_prod, coprod_inl_inr, map_id]
-- 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₂
s : Set M
t : Set M₂
⊢ Eq (α := Submodule R (M × M₂))
    (span R ((⇑(inl R M M₂) : (a : M) → M × M₂) '' s ∪ (⇑(inr R M M₂) : (a : M₂) → M × M₂) '' t))
    (Submodule.prod (span R s) (span R t))
have rw : Eq (α := Submodule R (M × M₂))
  (span R ((⇑(inl R M M₂) : (a : M) → M × M₂) '' s) ⊔ span R ((⇑(inr R M M₂) : (a : M₂) → M × M₂) '' t))
  (Submodule.prod (span R s) (span R t))
Tactic: rw [span_union, prod_eq_sup_map, ← span_image, ← span_image]
-- 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₂
s : Set M
t : Set M₂
rw :
  Eq (α := Submodule R (M × M₂))
    (span R ((⇑(inl R M M₂) : (a : M) → M × M₂) '' s) ⊔ span R ((⇑(inr R M M₂) : (a : M₂) → M × M₂) '' t))
    (Submodule.prod (span R s) (span R t))
⊢ Eq (α := Submodule R (M × M₂))
    (span R ((⇑(inl R M M₂) : (a : M) → M × M₂) '' s ∪ (⇑(inr R M M₂) : (a : M₂) → M × M₂) '' t))
    (Submodule.prod (span R s) (span R t))
have rw₁ : Eq (α := Submodule R (M × M₂))
  (span R ((⇑(inl R M M₂) : (a : M) → M × M₂) '' s) ⊔ span R ((⇑(inr R M M₂) : (a : M₂) → M × M₂) '' t))
  (map (inl R M M₂) (span R s) ⊔ map (inr R M M₂) (span R t))
Tactic: rw [span_union, prod_eq_sup_map, ← span_image, ← span_image]
-- 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₂
s : Set M
t : Set M₂
rw :
  Eq (α := Submodule R (M × M₂))
    (span R ((⇑(inl R M M₂) : (a : M) → M × M₂) '' s) ⊔ span R ((⇑(inr R M M₂) : (a : M₂) → M × M₂) '' t))
    (Submodule.prod (span R s) (span R t))
rw₁ :
  Eq (α := Submodule R (M × M₂))
    (span R ((⇑(inl R M M₂) : (a : M) → M × M₂) '' s) ⊔ span R ((⇑(inr R M M₂) : (a : M₂) → M × M₂) '' t))
    (map (inl R M M₂) (span R s) ⊔ map (inr R M M₂) (span R t))
⊢ Eq (α := Submodule R (M × M₂))
    (span R ((⇑(inl R M M₂) : (a : M) → M × M₂) '' s ∪ (⇑(inr R M M₂) : (a : M₂) → M × M₂) '' t))
    (Submodule.prod (span R s) (span R t))
have rw₂ : Eq (α := Submodule R (M × M₂))
  (span R ((⇑(inl R M M₂) : (a : M) → M × M₂) '' s) ⊔ span R ((⇑(inr R M M₂) : (a : M₂) → M × M₂) '' t))
  (span R ((⇑(inl R M M₂) : (a : M) → M × M₂) '' s) ⊔ map (inr R M M₂) (span R t))
Tactic: rw [span_union, prod_eq_sup_map, ← span_image, ← span_image]
-- 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₂
s : Set M
t : Set M₂
rw :
  Eq (α := Submodule R (M × M₂))
    (span R ((⇑(inl R M M₂) : (a : M) → M × M₂) '' s) ⊔ span R ((⇑(inr R M M₂) : (a : M₂) → M × M₂) '' t))
    (Submodule.prod (span R s) (span R t))
rw₁ :
  Eq (α := Submodule R (M × M₂))
    (span R ((⇑(inl R M M₂) : (a : M) → M × M₂) '' s) ⊔ span R ((⇑(inr R M M₂) : (a : M₂) → M × M₂) '' t))
    (map (inl R M M₂) (span R s) ⊔ map (inr R M M₂) (span R t))
rw₂ :
  Eq (α := Submodule R (M × M₂))
    (span R ((⇑(inl R M M₂) : (a : M) → M × M₂) '' s) ⊔ span R ((⇑(inr R M M₂) : (a : M₂) → M × M₂) '' t))
    (span R ((⇑(inl R M M₂) : (a : M) → M × M₂) '' s) ⊔ map (inr R M M₂) (span R t))
⊢ Eq (α := Submodule R (M × M₂))
    (span R ((⇑(inl R M M₂) : (a : M) → M × M₂) '' s ∪ (⇑(inr R M M₂) : (a : M₂) → M × M₂) '' t))
    (Submodule.prod (span R s) (span R t))
have rw₃ : Eq (α := Submodule R (M × M₂))
  (span R ((⇑(inl R M M₂) : (a : M) → M × M₂) '' s) ⊔ span R ((⇑(inr R M M₂) : (a : M₂) → M × M₂) '' t))
  (span R ((⇑(inl R M M₂) : (a : M) → M × M₂) '' s) ⊔ span R ((⇑(inr R M M₂) : (a : M₂) → M × M₂) '' t))
Tactic: rw [span_union, prod_eq_sup_map, ← span_image, ← span_image]
-- 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).ker = f.ker ⊓ g.ker
have rw : comap f ⊥ ⊓ comap g ⊥ = f.ker ⊓ g.ker
Tactic: rw [ker, ← prod_bot, comap_prod_prod]