awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
t_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    (↑s' : Set V) ⊆ s →
      s ∩ (↑t : Set V) = ∅ →
        s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V) →
          ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst_2 : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ (↑t : Set V) = ∅
this : ¬s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃ : b₃ ∈ s
⊢ b₃ ∈ (↑(span K (↑(insert b₂ s' ∪ t) : Set V)) : Set V)
have this₁ : (↑(s' ∪ insert b₁ t) : Set V) ⊆ insert b₁ (insert b₂ (↑(s' ∪ t) : Set V))
Tactic: have : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t) : Set V) := by
            simp only [insert_eq, union_subset_union, Subset.refl,
              subset_union_right, Finset.union_insert, Finset.coe_insert]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
t_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    (↑s' : Set V) ⊆ s →
      s ∩ (↑t : Set V) = ∅ →
        s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V) →
          ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst_2 : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ (↑t : Set V) = ∅
this_1 : ¬s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃ : b₃ ∈ s
this : (↑(s' ∪ insert b₁ t) : Set V) ⊆ insert b₁ (insert b₂ (↑(s' ∪ t) : Set V))
⊢ b₃ ∈ (↑(span K (↑(insert b₂ s' ∪ t) : Set V)) : Set V)
have hb₄ : Membership.mem (γ := Submodule K V) (span K (insert b₁ (insert b₂ (↑(s' ∪ t) : Set V)))) b₃
Tactic: have hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t) : Set V)) :=
            span_mono this (hss' hb₃)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
t_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    (↑s' : Set V) ⊆ s →
      s ∩ (↑t : Set V) = ∅ →
        s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V) →
          ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst_2 : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ (↑t : Set V) = ∅
this_1 : ¬s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃_1 : b₃ ∈ s
this : (↑(s' ∪ insert b₁ t) : Set V) ⊆ insert b₁ (insert b₂ (↑(s' ∪ t) : Set V))
hb₃ : Membership.mem (γ := Submodule K V) (span K (insert b₁ (insert b₂ (↑(s' ∪ t) : Set V)))) b₃
⊢ b₃ ∈ (↑(span K (↑(insert b₂ s' ∪ t) : Set V)) : Set V)
have this₁ : s ⊆ (↑(span K (insert b₁ (↑(s' ∪ t) : Set V))) : Set V)
Tactic: have : s ⊆ (span K (insert b₁ ↑(s' ∪ t)) : Submodule K V) := by
            simpa [insert_eq, -singleton_union, -union_singleton] using hss'
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
t_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    (↑s' : Set V) ⊆ s →
      s ∩ (↑t : Set V) = ∅ →
        s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V) →
          ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst_2 : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ (↑t : Set V) = ∅
this_1 : ¬s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃_1 : b₃ ∈ s
this_2 : (↑(s' ∪ insert b₁ t) : Set V) ⊆ insert b₁ (insert b₂ (↑(s' ∪ t) : Set V))
hb₃ : Membership.mem (γ := Submodule K V) (span K (insert b₁ (insert b₂ (↑(s' ∪ t) : Set V)))) b₃
this : s ⊆ (↑(span K (insert b₁ (↑(s' ∪ t) : Set V))) : Set V)
⊢ b₃ ∈ (↑(span K (↑(insert b₂ s' ∪ t) : Set V)) : Set V)
have hb₁ : Membership.mem (γ := Submodule K V) (span K (insert b₂ (↑(s' ∪ t) : Set V))) b₁
Tactic: have hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t)) :=
            mem_span_insert_exchange (this hb₂s) hb₂t
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
t_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    (↑s' : Set V) ⊆ s →
      s ∩ (↑t : Set V) = ∅ →
        s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V) →
          ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst_2 : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ (↑t : Set V) = ∅
this_1 : ¬s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃_1 : b₃ ∈ s
this_2 : (↑(s' ∪ insert b₁ t) : Set V) ⊆ insert b₁ (insert b₂ (↑(s' ∪ t) : Set V))
hb₃ : Membership.mem (γ := Submodule K V) (span K (insert b₁ (insert b₂ (↑(s' ∪ t) : Set V)))) b₃
this : s ⊆ (↑(span K (insert b₁ (↑(s' ∪ t) : Set V))) : Set V)
hb₁ : Membership.mem (γ := Submodule K V) (span K (insert b₂ (↑(s' ∪ t) : Set V))) b₁
⊢ b₃ ∈ (↑(span K (↑(insert b₂ s' ∪ t) : Set V)) : Set V)
have hb₄ : Membership.mem (γ := Submodule K V) (span K (insert b₂ (↑(s' ∪ t) : Set V))) b₃
Tactic: rw [span_insert_eq_span hb₁] at hb₃
Cleared hypotheses: hb₃, this, hb₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ (↑(span K (↑t : Set V)) : Set V)
⊢ ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = t.card
have this : ∀ (t s' : Finset V),
  (↑s' : Set V) ⊆ s →
    s ∩ (↑t : Set V) = ∅ →
      s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V) →
        ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = (s' ∪ t).card
Tactic: have :
    ∀ t : Finset V,
      ∀ s' : Finset V,
        ↑s' ⊆ s →
          s ∩ ↑t = ∅ →
            s ⊆ (span K ↑(s' ∪ t) : Submodule K V) →
              ∃ t' : Finset V, ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card :=
    fun t =>
    Finset.induction_on t
      (fun s' hs' _ hss' =>
        have : s = ↑s' := eq_of_linearIndepOn_id_of_span_subtype hs hs' <| by simpa using hss'
        ⟨s', by simp [this]⟩)
      fun b₁ t hb₁t ih s' hs' hst hss' =>
      have hb₁s : b₁ ∉ s := fun h => by
        have : b₁ ∈ s ∩ ↑(insert b₁ t) := ⟨h, Finset.mem_insert_self _ _⟩
        rwa [hst] at this
      have hb₁s' : b₁ ∉ s' := fun h => hb₁s <| hs' h
      have hst : s ∩ ↑t = ∅ :=
        eq_empty_of_subset_empty <|
          -- Porting note: `-subset_inter_iff` required.
          Subset.trans
            (by simp [inter_subset_inter, -subset_inter_iff])
            (le_of_eq hst)
      Classical.by_cases (p := s ⊆ (span K ↑(s' ∪ t) : Submodule K V))
        (fun this =>
          let ⟨u, hust, hsu, Eq⟩ := ih _ hs' hst this
          have hb₁u : b₁ ∉ u := fun h => (hust h).elim hb₁s hb₁t
          ⟨insert b₁ u, by simp [insert_subset_insert hust], Subset.trans hsu (by simp), by
            simp [Eq, hb₁t, hb₁s', hb₁u]⟩)
        fun this =>
        let ⟨b₂, hb₂s, hb₂t⟩ := not_subset.mp this
        have hb₂t' : b₂ ∉ s' ∪ t := fun h => hb₂t <| subset_span h
        have : s ⊆ (span K ↑(insert b₂ s' ∪ t) : Submodule K V) := fun b₃ hb₃ => by
          have : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t) : Set V) := by
            simp only [insert_eq, union_subset_union, Subset.refl,
              subset_union_right, Finset.union_insert, Finset.coe_insert]
          have hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t) : Set V)) :=
            span_mono this (hss' hb₃)
          have : s ⊆ (span K (insert b₁ ↑(s' ∪ t)) : Submodule K V) := by
            simpa [insert_eq, -singleton_union, -union_singleton] using hss'
          have hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t)) :=
            mem_span_insert_exchange (this hb₂s) hb₂t
          rw [span_insert_eq_span hb₁] at hb₃; simpa using hb₃
        let ⟨u, hust, hsu, eq⟩ := ih _ (by simp [insert_subset_iff, hb₂s, hs']) hst this
        ⟨u, Subset.trans hust <| union_subset_union (Subset.refl _) (by simp [subset_insert]), hsu,
          by simp [eq, hb₂t', hb₁t, hb₁s']⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ (↑(span K (↑t : Set V)) : Set V)
this :
  ∀ (t s' : Finset V),
    (↑s' : Set V) ⊆ s →
      s ∩ (↑t : Set V) = ∅ →
        s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V) →
          ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = (s' ∪ t).card
⊢ {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} = t
have h : ∀ (x : V), x ∈ {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} ↔ x ∈ t
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ (↑(span K (↑t : Set V)) : Set V)
this :
  ∀ (t s' : Finset V),
    (↑s' : Set V) ⊆ s →
      s ∩ (↑t : Set V) = ∅ →
        s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V) →
          ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = (s' ∪ t).card
x : V
⊢ x ∈ {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} ↔ x ∈ t
have pos : x ∈ s → (x ∈ {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} ↔ x ∈ t)
Tactic: by_cases x ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ (↑(span K (↑t : Set V)) : Set V)
this :
  ∀ (t s' : Finset V),
    (↑s' : Set V) ⊆ s →
      s ∩ (↑t : Set V) = ∅ →
        s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V) →
          ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = (s' ∪ t).card
x : V
pos : x ∈ s → (x ∈ {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} ↔ x ∈ t)
⊢ x ∈ {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} ↔ x ∈ t
have neg : x ∉ s → (x ∈ {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} ↔ x ∈ t)
Tactic: by_cases x ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ (↑(span K (↑t : Set V)) : Set V)
this :
  ∀ (t s' : Finset V),
    (↑s' : Set V) ⊆ s →
      s ∩ (↑t : Set V) = ∅ →
        s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V) →
          ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = (s' ∪ t).card
⊢ ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = t.card
have eq : {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} = t
Tactic: have eq : ((t.filter fun x => x ∈ s) ∪ t.filter fun x => x ∉ s) = t := by
    ext1 x
    by_cases x ∈ s <;> simp [*]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ (↑(span K (↑t : Set V)) : Set V)
this :
  ∀ (t s' : Finset V),
    (↑s' : Set V) ⊆ s →
      s ∩ (↑t : Set V) = ∅ →
        s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V) →
          ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = (s' ∪ t).card
eq : {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} = t
⊢ ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = t.card
have fun : ∀ (a : Finset V),
  (↑a : Set V) ⊆ s ∪ (↑({x ∈ t | x ∉ s}) : Set V) ∧
      s ⊆ (↑a : Set V) ∧ a.card = ({x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s}).card →
    ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = t.card
Tactic: apply
    Exists.elim
      (this (t.filter fun x => x ∉ s) (t.filter fun x => x ∈ s) (by simp [Set.subset_def])
        (by simp +contextual [Set.ext_iff]) (by rwa [eq]))
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s t : Set V
ht : t.Finite
hs : LinearIndepOn K id s
hst : s ⊆ (↑(span K t) : Set V)
this_1 : s ⊆ (↑(span K (↑(ht.toFinset (s := t)) : Set V)) : Set V)
u : Finset V
_hust : (↑u : Set V) ⊆ s ∪ (↑(ht.toFinset (s := t)) : Set V)
hsu : s ⊆ (↑u : Set V)
Eq : u.card = ht.toFinset (s := t).card
this : s.Finite
⊢ this.toFinset (s := s).card ≤ ht.toFinset (s := t).card
have rw : this.toFinset (s := s).card ≤ u.card
Tactic: rw [← Eq]
-- 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
f g : E →ₛₗ.[σ] F
h : f.domain = g.domain
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)
⊢ f = g
have rcases : ∀ (f_dom : Submodule R E) (f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥f_dom) F)
  (h : { domain := f_dom, toFun := f : E →ₛₗ.[σ] F }.domain = g.domain)
  (h' :
    ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f : E →ₛₗ.[σ] F }.domain⦄ ⦃hg : x ∈ g.domain⦄,
      (↑{ domain := f_dom, toFun := f : E →ₛₗ.[σ] F } : ↥{ domain := f_dom, toFun := f }.domain → F)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ { domain := f_dom, toFun := f : E →ₛₗ.[σ] F }.domain) x hf) =
        (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hg)),
  { domain := f_dom, toFun := f : E →ₛₗ.[σ] F } = g
Tactic: rcases f with ⟨f_dom, f⟩
Cleared hypotheses: f, h, 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
g : E →ₛₗ.[σ] F
f_dom : Submodule R E
f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥f_dom) F
h : { domain := f_dom, toFun := f : E →ₛₗ.[σ] F }.domain = g.domain
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f : E →ₛₗ.[σ] F }.domain⦄ ⦃hg : x ∈ g.domain⦄,
    (↑{ domain := f_dom, toFun := f : E →ₛₗ.[σ] F } : ↥{ domain := f_dom, toFun := f }.domain → F)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ { domain := f_dom, toFun := f : E →ₛₗ.[σ] F }.domain) x hf) =
      (↑g : ↥g.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ g.domain) x hg)
⊢ { domain := f_dom, toFun := f : E →ₛₗ.[σ] F } = g
have rcases : ∀ (g_dom : Submodule R E) (g : LinearMap.{u_1, u_2, u_4, u_5} σ (↥g_dom) F)
  (h : { domain := f_dom, toFun := f : E →ₛₗ.[σ] F }.domain = { domain := g_dom, toFun := g : E →ₛₗ.[σ] F }.domain)
  (h' :
    ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f : E →ₛₗ.[σ] F }.domain⦄
      ⦃hg : x ∈ { domain := g_dom, toFun := g : E →ₛₗ.[σ] F }.domain⦄,
      (↑{ domain := f_dom, toFun := f : E →ₛₗ.[σ] F } : ↥{ domain := f_dom, toFun := f }.domain → F)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ { domain := f_dom, toFun := f : E →ₛₗ.[σ] F }.domain) x hf) =
        (↑{ domain := g_dom, toFun := g : E →ₛₗ.[σ] F } : ↥{ domain := g_dom, toFun := g }.domain → F)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ { domain := g_dom, toFun := g : E →ₛₗ.[σ] F }.domain) x hg)),
  { domain := f_dom, toFun := f : E →ₛₗ.[σ] F } = { domain := g_dom, toFun := g }
Tactic: rcases g with ⟨g_dom, g⟩
Cleared hypotheses: g, h, 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
f_dom : Submodule R E
f : LinearMap.{u_1, u_2, u_4, u_5} σ (↥f_dom) F
g_dom : Submodule R E
g : LinearMap.{u_1, u_2, u_4, u_5} σ (↥g_dom) F
h : { domain := f_dom, toFun := f : E →ₛₗ.[σ] F }.domain = { domain := g_dom, toFun := g : E →ₛₗ.[σ] F }.domain
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f : E →ₛₗ.[σ] F }.domain⦄
    ⦃hg : x ∈ { domain := g_dom, toFun := g : E →ₛₗ.[σ] F }.domain⦄,
    (↑{ domain := f_dom, toFun := f : E →ₛₗ.[σ] F } : ↥{ domain := f_dom, toFun := f }.domain → F)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ { domain := f_dom, toFun := f : E →ₛₗ.[σ] F }.domain) x hf) =
      (↑{ domain := g_dom, toFun := g : E →ₛₗ.[σ] F } : ↥{ domain := g_dom, toFun := g }.domain → F)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ { domain := g_dom, toFun := g : E →ₛₗ.[σ] F }.domain) x hg)
⊢ { domain := f_dom, toFun := f : E →ₛₗ.[σ] F } = { domain := g_dom, toFun := g }
have obtain : ∀ (g : LinearMap.{u_1, u_2, u_4, u_5} σ (↥f_dom) F)
  (h' :
    ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f : E →ₛₗ.[σ] F }.domain⦄
      ⦃hg : x ∈ { domain := f_dom, toFun := g : E →ₛₗ.[σ] F }.domain⦄,
      (↑{ domain := f_dom, toFun := f : E →ₛₗ.[σ] F } : ↥{ domain := f_dom, toFun := f }.domain → F)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ { domain := f_dom, toFun := f : E →ₛₗ.[σ] F }.domain) x hf) =
        (↑{ domain := f_dom, toFun := g : E →ₛₗ.[σ] F } : ↥{ domain := f_dom, toFun := g }.domain → F)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ { domain := f_dom, toFun := g : E →ₛₗ.[σ] F }.domain) x hg)),
  { domain := f_dom, toFun := f : E →ₛₗ.[σ] F } = { domain := f_dom, toFun := g }
Tactic: obtain rfl : f_dom = g_dom := h
Cleared hypotheses: g_dom, g, h, 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
f_dom : Submodule R E
f g : LinearMap.{u_1, u_2, u_4, u_5} σ (↥f_dom) F
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f : E →ₛₗ.[σ] F }.domain⦄
    ⦃hg : x ∈ { domain := f_dom, toFun := g : E →ₛₗ.[σ] F }.domain⦄,
    (↑{ domain := f_dom, toFun := f : E →ₛₗ.[σ] F } : ↥{ domain := f_dom, toFun := f }.domain → F)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ { domain := f_dom, toFun := f : E →ₛₗ.[σ] F }.domain) x hf) =
      (↑{ domain := f_dom, toFun := g : E →ₛₗ.[σ] F } : ↥{ domain := f_dom, toFun := g }.domain → F)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ { domain := f_dom, toFun := g : E →ₛₗ.[σ] F }.domain) x hg)
⊢ { domain := f_dom, toFun := f : E →ₛₗ.[σ] F } = { domain := f_dom, toFun := g }
have e_toFun : f = g
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
f_dom : Submodule R E
f g : LinearMap.{u_1, u_2, u_4, u_5} σ (↥f_dom) F
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f : E →ₛₗ.[σ] F }.domain⦄
    ⦃hg : x ∈ { domain := f_dom, toFun := g : E →ₛₗ.[σ] F }.domain⦄,
    (↑{ domain := f_dom, toFun := f : E →ₛₗ.[σ] F } : ↥{ domain := f_dom, toFun := f }.domain → F)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ { domain := f_dom, toFun := f : E →ₛₗ.[σ] F }.domain) x hf) =
      (↑{ domain := f_dom, toFun := g : E →ₛₗ.[σ] F } : ↥{ domain := f_dom, toFun := g }.domain → F)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ { domain := f_dom, toFun := g : E →ₛₗ.[σ] F }.domain) x hg)
⊢ f = g
have e_toFun : ∀ (x : ↥f_dom), Eq.{u_5 + 1} (α := F) ((f : (a : ↥f_dom) → F) x : F) ((g : (a : ↥f_dom) → F) x : F)
Tactic: apply LinearMap.ext
-- 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
f g : E →ₛₗ.[σ] F
EQ : f = g
x y : ↥f.domain
h : (↑x : E) = (↑y : E)
⊢ (↑f : ↥f.domain → F) x = (↑f : ↥f.domain → F) y
have e_a : x = y
Tactic: congr
-- 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 : ∀ (c : R), c • x = 0 → HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) c : S) y = 0
c₁ c₂ : R
h : 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
have rw : ∀ (h : (c₁ - c₂) • x = 0), HSub.hSub (α := S) (β := S) ((σ : (a : R) → S) c₁ : S) ((σ : (a : R) → S) c₂ : S) • y = 0
Tactic: rw [← sub_eq_zero, ← sub_smul] at h ⊢
Cleared hypotheses: 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
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₁ c₂ : R
h : (c₁ - c₂) • x = 0
⊢ HSub.hSub (α := S) (β := S) ((σ : (a : R) → S) c₁ : S) ((σ : (a : R) → S) c₂ : S) • y = 0
have rw : HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((σ : (a : R) → S) (c₁ - c₂) : S) y = 0
Tactic: rw [← RingHom.map_sub]