awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
x : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
h rwa rwa₁ rwa₂ rwa₃ : x ∈ (mkSpanSingleton' x y H).domain
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := R) 1 x ∈ (mkSpanSingleton' x y H).domain

Tactic:
rwa [one_smul]

Premises used: one_smul
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ_1 : R →+* S
τ : S →+* T
E_1 : Type u_4
inst_3 : AddCommGroup E_1
inst_4 : Module R E_1
F_1 : Type u_5
inst_5 : AddCommGroup F_1
inst_6 : Module S F_1
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
K : Type u_7
L : Type u_8
E : Type u_9
F : Type u_10
inst_9 : DivisionRing K
inst_10 : DivisionRing L
σ : K →+* L
inst_11 : AddCommGroup E
inst_12 : Module K E
inst_13 : AddCommGroup F
inst_14 : Module L F
x : E
y : F
hx : x ≠ 0
c : K
hc_1 : c • x = 0
hc : c = 0
rw : HSMul.hSMul.{u_8, u_10, u_10} (α := L) ((σ : (a : K) → L) 0 : L) y = 0
rw₁ : HSMul.hSMul.{u_8, u_10, u_10} (α := L) 0 y = 0
rw₂ rw₃ : Eq.{u_10 + 1} (α := F) 0 0
⊢ HSMul.hSMul.{u_8, u_10, u_10} (α := L) ((σ : (a : K) → L) c : L) y = 0

Tactic:
rw [hc, RingHom.map_zero, zero_smul]

Premises used: zero_smul, RingHom.map_zero
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
K : Type u_7
L : Type u_8
E : Type u_9
F : Type u_10
inst : DivisionRing K
inst_1 : DivisionRing L
σ : K →+* L
inst_2 : AddCommGroup E
inst_3 : Module K E
inst_4 : AddCommGroup F
inst_5 : Module L F
x : E
hx : x ≠ 0
y : F
⊢ (↑(mkSpanSingleton x y hx) : ↥(mkSpanSingleton x y hx).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦
        Membership.mem (γ := Submodule K E) (domain.{u_7, u_8, u_9, u_10} (S := L) (σ := σ) (mkSpanSingleton x y hx))
          x_1)
        x ⋯) =
    y

Tactic:
LinearPMap.mkSpanSingleton'_apply_self _ _ _ _

Premises used: Set.Mem, LinearPMap.mkSpanSingleton'_apply_self
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
p : Submodule R E
p' : Submodule R F
x : ↥(p.prod p')
⊢ (↑(LinearPMap.fst p p') : ↥(LinearPMap.fst p p').domain → E) x = (↑x : E × F).1

Tactic:
rfl

Premises used: rfl, LinearPMap.toFun'
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
inst : Ring R
E : Type u_4
inst_1 : AddCommGroup E
inst_2 : Module R E
F : Type u_5
inst_3 : AddCommGroup F
inst_4 : Module R F
p : Submodule R E
p' : Submodule R F
x : ↥(p.prod p')
⊢ (↑(LinearPMap.snd p p') : ↥(LinearPMap.snd p p').domain → F) x = (↑x : E × F).2

Tactic:
rfl

Premises used: rfl, LinearPMap.toFun'
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S_1 : Type u_2
inst : Ring R
inst_1 : Ring S_1
σ : R →+* S_1
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S_1 F
T S : E →ₛₗ.[σ] F
h : T ≤ S
x : ↥T.domain
⊢ (↑T : ↥T.domain → F) x = (↑S : ↥S.domain → F) ((inclusion ⋯ : (a : ↥T.domain) → ↥S.domain) x)

Tactic:
h.2 rfl

Premises used: And.right, rfl
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S_1 : Type u_2
inst : Ring R
inst_1 : Ring S_1
σ : R →+* S_1
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S_1 F
T S : E →ₛₗ.[σ] F
h : T ≤ S
x : ↥T.domain
⊢ ∃ (y : ↥S.domain), (↑x : E) = (↑y : E) ∧ (↑T : ↥T.domain → F) x = (↑S : ↥S.domain → F) y

Tactic:
⟨⟨x.1, h.1 x.2⟩, ⟨rfl, h.2 rfl⟩⟩

Premises used: Subtype.mk, And.right, And.left, And.intro, Exists.intro, Subtype.val, rfl, Subtype.property
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
f g : E →ₛₗ.[σ] F
hle : f ≤ g
heq : f.domain = g.domain
⊢ f = g

Tactic:
dExt heq hle.2

Premises used: LinearPMap.dExt, And.right
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
x y : E
h :
  Membership.mem (γ := Set E)
    {x : E |
      ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain),
        (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hf) =
          (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hg)}
    x
h_1 :
  Membership.mem (γ := Set E)
    {x : E |
      ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain),
        (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hf) =
          (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hg)}
    y
