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
f : E →ₛₗ.[σ] F
⊢ f + 0 = f
have h : ∀ (x : E), x ∈ (f + 0).domain ↔ x ∈ f.domain
Tactic: ext x y hxy
-- 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 : E →ₛₗ.[σ] F
h : ∀ (x : E), x ∈ (f + 0).domain ↔ x ∈ f.domain
⊢ f + 0 = f
have h' : ∀ ⦃x : E⦄ ⦃y : x ∈ (f + 0).domain⦄ ⦃hxy : x ∈ f.domain⦄,
  (↑(f + 0) : ↥(f + 0).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + 0).domain) x y) =
    (↑f : ↥f.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hxy)
Tactic: ext x y hxy
-- 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
⊢ f + g = g + f
have h : ∀ (x : E), x ∈ (f + g).domain ↔ x ∈ (g + f).domain
Tactic: ext x y hxy
-- 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
h : ∀ (x : E), x ∈ (f + g).domain ↔ x ∈ (g + f).domain
⊢ f + g = g + f
have h' : ∀ ⦃x : E⦄ ⦃y : x ∈ (f + g).domain⦄ ⦃hxy : x ∈ (g + f).domain⦄,
  (↑(f + g) : ↥(f + g).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + g).domain) x y) =
    (↑(g + f) : ↥(g + f).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (g + f).domain) x hxy)
Tactic: ext x y hxy
-- 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
⊢ f - g = f + -g
have h : ∀ (x : E), x ∈ (f - g).domain ↔ x ∈ (f + -g).domain
Tactic: ext x _ h
-- 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
h : ∀ (x : E), x ∈ (f - g).domain ↔ x ∈ (f + -g).domain
⊢ f - g = f + -g
have h' : ∀ ⦃x : E⦄ ⦃hf : x ∈ (f - g).domain⦄ ⦃h : x ∈ (f + -g).domain⦄,
  (↑(f - g) : ↥(f - g).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f - g).domain) x hf) =
    (↑(f + -g) : ↥(f + -g).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + -g).domain) x h)
Tactic: ext x _ h
-- 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
⊢ -(f + g) = -g + -f
have h : ∀ (x : E), x ∈ (-(f + g)).domain ↔ x ∈ (-g + -f).domain
Tactic: ext x _ h
-- 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
h : ∀ (x : E), x ∈ (-(f + g)).domain ↔ x ∈ (-g + -f).domain
⊢ -(f + g) = -g + -f
have h' : ∀ ⦃x : E⦄ ⦃hf : x ∈ (-(f + g)).domain⦄ ⦃h : x ∈ (-g + -f).domain⦄,
  (↑(-(f + g)) : ↥(-(f + g)).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (-(f + g)).domain) x hf) =
    (↑(-g + -f) : ↥(-g + -f).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (-g + -f).domain) x h)
Tactic: ext x _ h
-- 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
h' : f + g = 0
⊢ -f = g
have h : ∀ (x : E), x ∈ (-f).domain ↔ x ∈ g.domain
Tactic: ext x hf hg
-- 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
h' : f + g = 0
h : ∀ (x : E), x ∈ (-f).domain ↔ x ∈ g.domain
⊢ -f = g
have h'₁ : ∀ ⦃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)
Tactic: ext x hf hg
-- 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
h' : f + g = 0
x : E
⊢ x ∈ (-f).domain ↔ x ∈ g.domain
have this : Eq.{u_4 + 1} (α := Submodule R E) (domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0) ⊤
Tactic: have : (0 : E →ₛₗ.[σ] F).domain = ⊤ := zero_domain
-- 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
h' : f + g = 0
x : E
this : Eq.{u_4 + 1} (α := Submodule R E) (domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0) ⊤
⊢ x ∈ (-f).domain ↔ x ∈ g.domain
have this₁ : f.domain = ⊤ ∧ g.domain = ⊤
Tactic: simp only [← h', add_domain, inf_eq_top_iff] at this
Cleared hypotheses: this
-- 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
h' : f + g = 0
x : E
this : f.domain = ⊤ ∧ g.domain = ⊤
⊢ x ∈ (-f).domain ↔ x ∈ g.domain
have h : x ∈ f.domain ↔ x ∈ g.domain
Tactic: rw [neg_domain, this.1, this.2]
-- 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
h' : f + g = 0
x : E
this : f.domain = ⊤ ∧ g.domain = ⊤
h : x ∈ f.domain ↔ x ∈ g.domain
⊢ x ∈ (-f).domain ↔ x ∈ g.domain
have h₁ : Membership.mem (γ := Submodule R E) ⊤ x ↔ x ∈ g.domain
Tactic: rw [neg_domain, this.1, this.2]
-- 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
h' : f + g = 0
x : E
this : f.domain = ⊤ ∧ g.domain = ⊤
h : x ∈ f.domain ↔ x ∈ g.domain
h₁ : Membership.mem (γ := Submodule R E) ⊤ x ↔ x ∈ g.domain
⊢ x ∈ (-f).domain ↔ x ∈ g.domain
have h₂ : Membership.mem (γ := Submodule R E) ⊤ x ↔ Membership.mem (γ := Submodule R E) ⊤ x
Tactic: rw [neg_domain, this.1, this.2]
-- 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
h' : f + g = 0
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)
have h'₁ : (↑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) =
  0
