awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) ↦ x1 ≤ x2) c
l : E →ₛₗ.[σ] F
hl : l ∈ c
x : ↥l.domain
⊢ (↑(LinearPMap.sSup c hc) : ↥(LinearPMap.sSup c hc).domain → F)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hc).domain) (↑x : E) ⋯) =
    (↑l : ↥l.domain → F) x
have symm : (↑l : ↥l.domain → F) x =
  (↑(LinearPMap.sSup c hc) : ↥(LinearPMap.sSup c hc).domain → F)
    (Subtype.mk (p := fun (x : E) ↦ x ∈ (LinearPMap.sSup c hc).domain) (↑x : E) sorry)
Tactic: symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
f : E →ₛₗ.[σ] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : (↑x : E) = (↑y : E)
⊢ (Submodule.inclusion ⋯ : (a : ↥(S ⊓ f.domain)) → ↥f.domain) x = y
have a : (↑((Submodule.inclusion sorry : (a : ↥(S ⊓ f.domain)) → ↥f.domain) x) : E) = (↑y : E)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (hypothesis)
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
f : E →ₛₗ.[σ] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : (↑x : E) = (↑y : E)
⊢ (↑(f.domRestrict S) : ↥(f.domRestrict S).domain → F) x = (↑f : ↥f.domain → F) y
have this : (Submodule.inclusion sorry : (a : ↥(S ⊓ f.domain)) → ↥f.domain) x = y
Tactic: have : Submodule.inclusion (by simp) x = y := by
    ext
    simp [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
f : E →ₛₗ.[σ] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : (↑x : E) = (↑y : E)
this : (Submodule.inclusion ⋯ : (a : ↥(S ⊓ f.domain)) → ↥f.domain) x = y
⊢ (↑(f.domRestrict S) : ↥(f.domRestrict S).domain → F) x = (↑f : ↥f.domain → F) y
have rw : (↑(f.domRestrict S) : ↥(f.domRestrict S).domain → F) x =
  (↑f : ↥f.domain → F) ((Submodule.inclusion sorry : (a : ↥(S ⊓ f.domain)) → ↥f.domain) x)
Tactic: rw [← this]
-- 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 × F
⊢ x ∈ f.graph ↔ ∃ (y : ↥f.domain), (↑y : E) = x.1 ∧ (↑f : ↥f.domain → F) y = x.2
have mk : ∀ (fst : E) (snd : F),
  (fst, snd) ∈ f.graph ↔ ∃ (y : ↥f.domain), (↑y : E) = (fst, snd).1 ∧ (↑f : ↥f.domain → F) y = (fst, snd).2
Tactic: cases x
Cleared hypotheses: 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
fst : E
snd : F
⊢ (fst, snd) ∈ f.graph ↔ ∃ (y : ↥f.domain), (↑y : E) = (fst, snd).1 ∧ (↑f : ↥f.domain → F) y = (fst, snd).2
have mk : (fst, snd) ∈ f.graph ↔ ∃ (y : ↥f.domain), (↑y : E) = fst ∧ (↑f : ↥f.domain → F) y = snd
Tactic: simp_rw [mem_graph_iff', Prod.mk_inj]
-- 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
fst : E
snd : F
mk mk₁ : (fst, snd) ∈ f.graph ↔ ∃ (y : ↥f.domain), (↑y : E) = fst ∧ (↑f : ↥f.domain → F) y = snd
⊢ (fst, snd) ∈ f.graph ↔ ∃ (y : ↥f.domain), (↑y : E) = (fst, snd).1 ∧ (↑f : ↥f.domain → F) y = (fst, snd).2
have mk₂ : (∃ (y : ↥f.domain), ((↑y : E), (↑f : ↥f.domain → F) y) = (fst, snd)) ↔
  ∃ (y : ↥f.domain), (↑y : E) = fst ∧ (↑f : ↥f.domain → F) y = snd
Tactic: simp_rw [mem_graph_iff', Prod.mk_inj]
-- 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
⊢ Submodule.map (LinearMap.fst R E F) f.graph = f.domain
have h : ∀ (x : E), x ∈ Submodule.map (LinearMap.fst R E F) f.graph ↔ x ∈ f.domain
Tactic: ext 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
x : E
⊢ x ∈ Submodule.map (LinearMap.fst R E F) f.graph ↔ x ∈ f.domain
have h : (∃ (x_1 : F) (h : x ∈ f.domain), (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x sorry) = x_1) ↔
  x ∈ f.domain
Tactic: simp only [Submodule.mem_map, mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left,
    LinearMap.fst_apply, Prod.exists, exists_and_right, exists_eq_right]
-- 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_1 : F) (h : x ∈ f.domain), (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x ⋯) = x_1) ↔
    x ∈ f.domain
have h : (∃ (x_1 : F) (h : x ∈ f.domain), (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x sorry) = x_1) →
  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_1 : F) (h : x ∈ f.domain), (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x ⋯) = x_1) →
    x ∈ f.domain
