awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
S : Type u_2
T : Type u_3
inst_2 : Semiring S
inst_3 : Semiring T
inst_4 : Module R T
inst_5 : Module S T
inst_6 : Module R S
inst_7 : IsScalarTower R S T
inst_8 : IsScalarTower S T T
inst_9 : FaithfulSMul S T
inst_10 : Module.Finite S T
inst_11 : Free R S
H : ¬Module.Finite R S
neg : 0 ≤ finrank R T
rw : ℵ₀ ≤ Module.rank R S
⊢ finrank R S ≤ finrank R T

Tactic:
rw [finrank, Cardinal.toNat_eq_zero.mpr (.inr _)]

Premises used: Iff.mpr, Cardinal.toNat_eq_zero, Module.finrank, Or.inr
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
S : Type u_2
T : Type u_3
inst_2 : Semiring S
inst_3 : Semiring T
inst_4 : Module R T
inst_5 : Module S T
inst_6 : Module R S
inst_7 : IsScalarTower R S T
inst_8 : IsScalarTower S T T
inst_9 : FaithfulSMul S T
inst_10 : Module.Finite S T
inst_11 : Free R S
H : ¬Module.Finite R S
⊢ 0 ≤ finrank R T

Tactic:
zero_le

Premises used: zero_le
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
S : Type u_2
T : Type u_3
inst_2 : Semiring S
inst_3 : Semiring T
inst_4 : Module R T
inst_5 : Module S T
inst_6 : Module R S
inst_7 : IsScalarTower R S T
inst_8 : IsScalarTower S T T
inst_9 : FaithfulSMul S T
inst_10 : Module.Finite S T
inst_11 : Free R S
H : ¬Module.Finite R S
⊢ 0 ≤ finrank R T

Tactic:
exact zero_le

Premises used: zero_le
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
S : Type u_2
T : Type u_3
inst_2 : Semiring S
inst_3 : Semiring T
inst_4 : Module R T
inst_5 : Module S T
inst_6 : Module R S
inst_7 : IsScalarTower R S T
inst_8 : IsScalarTower S T T
inst_9 : FaithfulSMul S T
inst_10 : Module.Finite S T
inst_11 : Free R S
H : ¬Module.Finite R S
rwa : ¬Module.rank R S < ℵ₀
rwa₁ rwa₂ rwa₃ rwa₄ : ¬Module.Finite R S
⊢ ℵ₀ ≤ Module.rank R S

Tactic:
rwa [← not_lt, Module.rank_lt_aleph0_iff]

Premises used: Module.rank_lt_aleph0_iff, not_lt
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : StrongRankCondition R
ι : Type u_2
b : Basis ι R M
d1 : finrank R M = 1
⊢ Nontrivial R

Tactic:
have : Nontrivial R := nontrivial_of_invariantBasisNumber R
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : StrongRankCondition R
ι : Type u_2
b : Basis ι R M
d1 : finrank R M = 1
this : Nontrivial R
⊢ Module.Finite R M

Tactic:
haveI : Module.Finite R M :=
    Module.finite_of_finrank_pos (Nat.lt_of_sub_eq_succ d1)
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : StrongRankCondition R
ι : Type u_2
b : Basis ι R M
d1 : finrank R M = 1
this_1 : Nontrivial R
this : Module.Finite R M
⊢ Finite ι

Tactic:
have : Finite ι := Module.Finite.finite_basis b
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : StrongRankCondition R
ι : Type u_2
b : Basis ι R M
d1 : finrank R M = 1
this_1 : Nontrivial R
this_2 : Module.Finite R M
this : Finite ι
have : ∀ (this : Fintype ι), Nonempty.{max 1 (u_2 + 1)} (Unique ι)
⊢ Nonempty.{max 1 (u_2 + 1)} (Unique ι)

