awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
f : ι →₀ R
⊢ Exists.choose (p := fun (r : R) ↦ r • x = HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x) ⋯ •
      x =
    HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x

Tactic:
(w (f default • x)).choose_spec

Premises used: Inhabited.default, Exists.choose_spec, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
f : ι →₀ R
⊢ Exists.choose (p := fun (r : R) ↦ r • x = HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x) ⋯ •
      x =
    HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x

Tactic:
exact (w (f default • x)).choose_spec

Premises used: Inhabited.default, Exists.choose_spec, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
y : M
mpr : ⋯.choose (p := fun (r : R) ↦ r • x = y) • x = y
⊢ (fun (f : ι →₀ R) ↦ HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x)
      ((fun (y : M) ↦ (single default (⋯.choose (p := fun (r : R) ↦ r • x = y)) : ι →₀ R)) y) =
    y

Tactic:
simp only [Finsupp.single_eq_same]

Premises used: Finsupp.single_eq_same
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
y : M
⊢ ⋯.choose (p := fun (r : R) ↦ r • x = y) • x = y

Tactic:
(w y).choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
y : M
⊢ ⋯.choose (p := fun (r : R) ↦ r • x = y) • x = y

Tactic:
exact (w y).choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
b : Basis ι R M
inst_4 : Fintype R
inst_5 : Fintype M
⊢ card M = card (ι → R)

Tactic:
card_congr b.equivFun.toEquiv

Premises used: Fintype.card_congr, LinearEquiv.toEquiv, Module.Basis.equivFun
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
b : Basis ι R M
inst_4 : Fintype R
inst_5 : Fintype M
⊢ card (ι → R) = card R ^ card ι

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
b : Basis ι R M
inst_4 : Fintype R
inst_5 : Fintype M
card : Fintype.card (ι → R) = Fintype.card R ^ Fintype.card ι
⊢ Fintype.card M = Fintype.card R ^ Fintype.card ι

Tactic:
calc
      card M = card (ι → R) := card_congr b.equivFun.toEquiv
      _ = card R ^ card ι := by simp

Premises used: Fintype.card_congr, Fintype.card, LinearEquiv.toEquiv, Module.Basis.equivFun
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
b : Basis ι R M
inst_4 : Fintype R
inst_5 : Fintype M
card : Fintype.card (ι → R) = Fintype.card R ^ Fintype.card ι
⊢ Fintype.card M = Fintype.card R ^ Fintype.card ι

Tactic:
classical
    calc
      card M = card (ι → R) := card_congr b.equivFun.toEquiv
      _ = card R ^ card ι := by simp

