awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Prod
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₁ f₂ : M →ₗ[R] M₃
g₁ g₂ : M₂ →ₗ[R] M₄
⊢ (f₁ + f₂).prodMap (g₁ + g₂) = f₁.prodMap g₁ + f₂.prodMap g₂

Tactic:
rfl

Premises used: Function.prod, LinearMap.prod, rfl, LinearMap.prodMap
-- Module: Mathlib.LinearAlgebra.Prod
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₄
⊢ Eq (α := M × M₃ →ₗ[R] M₂ × M₄) (prodMap 0 0) 0

Tactic:
rfl

Premises used: Function.prod, LinearMap.prod, rfl, LinearMap.prodMap
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
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 : Module R M
inst_7 : Module R M₂
inst_8 : Module R M₃
inst_9 : Module R M₄
inst_10 : DistribMulAction S M₃
inst_11 : DistribMulAction S M₄
inst_12 : SMulCommClass R S M₃
inst_13 : SMulCommClass R S M₄
s : S
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₄
⊢ (s • f).prodMap (s • g) = s • f.prodMap g

Tactic:
rfl

Premises used: Function.prod, LinearMap.prod, rfl, LinearMap.prodMap
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
inst : Semiring R
A : Type u_4
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
B : Type u_5
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
a₁ a₂ : A
⊢ ((inl R A B : (a : A) → A × B) (a₁ * a₂)).2 =
    (HMul.hMul (α := A × B) (β := A × B) ((inl R A B : (a : A) → A × B) a₁ : A × B)
        ((inl R A B : (a : A) → A × B) a₂ : A × B)).2

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
inst : Semiring R
A : Type u_4
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
B : Type u_5
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
b₁ b₂ : B
⊢ ((inr R A B : (a : B) → A × B) (b₁ * b₂)).1 =
    (HMul.hMul (α := A × B) (β := A × B) ((inr R A B : (a : B) → A × B) b₁ : A × B)
        ((inr R A B : (a : B) → A × B) b₂ : A × B)).1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
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₃
x : M₃
⊢ x ∈ (f.coprod g).range ↔ x ∈ f.range ⊔ g.range

Tactic:
simp [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₂
disjoint : Disjoint (α := Submodule R (M × M₂)) (range (inl R M M₂)) (range (inr R M M₂))
codisjoint : Codisjoint (α := 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₂))

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₂
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
⊢ Disjoint (α := Submodule R (M × M₂)) (range (inl R M M₂)) (range (inr R M M₂))

Tactic:
rw [disjoint_def]

Premises used: Submodule.disjoint_def
-- 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₂
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)
disjoint : ∀ (hx : x = fst ∧ 0 = snd) (hy : 0 = fst ∧ y = snd), fst = 0.1 ∧ snd = 0.2
⊢ (fst, snd) = 0

Tactic:
simp only [Prod.ext_iff, inl_apply, inr_apply] at hx hy ⊢

Premises used: LinearMap.inr_apply, Prod.ext_iff, 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₂
fst : M
snd : M₂
x : M
y : M₂
hx : x = fst ∧ 0 = snd
hy : 0 = fst ∧ y = snd
⊢ fst = 0.1 ∧ snd = 0.2

Tactic:
⟨hy.1.symm, hx.2.symm⟩

Premises used: And.right, And.left, And.intro, Eq.symm
-- 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₂
fst : M
snd : M₂
x : M
y : M₂
hx : x = fst ∧ 0 = snd
hy : 0 = fst ∧ y = snd
⊢ fst = 0.1 ∧ snd = 0.2

Tactic:
exact ⟨hy.1.symm, hx.2.symm⟩
-- 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₂
codisjoint : LE.le (α := Submodule R (M × M₂)) ⊤ (range (inl R M M₂) ⊔ range (inr R M M₂))
⊢ Codisjoint (α := Submodule R (M × M₂)) (range (inl R M M₂)) (range (inr R M M₂))

Tactic:
rw [codisjoint_iff_le_sup]

Premises used: codisjoint_iff_le_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₂
x : M
y : M₂
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)
⊢ Membership.mem (γ := Submodule R (M × M₂)) (range (inl R M M₂) ⊔ range (inr R M M₂)) (x, y)

Tactic:
simp only [mem_sup, mem_range]

Premises used: LinearMap.mem_range, 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₂
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)

Tactic:
⟨(x, 0), ⟨x, rfl⟩, (0, y), ⟨y, rfl⟩, ?_⟩