Tactic:
have : Fintype ι := Fintype.ofFinite ι
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : StrongRankCondition R
ι : Type u_2
b : Basis ι R M
d1 : finrank R M = 1
this_1 : Nontrivial R
this_2 : Module.Finite R M
this_3 : Finite ι
this : Fintype ι
rwa : ∀ (d1 : Fintype.card ι = 1), Nonempty.{max 1 (u_2 + 1)} (Unique ι)
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (d1 : Nonempty.{u_2 + 1} (Unique ι)), Nonempty.{max 1 (u_2 + 1)} (Unique ι)
⊢ Nonempty.{max 1 (u_2 + 1)} (Unique ι)

Tactic:
rwa [Module.finrank_eq_card_basis b, Fintype.card_eq_one_iff_nonempty_unique] at d1

Premises used: Fintype.card_eq_one_iff_nonempty_unique, Module.finrank_eq_card_basis
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : StrongRankCondition R
d1 : finrank R M = 1
let : ∀ (ι : Type v) (b : Basis ι R M), Nonempty (R ≃ₗ[R] M)
⊢ Nonempty (R ≃ₗ[R] M)

Tactic:
let ⟨ι, b⟩ := (Module.Free.exists_basis R M).some
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : StrongRankCondition R
d1 : finrank R M = 1
ι : Type v
b : Basis ι R M
have : ∀ (this : Unique ι), Nonempty (R ≃ₗ[R] M)
⊢ Nonempty (R ≃ₗ[R] M)

Tactic:
have : Unique ι := (b.nonempty_unique_index_of_finrank_eq_one d1).some
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : StrongRankCondition R
d1 : finrank R M = 1
ι : Type v
b : Basis ι R M
this : Unique ι
⊢ Nonempty (R ≃ₗ[R] M)

Tactic:
⟨((b.equivFun).trans (LinearEquiv.funUnique ι R R)).symm⟩

Premises used: LinearEquiv.symm, LinearEquiv.funUnique, Nonempty.intro, LinearEquiv.trans, Module.Basis.equivFun
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : StrongRankCondition R
d1 : finrank R M = 1
ι : Type v
b : Basis ι R M
this : Unique ι
⊢ Nonempty (R ≃ₗ[R] M)