Premises used: Fintype.card
-- Module: Mathlib.LinearAlgebra.Basis.Bilinear
Goal:
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
B B' : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
h :
  ∀ (i : ι₁) (j : ι₂),
    Eq.{u_9 + 1} (α := P)
      ((((B : (a : M) → N →ₛₗ[σ₁₂] P) ((b₁ : (a : ι₁) → M) i) : N →ₛₗ[σ₁₂] P) : (a : N) → P)
          ((b₂ : (a : ι₂) → N) j : N) :
        P)
      ((((B' : (a : M) → N →ₛₗ[σ₁₂] P) ((b₁ : (a : ι₁) → M) i) : N →ₛₗ[σ₁₂] P) : (a : N) → P)
          ((b₂ : (a : ι₂) → N) j : N) :
        P)
⊢ B = B'

Tactic:
b₁.ext fun i => b₂.ext fun j => h i j

Premises used: Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Basis.Bilinear
Goal:
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
rw :
  ((((B : (a : M) → N →ₛₗ[σ₁₂] P)
            ((Finsupp.linearCombination R (⇑b₁ : (a : ι₁) → M) : (a : ι₁ →₀ R) → M)
              ((b₁.repr : (a : M) → ι₁ →₀ R) x : ι₁ →₀ R)) :
          N →ₛₗ[σ₁₂] P) :
        (a : N) → P)
      ((Finsupp.linearCombination S (⇑b₂ : (a : ι₂) → N) : (a : ι₂ →₀ S) → N)
          ((b₂.repr : (a : N) → ι₂ →₀ S) y : ι₂ →₀ S) :
        N) :
    P)
| ((((B : (a : M) → N →ₛₗ[σ₁₂] P) x : N →ₛₗ[σ₁₂] P) : (a : N) → P) y : P)

Tactic:
rw [← b₁.linearCombination_repr x, ← b₂.linearCombination_repr y]

Premises used: Module.Basis.linearCombination_repr
-- Module: Mathlib.LinearAlgebra.Basis.Bilinear
Goal:
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
conv_rhs :
  Eq.{u_9 + 1} (α := P)
    (Finsupp.sum ((b₁.repr : (a : M) → ι₁ →₀ R) x) fun (i : ι₁) (xi : R) ↦
        Finsupp.sum ((b₂.repr : (a : N) → ι₂ →₀ S) y) fun (j : ι₂) (yj : S) ↦
          HSMul.hSMul.{u_4, u_9, u_9} (α := R₂) ((ρ₁₂ : (a : R) → R₂) xi : R₂)
            (HSMul.hSMul.{u_6, u_9, u_9} (α := S₂) (β := P) ((σ₁₂ : (a : S) → S₂) yj : S₂)
              ((((B : (a : M) → N →ₛₗ[σ₁₂] P) ((b₁ : (a : ι₁) → M) i) : N →ₛₗ[σ₁₂] P) : (a : N) → P)
                  ((b₂ : (a : ι₂) → N) j : N) :
                P)) :
      P)
    ((((B : (a : M) → N →ₛₗ[σ₁₂] P)
              ((Finsupp.linearCombination R (⇑b₁ : (a : ι₁) → M) : (a : ι₁ →₀ R) → M)
                ((b₁.repr : (a : M) → ι₁ →₀ R) x : ι₁ →₀ R)) :
            N →ₛₗ[σ₁₂] P) :
          (a : N) → P)
        ((Finsupp.linearCombination S (⇑b₂ : (a : ι₂) → N) : (a : ι₂ →₀ S) → N)
            ((b₂.repr : (a : N) → ι₂ →₀ S) y : ι₂ →₀ S) :
          N) :
      P)
⊢ Eq.{u_9 + 1} (α := P)
    (Finsupp.sum ((b₁.repr : (a : M) → ι₁ →₀ R) x) fun (i : ι₁) (xi : R) ↦
        Finsupp.sum ((b₂.repr : (a : N) → ι₂ →₀ S) y) fun (j : ι₂) (yj : S) ↦
          HSMul.hSMul.{u_4, u_9, u_9} (α := R₂) ((ρ₁₂ : (a : R) → R₂) xi : R₂)
            (HSMul.hSMul.{u_6, u_9, u_9} (α := S₂) (β := P) ((σ₁₂ : (a : S) → S₂) yj : S₂)
              ((((B : (a : M) → N →ₛₗ[σ₁₂] P) ((b₁ : (a : ι₁) → M) i) : N →ₛₗ[σ₁₂] P) : (a : N) → P)
                  ((b₂ : (a : ι₂) → N) j : N) :
                P)) :
      P)
    ((((B : (a : M) → N →ₛₗ[σ₁₂] P) x : N →ₛₗ[σ₁₂] P) : (a : N) → P) y : P)

Tactic:
conv_rhs => rw [← b₁.linearCombination_repr x, ← b₂.linearCombination_repr y]

Premises used: Module.Basis.linearCombination_repr
-- Module: Mathlib.LinearAlgebra.Basis.Bilinear
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ₗ
rw :
  ((((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ₗ)
| ((((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ) x : Nₗ →ₗ[Rₗ] Pₗ) : (a : Nₗ) → Pₗ) y : Pₗ)

Tactic:
rw [← b₁'.linearCombination_repr x, ← b₂'.linearCombination_repr y]

Premises used: Module.Basis.linearCombination_repr
-- Module: Mathlib.LinearAlgebra.Basis.Bilinear
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ₗ
conv_rhs :
  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ₗ)
⊢ 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ₗ) x : Nₗ →ₗ[Rₗ] Pₗ) : (a : Nₗ) → Pₗ) y : Pₗ)

Tactic:
conv_rhs => rw [← b₁'.linearCombination_repr x, ← b₂'.linearCombination_repr y]

Premises used: Module.Basis.linearCombination_repr
-- Module: Mathlib.LinearAlgebra.Basis.Cardinality
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial M
ι : Type u_1
s : Set (ι →₀ M)
hs : s.Finite
hsspan : Eq (α := Submodule R (ι →₀ M)) (span R s) ⊤
this : Eq.{u_1 + 1} (α := Set ι) (⋃ i ∈ s, (↑i.support : Set ι)) Set.univ
x : ι →₀ M
h : x ∈ s
⊢ (↑x.support : Set ι).Finite

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Cardinality
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
⊢ 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)
-- Module: Mathlib.LinearAlgebra.Basis.Cardinality
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) ⊤
⊢ 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

