awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
N : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
x : M × N
⊢ (fun (x : N × M) ↦ (x.2, -x.1)) ((fun (x : M × N) ↦ (-x.2, x.1)) x) = x

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
N : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
x : N × M
⊢ (fun (x : M × N) ↦ (-x.2, x.1)) ((fun (x : N × M) ↦ (x.2, -x.1)) x) = x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
N : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
x : M × N
⊢ (LinearEquiv.skewSwap R M N : (a : M × N) → N × M) x = (-x.2, x.1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
N : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
x : N × M
⊢ (symm (LinearEquiv.skewSwap R M N) : (a : N × M) → M × N) x = (x.2, -x.1)

Tactic:
rfl

Premises used: rfl
-- 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₃) × M₂ × M₄) ≃ₗ[R] (M × M₂) × M₃ × M₄) (symm (prodProdProdComm R M M₂ M₃ M₄))
    (prodProdProdComm R M M₃ M₂ M₄)

Tactic:
rfl

Premises used: LinearEquiv.prodProdProdComm, LinearEquiv.symm, rfl
-- 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₂) × M₃ × M₄ ≃+ (M × M₃) × M₂ × M₄)
    (↑(prodProdProdComm R M M₂ M₃ M₄) : (M × M₂) × M₃ × M₄ ≃+ (M × M₃) × M₂ × M₄) (AddEquiv.prodProdProdComm M M₂ M₃ M₄)

Tactic:
rfl

Premises used: AddEquiv.prodProdProdComm, EquivLike.toEquiv, rfl
-- 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₄
module_M : Module R M
module_M₂ : Module R M₂
module_M₃ : Module R M₃
module_M₄ : Module R M₄
e₁ : M ≃ₗ[R] M₂
e₂ : M₃ ≃ₗ[R] M₄
⊢ (e₁.prodCongr e₂).symm = e₁.symm.prodCongr e₂.symm

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearEquiv.prodCongr, Prod.map, rfl
-- 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₄
module_M : Module R M
module_M₂ : Module R M₂
module_M₃ : Module R M₃
module_M₄ : Module R M₄
e₁ : M ≃ₗ[R] M₂
e₂ : M₃ ≃ₗ[R] M₄
p : M × M₃
⊢ Eq (α := M₂ × M₄) ((e₁.prodCongr e₂ : (a : M × M₃) → M₂ × M₄) p : M₂ × M₄)
    (((e₁ : (a : M) → M₂) p.1, (e₂ : (a : M₃) → M₄) p.2) : M₂ × M₄)

Tactic:
rfl

Premises used: Prod.map, rfl
-- 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₄
module_M : Module R M
module_M₂ : Module R M₂
module_M₃ : Module R M₃
module_M₄ : Module R M₄
e₁ : M ≃ₗ[R] M₂
e₂ : M₃ ≃ₗ[R] M₄
⊢ (↑(e₁.prodCongr e₂) : M × M₃ →ₗ[R] M₂ × M₄) = (↑e₁ : M →ₗ[R] M₂).prodMap (↑e₂ : M₃ →ₗ[R] M₄)

Tactic:
rfl

Premises used: Prod.map, Function.prod, LinearMap.prod, rfl, LinearMap.prodMap
-- 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 : AddCommMonoid M₃
inst_4 : AddCommGroup M₄
module_M : Module R M
module_M₂ : Module R M₂
module_M₃ : Module R M₃
module_M₄ : Module R M₄
e₁ : M ≃ₗ[R] M₂
e₂ : M₃ ≃ₗ[R] M₄
f : M →ₗ[R] M₄
p : M × M₃
⊢ (fun (p : M₂ × M₄) ↦
        (((e₁.symm : (a : M₂) → M) p.1,
            (e₂.symm : (a : M₄) → M₃)
              (HSub.hSub (β := M₄) p.2 ((f : (a : M) → M₄) ((e₁.symm : (a : M₂) → M) p.1 : M) : M₄))) :
          M × M₃))
      ((LinearMap.prod ((↑e₁ : M →ₗ[R] M₂) ∘ₗ LinearMap.fst R M M₃)
            ((↑e₂ : M₃ →ₗ[R] M₄) ∘ₗ LinearMap.snd R M M₃ + f ∘ₗ LinearMap.fst R M M₃)).toFun
        p) =
    p

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 : AddCommMonoid M₃
inst_4 : AddCommGroup M₄
module_M : Module R M
module_M₂ : Module R M₂
module_M₃ : Module R M₃
module_M₄ : Module R M₄
e₁ : M ≃ₗ[R] M₂
e₂ : M₃ ≃ₗ[R] M₄
f : M →ₗ[R] M₄
p : M₂ × M₄
⊢ (LinearMap.prod ((↑e₁ : M →ₗ[R] M₂) ∘ₗ LinearMap.fst R M M₃)
          ((↑e₂ : M₃ →ₗ[R] M₄) ∘ₗ LinearMap.snd R M M₃ + f ∘ₗ LinearMap.fst R M M₃)).toFun
      ((fun (p : M₂ × M₄) ↦
          (((e₁.symm : (a : M₂) → M) p.1,
              (e₂.symm : (a : M₄) → M₃)
                (HSub.hSub (β := M₄) p.2 ((f : (a : M) → M₄) ((e₁.symm : (a : M₂) → M) p.1 : M) : M₄))) :
            M × M₃))
        p) =
    p

