awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
f : E →ₗ.[R] F
x : E
h : x ∈ f.domain
⊢ (x, (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x h)) ∈ f.graph

Tactic:
f.mem_graph ⟨x, h⟩

Premises used: Set.Mem, Subtype.mk, LinearPMap.mem_graph
-- 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
f : E →ₗ.[R] F
x : E
h : x ∈ f.domain
⊢ (x, (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x h)) ∈ f.graph

Tactic:
exact f.mem_graph ⟨x, h⟩

Premises used: Subtype.mk, LinearPMap.mem_graph
-- 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
f : E →ₗ.[R] F
x : E
h : ∃ (y : F), (x, y) ∈ f.graph
⊢ x ∈ f.domain

Tactic:
grind
-- 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
f : E →ₗ.[R] F
x : E
y : F
h : (x, y) ∈ f.graph
rw : ∃ (y : F), (x, y) ∈ f.graph
⊢ x ∈ f.domain

Tactic:
rw [mem_domain_iff]

Premises used: LinearPMap.mem_domain_iff
-- 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
f : E →ₗ.[R] F
x : E
y : F
h : (x, y) ∈ f.graph
⊢ ∃ (y : F), (x, y) ∈ f.graph

Tactic:
⟨y, h⟩

Premises used: Exists.intro
-- 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
f : E →ₗ.[R] F
x : E
y : F
h : (x, y) ∈ f.graph
⊢ ∃ (y : F), (x, y) ∈ f.graph

Tactic:
exact ⟨y, h⟩
-- 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
f : E →ₗ.[R] F
x : E
y : F
hx : x ∈ f.domain
⊢ y = (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) ↔ (x, y) ∈ f.graph

Tactic:
grind
-- 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
f : E →ₗ.[R] F
y : F
mp : y ∈ Set.range (↑f : ↥f.domain → F) → ∃ (x : E), (x, y) ∈ f.graph
mpr : (∃ (x : E), (x, y) ∈ f.graph) → y ∈ Set.range (↑f : ↥f.domain → F)
⊢ y ∈ Set.range (↑f : ↥f.domain → F) ↔ ∃ (x : E), (x, y) ∈ f.graph

Tactic:
constructor
-- 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
f : E →ₗ.[R] F
y : F
h : y ∈ Set.range (↑f : ↥f.domain → F)
⊢ ∃ (y_1 : ↥f.domain), (↑f : ↥f.domain → F) y_1 = y

Tactic:
rw [Set.mem_range] at h

Premises used: Set.mem_range
-- 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
f : E →ₗ.[R] F
y : F
h : ∃ (y_1 : ↥f.domain), (↑f : ↥f.domain → F) y_1 = y
mp :
  ∀ (x : E) (hx : x ∈ f.domain) (h : (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) = y),
    ∃ (x : E), (x, y) ∈ f.graph
⊢ ∃ (x : E), (x, y) ∈ f.graph

Tactic:
rcases h with ⟨⟨x, hx⟩, h⟩
-- 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
f : E →ₗ.[R] F
y : F
x : E
hx : x ∈ f.domain
h : (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) = y
h₁ : (x, y) ∈ f.graph
⊢ ∃ (x : E), (x, y) ∈ f.graph

Tactic:
use x
-- 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
f : E →ₗ.[R] F
y : F
x : E
hx : x ∈ f.domain
h : (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) = y
h₁ : (x, (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)) ∈ f.graph
⊢ (x, y) ∈ f.graph

Tactic:
rw [← h]
-- 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
f : E →ₗ.[R] F
y : F
x : E
hx : x ∈ f.domain
h : (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) = y
⊢ (x, (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)) ∈ f.graph

Tactic:
f.mem_graph ⟨x, hx⟩

Premises used: Set.Mem, Subtype.mk, LinearPMap.mem_graph
-- 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
f : E →ₗ.[R] F
y : F
x : E
hx : x ∈ f.domain
h : (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) = y
⊢ (x, (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)) ∈ f.graph

Tactic:
exact f.mem_graph ⟨x, hx⟩

