awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (hypothesis)
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_fst : E
x_snd : F
y : ↥(-f).domain
hy : (↑y : E) = (x_fst, x_snd).1
h : (↑(-f) : ↥(-f).domain → F) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (-LinearMap.id)) f.graph
have h₁ : -(↑f : ↥f.domain → F) y = (x_fst, x_snd).2
Tactic: rw [LinearPMap.neg_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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_fst : E
x_snd : F
y : ↥(-f).domain
hy : (↑y : E) = (x_fst, x_snd).1
h : -(↑f : ↥f.domain → F) y = (x_fst, x_snd).2
⊢ ∃ y ∈ f.graph, (LinearMap.prodMap LinearMap.id (-LinearMap.id) : (a : E × F) → E × F) y = (x_fst, x_snd)
have h₁ : ∃ (a : E) (a_1 : ↥f.domain), (↑a_1 : E) = a ∧ a = x_fst ∧ -(↑f : ↥f.domain → F) a_1 = x_snd
Tactic: simp only [mem_graph_iff, LinearMap.prodMap_apply, LinearMap.id_coe, id,
      LinearMap.neg_apply, Prod.mk_inj, Prod.exists, exists_exists_and_eq_and]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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_fst : E
x_snd : F
y : ↥(-f).domain
hy : (↑y : E) = (x_fst, x_snd).1
h : -(↑f : ↥f.domain → F) y = (x_fst, x_snd).2
w : E
⊢ ∃ (a : E) (a_1 : ↥f.domain), (↑a_1 : E) = a ∧ a = x_fst ∧ -(↑f : ↥f.domain → F) a_1 = x_snd
have w₁ : ↥f.domain
Tactic: use x_fst, y, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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_fst : E
x_snd : F
y : ↥(-f).domain
hy : (↑y : E) = (x_fst, x_snd).1
h : -(↑f : ↥f.domain → F) y = (x_fst, x_snd).2
w : E
w₁ : ↥f.domain
⊢ ∃ (a : E) (a_1 : ↥f.domain), (↑a_1 : E) = a ∧ a = x_fst ∧ -(↑f : ↥f.domain → F) a_1 = x_snd
have left : (↑y : E) = x_fst
Tactic: use x_fst, y, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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_fst : E
x_snd : F
y : ↥(-f).domain
hy : (↑y : E) = (x_fst, x_snd).1
h : -(↑f : ↥f.domain → F) y = (x_fst, x_snd).2
w : E
w₁ : ↥f.domain
left : (↑y : E) = x_fst
⊢ ∃ (a : E) (a_1 : ↥f.domain), (↑a_1 : E) = a ∧ a = x_fst ∧ -(↑f : ↥f.domain → F) a_1 = x_snd
have right : x_fst = x_fst ∧ -(↑f : ↥f.domain → F) y = x_snd
Tactic: use x_fst, y, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (hypothesis)
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_fst : E
x_snd : F
h : (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (-LinearMap.id)) f.graph
⊢ (x_fst, x_snd) ∈ (-f).graph
have h₁ : ∃ y ∈ f.graph, (LinearMap.prodMap LinearMap.id (-LinearMap.id) : (a : E × F) → E × F) y = (x_fst, x_snd)
Tactic: rw [Submodule.mem_map] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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_fst : E
x_snd : F
h : ∃ y ∈ f.graph, (LinearMap.prodMap LinearMap.id (-LinearMap.id) : (a : E × F) → E × F) y = (x_fst, x_snd)
⊢ (x_fst, x_snd) ∈ (-f).graph
have h₁ : ∀ (x' : E × F) (hx' : x' ∈ f.graph)
  (h : (LinearMap.prodMap LinearMap.id (-LinearMap.id) : (a : E × F) → E × F) x' = (x_fst, x_snd)),
  (x_fst, x_snd) ∈ (-f).graph
Tactic: rcases h with ⟨x', hx', h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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_fst : E
x_snd : F
x' : E × F
hx' : x' ∈ f.graph
h : (LinearMap.prodMap LinearMap.id (-LinearMap.id) : (a : E × F) → E × F) x' = (x_fst, x_snd)
⊢ (x_fst, x_snd) ∈ (-f).graph
have h₁ : ∀ (fst : E) (snd : F) (hx' : (fst, snd) ∈ f.graph)
  (h : (LinearMap.prodMap LinearMap.id (-LinearMap.id) : (a : E × F) → E × F) (fst, snd) = (x_fst, x_snd)),
  (x_fst, x_snd) ∈ (-f).graph
Tactic: cases x'
Cleared hypotheses: x', hx', h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (hypothesis)
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_fst : E
x_snd : F
fst : E
snd : F
hx' : (fst, snd) ∈ f.graph
h : (LinearMap.prodMap LinearMap.id (-LinearMap.id) : (a : E × F) → E × F) (fst, snd) = (x_fst, x_snd)
⊢ (x_fst, x_snd) ∈ (-f).graph
have h₁ : fst = x_fst ∧ -snd = x_snd
Tactic: simp only [LinearMap.prodMap_apply, LinearMap.id_coe, id, LinearMap.neg_apply,
    Prod.mk_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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_fst : E
x_snd : F
fst : E
snd : F
hx' : (fst, snd) ∈ f.graph
h : fst = x_fst ∧ -snd = x_snd
⊢ (x_fst, x_snd) ∈ (-f).graph
have h₁ : ∀ (hx' : ∃ (y : ↥f.domain), (↑y : E) = (fst, snd).1 ∧ (↑f : ↥f.domain → F) y = (fst, snd).2)
  (h : fst = x_fst ∧ -snd = x_snd),
  ∃ (y : ↥(-f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(-f) : ↥(-f).domain → F) y = (x_fst, x_snd).2
Tactic: rw [mem_graph_iff] at hx' ⊢
Cleared hypotheses: hx', h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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_fst : E
x_snd : F
fst : E
snd : F
hx' : ∃ (y : ↥f.domain), (↑y : E) = (fst, snd).1 ∧ (↑f : ↥f.domain → F) y = (fst, snd).2
h : fst = x_fst ∧ -snd = x_snd
⊢ ∃ (y : ↥(-f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(-f) : ↥(-f).domain → F) y = (x_fst, x_snd).2
have h₁ : ∀ (y : ↥f.domain) (hy : (↑y : E) = (fst, snd).1) (hx' : (↑f : ↥f.domain → F) y = (fst, snd).2),
  ∃ (y : ↥(-f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(-f) : ↥(-f).domain → F) y = (x_fst, x_snd).2
Tactic: rcases hx' with ⟨y, hy, hx'⟩
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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_fst : E
x_snd : F
fst : E
snd : F
h : fst = x_fst ∧ -snd = x_snd
y : ↥f.domain
hy : (↑y : E) = (fst, snd).1
hx' : (↑f : ↥f.domain → F) y = (fst, snd).2
⊢ ∃ (y : ↥(-f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(-f) : ↥(-f).domain → F) y = (x_fst, x_snd).2
have h₁ : (↑y : E) = (x_fst, x_snd).1 ∧ (↑(-f) : ↥(-f).domain → F) y = (x_fst, x_snd).2
Tactic: use y
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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_fst : E
x_snd : F
fst : E
snd : F
h : fst = x_fst ∧ -snd = x_snd
y : ↥f.domain
hy : (↑y : E) = (fst, snd).1
hx' : (↑f : ↥f.domain → F) y = (fst, snd).2
⊢ (↑y : E) = (x_fst, x_snd).1 ∧ (↑(-f) : ↥(-f).domain → F) y = (x_fst, x_snd).2
have h₁ : (↑y : E) = (fst, -snd).1 ∧ (↑(-f) : ↥(-f).domain → F) y = (fst, -snd).2
Tactic: rw [← h.1, ← h.2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ x ∈ f.domain ↔ ∃ (y : F), (x, y) ∈ f.graph
have mp : x ∈ f.domain → ∃ (y : F), (x, y) ∈ f.graph
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
mp : x ∈ f.domain → ∃ (y : F), (x, y) ∈ f.graph
⊢ x ∈ f.domain ↔ ∃ (y : F), (x, y) ∈ f.graph
have mpr : (∃ (y : F), (x, y) ∈ f.graph) → x ∈ f.domain
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ ∃ (y : F), (x, y) ∈ f.graph
have h₁ : (x, (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x h)) ∈ f.graph
Tactic: use f ⟨x, h⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ x ∈ f.domain
have rw : ∃ (y : F), (x, y) ∈ f.graph
Tactic: rw [mem_domain_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ y ∈ Set.range (↑f : ↥f.domain → F) ↔ ∃ (x : E), (x, y) ∈ f.graph
have mp : y ∈ Set.range (↑f : ↥f.domain → F) → ∃ (x : E), (x, y) ∈ f.graph
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ y ∈ Set.range (↑f : ↥f.domain → F) ↔ ∃ (x : E), (x, y) ∈ f.graph
have mpr : (∃ (x : E), (x, y) ∈ f.graph) → y ∈ Set.range (↑f : ↥f.domain → F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (hypothesis)
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)
⊢ ∃ (x : E), (x, y) ∈ f.graph
have h₁ : ∃ (y_1 : ↥f.domain), (↑f : ↥f.domain → F) y_1 = y
Tactic: rw [Set.mem_range] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ ∃ (x : E), (x, y) ∈ f.graph
have 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
Tactic: rcases h with ⟨⟨x, hx⟩, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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 : E), (x, y) ∈ f.graph
have h₁ : (x, y) ∈ f.graph
Tactic: use x
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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, y) ∈ f.graph
have h₁ : (x, (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)) ∈ f.graph
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
have simp_rw : (∃ (y : F), (x, y) ∈ f.graph) ↔ ∃ (y : F), (x, y) ∈ g.graph
Tactic: simp_rw [mem_domain_iff, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ f ≤ g
have left : f.domain ≤ g.domain
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ f ≤ g
have right : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄ (_h : (↑x : E) = (↑y : E)), (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ x ∈ g.domain
have left : ∀ (hx : ∃ (y : F), (x, y) ∈ f.graph), ∃ (y : F), (x, y) ∈ g.graph
Tactic: rw [mem_domain_iff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ ∃ (y : F), (x, y) ∈ g.graph
have left : ∀ (y : F) (hx : (x, y) ∈ f.graph), ∃ (y : F), (x, y) ∈ g.graph
Tactic: obtain ⟨y, hx⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ ∃ (y : F), (x, y) ∈ g.graph
have h₁ : (x, y) ∈ g.graph
Tactic: use y
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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)
⊢ (↑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)
have right : (y, (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)) ∈ g.graph
Tactic: rw [image_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
have right : (y, (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)) ∈ f.graph
Tactic: refine h ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (hypothesis)
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 : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx)) ∈ f.graph
have hx₁ : y ∈ f.domain
Tactic: rw [hxy] at hx
Cleared hypotheses: hy, hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ (y, (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx_1)) ∈ f.graph
have 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)
Tactic: rw [← image_iff hx]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ x ∈ g.graph
have 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
Tactic: rw [mem_graph_iff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ ∃ (y : ↥g.domain), (↑y : E) = x.1 ∧ (↑g : ↥g.domain → F) y = x.2
have 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
Tactic: obtain ⟨y, hx⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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 : ↥g.domain), (↑y : E) = x.1 ∧ (↑g : ↥g.domain → F) y = x.2
have h₁ : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (↑y : E) sorry) : E) = x.1 ∧
  (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (↑y : E) sorry) = x.2
Tactic: use ⟨y, h.1 y.2⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ (↑(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
have h₁ : (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x.1 sorry) = x.2
Tactic: simp only [hx, true_and]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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 ⋯) = x.2
have h₁ : (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x.1 sorry) = (↑f : ↥f.domain → F) y
Tactic: convert! hx.2 using 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
have h₁ : (↑y : E) = (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x.1 sorry) : E)
Tactic: refine (h.2 ?_).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ f = g
have h₁ : f.domain = g.domain
Tactic: apply dExt
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ f = g
have h' : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄ (_h : (↑x : E) = (↑y : E)), (↑f : ↥f.domain → F) x = (↑g : ↥g.domain → F) y
Tactic: apply dExt
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ f.domain = g.domain
have h₁ : ∀ (x : E), x ∈ f.domain ↔ x ∈ g.domain
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
have refine_1 : ∃ (x : F), (a, x) ∈ g
Tactic: refine existsUnique_of_exists_of_unique ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
⊢ ∃! b : F, (a, b) ∈ g
have refine_2 : ∀ (y₁ y₂ : F), (a, y₁) ∈ g → (a, y₂) ∈ g → y₁ = y₂
Tactic: refine existsUnique_of_exists_of_unique ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
have a₁ : (∃ (x : F), (a, x) ∈ g) ↔ a ∈ map (LinearMap.fst R E F) g
Tactic: convert! ha
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
have h : 0 = ((a, y₁) - (a, y₂)).1
Tactic: convert! g.sub_mem hy₁ hy₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (hypothesis)
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
⊢ y₁ = y₂
have hy : (0, y₁ - y₂) ∈ g
Tactic: have hy : ((0 : E), y₁ - y₂) ∈ g := by
    convert! g.sub_mem hy₁ hy₂
    exact (sub_self _).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (hypothesis)
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
inst_9 : Module R F
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
v w : ↥(map (LinearMap.fst R E F) g)
⊢ valFromGraph hg ⋯ = valFromGraph hg ⋯ + valFromGraph hg ⋯
have hadd : (↑v : E) + (↑w : E) ∈ map (LinearMap.fst R E F) g
Tactic: have hadd := (g.map (LinearMap.fst R E F)).add_mem v.2 w.2