Tactic:
simp
-- 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 : AddCommGroup M₄
module_M : Module R M
module_M₂ : Module R M₂
module_M₃ : Module R M₃
module_M₄ : Module R M₄
e₁ : M ≃ₗ[R] M₂
e₂ : M₃ ≃ₗ[R] M₄
f : M →ₗ[R] M₄
x : M × M₃
⊢ Eq (α := M₂ × M₄) ((e₁.skewProd e₂ f : (a : M × M₃) → M₂ × M₄) x : M₂ × M₄)
    (((e₁ : (a : M) → M₂) x.1,
        HAdd.hAdd (α := M₄) (β := M₄) ((e₂ : (a : M₃) → M₄) x.2 : M₄) ((f : (a : M) → M₄) x.1 : M₄)) :
      M₂ × M₄)

Tactic:
rfl

Premises used: Function.prod, rfl
-- 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 : AddCommGroup M₄
module_M : Module R M
module_M₂ : Module R M₂
module_M₃ : Module R M₃
module_M₄ : Module R M₄
e₁ : M ≃ₗ[R] M₂
e₂ : M₃ ≃ₗ[R] M₄
f : M →ₗ[R] M₄
x : M₂ × M₄
⊢ Eq (α := M × M₃) (((e₁.skewProd e₂ f).symm : (a : M₂ × M₄) → M × M₃) x : M × M₃)
    (((e₁.symm : (a : M₂) → M) x.1,
        (e₂.symm : (a : M₄) → M₃)
          (HSub.hSub (β := M₄) x.2 ((f : (a : M) → M₄) ((e₁.symm : (a : M₂) → M) x.1 : M) : M₄))) :
      M × M₃)

Tactic:
rfl

Premises used: rfl
-- 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₂
inst_5 : Unique M₂
⊢ ∀ (c : R) (x : M₂ × M),
    ((AddEquiv.uniqueProd : M₂ × M ≃+ M) : (a : M₂ × M) → M) (c • x) =
      HSMul.hSMul (β := M) c (((AddEquiv.uniqueProd : M₂ × M ≃+ M) : (a : M₂ × M) → M) x : M)

Tactic:
simp [AddEquiv.uniqueProd]

Premises used: AddEquiv.uniqueProd
-- 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₂
inst_5 : Unique M₂
⊢ (↑uniqueProd : M₂ × M ≃ M) = Equiv.uniqueProd M M₂

Tactic:
rfl

Premises used: Equiv.trans, Equiv.uniqueProd, rfl
-- 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₂
inst_5 : Unique M₂
⊢ ∀ (c : R) (x : M × M₂),
    ((AddEquiv.prodUnique : M × M₂ ≃+ M) : (a : M × M₂) → M) (c • x) =
      HSMul.hSMul (β := M) c (((AddEquiv.prodUnique : M × M₂ ≃+ M) : (a : M × M₂) → M) x : M)

Tactic:
simp [AddEquiv.prodUnique]

Premises used: AddEquiv.prodUnique
-- 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₂
inst_5 : Unique M₂
⊢ (↑prodUnique : M × M₂ ≃ M) = Equiv.prodUnique M M₂

Tactic:
rfl

Premises used: Equiv.trans, Equiv.prodUnique, rfl
-- Module: Mathlib.LinearAlgebra.Prod
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