Tactic: simp only [neg_domain, neg_apply, neg_eq_iff_add_eq_zero]
-- 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
h' : f + g = 0
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) =
    0
have h'₁ : ∀
  (h' :
    (f + g).domain = domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0 ∧
      ∀ ⦃x : E⦄ ⦃hf : x ∈ (f + g).domain⦄
        ⦃hg : Membership.mem (γ := Submodule R E) (domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0) x⦄,
        (↑(f + g) : ↥(f + g).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + g).domain) x hf) =
          (↑0 : ↥(domain 0) → F)
            (Subtype.mk (p := fun (x : E) ↦
              Membership.mem (γ := Submodule R E) (domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0) x) x hg))
  ⦃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) =
    0
Tactic: rw [ext_iff] at h'
Cleared hypotheses: h', x, hf, hg
-- 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
h' :
  (f + g).domain = domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0 ∧
    ∀ ⦃x : E⦄ ⦃hf : x ∈ (f + g).domain⦄
      ⦃hg : Membership.mem (γ := Submodule R E) (domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0) x⦄,
      (↑(f + g) : ↥(f + g).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + g).domain) x hf) =
        (↑0 : ↥(domain 0) → F)
          (Subtype.mk (p := fun (x : E) ↦
            Membership.mem (γ := Submodule R E) (domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0) x) x hg)
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) =
    0
have hdom : (f + g).domain = domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0
Tactic: rcases h' with ⟨hdom, h'⟩
Cleared hypotheses: 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
f g : E →ₛₗ.[σ] F
h' :
  (f + g).domain = domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0 ∧
    ∀ ⦃x : E⦄ ⦃hf : x ∈ (f + g).domain⦄
      ⦃hg : Membership.mem (γ := Submodule R E) (domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0) x⦄,
      (↑(f + g) : ↥(f + g).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + g).domain) x hf) =
        (↑0 : ↥(domain 0) → F)
          (Subtype.mk (p := fun (x : E) ↦
            Membership.mem (γ := Submodule R E) (domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0) x) x hg)
x : E
hf : x ∈ (-f).domain
hg : x ∈ g.domain
hdom : (f + g).domain = domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0
⊢ (↑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) =
    0
have h'₁ : ∀ ⦃x : E⦄ ⦃hf : x ∈ (f + g).domain⦄
  ⦃hg : Membership.mem (γ := Submodule R E) (domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0) x⦄,
  (↑(f + g) : ↥(f + g).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + g).domain) x hf) =
    (↑0 : ↥(domain 0) → F)
      (Subtype.mk (p := fun (x : E) ↦
        Membership.mem (γ := Submodule R E) (domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0) x) x hg)
