awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Bilinear (goal)
Goal:
ι₁ : Type u_1
ι₂ : Type u_2
Rₗ : Type u_10
Mₗ : Type u_11
Nₗ : Type u_12
Pₗ : Type u_13
inst : CommSemiring Rₗ
inst_1 : AddCommMonoid Mₗ
inst_2 : AddCommMonoid Nₗ
inst_3 : AddCommMonoid Pₗ
inst_4 : Module Rₗ Mₗ
inst_5 : Module Rₗ Nₗ
inst_6 : Module Rₗ Pₗ
b₁' : Basis ι₁ Rₗ Mₗ
b₂' : Basis ι₂ Rₗ Nₗ
B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ
x : Mₗ
y : Nₗ
⊢ Eq.{u_13 + 1} (α := Pₗ)
    (Finsupp.sum ((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x) fun (i : ι₁) (xi : Rₗ) ↦
        Finsupp.sum ((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y) fun (j : ι₂) (yj : Rₗ) ↦
          xi •
            HSMul.hSMul (β := Pₗ) yj
              ((((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ) ((b₁' : (a : ι₁) → Mₗ) i) : Nₗ →ₗ[Rₗ] Pₗ) : (a : Nₗ) → Pₗ)
                  ((b₂' : (a : ι₂) → Nₗ) j : Nₗ) :
                Pₗ) :
      Pₗ)
    ((((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ)
              ((Finsupp.linearCombination Rₗ (⇑b₁' : (a : ι₁) → Mₗ) : (a : ι₁ →₀ Rₗ) → Mₗ)
                ((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x : ι₁ →₀ Rₗ)) :
            Nₗ →ₗ[Rₗ] Pₗ) :
          (a : Nₗ) → Pₗ)
        ((Finsupp.linearCombination Rₗ (⇑b₂' : (a : ι₂) → Nₗ) : (a : ι₂ →₀ Rₗ) → Nₗ)
            ((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y : ι₂ →₀ Rₗ) :
          Nₗ) :
      Pₗ)
have simp_rw : Eq.{u_13 + 1} (α := Pₗ)
  (Finsupp.sum ((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x) fun (i : ι₁) (xi : Rₗ) ↦
      Finsupp.sum ((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y) fun (j : ι₂) (yj : Rₗ) ↦
        xi •
          HSMul.hSMul (β := Pₗ) yj
            ((((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ) ((b₁' : (a : ι₁) → Mₗ) i) : Nₗ →ₗ[Rₗ] Pₗ) : (a : Nₗ) → Pₗ)
                ((b₂' : (a : ι₂) → Nₗ) j : Nₗ) :
              Pₗ) :
    Pₗ)
  (((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ)
          (Finsupp.sum ((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x) fun (i : ι₁) (a : Rₗ) ↦
            HSMul.hSMul (β := Mₗ) a ((b₁' : (a : ι₁) → Mₗ) i : Mₗ)) :
        (a : Nₗ) → Pₗ)
      (Finsupp.sum ((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y) fun (i : ι₂) (a : Rₗ) ↦
        HSMul.hSMul (β := Nₗ) a ((b₂' : (a : ι₂) → Nₗ) i : Nₗ)) :
    Pₗ)
Tactic: simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum₂, map_sum, map_smul₂, map_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s : Set M
hs : s.Finite
hsspan : Eq (α := Submodule R M) (span R s) ⊤
ι : Type w
b : Basis ι R M
⊢ Finite ι
have this : Submodule.map (↑b.repr : M →ₗ[R] ι →₀ R) (span R s) = Submodule.map (↑b.repr : M →ₗ[R] ι →₀ R) ⊤
Tactic: have := congr(($hsspan).map b.repr.toLinearMap)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
s : Set M
hs : s.Finite
hsspan : Eq (α := Submodule R M) (span R s) ⊤
ι : Type w
b : Basis ι R M
this : Submodule.map (↑b.repr : M →ₗ[R] ι →₀ R) (span R s) = Submodule.map (↑b.repr : M →ₗ[R] ι →₀ R) ⊤
⊢ Finite ι
have this₁ : Eq (α := Submodule R (ι →₀ R)) (span R ((⇑(↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ R) '' s)) ⊤
Tactic: rw [← span_image, Submodule.map_top, LinearEquiv.range] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Nontrivial R
inst_3 : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
⊢ Eq.{w + 1} (α := Set ι) (⋃ (k : κ), (↑(support.{w, u} (M := R) ((b.repr : (a : M) → ι →₀ R) (v k))) : Set ι)) Set.univ
have by_contra : ∀
  (h :
    ¬Eq.{w + 1} (α := Set ι) (⋃ (k : κ), (↑(support.{w, u} (M := R) ((b.repr : (a : M) → ι →₀ R) (v k))) : Set ι))
        Set.univ),
  False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Nontrivial R
inst_3 : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
h :
  ¬Eq.{w + 1} (α := Set ι) (⋃ (k : κ), (↑(support.{w, u} (M := R) ((b.repr : (a : M) → ι →₀ R) (v k))) : Set ι))
      Set.univ
⊢ False
have h₁ : ∃ (a : ι), ∀ (x : κ), Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) (v x) : ι →₀ R) : (a : ι) → R) a : R) (0 : R)
Tactic: simp only [← Ne.eq_def, ne_univ_iff_exists_notMem, mem_iUnion, not_exists_not,
    Finsupp.mem_support_iff, Finset.mem_coe] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Nontrivial R
inst_3 : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
h :
  ∃ (a : ι), ∀ (x : κ), Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) (v x) : ι →₀ R) : (a : ι) → R) a : R) (0 : R)
⊢ False
have obtain : ∀ (i : ι)
  (w : ∀ (x : κ), Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) (v x) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)),
  False
Tactic: obtain ⟨i, w⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Nontrivial R
inst_3 : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) (v x) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
⊢ False
have repr_eq_zero : ∀ (l : κ →₀ R),
  Eq.{u + 1} (α := R)
    ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l) : ι →₀ R) : (a : ι) → R) i : R)
    (0 : R)
Tactic: have repr_eq_zero (l) : b.repr (linearCombination R v l) i = 0 := by
    simp [linearCombination_apply, Finsupp.sum, w]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Nontrivial R
inst_3 : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) (v x) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
repr_eq_zero :
  ∀ (l : κ →₀ R),
    Eq.{u + 1} (α := R)
      ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l) : ι →₀ R) : (a : ι) → R) i : R)
      (0 : R)
v' : (o : Option κ) → M := fun (o : Option κ) ↦ o.elim ((b : (a : ι) → M) i) v
⊢ False
have r : range v ⊆ range v'
Tactic: have r : range v ⊆ range v' := by rintro - ⟨k, rfl⟩; exact ⟨some k, rfl⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Nontrivial R
inst_3 : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) (v x) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
repr_eq_zero :
  ∀ (l : κ →₀ R),
    Eq.{u + 1} (α := R)
      ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l) : ι →₀ R) : (a : ι) → R) i : R)
      (0 : R)
v' : (o : Option κ) → M := fun (o : Option κ) ↦ o.elim ((b : (a : ι) → M) i) v
r : range v ⊆ range v'
⊢ False
have r' : ((b : (a : ι) → M) i : M) ∉ range v
Tactic: have r' : b i ∉ range v := fun ⟨k, p⟩ ↦ by simpa [w] using congr(b.repr $p i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Nontrivial R
inst_3 : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) (v x) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
repr_eq_zero :
  ∀ (l : κ →₀ R),
    Eq.{u + 1} (α := R)
      ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l) : ι →₀ R) : (a : ι) → R) i : R)
      (0 : R)
v' : (o : Option κ) → M := fun (o : Option κ) ↦ o.elim ((b : (a : ι) → M) i) v
r : range v ⊆ range v'
r' : ((b : (a : ι) → M) i : M) ∉ range v
⊢ False
have r'' : range v ≠ range v'
Tactic: have r'' : range v ≠ range v' := (r' <| · ▸ ⟨none, rfl⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Nontrivial R
inst_3 : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) (v x) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
repr_eq_zero :
  ∀ (l : κ →₀ R),
    Eq.{u + 1} (α := R)
      ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l) : ι →₀ R) : (a : ι) → R) i : R)
      (0 : R)
