awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Prod
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
h₁ :
  Eq.{u_5 + 1} (α := ↥f.range)
    ((codRestrict f.range f ⋯ ∘ₗ 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)) ⋯ : ↥f.range)
⊢ ∃ (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)

Tactic:
use ⟨y, hy⟩
-- Module: Mathlib.LinearAlgebra.Prod
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
⊢ Eq.{u_5 + 1} (α := ↥f.range)
    ((codRestrict f.range f ⋯ ∘ₗ 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)) ⋯ : ↥f.range)

Tactic:
simpa [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
x : M
⊢ x ∈ p ⊔ q ↔ x ∈ (p.subtype.coprod q.subtype).range

Tactic:
simp [Submodule.mem_sup]

Premises used: Submodule.mem_sup
-- Module: Mathlib.LinearAlgebra.Prod
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
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)
⊢ Eq (α := Submodule R (M × M₂)) (map (inl R M M₂) p) (p.prod ⊥)

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.LinearAlgebra.Prod
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
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:
simp only [and_left_comm, eq_comm, mem_map, Prod.mk_inj, inl_apply, mem_bot, exists_eq_left',
    mem_prod]

Premises used: Submodule.mem_prod, Submodule.mem_bot, Submodule.mem_map, Prod.mk_inj, exists_eq_left', and_left_comm, eq_comm, LinearMap.inl_apply
-- Module: Mathlib.LinearAlgebra.Prod
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₂
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)
⊢ Eq (α := Submodule R (M × M₂)) (map (inr R M M₂) q) (prod ⊥ q)

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.LinearAlgebra.Prod
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₂
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:
simp [and_left_comm, eq_comm, and_comm]

Premises used: and_left_comm, and_comm, eq_comm
-- Module: Mathlib.LinearAlgebra.Prod
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
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)
⊢ Eq (α := Submodule R (M × M₂)) (comap (fst R M M₂) p) (p.prod ⊤)

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.LinearAlgebra.Prod
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
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:
simp
-- Module: Mathlib.LinearAlgebra.Prod
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₂
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)
⊢ Eq (α := Submodule R (M × M₂)) (comap (snd R M M₂) q) (prod ⊤ q)

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.LinearAlgebra.Prod
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₂
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:
simp
-- Module: Mathlib.LinearAlgebra.Prod
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₂
h : ∀ (x : M), x ∈ comap (inl R M M₂) (p.prod q) ↔ x ∈ p
⊢ comap (inl R M M₂) (p.prod q) = p

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Prod
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₂
x : M
⊢ x ∈ comap (inl R M M₂) (p.prod q) ↔ x ∈ p

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
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₂
h : ∀ (x : M₂), x ∈ comap (inr R M M₂) (p.prod q) ↔ x ∈ q
⊢ comap (inr R M M₂) (p.prod q) = q

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Prod
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₂
x : M₂
⊢ x ∈ comap (inr R M M₂) (p.prod q) ↔ x ∈ q

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
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₂
h : ∀ (x : M), x ∈ map (fst R M M₂) (p.prod q) ↔ x ∈ p
⊢ map (fst R M M₂) (p.prod q) = p

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Prod
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₂
x : M
⊢ x ∈ map (fst R M M₂) (p.prod q) ↔ x ∈ p

Tactic:
simp [(⟨0, zero_mem _⟩ : ∃ x, x ∈ q)]

Premises used: Exists.intro, ZeroMemClass.zero_mem, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Prod
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₂
h : ∀ (x : M₂), x ∈ map (snd R M M₂) (p.prod q) ↔ x ∈ q
⊢ map (snd R M M₂) (p.prod q) = q

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Prod
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₂
x : M₂
⊢ x ∈ map (snd R M M₂) (p.prod q) ↔ x ∈ q

Tactic:
simp [(⟨0, zero_mem _⟩ : ∃ x, x ∈ p)]

Premises used: Exists.intro, ZeroMemClass.zero_mem, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Prod
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 ⊥ ⊥)) ⊥
rw₂ rw₃ : Eq.{v + 1} (α := Submodule R M) ⊥ ⊥
⊢ Eq (α := Submodule R M) (ker (inl R M M₂)) ⊥

Tactic:
rw [ker, ← prod_bot, prod_comap_inl]

Premises used: LinearMap.ker, Submodule.prod_comap_inl, Submodule.prod_bot
-- Module: Mathlib.LinearAlgebra.Prod
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 ⊥ ⊥)) ⊥
rw₂ rw₃ : Eq.{w + 1} (α := Submodule R M₂) ⊥ ⊥
⊢ Eq (α := Submodule R M₂) (ker (inr R M M₂)) ⊥

Tactic:
rw [ker, ← prod_bot, prod_comap_inr]

