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
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
x : E
y : F
H_1 : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
H :
  ∀ (c₁ c₂ : R),
    c₁ • x = c₂ • x →
      HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₁ : S) y =
        HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₂ : S) y
y' z' : ↥(R ∙ x)
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := S)
      ((σ : (a : R) → S) (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑(y' + z') : E)) ⋯) : S) y =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S)
        ((σ : (a : R) → S) (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑y' : E)) ⋯) : S) y +
      HSMul.hSMul.{u_2, u_5, u_5} (α := S)
        ((σ : (a : R) → S) (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑z' : E)) ⋯) : S) y
have a : Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑(y' + z') : E)) sorry • x =
  (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑y' : E)) sorry +
      Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑z' : E)) sorry) •
    x
Tactic: rw [← add_smul, ← RingHom.map_add, H]
-- 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
x : E
y : F
H_1 : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
H :
  ∀ (c₁ c₂ : R),
    c₁ • x = c₂ • x →
      HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₁ : S) y =
        HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₂ : S) y
y' z' : ↥(R ∙ x)
⊢ Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑(y' + z') : E)) ⋯ • x =
    (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑y' : E)) ⋯ +
        Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑z' : E)) ⋯) •
      x
have this : ∀ (w : ↥(R ∙ x)), Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑w : E)) sorry • x = (↑w : E)
Tactic: have (w : R ∙ x) := Classical.choose_spec (mem_span_singleton.1 w.prop)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
x : E
y : F
H_1 : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
H :
  ∀ (c₁ c₂ : R),
    c₁ • x = c₂ • x →
      HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₁ : S) y =
        HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₂ : S) y
c : R
z : ↥(R ∙ x)
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := S)
      ((σ : (a : R) → S) (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑(c • z) : E)) ⋯) : S) y =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S)
      (HSMul.hSMul.{u_2, u_5, u_5} (α := S)
        ((σ : (a : R) → S) (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑z : E)) ⋯) : S) y)
have a : Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑(c • z) : E)) sorry • x =
  (c * Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑z : E)) sorry) • x
Tactic: rw [smul_smul, ← RingHom.map_mul, H]
-- 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
x : E
y : F
H_1 : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
H :
  ∀ (c₁ c₂ : R),
    c₁ • x = c₂ • x →
      HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₁ : S) y =
        HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₂ : S) y
c : R
z : ↥(R ∙ x)
⊢ Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑(c • z) : E)) ⋯ • x =
    (c * Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑z : E)) ⋯) • x
have this : ∀ (w : ↥(R ∙ x)), Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑w : E)) sorry • x = (↑w : E)
Tactic: have (w : R ∙ x) := Classical.choose_spec (mem_span_singleton.1 w.prop)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
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
x : E
y : F
H_1 : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
H :
  ∀ (c₁ c₂ : R),
    c₁ • x = c₂ • x →
      HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₁ : S) y =
        HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c₂ : S) y
c : R
z : ↥(R ∙ x)
this : ∀ (w : ↥(R ∙ x)), Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑w : E)) ⋯ • x = (↑w : E)
⊢ Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑(c • z) : E)) ⋯ • x =
    (c * Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = (↑z : E)) ⋯) • x
have a : (↑(c • z) : E) = c • (↑z : E)
Tactic: simp only [mul_smul, this]
-- 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
x : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ (↑(mkSpanSingleton' x y H) : ↥(mkSpanSingleton' x y H).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (mkSpanSingleton' x y H).domain) (c • x) h) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y
have dsimp : HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = c • x) sorry) : S)
    y =
  HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y
Tactic: dsimp [mkSpanSingleton']
-- 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
x : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := S)
      ((σ : (a : R) → S) (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = c • x) ⋯) : S) y =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y
have rw : HSMul.hSMul.{u_2, u_5, u_5} (α := S)
    ((σ : (a : R) → S) (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = c • x) sorry - c) : S) y =
  0
Tactic: rw [← sub_eq_zero, ← sub_smul, ← RingHom.map_sub]
-- 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
x : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := S)
      ((σ : (a : R) → S) (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = c • x) ⋯ - c) : S) y =
    0