v' : (o : Option κ) → M := fun (o : Option κ) ↦ o.elim ((b : (a : ι) → M) i) v
r : range v ⊆ range v'
r' : ((b : (a : ι) → M) i : M) ∉ range v
r'' : range v ≠ range v'
⊢ LinearIndepOn R id (range v')
have i₁ : LinearIndependent R v'
Tactic: apply LinearIndependent.linearIndepOn_id
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Nontrivial R
inst_3 : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) (v x) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
repr_eq_zero :
  ∀ (l : κ →₀ R),
    Eq.{u + 1} (α := R)
      ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l) : ι →₀ R) : (a : ι) → R) i : R)
      (0 : R)
v' : (o : Option κ) → M := fun (o : Option κ) ↦ o.elim ((b : (a : ι) → M) i) v
r : range v ⊆ range v'
r' : ((b : (a : ι) → M) i : M) ∉ range v
r'' : range v ≠ range v'
l l' : Finsupp.{w', u} (Option κ) R
z :
  Eq.{v + 1} (α := M) ((linearCombination R v' : (a : Option κ →₀ R) → M) l : M)
    ((linearCombination R v' : (a : Option κ →₀ R) → M) l' : M)
⊢ l = l'
have z₁ : HAdd.hAdd (β := M)
    (HSMul.hSMul.{u, v, v} (α := R) (β := M) ((l : (a : Option κ) → R) none : R) ((b : (a : ι) → M) i : M))
    ((linearCombination R
            ((fun (o : Option κ) ↦
                match (motive := Option κ → M → (κ → M) → M) o, (b : (a : ι) → M) i, v with
                | Option.some x, x_1, f => f x
                | none, y, x => y) ∘
              Option.some) :
          (a : κ →₀ R) → M)
        l.some :
      M) =
  HAdd.hAdd (β := M)
    (HSMul.hSMul.{u, v, v} (α := R) (β := M) ((l' : (a : Option κ) → R) none : R) ((b : (a : ι) → M) i : M))
    ((linearCombination R
            ((fun (o : Option κ) ↦
                match (motive := Option κ → M → (κ → M) → M) o, (b : (a : ι) → M) i, v with
                | Option.some x, x_1, f => f x
                | none, y, x => y) ∘
              Option.some) :
          (a : κ →₀ R) → M)
        l'.some :
      M)
Tactic: simp_rw [linearCombination_option, v', Option.elim] at z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Nontrivial R
inst_3 : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) (v x) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
repr_eq_zero :
  ∀ (l : κ →₀ R),
    Eq.{u + 1} (α := R)
      ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l) : ι →₀ R) : (a : ι) → R) i : R)
      (0 : R)
v' : (o : Option κ) → M := fun (o : Option κ) ↦ o.elim ((b : (a : ι) → M) i) v
r : range v ⊆ range v'
r' : ((b : (a : ι) → M) i : M) ∉ range v
r'' : range v ≠ range v'
l l' : Finsupp.{w', u} (Option κ) R
z :
  HAdd.hAdd (β := M)
      (HSMul.hSMul.{u, v, v} (α := R) (β := M) ((l : (a : Option κ) → R) none : R) ((b : (a : ι) → M) i : M))
      ((linearCombination R
              ((fun (o : Option κ) ↦
                  match (motive := Option κ → M → (κ → M) → M) o, (b : (a : ι) → M) i, v with
                  | Option.some x, x_1, f => f x
                  | none, y, x => y) ∘
                Option.some) :
            (a : κ →₀ R) → M)
          l.some :
        M) =
    HAdd.hAdd (β := M)
      (HSMul.hSMul.{u, v, v} (α := R) (β := M) ((l' : (a : Option κ) → R) none : R) ((b : (a : ι) → M) i : M))
      ((linearCombination R
              ((fun (o : Option κ) ↦
                  match (motive := Option κ → M → (κ → M) → M) o, (b : (a : ι) → M) i, v with
                  | Option.some x, x_1, f => f x
                  | none, y, x => y) ∘
                Option.some) :
            (a : κ →₀ R) → M)
          l'.some :
        M)
⊢ l = l'
have z₁ : HAdd.hAdd (β := M)
    (HSMul.hSMul.{u, v, v} (α := R) (β := M) ((l : (a : Option κ) → R) none : R) ((b : (a : ι) → M) i : M))
    ((linearCombination R v : (a : κ →₀ R) → M) l.some : M) =
  HAdd.hAdd (β := M)
    (HSMul.hSMul.{u, v, v} (α := R) (β := M) ((l' : (a : Option κ) → R) none : R) ((b : (a : ι) → M) i : M))
    ((linearCombination R v : (a : κ →₀ R) → M) l'.some : M)
Tactic: change _ + linearCombination R v l.some = _ + linearCombination R v l'.some at z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Nontrivial R
inst_3 : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) (v x) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
repr_eq_zero :
  ∀ (l : κ →₀ R),
    Eq.{u + 1} (α := R)
      ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l) : ι →₀ R) : (a : ι) → R) i : R)
      (0 : R)
v' : (o : Option κ) → M := fun (o : Option κ) ↦ o.elim ((b : (a : ι) → M) i) v
r : range v ⊆ range v'
r' : ((b : (a : ι) → M) i : M) ∉ range v
r'' : range v ≠ range v'
l l' : Finsupp.{w', u} (Option κ) R
z :
  HAdd.hAdd (β := M)
      (HSMul.hSMul.{u, v, v} (α := R) (β := M) ((l : (a : Option κ) → R) none : R) ((b : (a : ι) → M) i : M))
      ((linearCombination R v : (a : κ →₀ R) → M) l.some : M) =
    HAdd.hAdd (β := M)
      (HSMul.hSMul.{u, v, v} (α := R) (β := M) ((l' : (a : Option κ) → R) none : R) ((b : (a : ι) → M) i : M))
      ((linearCombination R v : (a : κ →₀ R) → M) l'.some : M)
⊢ l = l'
have i₁ : Eq.{u + 1} (α := R) ((l : (a : Option κ) → R) none : R) ((l' : (a : Option κ) → R) none : R)
Tactic: ext (_ | a)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Nontrivial R
inst_3 : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) (v x) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
repr_eq_zero :
  ∀ (l : κ →₀ R),
    Eq.{u + 1} (α := R)
      ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l) : ι →₀ R) : (a : ι) → R) i : R)
      (0 : R)
v' : (o : Option κ) → M := fun (o : Option κ) ↦ o.elim ((b : (a : ι) → M) i) v
r : range v ⊆ range v'
r' : ((b : (a : ι) → M) i : M) ∉ range v
r'' : range v ≠ range v'
l l' : Finsupp.{w', u} (Option κ) R
z :
  HAdd.hAdd (β := M)
      (HSMul.hSMul.{u, v, v} (α := R) (β := M) ((l : (a : Option κ) → R) none : R) ((b : (a : ι) → M) i : M))
      ((linearCombination R v : (a : κ →₀ R) → M) l.some : M) =
    HAdd.hAdd (β := M)
      (HSMul.hSMul.{u, v, v} (α := R) (β := M) ((l' : (a : Option κ) → R) none : R) ((b : (a : ι) → M) i : M))
      ((linearCombination R v : (a : κ →₀ R) → M) l'.some : M)
i₁ : Eq.{u + 1} (α := R) ((l : (a : Option κ) → R) none : R) ((l' : (a : Option κ) → R) none : R)
⊢ l = l'
have i₂ : ∀ (a : κ),
  Eq.{u + 1} (α := R) ((l : (a : Option κ) → R) (Option.some a) : R) ((l' : (a : Option κ) → R) (Option.some a) : R)
Tactic: ext (_ | a)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Nontrivial R
inst_3 : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) (v x) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
repr_eq_zero :
  ∀ (l : κ →₀ R),
    Eq.{u + 1} (α := R)
      ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l) : ι →₀ R) : (a : ι) → R) i : R)
      (0 : R)
v' : (o : Option κ) → M := fun (o : Option κ) ↦ o.elim ((b : (a : ι) → M) i) v
r : range v ⊆ range v'
r' : ((b : (a : ι) → M) i : M) ∉ range v
r'' : range v ≠ range v'
l l' : Finsupp.{w', u} (Option κ) R
z :
  HAdd.hAdd (β := M)
      (HSMul.hSMul.{u, v, v} (α := R) (β := M) ((l : (a : Option κ) → R) none : R) ((b : (a : ι) → M) i : M))
      ((linearCombination R v : (a : κ →₀ R) → M) l.some : M) =
    HAdd.hAdd (β := M)
      (HSMul.hSMul.{u, v, v} (α := R) (β := M) ((l' : (a : Option κ) → R) none : R) ((b : (a : ι) → M) i : M))
      ((linearCombination R v : (a : κ →₀ R) → M) l'.some : M)
a : κ
j : ι
⊢ Eq.{u + 1} (α := R)
    ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l.some) : ι →₀ R) : (a : ι) → R) j : R)
    ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l'.some) : ι →₀ R) : (a : ι) → R) j : R)
have inl : Eq.{u + 1} (α := R)
  ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l.some) : ι →₀ R) : (a : ι) → R) i : R)
  ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l'.some) : ι →₀ R) : (a : ι) → R) i : R)