Tactic:
le_antisymm (f.range_prod_le g) ?_

Premises used: LinearMap.range_prod_le, le_antisymm
-- Module: Mathlib.LinearAlgebra.Prod
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 = ⊤
refine : f.range.prod g.range ≤ (f.prod g).range
⊢ (f.prod g).range = f.range.prod g.range

Tactic:
refine le_antisymm (f.range_prod_le g) ?_

Premises used: LinearMap.range_prod_le, le_antisymm
-- Module: Mathlib.LinearAlgebra.Prod
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 = ⊤
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)
⊢ f.range.prod g.range ≤ (f.prod g).range

Tactic:
simp only [SetLike.le_def, prod_apply, mem_range, mem_prod, exists_imp, and_imp,
    Prod.forall, Function.prod_apply]

Premises used: Submodule.mem_prod, and_imp, SetLike.le_def, LinearMap.mem_range, Prod.forall, Function.prod_apply, LinearMap.prod_apply, exists_imp
-- Module: Mathlib.LinearAlgebra.Prod
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 = ⊤
x y : M
simp : ∃ (y_1 : M), y_1 - x ∈ f.ker ∧ Eq.{y + 1} (α := M₃) ((g : (a : M) → M₃) y_1 : M₃) ((g : (a : M) → M₃) y : M₃)
⊢ ∃ (y_1 : M),
    Eq (α := M₂ × M₃) (((f : (a : M) → M₂) y_1, (g : (a : M) → M₃) y_1) : M₂ × M₃)
      (((f : (a : M) → M₂) x, (g : (a : M) → M₃) y) : M₂ × M₃)

Tactic:
simp only [Prod.mk_inj, ← sub_mem_ker_iff (f := f)]

Premises used: LinearMap.sub_mem_ker_iff, Prod.mk_inj
-- Module: Mathlib.LinearAlgebra.Prod
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 = ⊤
x y : M
⊢ y - x ∈ f.ker ⊔ g.ker

Tactic:
simp only [h, mem_top]

Premises used: Submodule.mem_top
-- Module: Mathlib.LinearAlgebra.Prod
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 = ⊤
x y : M
⊢ y - x ∈ f.ker ⊔ g.ker

Tactic:
have : y - x ∈ ker f ⊔ ker g := by simp only [h, mem_top]
-- Module: Mathlib.LinearAlgebra.Prod
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 = ⊤
x y : M
this : y - x ∈ f.ker ⊔ g.ker
rcases :
  ∀ (x' : M) (hx' : x' ∈ f.ker) (y' : M) (hy' : y' ∈ g.ker) (H : x' + y' = y - x),
    ∃ (y_1 : M), y_1 - x ∈ f.ker ∧ Eq.{y + 1} (α := M₃) ((g : (a : M) → M₃) y_1 : M₃) ((g : (a : M) → M₃) y : M₃)
⊢ ∃ (y_1 : M), y_1 - x ∈ f.ker ∧ Eq.{y + 1} (α := M₃) ((g : (a : M) → M₃) y_1 : M₃) ((g : (a : M) → M₃) y : M₃)

Tactic:
rcases mem_sup.1 this with ⟨x', hx', y', hy', H⟩

Premises used: Iff.mp, Submodule.mem_sup
-- Module: Mathlib.LinearAlgebra.Prod
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 = ⊤
x y : M
this : y - x ∈ f.ker ⊔ g.ker
x' : M
hx' : x' ∈ f.ker
y' : M
hy' : y' ∈ g.ker
H : x' + y' = y - x
⊢ ∃ (y_1 : M), y_1 - x ∈ f.ker ∧ Eq.{y + 1} (α := M₃) ((g : (a : M) → M₃) y_1 : M₃) ((g : (a : M) → M₃) y : M₃)

Tactic:
⟨x' + x, ?_, ?_⟩

