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
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
x : M
hx : x ∈ (↑p₁ : Set M)
⊢ Membership.mem (α := M × M₂) q ((inl R M M₂ : (a : M) → M × M₂) x : M × M₂)
have mp : Membership.mem (α := M × M₂) (p₁.prod p₂) ((inl R M M₂ : (a : M) → M × M₂) x : M × M₂)
Tactic: apply h
-- 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
x : M₂
hx : x ∈ (↑p₂ : Set M₂)
⊢ Membership.mem (α := M × M₂) q ((inr R M M₂ : (a : M₂) → M × M₂) x : M × M₂)
have mp : Membership.mem (α := M × M₂) (p₁.prod p₂) ((inr R M M₂ : (a : M₂) → M × M₂) x : M × M₂)
Tactic: apply h
-- 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₂)
hH : map (inl R M M₂) p₁ ≤ q
hK : map (inr R M M₂) p₂ ≤ q
x1 : M
x2 : M₂
h1 : (x1, x2).1 ∈ (↑p₁ : Set M)
h2 : (x1, x2).2 ∈ (↑p₂ : Set M₂)
⊢ Membership.mem (α := M × M₂) q ((inl R M M₂ : (a : M) → M × M₂) x1 : M × M₂)
have a : Membership.mem (α := M × M₂) (γ := Submodule R (M × M₂)) (map (inl R M M₂) p₁)
  ((inl R M M₂ : (a : M) → M × M₂) x1 : M × M₂)
Tactic: apply hH
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (hypothesis)
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₂)
hH : map (inl R M M₂) p₁ ≤ q
hK : map (inr R M M₂) p₂ ≤ q
x1 : M
x2 : M₂
h1 : (x1, x2).1 ∈ (↑p₁ : Set M)
h2 : (x1, x2).2 ∈ (↑p₂ : Set M₂)
⊢ (x1, x2) ∈ q
have h1' : Membership.mem (α := M × M₂) q ((inl R M M₂ : (a : M) → M × M₂) x1 : M × M₂)
Tactic: have h1' : (LinearMap.inl R _ _) x1 ∈ q := by
      apply hH
      simpa using h1
-- 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₂)
hH : map (inl R M M₂) p₁ ≤ q
hK : map (inr R M M₂) p₂ ≤ q
x1 : M
x2 : M₂
h1 : (x1, x2).1 ∈ (↑p₁ : Set M)
h2 : (x1, x2).2 ∈ (↑p₂ : Set M₂)
h1' : Membership.mem (α := M × M₂) q ((inl R M M₂ : (a : M) → M × M₂) x1 : M × M₂)
⊢ Membership.mem (α := M × M₂) q ((inr R M M₂ : (a : M₂) → M × M₂) x2 : M × M₂)
have a : Membership.mem (α := M × M₂) (γ := Submodule R (M × M₂)) (map (inr R M M₂) p₂)
  ((inr R M M₂ : (a : M₂) → M × M₂) x2 : M × M₂)
Tactic: apply hK
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (hypothesis)
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₂)
hH : map (inl R M M₂) p₁ ≤ q
hK : map (inr R M M₂) p₂ ≤ q
x1 : M
x2 : M₂
h1 : (x1, x2).1 ∈ (↑p₁ : Set M)
h2 : (x1, x2).2 ∈ (↑p₂ : Set M₂)
h1' : Membership.mem (α := M × M₂) q ((inl R M M₂ : (a : M) → M × M₂) x1 : M × M₂)
⊢ (x1, x2) ∈ q
have h2' : Membership.mem (α := M × M₂) q ((inr R M M₂ : (a : M₂) → M × M₂) x2 : M × M₂)
Tactic: have h2' : (LinearMap.inr R _ _) x2 ∈ q := by
      apply hK
      simpa using h2