hfx : x ∈ f.domain
hgx : x ∈ g.domain
hx :
  (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)
hfy : y ∈ f.domain
hgy : y ∈ g.domain
hy :
  (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) y hfy) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) y hgy)
⊢ (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x + y) ⋯) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (x + y) ⋯)

Tactic:
simp_all [← AddMemClass.mk_add_mk, f.map_add, g.map_add]

Premises used: LinearPMap.map_add, AddMemClass.mk_add_mk
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f_1 g : E →ₛₗ.[σ] F
c : R
x : E
h :
  Membership.mem (γ := Set E)
    {x : E |
      ∃ (hf : x ∈ f_1.domain) (hg : x ∈ g.domain),
        (↑f_1 : ↥f_1.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f_1.domain) x hf) =
          (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hg)}
    x
hfx_1 : x ∈ f_1.domain
hgx : x ∈ g.domain
hx :
  (↑f_1 : ↥f_1.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f_1.domain) x hfx_1) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)
f : E →ₛₗ.[σ] F
hfx : x ∈ f.domain
⊢ Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (c • x) ⋯ = c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
c : R
x : E
h :
  Membership.mem (γ := Set E)
    {x : E |
      ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain),
        (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hf) =
          (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hg)}
    x
hfx : x ∈ f.domain
hgx : x ∈ g.domain
hx :
  (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)
⊢ ∀ {f : E →ₛₗ.[σ] F} (hfx : x ∈ f.domain),
    Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (c • x) ⋯ = c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx

Tactic:
have {f : E →ₛₗ.[σ] F} (hfx) : (⟨c • x, smul_mem _ c hfx⟩ : f.domain) = c • ⟨x, hfx⟩ := by
        simp
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
c : R
x : E
h :
  Membership.mem (γ := Set E)
    {x : E |
      ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain),
        (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hf) =
          (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hg)}
    x
hfx : x ∈ f.domain
hgx : x ∈ g.domain
hx :
  (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)
this :
  ∀ {f : E →ₛₗ.[σ] F} (hfx : x ∈ f.domain),
    Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (c • x) ⋯ = c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx
rw :
  (↑f : ↥f.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (c • x) ⋯)
rw₁ :
  (↑f : ↥f.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑g : ↥g.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)
rw₂ :
  HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S)
      ((↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx)) =
    (↑g : ↥g.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)
rw₃ :
  HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S)
      ((↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx)) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S)
      ((↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx))
rw₄ rw₅ :
  HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S)
      ((↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S)
      ((↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx))
⊢ (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (c • x) ⋯) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (c • x) ⋯)

Tactic:
rw [this hfx, this hgx, f.map_smulₛₗ, g.map_smulₛₗ, hx]