Premises used: Subtype.mk, LinearPMap.mem_graph
-- 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
f : E →ₗ.[R] F
y : F
h : ∃ (x : E), (x, y) ∈ f.graph
⊢ y ∈ Set.range (↑f : ↥f.domain → F)

Tactic:
grind
-- 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
f g : E →ₗ.[R] F
h : f.graph = g.graph
x : E
simp_rw : (∃ (y : F), (x, y) ∈ f.graph) ↔ ∃ (y : F), (x, y) ∈ g.graph
⊢ x ∈ f.domain ↔ x ∈ g.domain

Tactic:
simp_rw [mem_domain_iff, h]

Premises used: LinearPMap.mem_domain_iff
-- 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
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
left : f.domain ≤ g.domain
right : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄ (_h : (↑x : E) = (↑y : E)), (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
⊢ f ≤ g

Tactic:
constructor
-- 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
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
left : ∀ (hx : ∃ (y : F), (x, y) ∈ f.graph), ∃ (y : F), (x, y) ∈ g.graph
⊢ x ∈ g.domain

Tactic:
rw [mem_domain_iff] at hx ⊢

Premises used: LinearPMap.mem_domain_iff
-- 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
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : ∃ (y : F), (x, y) ∈ f.graph
left : ∀ (y : F) (hx : (x, y) ∈ f.graph), ∃ (y : F), (x, y) ∈ g.graph
⊢ ∃ (y : F), (x, y) ∈ g.graph

Tactic:
obtain ⟨y, hx⟩ := hx
-- 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
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
y : F
hx : (x, y) ∈ f.graph
h₁ : (x, y) ∈ g.graph
⊢ ∃ (y : F), (x, y) ∈ g.graph

Tactic:
use y
-- 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
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
y : F
hx : (x, y) ∈ f.graph
⊢ (x, y) ∈ g.graph

Tactic:
h hx

Premises used: Set.Mem
-- 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
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
y : F
hx : (x, y) ∈ f.graph
⊢ (x, y) ∈ g.graph

Tactic:
exact h hx
-- 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
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy :
  (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) : E) =
    (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) y hy) : E)
right : (y, (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)) ∈ g.graph
⊢ (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) y hy)

Tactic:
rw [image_iff]

Premises used: LinearPMap.image_iff
-- 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
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy :
  (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) : E) =
    (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) y hy) : E)
⊢ (y, (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)) ∈ g.graph

Tactic:
h ?_

Premises used: Set.Mem
-- 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
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy :
  (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) : E) =
    (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) y hy) : E)
right : (y, (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)) ∈ f.graph
⊢ (y, (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)) ∈ g.graph

Tactic:
refine h ?_
-- 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
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : x = y
⊢ y ∈ f.domain

Tactic:
rw [hxy] at hx
-- 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
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : x = y
hx₁ : y ∈ f.domain
⊢ y ∈ g.domain

Tactic:
rw [hxy] at hx
-- 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
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : x = y
hx₁ : y ∈ f.domain
hy₁ : y ∈ g.domain
⊢ x = y

Tactic:
rw [hxy] at hx
-- 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
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx_1 : x ∈ f.domain
y : E
hx : y ∈ f.domain
hy : y ∈ g.domain
hxy : x = y
right :
  (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx_1) =
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) y hx)
⊢ (y, (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx_1)) ∈ f.graph

Tactic:
rw [← image_iff hx]

Premises used: LinearPMap.image_iff
-- 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
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx_1 : x ∈ f.domain
y : E
hx : y ∈ f.domain
hy : y ∈ g.domain
hxy : x = y
⊢ (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx_1) =
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) y hx)

Tactic:
simp [hxy]
-- 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
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
hx : x ∈ f.graph
rw :
  ∀ (hx : ∃ (y : ↥f.domain), (↑y : E) = x.1 ∧ (↑f : ↥f.domain → F) y = x.2),
    ∃ (y : ↥g.domain), (↑y : E) = x.1 ∧ (↑g : ↥g.domain → F) y = x.2