⊢ (∃ (x_1 : F) (h : x ∈ f.domain), (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x ⋯) = x_1) ↔
    x ∈ f.domain
have h₁ : x ∈ f.domain →
  ∃ (x_1 : F) (h : x ∈ f.domain), (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x sorry) = x_1
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_1 : F) (h : x ∈ f.domain), (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x ⋯) = x_1
⊢ x ∈ f.domain
have h₁ : ∀ (x_1 : F) (hx : x ∈ f.domain),
  (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x sorry) = x_1 → x ∈ f.domain
Tactic: rcases h with ⟨x, hx, _⟩
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 : E
h : x ∈ f.domain
⊢ ∃ (x_1 : F) (h : x ∈ f.domain), (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x ⋯) = x_1
have h₁ : ∃ (h_1 : x ∈ f.domain),
  (↑f : ↥f.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ f.domain) x sorry) =
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x h)
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
⊢ Submodule.map (LinearMap.snd R E F) f.graph = f.toFun.range
have h : ∀ (x : F), x ∈ Submodule.map (LinearMap.snd R E F) f.graph ↔ x ∈ f.toFun.range
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
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
⊢ (z • f).graph = Submodule.map (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id)) f.graph
have h : ∀ (x_fst : E) (x_snd : F),
  (x_fst, x_snd) ∈ (z • f).graph ↔
    (x_fst, x_snd) ∈
      Submodule.map (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id)) f.graph
Tactic: ext ⟨x_fst, x_snd⟩
-- 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
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
⊢ (x_fst, x_snd) ∈ (z • f).graph ↔
    (x_fst, x_snd) ∈
      Submodule.map (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id)) f.graph
have h : (x_fst, x_snd) ∈ (z • f).graph →
  (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id)) 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
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
h :
  (x_fst, x_snd) ∈ (z • f).graph →
    (x_fst, x_snd) ∈
      Submodule.map (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id)) f.graph
⊢ (x_fst, x_snd) ∈ (z • f).graph ↔
    (x_fst, x_snd) ∈
      Submodule.map (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id)) f.graph
have h₁ : (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id)) f.graph →
  (x_fst, x_snd) ∈ (z • f).graph
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
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
h : (x_fst, x_snd) ∈ (z • f).graph
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id)) f.graph
have h₁ : ∃ (y : ↥(z • f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(z • f) : ↥(z • f).domain → F) y = (x_fst, x_snd).2
Tactic: rw [mem_graph_iff] 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
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
h : ∃ (y : ↥(z • f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(z • f) : ↥(z • f).domain → F) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id)) f.graph
have h₁ : ∀ (y : ↥(z • f).domain) (hy : (↑y : E) = (x_fst, x_snd).1) (h : (↑(z • f) : ↥(z • f).domain → F) y = (x_fst, x_snd).2),
  (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id)) f.graph