Tactic: rcases h' with ⟨hdom, h'⟩
Cleared hypotheses: 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
f g : E →ₛₗ.[σ] F
x : E
hf : x ∈ (-f).domain
hg : x ∈ g.domain
hdom : (f + g).domain = domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ (f + g).domain⦄
    ⦃hg : Membership.mem (γ := Submodule R E) (domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0) x⦄,
    (↑(f + g) : ↥(f + g).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + g).domain) x hf) =
      (↑0 : ↥(domain 0) → F)
        (Subtype.mk (p := fun (x : E) ↦
          Membership.mem (γ := Submodule R E) (domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0) x) x hg)
⊢ (↑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) =
    0
have hdom₁ : (f + g).domain = ⊤
Tactic: rw [zero_domain] at hdom
Cleared hypotheses: hdom, 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
f g : E →ₛₗ.[σ] F
x : E
hf : x ∈ (-f).domain
hg : x ∈ g.domain
hdom : (f + g).domain = ⊤
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ (f + g).domain⦄
    ⦃hg : Membership.mem (γ := Submodule R E) (domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0) x⦄,
    (↑(f + g) : ↥(f + g).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + g).domain) x hf) =
      (↑0 : ↥(domain 0) → F)
        (Subtype.mk (p := fun (x : E) ↦
          Membership.mem (γ := Submodule R E) (domain.{u_1, u_2, u_4, u_5} (S := S) (σ := σ) (F := F) 0) x) x hg)
⊢ (↑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) =
    0
have h'₁ : ∀ ⦃x : E⦄, (↑(f + g) : ↥(f + g).domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ (f + g).domain) x sorry) = 0
Tactic: simp only [hdom, zero_domain, mem_top, zero_apply, forall_true_left] at h'
Cleared hypotheses: 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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) ↦ x1 ≤ x2) c
⊢ ∃ (f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F),
    { domain := sSup (domain '' c), toFun := f : E →ₛₗ.[σ] F } ∈ upperBounds c
have inl : ∀ (hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) ↦ x1 ≤ x2) ∅),
  ∃ (f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (Set.image (α := E →ₛₗ.[σ] F) domain ∅))) F),
    Membership.mem (γ := Set (E →ₛₗ.[σ] F)) (upperBounds ∅)
      { domain := sSup (Set.image (α := E →ₛₗ.[σ] F) domain ∅), toFun := f : E →ₛₗ.[σ] F }
Tactic: rcases c.eq_empty_or_nonempty with rfl | cne
Cleared hypotheses: c, hc
-- 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
inl :
  ∀ (hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) ↦ x1 ≤ x2) ∅),
    ∃ (f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (Set.image (α := E →ₛₗ.[σ] F) domain ∅))) F),
      Membership.mem (γ := Set (E →ₛₗ.[σ] F)) (upperBounds ∅)
        { domain := sSup (Set.image (α := E →ₛₗ.[σ] F) domain ∅), toFun := f : E →ₛₗ.[σ] F }
⊢ ∃ (f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F),
    { domain := sSup (domain '' c), toFun := f : E →ₛₗ.[σ] F } ∈ upperBounds c
have inr : ∀ (cne : c.Nonempty),
  ∃ (f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F),
    { domain := sSup (domain '' c), toFun := f : E →ₛₗ.[σ] F } ∈ upperBounds c
Tactic: rcases c.eq_empty_or_nonempty with rfl | cne
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (hypothesis)
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
cne : c.Nonempty
⊢ ∃ (f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥(sSup (domain '' c))) F),
    { domain := sSup (domain '' c), toFun := f : E →ₛₗ.[σ] F } ∈ upperBounds c
have hdir : DirectedOn (fun (x1 x2 : Submodule R E) ↦ x1 ≤ x2) (domain '' c)
Tactic: have hdir : DirectedOn (· ≤ ·) (domain '' c) :=
    directedOn_image.2 (hc.mono @(domain_mono.monotone))