Premises used: LinearPMap.map_smulₛₗ
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g h : E →ₛₗ.[σ] F
this :
  ∀ (fg_le : f.domain ≤ g.domain)
    (fg_eq :
      ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄ (_h : (↑x : E) = (↑y : E)), (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y),
    f ≤ h → f ≤ { domain := g.eqLocus h, toFun := g.toFun ∘ₛₗ inclusion ⋯ }
⊢ f ≤ g → f ≤ h → f ≤ { domain := g.eqLocus h, toFun := g.toFun ∘ₛₗ inclusion ⋯ }

Tactic:
⟨fg_le, fg_eq⟩
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g h : E →ₛₗ.[σ] F
fg_le : f.domain ≤ g.domain
fg_eq : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄ (_h : (↑x : E) = (↑y : E)), (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
this :
  ∀ (fh_le : f.domain ≤ h.domain)
    (fh_eq :
      ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥h.domain⦄ (_h : (↑x : E) = (↑y : E)), (↑f : ↥f.domain → F) x = (↑h : ↥h.domain → F) y),
    f ≤ { domain := g.eqLocus h, toFun := g.toFun ∘ₛₗ inclusion ⋯ }
⊢ f ≤ h → f ≤ { domain := g.eqLocus h, toFun := g.toFun ∘ₛₗ inclusion ⋯ }

Tactic:
⟨fh_le, fh_eq⟩
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g h : E →ₛₗ.[σ] F
fg_le : f.domain ≤ g.domain
fg_eq : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄ (_h : (↑x : E) = (↑y : E)), (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
fh_le : f.domain ≤ h.domain
fh_eq : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥h.domain⦄ (_h : (↑x : E) = (↑y : E)), (↑f : ↥f.domain → F) x = (↑h : ↥h.domain → F) y
⊢ f ≤ { domain := g.eqLocus h, toFun := g.toFun ∘ₛₗ inclusion ⋯ }

Tactic:
⟨fun x hx =>
      ⟨fg_le hx, fh_le hx,
      (fg_eq (x := ⟨x, hx⟩) rfl).symm.trans (fh_eq rfl)⟩,
      fun x ⟨y, yg, hy⟩ h => fg_eq h⟩

Premises used: Exists.fst, _private.0.LinearPMap.semilatticeInf.match_3, Submodule.inclusion, LinearMap.comp, LinearPMap.toFun, LinearPMap.eqLocus, And.intro, Exists.intro, Eq.symm, LinearPMap.mk, Eq, rfl, Eq.trans, LinearPMap.toFun'
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g h : E →ₛₗ.[σ] F
fg_le : f.domain ≤ g.domain
fg_eq : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄ (_h : (↑x : E) = (↑y : E)), (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
fh_le : f.domain ≤ h.domain
fh_eq : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥h.domain⦄ (_h : (↑x : E) = (↑y : E)), (↑f : ↥f.domain → F) x = (↑h : ↥h.domain → F) y
⊢ f ≤ { domain := g.eqLocus h, toFun := g.toFun ∘ₛₗ inclusion ⋯ }

Tactic:
exact ⟨fun x hx =>
      ⟨fg_le hx, fh_le hx,
      (fg_eq (x := ⟨x, hx⟩) rfl).symm.trans (fh_eq rfl)⟩,
      fun x ⟨y, yg, hy⟩ h => fg_eq h⟩
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f : E →ₛₗ.[σ] F
x : ↥(domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) ⊥)
y : ↥f.domain
h : (↑x : E) = (↑y : E)
⊢ x = 0

Tactic:
have hx : x = 0 := Subtype.ext ((mem_bot R).1 x.2)
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f : E →ₛₗ.[σ] F
x : ↥(domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) ⊥)
y : ↥f.domain
h : (↑x : E) = (↑y : E)
hx : x = 0
⊢ y = 0

Tactic:
have hy : y = 0 := Subtype.ext (h.symm.trans (congr_arg _ hx))
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f : E →ₛₗ.[σ] F
x : ↥(domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) ⊥)
y : ↥f.domain
h : (↑x : E) = (↑y : E)
hx : x = 0
hy : y = 0
rw : (↑⊥ : ↥⊥.domain → F) 0 = (↑f : ↥f.domain → F) y
rw₁ : (↑⊥ : ↥⊥.domain → F) 0 = (↑f : ↥f.domain → F) 0
rw₂ : 0 = (↑f : ↥f.domain → F) 0
rw₃ rw₄ : Eq.{u_5 + 1} (α := F) 0 0
⊢ (↑⊥ : ↥⊥.domain → F) x = (↑f : ↥f.domain → F) y

Tactic:
rw [hx, hy, map_zero, map_zero]

Premises used: LinearPMap.map_zero
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
f g : E →ₛₗ.[σ] F
H : f.domain ≤ f.eqLocus g
⊢ f ≤ g

Tactic:
suffices f ≤ f ⊓ g from le_trans this inf_le_right
  ⟨H, fun _x _y hxy => ((inf_le_left : f ⊓ g ≤ f).2 hxy.symm).symm⟩

Premises used: inf_le_right, And.right, And.intro, inf_le_left, Eq.symm, le_trans
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
⊢ StrictMono (α := E →ₛₗ.[σ] F) domain

Tactic:
fun _f _g hlt =>
    lt_of_le_of_ne hlt.1.1 fun heq => ne_of_lt hlt <| eq_of_le_of_domain_eq (le_of_lt hlt) heq

Premises used: LinearPMap.eq_of_le_of_domain_eq, StrictMono, le_of_lt, And.left, ne_of_lt, lt_of_le_of_ne
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
choose :
  ∀ (x : (z : ↥(f.domain ⊔ g.domain)) → E) (hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain)
    (y : (z : ↥(f.domain ⊔ g.domain)) → E) (hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain)
    (hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = (↑z : E)),
    ∃ (fg : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(f.domain ⊔ g.domain)) F),
      ∀ (x : ↥f.domain) (y : ↥g.domain) (z : ↥(f.domain ⊔ g.domain)),
        (↑x : E) + (↑y : E) = (↑z : E) →
          (fg : (a : ↥(f.domain ⊔ g.domain)) → F) z = (↑f : ↥f.domain → F) x + (↑g : ↥g.domain → F) y
⊢ ∃ (fg : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(f.domain ⊔ g.domain)) F),
    ∀ (x : ↥f.domain) (y : ↥g.domain) (z : ↥(f.domain ⊔ g.domain)),
      (↑x : E) + (↑y : E) = (↑z : E) →
        (fg : (a : ↥(f.domain ⊔ g.domain)) → F) z = (↑f : ↥f.domain → F) x + (↑g : ↥g.domain → F) y