Tactic: obtain rfl | ne := eq_or_ne i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Nontrivial R
inst_3 : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) (v x) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
repr_eq_zero :
  ∀ (l : κ →₀ R),
    Eq.{u + 1} (α := R)
      ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l) : ι →₀ R) : (a : ι) → R) i : R)
      (0 : R)
v' : (o : Option κ) → M := fun (o : Option κ) ↦ o.elim ((b : (a : ι) → M) i) v
r : range v ⊆ range v'
r' : ((b : (a : ι) → M) i : M) ∉ range v
r'' : range v ≠ range v'
l l' : Finsupp.{w', u} (Option κ) R
z :
  HAdd.hAdd (β := M)
      (HSMul.hSMul.{u, v, v} (α := R) (β := M) ((l : (a : Option κ) → R) none : R) ((b : (a : ι) → M) i : M))
      ((linearCombination R v : (a : κ →₀ R) → M) l.some : M) =
    HAdd.hAdd (β := M)
      (HSMul.hSMul.{u, v, v} (α := R) (β := M) ((l' : (a : Option κ) → R) none : R) ((b : (a : ι) → M) i : M))
      ((linearCombination R v : (a : κ →₀ R) → M) l'.some : M)
a : κ
j : ι
inl :
  Eq.{u + 1} (α := R)
    ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l.some) : ι →₀ R) : (a : ι) → R) i : R)
    ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l'.some) : ι →₀ R) : (a : ι) → R) i : R)