have a : (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = c • x) sorry - c) • x = 0
Tactic: apply H
-- 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
x : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ (Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = c • x) ⋯ - c) • x = 0
have a : Classical.choose (p := fun (x_1 : R) ↦ x_1 • x = c • x) sorry • x = c • x
Tactic: simp only [sub_smul, sub_eq_zero]
-- 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
x : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
| y
have rw : HSMul.hSMul.{u_2, u_5, u_5} (α := S) 1 y
Tactic: rw [← one_smul S y]
-- 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
x : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
⊢ (↑(mkSpanSingleton' x y H) : ↥(mkSpanSingleton' x y H).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (mkSpanSingleton' x y H).domain) x h) =
    y
have conv_rhs : (↑(mkSpanSingleton' x y H) : ↥(mkSpanSingleton' x y H).domain → F)
    (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (mkSpanSingleton' x y H).domain) x h) =
  HSMul.hSMul.{u_2, u_5, u_5} (α := S) 1 y
Tactic: conv_rhs => rw [← one_smul S y]
-- 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
x : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
⊢ (↑(mkSpanSingleton' x y H) : ↥(mkSpanSingleton' x y H).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (mkSpanSingleton' x y H).domain) x h) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) 1 y
have rw : (↑(mkSpanSingleton' x y H) : ↥(mkSpanSingleton' x y H).domain → F)
    (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (mkSpanSingleton' x y H).domain) x h) =
  (↑(mkSpanSingleton' x y H) : ↥(mkSpanSingleton' x y H).domain → F)
    (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (mkSpanSingleton' x y H).domain) (HSMul.hSMul.{u_1, u_4, u_4} (α := R) 1 x)
      sorry)
Tactic: rw [← RingHom.map_one, ← mkSpanSingleton'_apply x y H 1 ?_]
-- 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
x : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
rw :
  (↑(mkSpanSingleton' x y H) : ↥(mkSpanSingleton' x y H).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (mkSpanSingleton' x y H).domain) x h) =
    (↑(mkSpanSingleton' x y H) : ↥(mkSpanSingleton' x y H).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (mkSpanSingleton' x y H).domain)
        (HSMul.hSMul.{u_1, u_4, u_4} (α := R) 1 x) ⋯)
⊢ (↑(mkSpanSingleton' x y H) : ↥(mkSpanSingleton' x y H).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (mkSpanSingleton' x y H).domain) x h) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) 1 y
have rw₁ : HSMul.hSMul.{u_1, u_4, u_4} (α := R) 1 x ∈ (mkSpanSingleton' x y H).domain
Tactic: rw [← RingHom.map_one, ← mkSpanSingleton'_apply x y H 1 ?_]
-- 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
x : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
⊢ (↑(mkSpanSingleton' x y H) : ↥(mkSpanSingleton' x y H).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (mkSpanSingleton' x y H).domain) x h) =
    (↑(mkSpanSingleton' x y H) : ↥(mkSpanSingleton' x y H).domain → F)
      (Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ (mkSpanSingleton' x y H).domain)
        (HSMul.hSMul.{u_1, u_4, u_4} (α := R) 1 x) ⋯)
have e_a : x = HSMul.hSMul.{u_1, u_4, u_4} (α := R) 1 x
Tactic: congr
-- 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
x : E
y : F
H : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
⊢ x = HSMul.hSMul.{u_1, u_4, u_4} (α := R) 1 x
have e_a : x = x
Tactic: rw [one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ_1 : R →+* S
τ : S →+* T
E_1 : Type u_4
inst_3 : AddCommGroup E_1
inst_4 : Module R E_1
F_1 : Type u_5
inst_5 : AddCommGroup F_1
inst_6 : Module S F_1
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
K : Type u_7
L : Type u_8
E : Type u_9
F : Type u_10
inst_9 : DivisionRing K
inst_10 : DivisionRing L
σ : K →+* L
inst_11 : AddCommGroup E
inst_12 : Module K E
inst_13 : AddCommGroup F
inst_14 : Module L F
x : E
y : F
hx : x ≠ 0
c : K
hc_1 : c • x = 0
hc : c = 0
⊢ HSMul.hSMul.{u_8, u_10, u_10} (α := L) ((σ : (a : K) → L) c : L) y = 0
have rw : HSMul.hSMul.{u_8, u_10, u_10} (α := L) ((σ : (a : K) → L) 0 : L) y = 0
Tactic: rw [hc, RingHom.map_zero, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ_1 : R →+* S
τ : S →+* T
E_1 : Type u_4
inst_3 : AddCommGroup E_1
inst_4 : Module R E_1
F_1 : Type u_5
inst_5 : AddCommGroup F_1
inst_6 : Module S F_1
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
K : Type u_7
L : Type u_8
E : Type u_9
F : Type u_10
inst_9 : DivisionRing K
inst_10 : DivisionRing L
σ : K →+* L
inst_11 : AddCommGroup E
inst_12 : Module K E
inst_13 : AddCommGroup F
inst_14 : Module L F
x : E
y : F
hx : x ≠ 0
c : K
hc_1 : c • x = 0
hc : c = 0
rw : HSMul.hSMul.{u_8, u_10, u_10} (α := L) ((σ : (a : K) → L) 0 : L) y = 0
⊢ HSMul.hSMul.{u_8, u_10, u_10} (α := L) ((σ : (a : K) → L) c : L) y = 0
have rw₁ : HSMul.hSMul.{u_8, u_10, u_10} (α := L) 0 y = 0
Tactic: rw [hc, RingHom.map_zero, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ_1 : R →+* S
τ : S →+* T
E_1 : Type u_4
inst_3 : AddCommGroup E_1
inst_4 : Module R E_1
F_1 : Type u_5
inst_5 : AddCommGroup F_1
inst_6 : Module S F_1
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
K : Type u_7
L : Type u_8
E : Type u_9
F : Type u_10
inst_9 : DivisionRing K
inst_10 : DivisionRing L
σ : K →+* L
inst_11 : AddCommGroup E
inst_12 : Module K E
inst_13 : AddCommGroup F
inst_14 : Module L F
x : E
y : F
hx : x ≠ 0
c : K
hc_1 : c • x = 0
hc : c = 0
rw : HSMul.hSMul.{u_8, u_10, u_10} (α := L) ((σ : (a : K) → L) 0 : L) y = 0
rw₁ : HSMul.hSMul.{u_8, u_10, u_10} (α := L) 0 y = 0
⊢ HSMul.hSMul.{u_8, u_10, u_10} (α := L) ((σ : (a : K) → L) c : L) y = 0
have rw₂ : Eq.{u_10 + 1} (α := F) 0 0
Tactic: rw [hc, RingHom.map_zero, zero_smul]
-- 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
f g : E →ₛₗ.[σ] F
c : R
x : E
h :
  Membership.mem (γ := Set E)
    {x : E |
      ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain),
        (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hf) =
          (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hg)}
    x
hfx : x ∈ f.domain
hgx : x ∈ g.domain
hx :
  (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)
⊢ (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (c • x) ⋯) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (c • x) ⋯)
have this : ∀ {f : E →ₛₗ.[σ] F} (hfx : x ∈ f.domain),
  Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (c • x) sorry = c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx
Tactic: have {f : E →ₛₗ.[σ] F} (hfx) : (⟨c • x, smul_mem _ c hfx⟩ : f.domain) = c • ⟨x, hfx⟩ := by
        simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
c : R
x : E
h :
  Membership.mem (γ := Set E)
    {x : E |
      ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain),
        (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hf) =
          (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hg)}
    x
hfx : x ∈ f.domain
hgx : x ∈ g.domain
hx :
  (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)
this :
  ∀ {f : E →ₛₗ.[σ] F} (hfx : x ∈ f.domain),
    Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (c • x) ⋯ = c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx
⊢ (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (c • x) ⋯) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (c • x) ⋯)
have rw : (↑f : ↥f.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
  (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (c • x) sorry)
Tactic: rw [this hfx, this hgx, f.map_smulₛₗ, g.map_smulₛₗ, hx]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
c : R
x : E
h :
  Membership.mem (γ := Set E)
    {x : E |
      ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain),
        (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hf) =
          (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hg)}
    x
hfx : x ∈ f.domain
hgx : x ∈ g.domain
hx :
  (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)
this :
  ∀ {f : E →ₛₗ.[σ] F} (hfx : x ∈ f.domain),
    Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (c • x) ⋯ = c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx
rw :
  (↑f : ↥f.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (c • x) ⋯)
⊢ (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (c • x) ⋯) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (c • x) ⋯)
have rw₁ : (↑f : ↥f.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
  (↑g : ↥g.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)
Tactic: rw [this hfx, this hgx, f.map_smulₛₗ, g.map_smulₛₗ, hx]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
c : R
x : E
h :
  Membership.mem (γ := Set E)
    {x : E |
      ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain),
        (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hf) =
          (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hg)}
    x
hfx : x ∈ f.domain
hgx : x ∈ g.domain
hx :
  (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)
this :
  ∀ {f : E →ₛₗ.[σ] F} (hfx : x ∈ f.domain),
    Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (c • x) ⋯ = c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx
rw :
  (↑f : ↥f.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (c • x) ⋯)
rw₁ :
  (↑f : ↥f.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑g : ↥g.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)
⊢ (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (c • x) ⋯) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (c • x) ⋯)
have rw₂ : HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S)
    ((↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx)) =
  (↑g : ↥g.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)
Tactic: rw [this hfx, this hgx, f.map_smulₛₗ, g.map_smulₛₗ, hx]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst_3 : AddCommGroup E
inst_4 : Module R E
F : Type u_5
inst_5 : AddCommGroup F
inst_6 : Module S F
G : Type u_6
inst_7 : AddCommGroup G
inst_8 : Module T G
f g : E →ₛₗ.[σ] F
c : R
x : E
h :
  Membership.mem (γ := Set E)
    {x : E |
      ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain),
        (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hf) =
          (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hg)}
    x
hfx : x ∈ f.domain
hgx : x ∈ g.domain
hx :
  (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)
this :
  ∀ {f : E →ₛₗ.[σ] F} (hfx : x ∈ f.domain),
    Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (c • x) ⋯ = c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx
rw :
  (↑f : ↥f.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (c • x) ⋯)
rw₁ :
  (↑f : ↥f.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx) =
    (↑g : ↥g.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)
rw₂ :
  HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S)
      ((↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx)) =
    (↑g : ↥g.domain → F) (c • Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx)
⊢ (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (c • x) ⋯) =
    (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) (c • x) ⋯)
have rw₃ : HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S)
    ((↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hfx)) =
  HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S)
    ((↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hgx))
Tactic: rw [this hfx, this hgx, f.map_smulₛₗ, g.map_smulₛₗ, hx]