awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
hadd : (↑v : E) + (↑w : E) ∈ map (LinearMap.fst R E F) g
⊢ valFromGraph hg ⋯ = valFromGraph hg ⋯ + valFromGraph hg ⋯
have hvw : ((↑v : E) + (↑w : E), valFromGraph hg hadd) ∈ g
Tactic: have hvw := valFromGraph_mem hg hadd
-- 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)
hadd : (↑v : E) + (↑w : E) ∈ map (LinearMap.fst R E F) g
hvw : ((↑v : E) + (↑w : E), valFromGraph hg hadd) ∈ g
⊢ valFromGraph hg ⋯ = valFromGraph hg ⋯ + valFromGraph hg ⋯
have hvw' : ((↑v : E), valFromGraph hg sorry) + ((↑w : E), valFromGraph hg sorry) ∈ g
Tactic: have hvw' := g.add_mem (valFromGraph_mem hg v.2) (valFromGraph_mem hg w.2)
-- 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)
hadd : (↑v : E) + (↑w : E) ∈ map (LinearMap.fst R E F) g
hvw : ((↑v : E) + (↑w : E), valFromGraph hg hadd) ∈ g
hvw' : ((↑v : E), valFromGraph hg ⋯) + ((↑w : E), valFromGraph hg ⋯) ∈ g
⊢ valFromGraph hg ⋯ = valFromGraph hg ⋯ + valFromGraph hg ⋯
have hvw'₁ : ((↑v : E) + (↑w : E), valFromGraph hg sorry + valFromGraph hg sorry) ∈ g
Tactic: rw [Prod.mk_add_mk] at hvw'
Cleared hypotheses: hvw'
-- 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
a : R
v : ↥(map (LinearMap.fst R E F) g)
⊢ valFromGraph hg ⋯ = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (valFromGraph hg ⋯)
have hsmul : a • (↑v : E) ∈ map (LinearMap.fst R E F) g
Tactic: have hsmul := (g.map (LinearMap.fst R E F)).smul_mem a v.2
-- 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
a : R
v : ↥(map (LinearMap.fst R E F) g)
hsmul : a • (↑v : E) ∈ map (LinearMap.fst R E F) g
⊢ valFromGraph hg ⋯ = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (valFromGraph hg ⋯)
have hav : (a • (↑v : E), valFromGraph hg hsmul) ∈ g
Tactic: have hav := valFromGraph_mem hg hsmul
-- 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
a : R
v : ↥(map (LinearMap.fst R E F) g)
hsmul : a • (↑v : E) ∈ map (LinearMap.fst R E F) g
hav : (a • (↑v : E), valFromGraph hg hsmul) ∈ g
⊢ valFromGraph hg ⋯ = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (valFromGraph hg ⋯)
have hav' : a • ((↑v : E), valFromGraph hg sorry) ∈ g
Tactic: have hav' := g.smul_mem a (valFromGraph_mem hg v.2)
-- 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
a : R
v : ↥(map (LinearMap.fst R E F) g)
hsmul : a • (↑v : E) ∈ map (LinearMap.fst R E F) g
hav : (a • (↑v : E), valFromGraph hg hsmul) ∈ g
hav' : a • ((↑v : E), valFromGraph hg ⋯) ∈ g
⊢ valFromGraph hg ⋯ = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (valFromGraph hg ⋯)
have hav'₁ : (a • (↑v : E), a • valFromGraph hg sorry) ∈ g
Tactic: rw [Prod.smul_mk] at hav'
Cleared hypotheses: hav'
-- 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
x : ↥(map (LinearMap.fst R E F) g)
⊢ (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) x = valFromGraph hg ⋯
have change : (if hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0 then g.toLinearPMapAux hg else 0 :
      (a : ↥(map (LinearMap.fst R E F) g)) → F)
    x =
  valFromGraph hg sorry