⊢ Eq.{u + 1} (α := R)
    ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l.some) : ι →₀ R) : (a : ι) → R) j : R)
    ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l'.some) : ι →₀ R) : (a : ι) → R) j : R)
have inr : ∀ (ne : i ≠ j),
  Eq.{u + 1} (α := R)
    ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l.some) : ι →₀ R) : (a : ι) → R) j : R)
    ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l'.some) : ι →₀ R) : (a : ι) → R) j : R)
Tactic: obtain rfl | ne := eq_or_ne i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Nontrivial R
inst_3 : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) (v x) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
repr_eq_zero :
  ∀ (l : κ →₀ R),
    Eq.{u + 1} (α := R)
      ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l) : ι →₀ R) : (a : ι) → R) i : R)
      (0 : R)
v' : (o : Option κ) → M := fun (o : Option κ) ↦ o.elim ((b : (a : ι) → M) i) v
r : range v ⊆ range v'
r' : ((b : (a : ι) → M) i : M) ∉ range v
r'' : range v ≠ range v'
l l' : Finsupp.{w', u} (Option κ) R
z :
  HAdd.hAdd (β := M)
      (HSMul.hSMul.{u, v, v} (α := R) (β := M) ((l : (a : Option κ) → R) none : R) ((b : (a : ι) → M) i : M))
      ((linearCombination R v : (a : κ →₀ R) → M) l.some : M) =
    HAdd.hAdd (β := M)
      (HSMul.hSMul.{u, v, v} (α := R) (β := M) ((l' : (a : Option κ) → R) none : R) ((b : (a : ι) → M) i : M))
      ((linearCombination R v : (a : κ →₀ R) → M) l'.some : M)
a : κ
⊢ Eq.{u + 1} (α := R) ((l : (a : Option κ) → R) (Option.some a) : R) ((l' : (a : Option κ) → R) (Option.some a) : R)
have l₁ : l.some = l'.some
Tactic: have l₁ : l.some = l'.some := ind <| b.repr.injective <| ext fun j ↦ by
      obtain rfl | ne := eq_or_ne i j
      · simp_rw [repr_eq_zero]
      classical simpa [single_apply, ne] using congr(b.repr $z j)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Nontrivial R
inst_3 : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) (v x) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
repr_eq_zero :
  ∀ (l : κ →₀ R),
    Eq.{u + 1} (α := R)
      ((((b.repr : (a : M) → ι →₀ R) ((linearCombination R v : (a : κ →₀ R) → M) l) : ι →₀ R) : (a : ι) → R) i : R)
      (0 : R)
v' : (o : Option κ) → M := fun (o : Option κ) ↦ o.elim ((b : (a : ι) → M) i) v
r : range v ⊆ range v'
r' : ((b : (a : ι) → M) i : M) ∉ range v
r'' : range v ≠ range v'
⊢ False
have i' : LinearIndepOn R id (range v')
Tactic: have i' : LinearIndepOn R id (range v') := by
    apply LinearIndependent.linearIndepOn_id
    rw [linearIndependent_iffₛ]
    intro l l' z
    simp_rw [linearCombination_option, v', Option.elim] at z
    change _ + linearCombination R v l.some = _ + linearCombination R v l'.some at z
    -- We have some equality between linear combinations of `b i` and the `v k`,
    -- and want to show the coefficients are equal.
    ext (_ | a)
    -- We'll first show the coefficient of `b i` is zero,
    -- by expressing the `v k` in the basis `b`, and using that the `v k` have no `b i` term.
    · simpa [repr_eq_zero] using congr(b.repr $z i)
    -- All the other coefficients are also equal, because `v` is linear independent,
    -- by comparing the coefficients in the basis `b`.
    have l₁ : l.some = l'.some := ind <| b.repr.injective <| ext fun j ↦ by
      obtain rfl | ne := eq_or_ne i j
      · simp_rw [repr_eq_zero]
      classical simpa [single_apply, ne] using congr(b.repr $z j)
    exact DFunLike.congr_fun l₁ a
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Cardinality (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Nontrivial R
inst_3 : Module R M
ι : Type w
b : Basis ι R M
inst_4 : Infinite ι
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : i.Maximal
Φ : (k : κ) → Finset ι := fun (k : κ) ↦ support.{w, u} (M := R) ((b.repr : (a : M) → ι →₀ R) (v k))
⊢ #ι ≤ #(↑(range Φ) : Type w)
have w : Eq.{w + 1} (α := Set ι) (⋃ (a : κ), (↑(Φ a) : Set ι)) Set.univ
Tactic: apply Cardinal.le_range_of_union_finset_eq_univ