Tactic:
choose x hx y hy hxy using fun z : ↥(f.domain ⊔ g.domain) => mem_sup.1 z.prop

Premises used: Subtype.prop, Iff.mp, Submodule.mem_sup
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
x : (z : ↥(f.domain ⊔ g.domain)) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : (z : ↥(f.domain ⊔ g.domain)) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = (↑z : E)
fg : (z : ↥(f.domain ⊔ g.domain)) → F :=
  fun (z : ↥(f.domain ⊔ g.domain)) ↦
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) ⋯) +
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) ⋯)
x' : ↥f.domain
y' : ↥g.domain
z' : ↥(f.domain ⊔ g.domain)
H : (↑x' : E) + (↑y' : E) = (↑z' : E)
dsimp :
  (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z') ⋯) +
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z') ⋯) =
    (↑f : ↥f.domain → F) x' + (↑g : ↥g.domain → F) y'
⊢ fg z' = (↑f : ↥f.domain → F) x' + (↑g : ↥g.domain → F) y'

Tactic:
dsimp [fg]
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
x : (z : ↥(f.domain ⊔ g.domain)) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : (z : ↥(f.domain ⊔ g.domain)) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = (↑z : E)
fg : (z : ↥(f.domain ⊔ g.domain)) → F :=
  fun (z : ↥(f.domain ⊔ g.domain)) ↦
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) ⋯) +
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) ⋯)
x' : ↥f.domain
y' : ↥g.domain
z' : ↥(f.domain ⊔ g.domain)
H : (↑x' : E) + (↑y' : E) = (↑z' : E)
rw :
  (↑f : ↥f.domain → F) (x' - Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z') ⋯) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z') ⋯ - y')
⊢ (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z') ⋯) +
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z') ⋯) =
    (↑f : ↥f.domain → F) x' + (↑g : ↥g.domain → F) y'

Tactic:
rw [add_comm, ← sub_eq_sub_iff_add_eq_add, eq_comm, ← map_sub, ← map_sub]

Premises used: sub_eq_sub_iff_add_eq_add, eq_comm, add_comm, LinearPMap.map_sub
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
x : (z : ↥(f.domain ⊔ g.domain)) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : (z : ↥(f.domain ⊔ g.domain)) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = (↑z : E)
fg : (z : ↥(f.domain ⊔ g.domain)) → F :=
  fun (z : ↥(f.domain ⊔ g.domain)) ↦
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) ⋯) +
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) ⋯)
x' : ↥f.domain
y' : ↥g.domain
z' : ↥(f.domain ⊔ g.domain)
H : (↑x' : E) + (↑y' : E) = (↑z' : E)
a :
  (↑(x' - Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z') ⋯) : E) =
    (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z') ⋯ - y') : E)
⊢ (↑f : ↥f.domain → F) (x' - Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z') ⋯) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z') ⋯ - y')

Tactic:
apply h
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
x : (z : ↥(f.domain ⊔ g.domain)) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : (z : ↥(f.domain ⊔ g.domain)) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = (↑z : E)
fg : (z : ↥(f.domain ⊔ g.domain)) → F :=
  fun (z : ↥(f.domain ⊔ g.domain)) ↦
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) ⋯) +
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) ⋯)
x' : ↥f.domain
y' : ↥g.domain
z' : ↥(f.domain ⊔ g.domain)
H : (↑x' : E) + (↑y' : E) = (↑z' : E)
⊢ ∀ (z : ↥(f.domain ⊔ g.domain)), x z = (↑z : E) - y z

Tactic:
simp only [← eq_sub_iff_add_eq] at hxy

Premises used: eq_sub_iff_add_eq
-- Module: Mathlib.LinearAlgebra.LinearPMap
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
σ : R →+* S
E : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module R E
F : Type u_5
inst_4 : AddCommGroup F
inst_5 : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), (↑x : E) = (↑y : E) → (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
x : (z : ↥(f.domain ⊔ g.domain)) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : (z : ↥(f.domain ⊔ g.domain)) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
fg : (z : ↥(f.domain ⊔ g.domain)) → F :=
  fun (z : ↥(f.domain ⊔ g.domain)) ↦
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z) ⋯) +
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z) ⋯)
x' : ↥f.domain
y' : ↥g.domain
z' : ↥(f.domain ⊔ g.domain)
H : (↑x' : E) + (↑y' : E) = (↑z' : E)
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z = (↑z : E) - y z
a : -(↑y' : E) + y z' = y z' - (↑y' : E)
⊢ (↑(x' - Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (x z') ⋯) : E) =
    (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (y z') ⋯ - y') : E)

Tactic:
simp only [AddSubgroupClass.coe_sub, hxy, ← sub_add, ← sub_sub, sub_self,
      zero_sub, ← H]

Premises used: sub_add, AddSubgroupClass.coe_sub, sub_self, sub_sub, zero_sub