Premises used: Submodule.map_top, Submodule.span_image, LinearEquiv.range
-- Module: Mathlib.LinearAlgebra.Basis.Cardinality
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 : Eq (α := Submodule R (ι →₀ R)) (span R ((⇑(↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ R) '' s)) ⊤
⊢ Finite ι

Tactic:
finite_of_span_finite_eq_top_finsupp (hs.image _) this

Premises used: Set.Finite.image, finite_of_span_finite_eq_top_finsupp
-- Module: Mathlib.LinearAlgebra.Basis.Cardinality
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 : Eq (α := Submodule R (ι →₀ R)) (span R ((⇑(↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ R) '' s)) ⊤
⊢ Finite ι

Tactic:
exact finite_of_span_finite_eq_top_finsupp (hs.image _) this

Premises used: Set.Finite.image, finite_of_span_finite_eq_top_finsupp
-- Module: Mathlib.LinearAlgebra.Basis.Cardinality
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
by_contra :
  ∀
    (h :
      ¬Eq.{w + 1} (α := Set ι) (⋃ (k : κ), (↑(support.{w, u} (M := R) ((b.repr : (a : M) → ι →₀ R) (v k))) : Set ι))
          Set.univ),
    False
⊢ Eq.{w + 1} (α := Set ι) (⋃ (k : κ), (↑(support.{w, u} (M := R) ((b.repr : (a : M) → ι →₀ R) (v k))) : Set ι)) Set.univ

Tactic:
by_contra h
-- Module: Mathlib.LinearAlgebra.Basis.Cardinality
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
⊢ ∃ (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

Premises used: Finsupp.mem_support_iff, Set.mem_iUnion, Ne.eq_def, Set.ne_univ_iff_exists_notMem, Finset.mem_coe, Classical.not_exists_not
-- Module: Mathlib.LinearAlgebra.Basis.Cardinality
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)
obtain :
  ∀ (i : ι)
    (w : ∀ (x : κ), Eq.{u + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) (v x) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)),
    False
⊢ False

Tactic:
obtain ⟨i, w⟩ := h
-- Module: Mathlib.LinearAlgebra.Basis.Cardinality
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)
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:
simp [linearCombination_apply, Finsupp.sum, w]

Premises used: Finsupp.sum, Finsupp.linearCombination_apply
-- Module: Mathlib.LinearAlgebra.Basis.Cardinality
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)
⊢ ∀ (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]
-- Module: Mathlib.LinearAlgebra.Basis.Cardinality
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
k : κ
⊢ v k ∈ range v'

Tactic:
⟨some k, rfl⟩

Premises used: Set.Mem, setOf, Option.some, Exists.intro, Set.range, rfl
-- Module: Mathlib.LinearAlgebra.Basis.Cardinality
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
k : κ
⊢ v k ∈ range v'

Tactic:
exact ⟨some k, rfl⟩
-- Module: Mathlib.LinearAlgebra.Basis.Cardinality
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
⊢ range v ⊆ range v'

Tactic:
have r : range v ⊆ range v' := by rintro - ⟨k, rfl⟩; exact ⟨some k, rfl⟩
-- Module: Mathlib.LinearAlgebra.Basis.Cardinality
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'
h : Membership.mem (α := M) (range v) ((b : (a : ι) → M) i : M)
k : κ
p : v k = (b : (a : ι) → M) i
⊢ False

Tactic:
simpa [w] using congr(b.repr $p i)
-- Module: Mathlib.LinearAlgebra.Basis.Cardinality
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'
⊢ ((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)
-- Module: Mathlib.LinearAlgebra.Basis.Cardinality
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
⊢ range v ≠ range v'

Tactic:
have r'' : range v ≠ range v' := (r' <| · ▸ ⟨none, rfl⟩)
-- Module: Mathlib.LinearAlgebra.Basis.Cardinality
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'
i₁ : LinearIndependent R v'
⊢ LinearIndepOn R id (range v')

Tactic:
apply LinearIndependent.linearIndepOn_id

Premises used: LinearIndependent.linearIndepOn_id