Premises used: Submodule.prod_comap_inr, LinearMap.ker, Submodule.prod_bot
-- Module: Mathlib.LinearAlgebra.Prod
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 ⊤ ⊤)) ⊤
rw₂ rw₃ : Eq.{v + 1} (α := Submodule R M) ⊤ ⊤
⊢ Eq (α := Submodule R M) (range (fst R M M₂)) ⊤

Tactic:
rw [range_eq_map, ← prod_top, prod_map_fst]

Premises used: Submodule.prod_top, LinearMap.range_eq_map, Submodule.prod_map_fst
-- Module: Mathlib.LinearAlgebra.Prod
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 ⊤ ⊤)) ⊤
rw₂ rw₃ : Eq.{w + 1} (α := Submodule R M₂) ⊤ ⊤
⊢ Eq (α := Submodule R M₂) (range (snd R M M₂)) ⊤

Tactic:
rw [range_eq_map, ← prod_top, prod_map_snd]

Premises used: Submodule.prod_top, LinearMap.range_eq_map, Submodule.prod_map_snd
-- Module: Mathlib.LinearAlgebra.Prod
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
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₂
⊢ ∀ (x y : ↥(fst R M M₂)), (↑(x + y) : M × M₂).1 = (↑x : M × M₂).1 + (↑y : M × M₂).1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
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
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₂
⊢ ∀ (m : R) (x : ↥(fst R M M₂)),
    (↑(m • x) : M × M₂).1 = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R) (↑x : M × M₂).1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
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
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₂
m : M
⊢ Membership.mem (γ := Submodule R (M × M₂)) (fst R M M₂) (m, 0)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Prod
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
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₂
x : ↥(fst R M M₂)
⊢ (fun (m : M) ↦
        (Subtype.mk (p := fun (x : M × M₂) ↦ Membership.mem (γ := Submodule R (M × M₂)) (fst R M M₂) x) (m, 0) ⋯ :
          ↥(fst R M M₂)))
      ((fun (x : ↥(fst R M M₂)) ↦ (↑x : M × M₂).1) x) =
    x

Tactic:
aesop (add norm simp Submodule.fst)

Premises used: Submodule.fst
-- Module: Mathlib.LinearAlgebra.Prod
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
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₂
x : M
⊢ (fun (x : ↥(fst R M M₂)) ↦ (↑x : M × M₂).1)
      ((fun (m : M) ↦
          (Subtype.mk (p := fun (x : M × M₂) ↦ Membership.mem (γ := Submodule R (M × M₂)) (fst R M M₂) x) (m, 0) ⋯ :
            ↥(fst R M M₂)))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
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) (map (LinearMap.fst R M M₂) (fst R M M₂)) ⊤

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Prod
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₂) (map (snd R M M₂) (fst R M M₂)) ⊥

Tactic:
aesop (add simp fst)

Premises used: Submodule.fst
-- Module: Mathlib.LinearAlgebra.Prod
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
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₂
⊢ ∀ (x y : ↥(snd R M M₂)), (↑(x + y) : M × M₂).2 = (↑x : M × M₂).2 + (↑y : M × M₂).2

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
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
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₂
⊢ ∀ (m : R) (x : ↥(snd R M M₂)),
    (↑(m • x) : M × M₂).2 = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R) (↑x : M × M₂).2

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
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
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₂
n : M₂
⊢ Membership.mem (γ := Submodule R (M × M₂)) (snd R M M₂) (0, n)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Prod
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
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₂
x : ↥(snd R M M₂)
⊢ (fun (n : M₂) ↦
        (Subtype.mk (p := fun (x : M × M₂) ↦ Membership.mem (γ := Submodule R (M × M₂)) (snd R M M₂) x) (0, n) ⋯ :
          ↥(snd R M M₂)))
      ((fun (x : ↥(snd R M M₂)) ↦ (↑x : M × M₂).2) x) =
    x

Tactic:
aesop (add norm simp Submodule.snd)

Premises used: Submodule.snd
-- Module: Mathlib.LinearAlgebra.Prod
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) (map (LinearMap.fst R M M₂) (snd R M M₂)) ⊥

Tactic:
aesop (add simp snd)

Premises used: Submodule.snd
-- Module: Mathlib.LinearAlgebra.Prod
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₂) (map (LinearMap.snd R M M₂) (snd R M M₂)) ⊤

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Prod
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 : LE.le (α := Submodule R (M × M₂)) ⊤ (fst R M M₂ ⊔ snd R M M₂)
⊢ Eq (α := Submodule R (M × M₂)) (fst R M M₂ ⊔ snd R M M₂) ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.LinearAlgebra.Prod
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₂
⊢ (m, n) = (m, 0) + (0, n)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
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₂
rw : Membership.mem (γ := Submodule R (M × M₂)) (fst R M M₂ ⊔ snd R M M₂) ((m, 0) + (0, n))
⊢ Membership.mem (γ := Submodule R (M × M₂)) (fst R M M₂ ⊔ snd R M M₂) (m, n)