Tactic: rcases h with ⟨y, hy, h⟩
Cleared hypotheses: 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
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
y : ↥(z • f).domain
hy : (↑y : E) = (x_fst, x_snd).1
h : (↑(z • f) : ↥(z • f).domain → F) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id)) f.graph
have h₁ : z • (↑f : ↥f.domain → F) y = (x_fst, x_snd).2
Tactic: rw [LinearPMap.smul_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
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
y : ↥(z • f).domain
hy : (↑y : E) = (x_fst, x_snd).1
h : z • (↑f : ↥f.domain → F) y = (x_fst, x_snd).2
⊢ ∃ y ∈ f.graph,
    (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z 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 ∧ z • (↑f : ↥f.domain → F) a_1 = x_snd
Tactic: simp only [mem_graph_iff, LinearMap.prodMap_apply, LinearMap.id_coe, id,
      LinearMap.smul_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
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
y : ↥(z • f).domain
hy : (↑y : E) = (x_fst, x_snd).1
h : z • (↑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 ∧ z • (↑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
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
y : ↥(z • f).domain
hy : (↑y : E) = (x_fst, x_snd).1
h : z • (↑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 ∧ z • (↑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
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
y : ↥(z • f).domain
hy : (↑y : E) = (x_fst, x_snd).1
h : z • (↑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 ∧ z • (↑f : ↥f.domain → F) a_1 = x_snd
have right : x_fst = x_fst ∧ z • (↑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
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
h :
  (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id)) f.graph
⊢ (x_fst, x_snd) ∈ (z • f).graph
have h₁ : ∃ y ∈ f.graph,
  (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z 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
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
h :
  ∃ y ∈ f.graph,
    (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id) : (a : E × F) → E × F) y =
      (x_fst, x_snd)
⊢ (x_fst, x_snd) ∈ (z • f).graph
have h₁ : ∀ (x' : E × F) (hx' : x' ∈ f.graph)
  (h :
    (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id) : (a : E × F) → E × F) x' =
      (x_fst, x_snd)),
  (x_fst, x_snd) ∈ (z • 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
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
x' : E × F
hx' : x' ∈ f.graph
h :
  (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id) : (a : E × F) → E × F) x' =
    (x_fst, x_snd)
⊢ (x_fst, x_snd) ∈ (z • f).graph
have h₁ : ∀ (fst : E) (snd : F) (hx' : (fst, snd) ∈ f.graph)
  (h :
    (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id) : (a : E × F) → E × F) (fst, snd) =
      (x_fst, x_snd)),
  (x_fst, x_snd) ∈ (z • 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
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
fst : E
snd : F
hx' : (fst, snd) ∈ f.graph
h :
  (LinearMap.prodMap LinearMap.id (HSMul.hSMul (β := F →ₗ[R] F) z LinearMap.id) : (a : E × F) → E × F) (fst, snd) =
    (x_fst, x_snd)
⊢ (x_fst, x_snd) ∈ (z • f).graph
have h₁ : fst = x_fst ∧ z • snd = x_snd
Tactic: simp only [LinearMap.prodMap_apply, LinearMap.id_coe, id, LinearMap.smul_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
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
fst : E
snd : F
hx' : (fst, snd) ∈ f.graph
h : fst = x_fst ∧ z • snd = x_snd
⊢ (x_fst, x_snd) ∈ (z • 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 ∧ z • snd = x_snd),
  ∃ (y : ↥(z • f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(z • f) : ↥(z • 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
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
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 ∧ z • snd = x_snd
⊢ ∃ (y : ↥(z • f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(z • f) : ↥(z • 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 : ↥(z • f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(z • f) : ↥(z • 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
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
fst : E
snd : F
h : fst = x_fst ∧ z • snd = x_snd
y : ↥f.domain
hy : (↑y : E) = (fst, snd).1
hx' : (↑f : ↥f.domain → F) y = (fst, snd).2
⊢ ∃ (y : ↥(z • f).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(z • f) : ↥(z • f).domain → F) y = (x_fst, x_snd).2
have h₁ : (↑y : E) = (x_fst, x_snd).1 ∧ (↑(z • f) : ↥(z • 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
M : Type u_7
inst_4 : Monoid M
inst_5 : DistribMulAction M F
inst_6 : Module R F
inst_7 : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
fst : E
snd : F
h : fst = x_fst ∧ z • 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 ∧ (↑(z • f) : ↥(z • f).domain → F) y = (x_fst, x_snd).2
have h₁ : (↑y : E) = (fst, z • snd).1 ∧ (↑(z • f) : ↥(z • f).domain → F) y = (fst, z • 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
⊢ (-f).graph = Submodule.map (LinearMap.prodMap LinearMap.id (-LinearMap.id)) f.graph
have h : ∀ (x_fst : E) (x_snd : F),
  (x_fst, x_snd) ∈ (-f).graph ↔ (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (-LinearMap.id)) f.graph
Tactic: ext ⟨x_fst, x_snd⟩
-- 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_fst, x_snd) ∈ (-f).graph ↔ (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (-LinearMap.id)) f.graph
have h : (x_fst, x_snd) ∈ (-f).graph → (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (-LinearMap.id)) 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_fst : E
x_snd : F
h :
  (x_fst, x_snd) ∈ (-f).graph → (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (-LinearMap.id)) f.graph
⊢ (x_fst, x_snd) ∈ (-f).graph ↔ (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (-LinearMap.id)) f.graph
have h₁ : (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (-LinearMap.id)) f.graph → (x_fst, x_snd) ∈ (-f).graph
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
x_fst : E
x_snd : F
h : (x_fst, x_snd) ∈ (-f).graph
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.prodMap LinearMap.id (-LinearMap.id)) f.graph
have h₁ : ∃ (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 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).domain), (↑y : E) = (x_fst, x_snd).1 ∧ (↑(-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₁ : ∀ (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
Tactic: rcases h with ⟨y, hy, h⟩
Cleared hypotheses: h