Premises used: Prod.mk, And.intro, Exists.intro, OfNat.ofNat, 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₂
x : M
y : M₂
codisjoint : (x, 0) + (0, y) = (x, y)
⊢ ∃ (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:
refine ⟨(x, 0), ⟨x, rfl⟩, (0, y), ⟨y, 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₂
x : M
y : M₂
⊢ (x, 0) + (0, y) = (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₂
⊢ Eq (α := Submodule R (M × M₂)) (range (inl R M M₂) ⊔ range (inr R M M₂)) ⊤

Tactic:
IsCompl.sup_eq_top isCompl_range_inl_inr

Premises used: IsCompl.sup_eq_top, LinearMap.isCompl_range_inl_inr
-- 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₂
⊢ Disjoint (α := Submodule R (M × M₂)) (range (inl R M M₂)) (range (inr R M M₂))

Tactic:
simp +contextual [disjoint_def, @eq_comm M 0]

Premises used: eq_comm, Submodule.disjoint_def
-- Module: Mathlib.LinearAlgebra.Prod
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₃
p : Submodule R M
q : Submodule R M₂
⊢ map (f.coprod g) (p.prod q) = map f p ⊔ map g q

Tactic:
coprod_map_prod f g p q

Premises used: LinearMap.coprod_map_prod
-- Module: Mathlib.LinearAlgebra.Prod
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₃
p : Submodule R M₂
q : Submodule R M₃
⊢ comap (f.prod g) (p.prod q) = comap f p ⊓ comap g q

Tactic:
Submodule.ext fun _x => Iff.rfl

Premises used: Iff.rfl, Submodule.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₂
⊢ p.prod q = comap (fst R M M₂) p ⊓ comap (snd R M M₂) q

Tactic:
Submodule.ext fun _x => Iff.rfl

Premises used: Iff.rfl, Submodule.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₂
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)
rw₂ rw₃ : p.prod q = p.prod q
⊢ p.prod q = map (inl R M M₂) p ⊔ map (inr R M M₂) q

Tactic:
rw [← map_coprod_prod, coprod_inl_inr, map_id]

Premises used: Submodule.map_id, LinearMap.map_coprod_prod, LinearMap.coprod_inl_inr
-- 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₂
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))
rw₃ 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))
⊢ 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))

Tactic:
rw [span_union, prod_eq_sup_map, ← span_image, ← span_image]

Premises used: Submodule.span_union, Submodule.span_image, LinearMap.prod_eq_sup_map
-- Module: Mathlib.LinearAlgebra.Prod
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₃
rw : comap f ⊥ ⊓ comap g ⊥ = f.ker ⊓ g.ker
⊢ (f.prod g).ker = f.ker ⊓ g.ker

Tactic:
rw [ker, ← prod_bot, comap_prod_prod]

Premises used: LinearMap.ker, Submodule.prod_bot, LinearMap.comap_prod_prod
-- Module: Mathlib.LinearAlgebra.Prod
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₃
⊢ comap f ⊥ ⊓ comap g ⊥ = f.ker ⊓ g.ker

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Prod
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₃
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
⊢ (f.prod g).range ≤ f.range.prod g.range

Tactic:
simp only [SetLike.le_def, prod_apply, mem_range, mem_prod, exists_imp]

Premises used: Submodule.mem_prod, SetLike.le_def, LinearMap.mem_range, LinearMap.prod_apply, exists_imp
-- Module: Mathlib.LinearAlgebra.Prod
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₃
x : M
⊢ (∃ (y : M),
      Eq.{w + 1} (α := M₂) ((f : (a : M) → M₂) y : M₂)
        ((Function.prod (α := fun (a : M) ↦ M₂) (β := fun (a : M) ↦ M₃) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₃) x).1 :
          M₂)) ∧
    ∃ (y : M),
      Eq.{y + 1} (α := M₃) ((g : (a : M) → M₃) y : M₃)
        ((Function.prod (α := fun (a : M) ↦ M₂) (β := fun (a : M) ↦ M₃) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₃) x).2 :
          M₃)

Tactic:
⟨⟨x, rfl⟩, ⟨x, rfl⟩⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.LinearAlgebra.Prod
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₃
x : M
⊢ (∃ (y : M),
      Eq.{w + 1} (α := M₂) ((f : (a : M) → M₂) y : M₂)
        ((Function.prod (α := fun (a : M) ↦ M₂) (β := fun (a : M) ↦ M₃) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₃) x).1 :
          M₂)) ∧
    ∃ (y : M),
      Eq.{y + 1} (α := M₃) ((g : (a : M) → M₃) y : M₃)
        ((Function.prod (α := fun (a : M) ↦ M₂) (β := fun (a : M) ↦ M₃) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₃) x).2 :
          M₃)