Tactic:
rw [show (m, n) = (m, 0) + (0, n) by simp]
-- Module: Mathlib.LinearAlgebra.Prod
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)
h₂ : Membership.mem (γ := Submodule R (M × M₂)) (fst R M M₂ ⊔ snd R M M₂) (0, n)
⊢ Membership.mem (γ := Submodule R (M × M₂)) (fst R M M₂ ⊔ snd R M M₂) ((m, 0) + (0, n))

Tactic:
apply Submodule.add_mem (Submodule.fst R M M₂ ⊔ Submodule.snd R M M₂)

Premises used: Submodule.snd, Submodule.fst, Max.max, Submodule.add_mem
-- Module: Mathlib.LinearAlgebra.Prod
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.{w, w} (α := M₂) (γ := Submodule R M₂) ⊥ ((LinearMap.snd R M M₂ : (a : M × M₂) → M₂) (m, 0) : M₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
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)

Tactic:
exact Submodule.mem_sup_left (Submodule.mem_comap.mpr (by simp))

Premises used: Iff.mpr, Submodule.mem_comap, Submodule.mem_sup_left
-- Module: Mathlib.LinearAlgebra.Prod
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.{v, v} (α := M) (γ := Submodule R M) ⊥ ((LinearMap.fst R M M₂ : (a : M × M₂) → M) (0, n) : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
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₂) (0, n)

Tactic:
exact Submodule.mem_sup_right (Submodule.mem_comap.mpr (by simp))

Premises used: Iff.mpr, Submodule.mem_comap, Submodule.mem_sup_right
-- Module: Mathlib.LinearAlgebra.Prod
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₂) ⊥

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Prod
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₂
mpr : map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂ → q ≤ p₁.prod p₂
⊢ q ≤ p₁.prod p₂ ↔ map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Prod
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₁
mp₁ : map (LinearMap.snd R M M₂) q ≤ p₂
⊢ map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Prod
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₂
y1 : M
y2 : M₂
hy1 : (y1, y2) ∈ (↑q : Set (M × M₂))
⊢ Membership.mem (α := M) p₁ ((LinearMap.fst R M M₂ : (a : M × M₂) → M) (y1, y2) : M)

Tactic:
(h hy1).1

Premises used: Set.Mem, And.left
-- Module: Mathlib.LinearAlgebra.Prod
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₂
y1 : M
y2 : M₂
hy1 : (y1, y2) ∈ (↑q : Set (M × M₂))
⊢ Membership.mem (α := M) p₁ ((LinearMap.fst R M M₂ : (a : M × M₂) → M) (y1, y2) : M)

Tactic:
exact (h hy1).1

Premises used: And.left
-- Module: Mathlib.LinearAlgebra.Prod
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₂
y1 : M
y2 : M₂
hy1 : (y1, y2) ∈ (↑q : Set (M × M₂))
⊢ Membership.mem (α := M₂) p₂ ((LinearMap.snd R M M₂ : (a : M × M₂) → M₂) (y1, y2) : M₂)

Tactic:
(h hy1).2

Premises used: Set.Mem, And.right
-- Module: Mathlib.LinearAlgebra.Prod
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₂
y1 : M
y2 : M₂
hy1 : (y1, y2) ∈ (↑q : Set (M × M₂))
⊢ Membership.mem (α := M₂) p₂ ((LinearMap.snd R M M₂ : (a : M × M₂) → M₂) (y1, y2) : M₂)

Tactic:
exact (h hy1).2

Premises used: And.right
-- Module: Mathlib.LinearAlgebra.Prod
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 (LinearMap.fst R M M₂) q ≤ p₁
hK : map (LinearMap.snd R M M₂) q ≤ p₂
x1 : M
x2 : M₂
h : (x1, x2) ∈ q
⊢ (x1, x2) ∈ p₁.prod p₂

Tactic:
⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩

Premises used: Set.Mem, setOf, Set.prod, And.intro, Exists.intro, rfl
-- Module: Mathlib.LinearAlgebra.Prod
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 (LinearMap.fst R M M₂) q ≤ p₁
hK : map (LinearMap.snd R M M₂) q ≤ p₂
x1 : M
x2 : M₂
h : (x1, x2) ∈ q
⊢ (x1, x2) ∈ p₁.prod p₂

Tactic:
exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩
-- Module: Mathlib.LinearAlgebra.Prod
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
mpr : map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q → p₁.prod p₂ ≤ q
⊢ p₁.prod p₂ ≤ q ↔ map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q

Tactic:
constructor