⊢ x ∈ g.graph

Tactic:
rw [mem_graph_iff] at hx ⊢

Premises used: LinearPMap.mem_graph_iff
-- 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
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
hx : ∃ (y : ↥f.domain), (↑y : E) = x.1 ∧ (↑f : ↥f.domain → F) y = x.2
obtain :
  ∀ (y : ↥f.domain) (hx : (↑y : E) = x.1 ∧ (↑f : ↥f.domain → F) y = x.2),
    ∃ (y : ↥g.domain), (↑y : E) = x.1 ∧ (↑g : ↥g.domain → F) y = x.2
⊢ ∃ (y : ↥g.domain), (↑y : E) = x.1 ∧ (↑g : ↥g.domain → F) y = x.2

Tactic:
obtain ⟨y, hx⟩ := hx
-- 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
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
y : ↥f.domain
hx : (↑y : E) = x.1 ∧ (↑f : ↥f.domain → F) y = x.2
h₁ :
  (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (↑y : E) ⋯) : E) = x.1 ∧
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (↑y : E) ⋯) = x.2
⊢ ∃ (y : ↥g.domain), (↑y : E) = x.1 ∧ (↑g : ↥g.domain → F) y = x.2

Tactic:
use ⟨y, h.1 y.2⟩
-- 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
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
y : ↥f.domain
hx : (↑y : E) = x.1 ∧ (↑f : ↥f.domain → F) y = x.2
h₁ : (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x.1 ⋯) = x.2
⊢ (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (↑y : E) ⋯) : E) = x.1 ∧
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (↑y : E) ⋯) = x.2

Tactic:
simp only [hx, true_and]

Premises used: true_and
-- 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
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
y : ↥f.domain
hx : (↑y : E) = x.1 ∧ (↑f : ↥f.domain → F) y = x.2
⊢ (↑f : ↥f.domain → F) y = x.2

Tactic:
hx.2

Premises used: And.right
-- 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
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
y : ↥f.domain
hx : (↑y : E) = x.1 ∧ (↑f : ↥f.domain → F) y = x.2
h₁ : (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x.1 ⋯) = (↑f : ↥f.domain → F) y
⊢ (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x.1 ⋯) = x.2

Tactic:
convert! hx.2 using 1

Premises used: And.right
-- 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
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
y : ↥f.domain
hx : (↑y : E) = x.1 ∧ (↑f : ↥f.domain → F) y = x.2
⊢ (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x.1 ⋯) = (↑f : ↥f.domain → F) y

Tactic:
(h.2 ?_).symm

Premises used: And.right, Eq.symm
-- 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
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
y : ↥f.domain
hx : (↑y : E) = x.1 ∧ (↑f : ↥f.domain → F) y = x.2
h₁ : (↑y : E) = (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x.1 ⋯) : E)
⊢ (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x.1 ⋯) = (↑f : ↥f.domain → F) y

Tactic:
refine (h.2 ?_).symm

Premises used: And.right, Eq.symm
-- 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
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
y : ↥f.domain
hx : (↑y : E) = x.1 ∧ (↑f : ↥f.domain → F) y = x.2
⊢ (↑y : E) = (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x.1 ⋯) : E)

Tactic:
simp only [hx.1]

Premises used: And.left
-- 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
f g : E →ₗ.[R] F
⊢ f.graph ≤ g.graph ↔ f ≤ g

Tactic:
⟨le_of_le_graph, le_graph_of_le⟩

Premises used: LinearPMap.le_of_le_graph, Iff.intro, LinearPMap.le_graph_of_le
-- 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
f g : E →ₗ.[R] F
h : f.graph = g.graph
h₁ : f.domain = g.domain
h' : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄ (_h : (↑x : E) = (↑y : E)), (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
⊢ f = g

Tactic:
apply dExt

Premises used: LinearPMap.dExt
-- 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
f g : E →ₗ.[R] F
h : f.graph = g.graph
h₁ : ∀ (x : E), x ∈ f.domain ↔ x ∈ g.domain
⊢ f.domain = g.domain