-- 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₂) (LinearMap.fst R M₂ M ∘ₗ (↑(prodComm R M M₂) : M × M₂ →ₗ[R] M₂ × M)) (LinearMap.snd R M M₂)
have hl : ∀ (x : M),
  Eq.{w + 1} (α := M₂)
    (((LinearMap.fst R M₂ M ∘ₗ (↑(prodComm R M M₂) : M × M₂ →ₗ[R] M₂ × M)) ∘ₗ LinearMap.inl R M M₂ : (a : M) → M₂) x :
      M₂)
    ((LinearMap.snd R M M₂ ∘ₗ LinearMap.inl R M M₂ : (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₂
hl :
  ∀ (x : M),
    Eq.{w + 1} (α := M₂)
      (((LinearMap.fst R M₂ M ∘ₗ (↑(prodComm R M M₂) : M × M₂ →ₗ[R] M₂ × M)) ∘ₗ LinearMap.inl R M M₂ : (a : M) → M₂) x :
        M₂)
      ((LinearMap.snd R M M₂ ∘ₗ LinearMap.inl R M M₂ : (a : M) → M₂) x : M₂)
⊢ Eq (α := M × M₂ →ₗ[R] M₂) (LinearMap.fst R M₂ M ∘ₗ (↑(prodComm R M M₂) : M × M₂ →ₗ[R] M₂ × M)) (LinearMap.snd R M M₂)
have hr : ∀ (x : M₂),
  Eq (α := M₂)
    (((LinearMap.fst R M₂ M ∘ₗ (↑(prodComm R M M₂) : M × M₂ →ₗ[R] M₂ × M)) ∘ₗ LinearMap.inr R M M₂ : (a : M₂) → M₂) x :
      M₂)
    ((LinearMap.snd R M M₂ ∘ₗ LinearMap.inr R M M₂ : (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) (LinearMap.snd R M₂ M ∘ₗ (↑(prodComm R M M₂) : M × M₂ →ₗ[R] M₂ × M)) (LinearMap.fst R M M₂)
have hl : ∀ (x : M),
  Eq (α := M)
    (((LinearMap.snd R M₂ M ∘ₗ (↑(prodComm R M M₂) : M × M₂ →ₗ[R] M₂ × M)) ∘ₗ LinearMap.inl R M M₂ : (a : M) → M) x : M)
    ((LinearMap.fst R M M₂ ∘ₗ LinearMap.inl R M M₂ : (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₂
hl :
  ∀ (x : M),
    Eq (α := M)
      (((LinearMap.snd R M₂ M ∘ₗ (↑(prodComm R M M₂) : M × M₂ →ₗ[R] M₂ × M)) ∘ₗ LinearMap.inl R M M₂ : (a : M) → M) x :
        M)
      ((LinearMap.fst R M M₂ ∘ₗ LinearMap.inl R M M₂ : (a : M) → M) x : M)
⊢ Eq (α := M × M₂ →ₗ[R] M) (LinearMap.snd R M₂ M ∘ₗ (↑(prodComm R M M₂) : M × M₂ →ₗ[R] M₂ × M)) (LinearMap.fst R M M₂)
have hr : ∀ (x : M₂),
  Eq.{v + 1} (α := M)
    (((LinearMap.snd R M₂ M ∘ₗ (↑(prodComm R M M₂) : M × M₂ →ₗ[R] M₂ × M)) ∘ₗ LinearMap.inr R M M₂ : (a : M₂) → M) x :
      M)
    ((LinearMap.fst R M M₂ ∘ₗ LinearMap.inr R M M₂ : (a : M₂) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
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₃
⊢ Eq (α := (M₁ × M₂) × M₃ →ₗ[R] M₁)
    (LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃))
    (LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃)
have hl : ∀ (x : M₁),
  Eq (α := M₁)
    ((((LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
              LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inl R M₁ M₂ :
          (a : M₁) → M₁)
        x :
      M₁)
    ((((LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inl R M₁ M₂ :
          (a : M₁) → M₁)
        x :
      M₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
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₃
hl :
  ∀ (x : M₁),
    Eq (α := M₁)
      ((((LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₁)
          x :
        M₁)
      ((((LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₁)
          x :
        M₁)
⊢ Eq (α := (M₁ × M₂) × M₃ →ₗ[R] M₁)
    (LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃))
    (LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃)
have hl₁ : ∀ (x : M₂),
  Eq.{u_3 + 1} (α := M₁)
    ((((LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
              LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inr R M₁ M₂ :
          (a : M₂) → M₁)
        x :
      M₁)
    ((((LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inr R M₁ M₂ :
          (a : M₂) → M₁)
        x :
      M₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
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₃
hl :
  ∀ (x : M₁),
    Eq (α := M₁)
      ((((LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₁)
          x :
        M₁)
      ((((LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₁)
          x :
        M₁)
hl₁ :
  ∀ (x : M₂),
    Eq.{u_3 + 1} (α := M₁)
      ((((LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inr R M₁ M₂ :
            (a : M₂) → M₁)
          x :
        M₁)
      ((((LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inr R M₁ M₂ :
            (a : M₂) → M₁)
          x :
        M₁)
⊢ Eq (α := (M₁ × M₂) × M₃ →ₗ[R] M₁)
    (LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃))
    (LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃)
have hr : ∀ (x : M₃),
  Eq.{u_3 + 1} (α := M₁)
    (((LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
            LinearMap.inr R (M₁ × M₂) M₃ :
          (a : M₃) → M₁)
        x :
      M₁)
    (((LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃) ∘ₗ LinearMap.inr R (M₁ × M₂) M₃ : (a : M₃) → M₁) x : M₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
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₃
⊢ Eq (α := (M₁ × M₂) × M₃ →ₗ[R] M₂ × M₃)
    (LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃))
    (LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id)
have hl : ∀ (x : M₁),
  Eq.{w + 1} (α := M₂)
    ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
              LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inl R M₁ M₂ :
          (a : M₁) → M₂ × M₃)
        x).1
    (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inl R M₁ M₂ :
          (a : M₁) → M₂ × M₃)
        x).1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
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₃
hl :
  ∀ (x : M₁),
    Eq.{w + 1} (α := M₂)
      ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).1
      (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).1
⊢ Eq (α := (M₁ × M₂) × M₃ →ₗ[R] M₂ × M₃)
    (LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃))
    (LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id)
have hl₁ : ∀ (x : M₁),
  Eq.{y + 1} (α := M₃)
    ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
              LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inl R M₁ M₂ :
          (a : M₁) → M₂ × M₃)
        x).2
    (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inl R M₁ M₂ :
          (a : M₁) → M₂ × M₃)
        x).2
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
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₃
hl :
  ∀ (x : M₁),
    Eq.{w + 1} (α := M₂)
      ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).1
      (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).1
hl₁ :
  ∀ (x : M₁),
    Eq.{y + 1} (α := M₃)
      ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).2
      (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).2
⊢ Eq (α := (M₁ × M₂) × M₃ →ₗ[R] M₂ × M₃)
    (LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃))
    (LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id)
have hl₂ : ∀ (x : M₂),
  Eq.{w + 1} (α := M₂)
    ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
              LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inr R M₁ M₂ :
          (a : M₂) → M₂ × M₃)
        x).1
    (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inr R M₁ M₂ :
          (a : M₂) → M₂ × M₃)
        x).1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
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₃
hl :
  ∀ (x : M₁),
    Eq.{w + 1} (α := M₂)
      ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).1
      (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).1
hl₁ :
  ∀ (x : M₁),
    Eq.{y + 1} (α := M₃)
      ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).2
      (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).2
hl₂ :
  ∀ (x : M₂),
    Eq.{w + 1} (α := M₂)
      ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inr R M₁ M₂ :
            (a : M₂) → M₂ × M₃)
          x).1
      (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inr R M₁ M₂ :
            (a : M₂) → M₂ × M₃)
          x).1
⊢ Eq (α := (M₁ × M₂) × M₃ →ₗ[R] M₂ × M₃)
    (LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃))
    (LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id)
have hl₃ : ∀ (x : M₂),
  Eq.{y + 1} (α := M₃)
    ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
              LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inr R M₁ M₂ :
          (a : M₂) → M₂ × M₃)
        x).2
    (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inr R M₁ M₂ :
          (a : M₂) → M₂ × M₃)
        x).2
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
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₃
hl :
  ∀ (x : M₁),
    Eq.{w + 1} (α := M₂)
      ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).1
      (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).1
hl₁ :
  ∀ (x : M₁),
    Eq.{y + 1} (α := M₃)
      ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).2
      (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).2
hl₂ :
  ∀ (x : M₂),
    Eq.{w + 1} (α := M₂)
      ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inr R M₁ M₂ :
            (a : M₂) → M₂ × M₃)
          x).1
      (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inr R M₁ M₂ :
            (a : M₂) → M₂ × M₃)
          x).1
hl₃ :
  ∀ (x : M₂),
    Eq.{y + 1} (α := M₃)
      ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inr R M₁ M₂ :
            (a : M₂) → M₂ × M₃)
          x).2
      (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inr R M₁ M₂ :
            (a : M₂) → M₂ × M₃)
          x).2