Tactic:
exact ⟨⟨x, rfl⟩, ⟨x, rfl⟩⟩
-- Module: Mathlib.LinearAlgebra.Prod
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 : AddCommMonoid M₂
inst_4 : Module R M₂
M₃ : Type u_4
inst_5 : AddCommMonoid M₃
inst_6 : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
y : M
z : M₂
⊢ (y, z) ∈ f.ker.prod g.ker → (y, z) ∈ (f.coprod g).ker

Tactic:
simp +contextual
-- Module: Mathlib.LinearAlgebra.Prod
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
apply : (f.coprod g).ker ≤ f.ker.prod g.ker
⊢ (f.coprod g).ker = f.ker.prod g.ker

Tactic:
apply le_antisymm _ (ker_prod_ker_le_ker_coprod f g)

Premises used: LinearMap.ker_prod_ker_le_ker_coprod, le_antisymm
-- Module: Mathlib.LinearAlgebra.Prod
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
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₃)
⊢ (y, z) ∈ f.ker.prod g.ker

Tactic:
simp only [mem_ker, mem_prod, coprod_apply] at h ⊢

Premises used: Submodule.mem_prod, LinearMap.coprod_apply, LinearMap.mem_ker
-- Module: Mathlib.LinearAlgebra.Prod
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
simp : ∃ (y_1 : M₂), Eq.{u_4 + 1} (α := M₃) ((g : (a : M₂) → M₃) y_1 : M₃) ((f : (a : M) → M₃) y : M₃)
⊢ Membership.mem (α := M₃) (f.range ⊓ g.range) ((f : (a : M) → M₃) y : M₃)

Tactic:
simp only [true_and, mem_range, mem_inf, exists_apply_eq_apply]

Premises used: Submodule.mem_inf, LinearMap.mem_range, true_and, exists_apply_eq_apply
-- Module: Mathlib.LinearAlgebra.Prod
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₃) ((g : (a : M₂) → M₃) (-z) : M₃) ((f : (a : M) → M₃) y : M₃)
⊢ ∃ (y_1 : M₂), Eq.{u_4 + 1} (α := M₃) ((g : (a : M₂) → M₃) y_1 : M₃) ((f : (a : M) → M₃) y : M₃)

Tactic:
use -z
-- Module: Mathlib.LinearAlgebra.Prod
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₃)
h₃ : HSub.hSub (α := M₃) (β := M₃) ((f : (a : M) → M₃) y : M₃) (-(g : (a : M₂) → M₃) z : M₃) = 0
h₄ h₅ h₆ 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₃)

Tactic:
rwa [eq_comm, map_neg, ← sub_eq_zero, sub_neg_eq_add]

Premises used: sub_eq_zero, map_neg, eq_comm, sub_neg_eq_add
-- Module: Mathlib.LinearAlgebra.Prod
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₃)

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]
-- Module: Mathlib.LinearAlgebra.Prod
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₃)

Tactic:
rw [hd.eq_bot, mem_bot] at this

Premises used: Submodule.mem_bot, Disjoint.eq_bot
-- Module: Mathlib.LinearAlgebra.Prod
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₃)
⊢ HAdd.hAdd (α := M₃) (β := M₃) (0 : M₃) ((g : (a : M₂) → M₃) z : M₃) = 0

Tactic:
rw [this] at h
-- Module: Mathlib.LinearAlgebra.Prod
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₃)
h₁ : HAdd.hAdd (α := M₃) (β := M₃) (0 : M₃) ((g : (a : M₂) → M₃) z : M₃) = 0
⊢ Eq.{u_4 + 1} (α := M₃) ((f : (a : M) → M₃) y : M₃) (0 : M₃)

Tactic:
rw [this] at h
-- Module: Mathlib.LinearAlgebra.Prod
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₃) (0 : 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₃)

Tactic:
simpa [this] using h
-- 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
⊢ Function.Injective.{u_4 + 1, u_5 + 1} (α := ↥C) (β := ↥f.range)
    (⇑(codRestrict f.range f ⋯ ∘ₗ C.subtype) : (a : ↥C) → ↥f.range)

Tactic:
simpa [← ker_eq_bot, ker_codRestrict, ker_comp, ← disjoint_iff_comap_eq_bot] using h.disjoint

Premises used: LinearMap.ker_eq_bot, LinearMap.ker_codRestrict, LinearMap.ker_comp, IsCompl.disjoint, Submodule.disjoint_iff_comap_eq_bot
-- 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
x : M
obtain :
  ∀ (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)
⊢ ∃ (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)

Tactic:
obtain ⟨y, z, hy, hz, rfl⟩ := codisjoint_iff_exists_add_eq.mp h.codisjoint x

Premises used: Submodule.codisjoint_iff_exists_add_eq, Iff.mp, IsCompl.codisjoint, rfl