Tactic:
ext
-- 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
f g : E →ₗ.[R] F
h : f.graph = g.graph
x : E
⊢ x ∈ f.domain ↔ x ∈ g.domain

Tactic:
mem_domain_iff_of_eq_graph h

Premises used: LinearPMap.mem_domain_iff_of_eq_graph
-- 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
f g : E →ₗ.[R] F
h : f.graph = g.graph
x : E
⊢ x ∈ f.domain ↔ x ∈ g.domain

Tactic:
exact mem_domain_iff_of_eq_graph h

Premises used: LinearPMap.mem_domain_iff_of_eq_graph
-- 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
f g : E →ₗ.[R] F
h : f.graph = g.graph
⊢ ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄ (_h : (↑x : E) = (↑y : E)), (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y

Tactic:
apply (le_of_le_graph h.le).2

Premises used: LinearPMap.le_of_le_graph, Eq.le, And.right
-- 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
g : Submodule R (E × F)
hg : ∀ {x : E × F} (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ ∃! b : F, (a, b) ∈ g

Tactic:
existsUnique_of_exists_of_unique ?_ ?_

Premises used: existsUnique_of_exists_of_unique
-- 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
g : Submodule R (E × F)
hg : ∀ {x : E × F} (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
refine_1 : ∃ (x : F), (a, x) ∈ g
refine_2 : ∀ (y₁ y₂ : F), (a, y₁) ∈ g → (a, y₂) ∈ g → y₁ = y₂
⊢ ∃! b : F, (a, b) ∈ g

Tactic:
refine existsUnique_of_exists_of_unique ?_ ?_

Premises used: existsUnique_of_exists_of_unique
-- 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
g : Submodule R (E × F)
hg : ∀ {x : E × F} (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ a ∈ map (LinearMap.fst R E F) g

Tactic:
ha
-- 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
g : Submodule R (E × F)
hg : ∀ {x : E × F} (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
a₁ : (∃ (x : F), (a, x) ∈ g) ↔ a ∈ map (LinearMap.fst R E F) g
⊢ ∃ (x : F), (a, x) ∈ g

Tactic:
convert! ha
-- 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
g : Submodule R (E × F)
hg : ∀ {x : E × F} (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ (∃ (x : F), (a, x) ∈ g) ↔ a ∈ map (LinearMap.fst R E F) g

Tactic:
simp
-- 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
g : Submodule R (E × F)
hg : ∀ {x : E × F} (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
⊢ (a, y₁) - (a, y₂) ∈ g

Tactic:
g.sub_mem hy₁ hy₂

Premises used: Submodule.sub_mem
-- 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
g : Submodule R (E × F)
hg : ∀ {x : E × F} (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
h : 0 = ((a, y₁) - (a, y₂)).1
⊢ (0, y₁ - y₂) ∈ g

Tactic:
convert! g.sub_mem hy₁ hy₂

Premises used: Submodule.sub_mem
-- 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
g : Submodule R (E × F)
hg : ∀ {x : E × F} (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
⊢ 0 = ((a, y₁) - (a, y₂)).1

Tactic:
(sub_self _).symm

Premises used: sub_self, Eq.symm
-- 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
g : Submodule R (E × F)
hg : ∀ {x : E × F} (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
⊢ 0 = ((a, y₁) - (a, y₂)).1

Tactic:
exact (sub_self _).symm

Premises used: sub_self, Eq.symm
-- 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
g : Submodule R (E × F)
hg : ∀ {x : E × F} (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
⊢ (0, y₁ - y₂) ∈ g

Tactic:
have hy : ((0 : E), y₁ - y₂) ∈ g := by
    convert! g.sub_mem hy₁ hy₂
    exact (sub_self _).symm
-- 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
g : Submodule R (E × F)
hg : ∀ {x : E × F} (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
hy : (0, y₁ - y₂) ∈ g
⊢ Eq.{u_4 + 1} (α := E) (0, y₁ - y₂).1 0

Tactic:
simp