⊢ Eq (α := (M₁ × M₂) × M₃ →ₗ[R] M₂ × M₃)
    (LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃))
    (LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id)
have hr : ∀ (x : M₃),
  Eq.{w + 1} (α := M₂)
    (((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
            LinearMap.inr R (M₁ × M₂) M₃ :
          (a : M₃) → M₂ × M₃)
        x).1
    ((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inr R (M₁ × M₂) M₃ : (a : M₃) → M₂ × M₃) x).1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
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₃
hl :
  ∀ (x : M₁),
    Eq.{w + 1} (α := M₂)
      ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).1
      (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).1
hl₁ :
  ∀ (x : M₁),
    Eq.{y + 1} (α := M₃)
      ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).2
      (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).2
hl₂ :
  ∀ (x : M₂),
    Eq.{w + 1} (α := M₂)
      ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inr R M₁ M₂ :
            (a : M₂) → M₂ × M₃)
          x).1
      (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inr R M₁ M₂ :
            (a : M₂) → M₂ × M₃)
          x).1
hl₃ :
  ∀ (x : M₂),
    Eq.{y + 1} (α := M₃)
      ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inr R M₁ M₂ :
            (a : M₂) → M₂ × M₃)
          x).2
      (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inr R M₁ M₂ :
            (a : M₂) → M₂ × M₃)
          x).2