Premises used: HAdd.hAdd, And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.Prod
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 = ⊤
x y : M
this : y - x ∈ f.ker ⊔ g.ker
x' : M
hx' : x' ∈ f.ker
y' : M
hy' : y' ∈ g.ker
H : x' + y' = y - x
refine_1 : x' + x - x ∈ f.ker
refine_2 : Eq.{y + 1} (α := M₃) ((g : (a : M) → M₃) (x' + x) : M₃) ((g : (a : M) → M₃) y : M₃)
⊢ ∃ (y_1 : M), y_1 - x ∈ f.ker ∧ Eq.{y + 1} (α := M₃) ((g : (a : M) → M₃) y_1 : M₃) ((g : (a : M) → M₃) y : M₃)

Tactic:
refine ⟨x' + x, ?_, ?_⟩
-- Module: Mathlib.LinearAlgebra.Prod
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 = ⊤
x y : M
this : y - x ∈ f.ker ⊔ g.ker
x' : M
hx' : x' ∈ f.ker
y' : M
hy' : y' ∈ g.ker
H : x' + y' = y - x
refine_1 refine_1₁ refine_1₂ refine_1₃ : x' ∈ f.ker
⊢ x' + x - x ∈ f.ker

Tactic:
rwa [add_sub_cancel_right]

Premises used: add_sub_cancel_right
-- Module: Mathlib.LinearAlgebra.Prod
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 = ⊤
x y : M
this : y - x ∈ f.ker ⊔ g.ker
x' : M
hx' : x' ∈ f.ker
y' : M
hy' : y' ∈ g.ker
H : x' + y' = y - x
⊢ Eq.{y + 1} (α := M₃) ((g : (a : M) → M₃) (x' + x) : M₃) ((g : (a : M) → M₃) y : M₃)

Tactic:
simp [← eq_sub_iff_add_eq.1 H, map_add, mem_ker.mp hy']

Premises used: eq_sub_iff_add_eq, map_add, LinearMap.mem_ker, Iff.mp
-- 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 : AddCommGroup M₃
inst_4 : AddCommGroup 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₄
a b : M × M₂
ha : a.2 = (f : (a : M) → M₂) a.1
hb : b.2 = (f : (a : M) → M₂) b.1
change : a.2 + b.2 = (f : (a : M) → M₂) (a.1 + b.1)
⊢ Membership.mem (γ := Set (M × M₂)) {p : M × M₂ | p.2 = (f : (a : M) → M₂) p.1} (a + b)

Tactic:
change _ + _ = f (_ + _)

Premises used: HAdd.hAdd, DFunLike.coe
-- 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 : AddCommGroup M₃
inst_4 : AddCommGroup 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₄
a b : M × M₂
ha : a.2 = (f : (a : M) → M₂) a.1
hb : b.2 = (f : (a : M) → M₂) b.1
rw : a.2 + b.2 = HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) a.1 : M₂) ((f : (a : M) → M₂) b.1 : M₂)
rw₁ :
  HAdd.hAdd (α := M₂) ((f : (a : M) → M₂) a.1 : M₂) b.2 =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) a.1 : M₂) ((f : (a : M) → M₂) b.1 : M₂)
rw₂ rw₃ :
  HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) a.1 : M₂) ((f : (a : M) → M₂) b.1 : M₂) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) a.1 : M₂) ((f : (a : M) → M₂) b.1 : M₂)
⊢ a.2 + b.2 = (f : (a : M) → M₂) (a.1 + b.1)

Tactic:
rw [map_add, ha, hb]

Premises used: map_add
-- 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 : AddCommGroup M₃
inst_4 : AddCommGroup 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₄
c : R
x : M × M₂
hx : x.2 = (f : (a : M) → M₂) x.1
change : c • x.2 = (f : (a : M) → M₂) (c • x.1)
⊢ Membership.mem (γ := Set (M × M₂)) {p : M × M₂ | p.2 = (f : (a : M) → M₂) p.1} (c • x)

Tactic:
change _ • _ = f (_ • _)

Premises used: HSMul.hSMul, DFunLike.coe
-- 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 : AddCommGroup M₃
inst_4 : AddCommGroup 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₄
c : R
x : M × M₂
hx : x.2 = (f : (a : M) → M₂) x.1
rw : c • x.2 = HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x.1 : M₂)
rw₁ rw₂ : HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x.1 : M₂) = HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) x.1 : M₂)
⊢ c • x.2 = (f : (a : M) → M₂) (c • x.1)

Tactic:
rw [map_smul, hx]