-- 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
cne : c.Nonempty
hdir : DirectedOn (fun (x1 x2 : Submodule R E) ↦ x1 ≤ x2) (domain '' c)
x : ↥(sSup (domain '' c))
⊢ { p : (↑c : Type (max u_4 u_5)) // (↑x : E) ∈ (↑p : E →ₛₗ.[σ] F).domain }
have h : ∃ (x_1 : (↑c : Type (max u_4 u_5))), (↑x : E) ∈ (↑x_1 : E →ₛₗ.[σ] F).domain
Tactic: apply Classical.indefiniteDescription
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearPMap (hypothesis)
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
cne : c.Nonempty
hdir : DirectedOn (fun (x1 x2 : Submodule R E) ↦ x1 ≤ x2) (domain '' c)
x : ↥(sSup (domain '' c))
⊢ ∃ (x_1 : (↑c : Type (max u_4 u_5))), (↑x : E) ∈ (↑x_1 : E →ₛₗ.[σ] F).domain
have this : ∃ y ∈ domain '' c, (↑x : E) ∈ y
Tactic: have := (mem_sSup_of_directed (cne.image _) hdir).1 x.2
-- 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
cne : c.Nonempty
hdir : DirectedOn (fun (x1 x2 : Submodule R E) ↦ x1 ≤ x2) (domain '' c)
x : ↥(sSup (domain '' c))
this : ∃ y ∈ domain '' c, (↑x : E) ∈ y
⊢ ∃ (x_1 : (↑c : Type (max u_4 u_5))), (↑x : E) ∈ (↑x_1 : E →ₛₗ.[σ] F).domain
have h : ∀ (this : ∃ x_1 ∈ c, (↑x : E) ∈ x_1.domain), ∃ (x_1 : (↑c : Type (max u_4 u_5))), (↑x : E) ∈ (↑x_1 : E →ₛₗ.[σ] F).domain
Tactic: rwa [Set.exists_mem_image, ← bex_def, SetCoe.exists'] at this
Cleared hypotheses: 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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun (x1 x2 : Submodule R E) ↦ x1 ≤ x2) (domain '' c)
x : ↥(sSup (domain '' c))
this : ∃ y ∈ domain '' c, (↑x : E) ∈ y
h :
  ∀ (this : ∃ x_1 ∈ c, (↑x : E) ∈ x_1.domain),
    ∃ (x_1 : (↑c : Type (max u_4 u_5))), (↑x : E) ∈ (↑x_1 : E →ₛₗ.[σ] F).domain
⊢ ∃ (x_1 : (↑c : Type (max u_4 u_5))), (↑x : E) ∈ (↑x_1 : E →ₛₗ.[σ] F).domain
have h₁ : ∀ (this : ∃ (x_1 : E →ₛₗ.[σ] F) (_ : x_1 ∈ c), (↑x : E) ∈ x_1.domain),
  ∃ (x_1 : (↑c : Type (max u_4 u_5))), (↑x : E) ∈ (↑x_1 : E →ₛₗ.[σ] F).domain
Tactic: rwa [Set.exists_mem_image, ← bex_def, SetCoe.exists'] at this
Cleared hypotheses: 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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun (x1 x2 : E →ₛₗ.[σ] F) ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun (x1 x2 : Submodule R E) ↦ x1 ≤ x2) (domain '' c)
x : ↥(sSup (domain '' c))
this : ∃ y ∈ domain '' c, (↑x : E) ∈ y
h :
  ∀ (this : ∃ x_1 ∈ c, (↑x : E) ∈ x_1.domain),
    ∃ (x_1 : (↑c : Type (max u_4 u_5))), (↑x : E) ∈ (↑x_1 : E →ₛₗ.[σ] F).domain
h₁ :
  ∀ (this : ∃ (x_1 : E →ₛₗ.[σ] F) (_ : x_1 ∈ c), (↑x : E) ∈ x_1.domain),
    ∃ (x_1 : (↑c : Type (max u_4 u_5))), (↑x : E) ∈ (↑x_1 : E →ₛₗ.[σ] F).domain
⊢ ∃ (x_1 : (↑c : Type (max u_4 u_5))), (↑x : E) ∈ (↑x_1 : E →ₛₗ.[σ] F).domain
have h₂ : ∀ (this : ∃ (x_1 : (↑c : Type (max u_4 u_5))), (↑x : E) ∈ (↑x_1 : E →ₛₗ.[σ] F).domain),
  ∃ (x_1 : (↑c : Type (max u_4 u_5))), (↑x : E) ∈ (↑x_1 : E →ₛₗ.[σ] F).domain
Tactic: rwa [Set.exists_mem_image, ← bex_def, SetCoe.exists'] at this
Cleared hypotheses: this