hr :
  ∀ (x : M₃),
    Eq.{w + 1} (α := M₂)
      (((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
              LinearMap.inr R (M₁ × M₂) M₃ :
            (a : M₃) → M₂ × M₃)
          x).1
      ((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inr R (M₁ × M₂) M₃ : (a : M₃) → M₂ × M₃)
          x).1
⊢ Eq (α := (M₁ × M₂) × M₃ →ₗ[R] M₂ × M₃)
    (LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃))
    (LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id)
have hr₁ : ∀ (x : M₃),
  Eq.{y + 1} (α := M₃)
    (((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
            LinearMap.inr R (M₁ × M₂) M₃ :
          (a : M₃) → M₂ × M₃)
        x).2
    ((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inr R (M₁ × M₂) M₃ : (a : 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
M₃ : Type y
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
⊢ (f.prod g).range = f.range.prod g.range
have refine : f.range.prod g.range ≤ (f.prod g).range
Tactic: refine le_antisymm (f.range_prod_le g) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
⊢ f.range.prod g.range ≤ (f.prod g).range
have simp : ∀ (a : M₂) (b : M₃) (x : M),
  (f : (a : M) → M₂) x = a →
    ∀ (x : M), (g : (a : M) → M₃) x = b → ∃ (y : M), ((f : (a : M) → M₂) y, (g : (a : M) → M₃) y) = (a, b)
Tactic: simp only [SetLike.le_def, prod_apply, mem_range, mem_prod, exists_imp, and_imp,
    Prod.forall, Function.prod_apply]