Premises used: map_smul
-- 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₂
f : M →ₗ[R] M₂
x : M × M₂
⊢ x ∈ f.graph ↔ x.2 = (f : (a : M) → M₂) x.1

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M₃ : Type y
M₄ : Type z
inst : Semiring R
inst_1 : AddCommGroup M₃
inst_2 : AddCommGroup M₄
inst_3 : Module R M₃
inst_4 : Module R M₄
g : M₃ →ₗ[R] M₄
h : ∀ (x : M₃ × M₄), x ∈ g.graph ↔ x ∈ ((-g).coprod id).ker
⊢ g.graph = ((-g).coprod id).ker

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M₃ : Type y
M₄ : Type z
inst : Semiring R
inst_1 : AddCommGroup M₃
inst_2 : AddCommGroup M₄
inst_3 : Module R M₃
inst_4 : Module R M₄
g : M₃ →ₗ[R] M₄
x : M₃ × M₄
h : x.2 = (g : (a : M₃) → M₄) x.1 ↔ HAdd.hAdd (α := M₄) (-(g : (a : M₃) → M₄) x.1 : M₄) x.2 = 0
⊢ x ∈ g.graph ↔ x ∈ ((-g).coprod id).ker

Tactic:
change _ = _ ↔ -g x.1 + x.2 = _

Premises used: Prod.fst, Prod.snd, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M₃ : Type y
M₄ : Type z
inst : Semiring R
inst_1 : AddCommGroup M₃
inst_2 : AddCommGroup M₄
inst_3 : Module R M₃
inst_4 : Module R M₄
g : M₃ →ₗ[R] M₄
x : M₃ × M₄
h : x.2 = (g : (a : M₃) → M₄) x.1 ↔ HAdd.hAdd (β := M₄) x.2 (-(g : (a : M₃) → M₄) x.1 : M₄) = 0
h₁ h₂ : x.2 = (g : (a : M₃) → M₄) x.1 ↔ x.2 = (g : (a : M₃) → M₄) x.1
⊢ x.2 = (g : (a : M₃) → M₄) x.1 ↔ HAdd.hAdd (α := M₄) (-(g : (a : M₃) → M₄) x.1 : M₄) x.2 = 0

Tactic:
rw [add_comm, add_neg_eq_zero]

Premises used: add_neg_eq_zero, add_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₂
f : M →ₗ[R] M₂
h : ∀ (x : M × M₂), x ∈ f.graph ↔ x ∈ (prod id f).range
⊢ f.graph = (prod id f).range

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₂
f : M →ₗ[R] M₂
x : M × M₂
⊢ x ∈ f.graph ↔ x ∈ (prod id f).range

Tactic:
⟨fun hx => ⟨x.1, Prod.ext rfl hx.symm⟩, fun ⟨u, hu⟩ => hu ▸ rfl⟩

Premises used: Membership.mem, Eq.rec, LinearMap.graph, _private.0.LinearMap.graph_eq_range_prod.match_1, Prod.fst, Prod.ext, Iff.intro, Exists.intro, Eq.symm, 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₂
f : M →ₗ[R] M₂
x : M × M₂
⊢ x ∈ f.graph ↔ x ∈ (prod id f).range

Tactic:
exact ⟨fun hx => ⟨x.1, Prod.ext rfl hx.symm⟩, fun ⟨u, hu⟩ => hu ▸ rfl⟩
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
obtain :
  ∀ (f' : H →+ I) (hf' : AddMonoidHom.mrange (F := G →+ H × I) (↑f : G →+ H × I) = f'.mgraph),
    ∃ (f' : H →ₗ[S] I), f.range = f'.graph
⊢ ∃ (f' : H →ₗ[S] I), f.range = f'.graph

Tactic:
obtain ⟨f', hf'⟩ :=
    AddMonoidHom.exists_mrange_eq_mgraph (G := G) (H := H) (I := I) (f := f) hf₁ hf

Premises used: AddMonoidHom.exists_mrange_eq_mgraph
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 →
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
f' : H →+ I
hf' : AddMonoidHom.mrange (F := G →+ H × I) (↑f : G →+ H × I) = f'.mgraph
⊢ ∀ (x : H × I), (∃ (x_1 : G), (f : (a : G) → H × I) x_1 = x) ↔ (f' : (a : H) → I) x.1 = x.2

Tactic:
simp only [SetLike.ext_iff, AddMonoidHom.mem_mrange, AddMonoidHom.coe_coe,
    AddMonoidHom.mem_mgraph] at hf'

Premises used: AddMonoidHom.coe_coe, AddMonoidHom.mem_mrange, SetLike.ext_iff, AddMonoidHom.mem_mgraph