awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
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)
⊢ 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

Premises used: Finsupp.linearCombination_option, Option.elim
-- 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'
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)
⊢ 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

Premises used: Finsupp.some, Finsupp.linearCombination, DFunLike.coe
-- 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'
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)
i₂ :
  ∀ (a : κ),
    Eq.{u + 1} (α := R) ((l : (a : Option κ) → R) (Option.some a) : R) ((l' : (a : Option κ) → R) (Option.some a) : R)
⊢ l = l'

Tactic:
ext (_ | a)
-- 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'
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)
⊢ Eq.{u + 1} (α := R) ((l : (a : Option κ) → R) none : R) ((l' : (a : Option κ) → R) none : R)

Tactic:
simpa [repr_eq_zero] using congr(b.repr $z 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
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)
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)
⊢ 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

Premises used: eq_or_ne, 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'
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)
    ((((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:
simp_rw [repr_eq_zero]
-- 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'
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 : ι
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:
simpa [single_apply, ne] using congr(b.repr $z j)

Premises used: Finsupp.single_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)
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 : ι
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:
classical simpa [single_apply, ne] using congr(b.repr $z j)

Premises used: Finsupp.single_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)
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 : κ
⊢ 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)
-- 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'
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 : κ
l₁ : l.some = l'.some
⊢ Eq.{u + 1} (α := R) ((l : (a : Option κ) → R) (Option.some a) : R) ((l' : (a : Option κ) → R) (Option.some a) : R)

Tactic:
DFunLike.congr_fun l₁ a

Premises used: DFunLike.congr_fun
-- 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'
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 : κ
l₁ : l.some = l'.some
⊢ Eq.{u + 1} (α := R) ((l : (a : Option κ) → R) (Option.some a) : R) ((l' : (a : Option κ) → R) (Option.some a) : R)

Tactic:
exact DFunLike.congr_fun l₁ a

Premises used: DFunLike.congr_fun
-- 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'
⊢ 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
-- 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' : LinearIndepOn R id (range v')
⊢ False

Tactic:
r'' (m (range v') i' r)

Premises used: Set.range
-- 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' : LinearIndepOn R id (range v')
⊢ False

Tactic:
exact r'' (m (range v') i' r)

Premises used: Set.range
-- 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
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))
w : Eq.{w + 1} (α := Set ι) (⋃ (a : κ), (↑(Φ a) : Set ι)) Set.univ
⊢ #ι ≤ #(↑(range Φ) : Type w)

Tactic:
apply Cardinal.le_range_of_union_finset_eq_univ

Premises used: Cardinal.le_range_of_union_finset_eq_univ
-- 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
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))
⊢ Eq.{w + 1} (α := Set ι) (⋃ (a : κ), (↑(Φ a) : Set ι)) Set.univ

Tactic:
union_support_maximal_linearIndependent_eq_range_basis b v i m

Premises used: setOf, union_support_maximal_linearIndependent_eq_range_basis
-- 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
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))
⊢ Eq.{w + 1} (α := Set ι) (⋃ (a : κ), (↑(Φ a) : Set ι)) Set.univ

Tactic:
exact union_support_maximal_linearIndependent_eq_range_basis b v i m

Premises used: union_support_maximal_linearIndependent_eq_range_basis
-- 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
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)

Tactic:
have w₁ : #ι ≤ #(Set.range Φ) := by
    apply Cardinal.le_range_of_union_finset_eq_univ
    exact union_support_maximal_linearIndependent_eq_range_basis b v i m
-- 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
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))
w₁ : #ι ≤ #(↑(range Φ) : Type w)
⊢ Cardinal.lift.{w', w} #(↑(range Φ) : Type w) ≤ Cardinal.lift.{w, w'} #κ

Tactic:
have w₂ : Cardinal.lift.{w'} #(Set.range Φ) ≤ Cardinal.lift.{w} #κ := Cardinal.mk_range_le_lift