Tactic: change (if hg : _ then g.toLinearPMapAux hg else 0) 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ (if hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0 then g.toLinearPMapAux hg else 0 :
        (a : ↥(map (LinearMap.fst R E F) g)) → F)
      x =
    valFromGraph hg ⋯
have rw : (g.toLinearPMapAux hg : (a : ↥(map (LinearMap.fst R E F) g)) → F) x = valFromGraph hg sorry
Tactic: rw [dif_pos]
-- 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
x : ↥(map (LinearMap.fst R E F) g)
⊢ (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) x = valFromGraph hg ⋯
have change : (if hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0 then g.toLinearPMapAux hg else 0 :
      (a : ↥(map (LinearMap.fst R E F) g)) → F)
    x =
  valFromGraph hg sorry
Tactic: classical
  change (if hg : _ then g.toLinearPMapAux hg else 0) x = _
  rw [dif_pos]
  · rfl
  · exact hg
-- 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
x : ↥(map (LinearMap.fst R E F) g)
change :
  (if hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0 then g.toLinearPMapAux hg else 0 :
        (a : ↥(map (LinearMap.fst R E F) g)) → F)
      x =
    valFromGraph hg ⋯
⊢ (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) x = valFromGraph hg ⋯
have change₁ : (g.toLinearPMapAux hg : (a : ↥(map (LinearMap.fst R E F) g)) → F) x = valFromGraph hg sorry
Tactic: classical
  change (if hg : _ then g.toLinearPMapAux hg else 0) x = _
  rw [dif_pos]
  · rfl
  · exact hg