Tactic:
exact ⟨((b.equivFun).trans (LinearEquiv.funUnique ι R R)).symm⟩
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : StrongRankCondition R
ι : Type u_2
inst_5 : Unique ι
h : finrank R M = 1
v : M
i : ι
hv : v = 0
rw : Eq.{u + 1} (α := R) ((((basisUnique ι h).repr : (a : M) → ι →₀ R) 0 : (a : ι) → R) i : R) (0 : R)
rw₁ : Eq.{u + 1} (α := R) ((0 : (a : ι) → R) i : R) (0 : R)
rw₂ rw₃ : Eq.{u + 1} (α := R) 0 0
⊢ Eq.{u + 1} (α := R) (((((basisUnique ι h).repr : (a : M) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i : R) (0 : R)

Tactic:
rw [hv, map_zero, Finsupp.zero_apply]

Premises used: map_zero, Finsupp.zero_apply
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : StrongRankCondition R
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
⊢ let c : R := (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M);
  c = (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)

Tactic:
set c := e.symm (u (e 1)) with hc

Premises used: LinearEquiv.symm, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : StrongRankCondition R
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
hc : c = (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
this : u = HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id
h :
  (fun (c : R) ↦ u = HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id) c ∧
    ∀ (y : R), (fun (c : R) ↦ u = HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id) y → y = c
⊢ ∃! c : R, u = HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id

Tactic:
use c
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : StrongRankCondition R
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
hc : c = (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
this : u = HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id
h : ∀ (y : R), HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id = HSMul.hSMul (β := M →ₗ[R] M) y LinearMap.id → y = c
⊢ (fun (c : R) ↦ u = HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id) c ∧
    ∀ (y : R), (fun (c : R) ↦ u = HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id) y → y = c

Tactic:
simp only [this, true_and]

Premises used: true_and
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : StrongRankCondition R
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
hc : c = (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
this : u = HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id
d : R
hcd : HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id = HSMul.hSMul (β := M →ₗ[R] M) d LinearMap.id
⊢ ∀ (x : M),
    Eq (α := M) ((HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id : (a : M) → M) x : M)
      ((HSMul.hSMul (β := M →ₗ[R] M) d LinearMap.id : (a : M) → M) x : M)

Tactic:
rw [LinearMap.ext_iff] at hcd

Premises used: LinearMap.ext_iff
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : StrongRankCondition R
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
hc : c = (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
this : u = HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id
d : R
hcd :
  ∀ (x : M),
    Eq (α := M) ((HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id : (a : M) → M) x : M)
      ((HSMul.hSMul (β := M →ₗ[R] M) d LinearMap.id : (a : M) → M) x : M)
⊢ d = c

Tactic:
simpa using (LinearEquiv.congr_arg (e := e.symm) (hcd (e 1))).symm

Premises used: LinearEquiv.congr_arg, OfNat.ofNat, Eq.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : StrongRankCondition R
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
hc : c = (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
suffices : u = HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id
⊢ ∃! c : R, u = HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id

Tactic:
suffices u = c • LinearMap.id by
    use c
    simp only [this, true_and]
    intro d hcd
    rw [LinearMap.ext_iff] at hcd
    simpa using (LinearEquiv.congr_arg (e := e.symm) (hcd (e 1))).symm
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : StrongRankCondition R
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
hc : c = (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
h : ∀ (x : M), Eq (α := M) ((u : (a : M) → M) x : M) ((HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id : (a : M) → M) x : M)
⊢ u = HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : StrongRankCondition R
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
hc : c = (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
x_1 x : M
⊢ x = HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((e.symm : (a : M) → R) x : R) ((e : (a : R) → M) 1 : M)

Tactic:
simp [← LinearEquiv.map_smul]

Premises used: LinearEquiv.map_smul
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : StrongRankCondition R
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
hc : c = (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
x : M
⊢ ∀ (x : M), x = HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((e.symm : (a : M) → R) x : R) ((e : (a : R) → M) 1 : M)

Tactic:
have (x : M) : x = (e.symm x) • (e 1) := by simp [← LinearEquiv.map_smul]
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : StrongRankCondition R
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
hc : c = (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
x : M
this :
  ∀ (x : M), x = HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((e.symm : (a : M) → R) x : R) ((e : (a : R) → M) 1 : M)
h :
  Eq (α := M)
    ((u : (a : M) → M)
        (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((e.symm : (a : M) → R) x : R) ((e : (a : R) → M) 1 : M)) :
      M)
    ((HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id : (a : M) → M)
        (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((e.symm : (a : M) → R) x : R) ((e : (a : R) → M) 1 : M)) :
      M)
⊢ Eq (α := M) ((u : (a : M) → M) x : M) ((HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id : (a : M) → M) x : M)

Tactic:
rw [this x]
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : StrongRankCondition R
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
hc : c = (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
x : M
this :
  ∀ (x : M), x = HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((e.symm : (a : M) → R) x : R) ((e : (a : R) → M) 1 : M)
h :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((e.symm : (a : M) → R) x : R)
      ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((e.symm : (a : M) → R) x : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M) : R) ((e : (a : R) → M) 1 : M))
⊢ Eq (α := M)
    ((u : (a : M) → M)
        (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((e.symm : (a : M) → R) x : R) ((e : (a : R) → M) 1 : M)) :
      M)
    ((HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id : (a : M) → M)
        (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((e.symm : (a : M) → R) x : R) ((e : (a : R) → M) 1 : M)) :
      M)

Tactic:
simp only [hc, map_smul, LinearMap.smul_apply, LinearMap.id_coe, id_eq]

Premises used: LinearMap.smul_apply, LinearMap.id_coe, map_smul, id_eq
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : StrongRankCondition R
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
hc : c = (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
x : M
this :
  ∀ (x : M), x = HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((e.symm : (a : M) → R) x : R) ((e : (a : R) → M) 1 : M)
h h₁ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((e.symm : (a : M) → R) x : R)
      ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((e.symm : (a : M) → R) x : R)
      ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((e.symm : (a : M) → R) x : R)
      ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((e.symm : (a : M) → R) x : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M) : R) ((e : (a : R) → M) 1 : M))

Tactic:
rw [← this]
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R_1 : Type u
S : Type u_1
M_1 M₁ : Type v
M' : Type v'
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : Free R_1 M_1
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M'
inst_6 : Free R_1 M'
inst_7 : AddCommMonoid M₁
inst_8 : Module R_1 M₁
inst_9 : Free R_1 M₁
inst_10 : StrongRankCondition R_1
R : Type u_2
inst_11 : CommSemiring R
inst_12 : StrongRankCondition R
M : Type u_3
inst_13 : AddCommMonoid M
inst_14 : Module R M
inst_15 : Free R M
d1 : finrank R M = 1
c d : R
h :
  ∀ (x : M),
    Eq (α := M) ((HSMul.hSMul (β := M →ₗ[R] M) (c + d) LinearMap.id : (a : M) → M) x : M)
      ((HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id + HSMul.hSMul (β := M →ₗ[R] M) d LinearMap.id : (a : M) → M) x : M)
⊢ HSMul.hSMul (β := M →ₗ[R] M) (c + d) LinearMap.id =
    HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id + HSMul.hSMul (β := M →ₗ[R] M) d LinearMap.id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R_1 : Type u
S : Type u_1
M_1 M₁ : Type v
M' : Type v'
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : Free R_1 M_1
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M'
inst_6 : Free R_1 M'
inst_7 : AddCommMonoid M₁
inst_8 : Module R_1 M₁
inst_9 : Free R_1 M₁
inst_10 : StrongRankCondition R_1
R : Type u_2
inst_11 : CommSemiring R
inst_12 : StrongRankCondition R
M : Type u_3
inst_13 : AddCommMonoid M
inst_14 : Module R M
inst_15 : Free R M
d1 : finrank R M = 1
c d : R
x : M
⊢ Eq (α := M) ((HSMul.hSMul (β := M →ₗ[R] M) (c + d) LinearMap.id : (a : M) → M) x : M)
    ((HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id + HSMul.hSMul (β := M →ₗ[R] M) d LinearMap.id : (a : M) → M) x : M)

Tactic:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R_1 : Type u
S : Type u_1
M_1 M₁ : Type v
M' : Type v'
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : Free R_1 M_1
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M'
inst_6 : Free R_1 M'
inst_7 : AddCommMonoid M₁
inst_8 : Module R_1 M₁
inst_9 : Free R_1 M₁
inst_10 : StrongRankCondition R_1
R : Type u_2
inst_11 : CommSemiring R
inst_12 : StrongRankCondition R
M : Type u_3
inst_13 : AddCommMonoid M
inst_14 : Module R M
inst_15 : Free R M
d1 : finrank R M = 1
c d : R
h :
  ∀ (x : M),
    Eq (α := M) ((HSMul.hSMul (β := M →ₗ[R] M) (c • d) LinearMap.id : (a : M) → M) x : M)
      ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (HSMul.hSMul (β := M →ₗ[R] M) d LinearMap.id) :
            (a : M) → M)
          x :
        M)
⊢ HSMul.hSMul (β := M →ₗ[R] M) (c • d) LinearMap.id =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (HSMul.hSMul (β := M →ₗ[R] M) d LinearMap.id)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R_1 : Type u
S : Type u_1
M_1 M₁ : Type v
M' : Type v'
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : Free R_1 M_1
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M'
inst_6 : Free R_1 M'
inst_7 : AddCommMonoid M₁
inst_8 : Module R_1 M₁
inst_9 : Free R_1 M₁
inst_10 : StrongRankCondition R_1
R : Type u_2
inst_11 : CommSemiring R
inst_12 : StrongRankCondition R
M : Type u_3
inst_13 : AddCommMonoid M
inst_14 : Module R M
inst_15 : Free R M
d1 : finrank R M = 1
c d : R
x : M
⊢ Eq (α := M) ((HSMul.hSMul (β := M →ₗ[R] M) (c • d) LinearMap.id : (a : M) → M) x : M)
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (HSMul.hSMul (β := M →ₗ[R] M) d LinearMap.id) :
          (a : M) → M)
        x :
      M)

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R_1 : Type u
S : Type u_1
M_1 M₁ : Type v
M' : Type v'
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : Free R_1 M_1
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M'
inst_6 : Free R_1 M'
inst_7 : AddCommMonoid M₁
inst_8 : Module R_1 M₁
inst_9 : Free R_1 M₁
inst_10 : StrongRankCondition R_1
R : Type u_2
inst_11 : CommSemiring R
inst_12 : StrongRankCondition R
M : Type u_3
inst_13 : AddCommMonoid M
inst_14 : Module R M
inst_15 : Free R M
d1 : finrank R M = 1
c : R
⊢ (fun (u : M →ₗ[R] M) ↦
        Exists.choose (p := fun (x : R) ↦
          (fun (c : R) ↦ u = HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id) x ∧
            ∀ (y : R), u = HSMul.hSMul (β := M →ₗ[R] M) y LinearMap.id → y = x)
          ⋯)
      ((fun (c : R) ↦ HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id) c) =
    c

Tactic:
simp [← (LinearMap.existsUnique_eq_smul_id_of_finrank_eq_one d1 _).choose_spec.2 c]

Premises used: Exists.choose_spec, And.right, LinearMap.existsUnique_eq_smul_id_of_finrank_eq_one
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R_1 : Type u
S_1 : Type u_1
M M₁ : Type v
M' : Type v'
inst : Semiring R_1
inst_1 : AddCommMonoid M
inst_2 : Module R_1 M
inst_3 : Free R_1 M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M'
inst_6 : Free R_1 M'
inst_7 : AddCommMonoid M₁
inst_8 : Module R_1 M₁
inst_9 : Free R_1 M₁
R : Type u_2
S : Type u_3
inst_10 : CommSemiring R
inst_11 : StrongRankCondition R
inst_12 : Semiring S
inst_13 : Algebra R S
inst_14 : IsQuadraticExtension R S
⊢ Module.Finite R S

Tactic:
finite_of_finrank_eq_succ <| IsQuadraticExtension.finrank_eq_two R S

Premises used: Module.finite_of_finrank_eq_succ, Algebra.IsQuadraticExtension.finrank_eq_two
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
ι : Type u_1
inst_5 : IsEmpty ι
hV : Module.rank K V = 0
obtain : ∀ (fst : Type v) (b : Basis fst K V), Subsingleton V
⊢ Subsingleton V

Tactic:
obtain ⟨_, b⟩ := Module.Free.exists_basis (R := K) (M := V)

Premises used: Module.Free.exists_basis
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
ι : Type u_1
inst_5 : IsEmpty ι
hV : Module.rank K V = 0
fst : Type v
b : Basis fst K V
⊢ IsEmpty fst

Tactic:
haveI := mk_eq_zero_iff.1 (hV ▸ b.mk_eq_rank'')
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
ι : Type u_1
inst_5 : IsEmpty ι
hV : Module.rank K V = 0
fst : Type v
b : Basis fst K V
this : IsEmpty fst
⊢ Subsingleton V

Tactic:
b.repr.toEquiv.subsingleton

Premises used: Module.Basis.repr, LinearEquiv.toEquiv, Equiv.subsingleton
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
ι : Type u_1
inst_5 : IsEmpty ι
hV : Module.rank K V = 0
fst : Type v
b : Basis fst K V
this : IsEmpty fst
⊢ Subsingleton V

Tactic:
exact b.repr.toEquiv.subsingleton

Premises used: Module.Basis.repr, LinearEquiv.toEquiv, Equiv.subsingleton
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
ι : Type u_1
inst_5 : IsEmpty ι
hV : Module.rank K V = 0
i : ι
⊢ Eq.{v + 1} (α := V) ((ofRankEqZero hV : (a : ι) → V) i : V) (0 : V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
c : Cardinal.{v}
⊢ Nontrivial K

Tactic:
haveI := nontrivial_of_invariantBasisNumber K