-- 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
x : ↥(map (LinearMap.fst R E F) g)
⊢ ((↑x : E), (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) x) ∈ g
have rw : ((↑x : E), valFromGraph hg sorry) ∈ g
Tactic: rw [toLinearPMap_apply_aux hg]
-- 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
⊢ g.toLinearPMap.graph = g
have h : ∀ (x_fst : E) (x_snd : F), (x_fst, x_snd) ∈ g.toLinearPMap.graph ↔ (x_fst, x_snd) ∈ g
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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
⊢ (x_fst, x_snd) ∈ g.toLinearPMap.graph ↔ (x_fst, x_snd) ∈ g
have h : (x_fst, x_snd) ∈ g.toLinearPMap.graph → (x_fst, x_snd) ∈ g
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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
h : (x_fst, x_snd) ∈ g.toLinearPMap.graph → (x_fst, x_snd) ∈ g
⊢ (x_fst, x_snd) ∈ g.toLinearPMap.graph ↔ (x_fst, x_snd) ∈ g
have h₁ : (x_fst, x_snd) ∈ g → (x_fst, x_snd) ∈ g.toLinearPMap.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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g.toLinearPMap.graph
⊢ (x_fst, x_snd) ∈ g
have hx₁ : ∃ (y : ↥g.toLinearPMap.domain),
  (↑y : E) = (x_fst, x_snd).1 ∧ (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y = (x_fst, x_snd).2
Tactic: rw [LinearPMap.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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
hx :
  ∃ (y : ↥g.toLinearPMap.domain),
    (↑y : E) = (x_fst, x_snd).1 ∧ (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ g
have h : ∀ (y : ↥g.toLinearPMap.domain) (hx1 : (↑y : E) = (x_fst, x_snd).1)
  (hx2 : (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y = (x_fst, x_snd).2), (x_fst, x_snd) ∈ g
Tactic: rcases hx with ⟨y, hx1, hx2⟩
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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
y : ↥g.toLinearPMap.domain
hx1 : (↑y : E) = (x_fst, x_snd).1
hx2 : (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ g
have h : (x_fst, x_snd) = ((↑y : E), (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y)
Tactic: convert! g.mem_graph_toLinearPMap hg y 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
⊢ (x_fst, x_snd) ∈ g.toLinearPMap.graph
have h : ∃ (y : ↥g.toLinearPMap.domain),
  (↑y : E) = (x_fst, x_snd).1 ∧ (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y = (x_fst, x_snd).2
Tactic: rw [LinearPMap.mem_graph_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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
⊢ x_fst ∈ map (LinearMap.fst R E F) g
have simp : ∃ (x : F), (x_fst, x) ∈ g
Tactic: simp only [mem_map, LinearMap.fst_apply, Prod.exists, exists_and_right, exists_eq_right]
-- 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
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
⊢ ∃ (y : ↥g.toLinearPMap.domain),
    (↑y : E) = (x_fst, x_snd).1 ∧ (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y = (x_fst, x_snd).2
have hx_fst : x_fst ∈ map (LinearMap.fst R E F) g
Tactic: have hx_fst : x_fst ∈ g.map (LinearMap.fst R E F) := by
    simp only [mem_map, LinearMap.fst_apply, Prod.exists, exists_and_right, exists_eq_right]
    exact ⟨x_snd, 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
g : Submodule R (E × F)
hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.1 = 0), x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
hx_fst : x_fst ∈ map (LinearMap.fst R E F) g
⊢ ∃ (y : ↥g.toLinearPMap.domain),
    (↑y : E) = (x_fst, x_snd).1 ∧ (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F) y = (x_fst, x_snd).2
have h : (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F)
    (Subtype.mk (p := fun (x : E) ↦ x ∈ g.toLinearPMap.domain) x_fst hx_fst) =
  (x_fst, x_snd).2
Tactic: refine ⟨⟨x_fst, hx_fst⟩, Subtype.coe_mk x_fst hx_fst, ?_⟩
-- 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
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
hx_fst : x_fst ∈ map (LinearMap.fst R E F) g
⊢ (↑g.toLinearPMap : ↥g.toLinearPMap.domain → F)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ g.toLinearPMap.domain) x_fst hx_fst) =
    (x_fst, x_snd).2
have h : valFromGraph hg sorry = (x_fst, x_snd).2
Tactic: rw [toLinearPMap_apply_aux hg]
-- 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
⊢ g.toLinearPMap.toFun.range = map (LinearMap.snd R E F) g
have rwa : map (LinearMap.snd R E F) g.toLinearPMap.graph = map (LinearMap.snd R E F) g
Tactic: rwa [← LinearPMap.graph_map_snd_eq_range, toLinearPMap_graph_eq]
-- 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
rwa : map (LinearMap.snd R E F) g.toLinearPMap.graph = map (LinearMap.snd R E F) g
⊢ g.toLinearPMap.toFun.range = map (LinearMap.snd R E F) g
have rwa₁ : map (LinearMap.snd R E F) g = map (LinearMap.snd R E F) g
Tactic: rwa [← LinearPMap.graph_map_snd_eq_range, toLinearPMap_graph_eq]
-- 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.inverse.domain = f.toFun.range
have rw : (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).toLinearPMap.domain = f.toFun.range
Tactic: rw [inverse, Submodule.toLinearPMap_domain, ← graph_map_snd_eq_range,
    ← LinearEquiv.fst_comp_prodComm, Submodule.map_comp]
-- 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
rw : (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).toLinearPMap.domain = f.toFun.range
⊢ f.inverse.domain = f.toFun.range
have rw₁ : Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
  f.toFun.range
Tactic: rw [inverse, Submodule.toLinearPMap_domain, ← graph_map_snd_eq_range,
    ← LinearEquiv.fst_comp_prodComm, Submodule.map_comp]
-- 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
rw : (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).toLinearPMap.domain = f.toFun.range
rw₁ :
  Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
    f.toFun.range
⊢ f.inverse.domain = f.toFun.range
have rw₂ : Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
  Submodule.map (LinearMap.snd R E F) f.graph
Tactic: rw [inverse, Submodule.toLinearPMap_domain, ← graph_map_snd_eq_range,
    ← LinearEquiv.fst_comp_prodComm, Submodule.map_comp]
-- 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
rw : (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).toLinearPMap.domain = f.toFun.range
rw₁ :
  Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
    f.toFun.range
rw₂ :
  Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
    Submodule.map (LinearMap.snd R E F) f.graph
⊢ f.inverse.domain = f.toFun.range
have rw₃ : Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
  Submodule.map (LinearMap.fst R F E ∘ₗ (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E)) f.graph
Tactic: rw [inverse, Submodule.toLinearPMap_domain, ← graph_map_snd_eq_range,
    ← LinearEquiv.fst_comp_prodComm, Submodule.map_comp]
-- 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
rw : (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).toLinearPMap.domain = f.toFun.range
rw₁ :
  Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
    f.toFun.range
rw₂ :
  Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
    Submodule.map (LinearMap.snd R E F) f.graph
rw₃ :
  Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
    Submodule.map (LinearMap.fst R F E ∘ₗ (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E)) f.graph
⊢ f.inverse.domain = f.toFun.range
have rw₄ : Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph) =
  Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph)
Tactic: rw [inverse, Submodule.toLinearPMap_domain, ← graph_map_snd_eq_range,
    ← LinearEquiv.fst_comp_prodComm, Submodule.map_comp]
-- 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
hf : f.toFun.ker = ⊥
x : F × E
hv : x ∈ Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph
hv' : x.1 = 0
⊢ x.2 = 0
have rcases : ∀ (x : F) (y : E) (hv : (x, y) ∈ Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph)
  (hv' : (x, y).1 = 0), (x, y).2 = 0
Tactic: rcases x with ⟨x, y⟩
Cleared hypotheses: x, hv, hv'
-- 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
hf : f.toFun.ker = ⊥
x : F
y : E
hv : (x, y) ∈ Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph
hv' : (x, y).1 = 0
⊢ (x, y).2 = 0
have subst : ∀ (hv : (0, y) ∈ Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph), (0, y).2 = 0
Tactic: subst hv'
Cleared hypotheses: x, hv, hv'
-- 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
hf : f.toFun.ker = ⊥
y : E
hv : (0, y) ∈ Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph
⊢ (0, y).2 = 0
have hv₁ : ∃ (y_1 : ↥f.domain), (↑y_1 : E) = y ∧ (↑f : ↥f.domain → F) y_1 = 0
Tactic: simp only [Submodule.map_equiv_eq_comap_symm, Submodule.mem_comap, LinearEquiv.symm_prodComm,
    LinearEquiv.coe_coe, LinearEquiv.prodComm_apply, mem_graph_iff, Prod.swap] at hv
Cleared hypotheses: hv
-- 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
hf : f.toFun.ker = ⊥
y : E
hv : ∃ (y_1 : ↥f.domain), (↑y_1 : E) = y ∧ (↑f : ↥f.domain → F) y_1 = 0
⊢ (0, y).2 = 0
have rcases : ∀ (z : ↥f.domain) (hz : (↑f : ↥f.domain → F) z = 0), (0, (↑z : E)).2 = 0
Tactic: rcases hv with ⟨z, rfl, hz⟩
Cleared hypotheses: y, hv
-- 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
hf : f.toFun.ker = ⊥
z : ↥f.domain
hz : (↑f : ↥f.domain → F) z = 0
⊢ (0, (↑z : E)).2 = 0
have rw : ∀ (hf : ∀ (m : ↥f.domain), Eq.{u_5 + 1} (α := F) ((f.toFun : (a : ↥f.domain) → F) m : F) (0 : F) → m = 0)
  (z : ↥f.domain) (hz : (↑f : ↥f.domain → F) z = 0), (0, (↑z : E)).2 = 0
Tactic: rw [LinearMap.ker_eq_bot'] at hf
Cleared hypotheses: hf, z, hz
-- 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
hf : f.toFun.ker = ⊥
⊢ f.inverse.graph = Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph
have rw : (Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph).toLinearPMap.graph =
  Submodule.map (↑(LinearEquiv.prodComm R E F) : E × F →ₗ[R] F × E) f.graph
Tactic: rw [inverse, Submodule.toLinearPMap_graph_eq _ (mem_inverse_graph_snd_eq_zero hf)]