awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Free R M'
inst_7 : StrongRankCondition R
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
β : Type v'
B' : Basis β R M'
⊢ lift.{v', v} #α = lift.{v, v'} #β
have rw : lift.{v', v} (Module.rank R M) = lift.{v, v'} #β
Tactic: rw [B.mk_eq_rank'', cnd, B'.mk_eq_rank'']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Free R M'
inst_7 : StrongRankCondition R
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
β : Type v'
B' : Basis β R M'
rw : lift.{v', v} (Module.rank R M) = lift.{v, v'} #β
⊢ lift.{v', v} #α = lift.{v, v'} #β
have rw₁ : lift.{v, v'} (Module.rank R M') = lift.{v, v'} #β
Tactic: rw [B.mk_eq_rank'', cnd, B'.mk_eq_rank'']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Free R M'
inst_7 : StrongRankCondition R
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
β : Type v'
B' : Basis β R M'
rw : lift.{v', v} (Module.rank R M) = lift.{v, v'} #β
rw₁ : lift.{v, v'} (Module.rank R M') = lift.{v, v'} #β
⊢ lift.{v', v} #α = lift.{v, v'} #β
have rw₂ : lift.{v, v'} (Module.rank R M') = lift.{v, v'} (Module.rank R M')
Tactic: rw [B.mk_eq_rank'', cnd, B'.mk_eq_rank'']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (hypothesis)
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Free R M'
inst_7 : StrongRankCondition R
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
β : Type v'
B' : Basis β R M'
⊢ Nonempty (M ≃ₗ[R] M')
have this : lift.{v', v} #α = lift.{v, v'} #β
Tactic: have : Cardinal.lift.{v', v} #α = Cardinal.lift.{v, v'} #β := by
    rw [B.mk_eq_rank'', cnd, B'.mk_eq_rank'']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (hypothesis)
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
h : Module.rank R M = 0
⊢ Subsingleton M
have h₁ : IsEmpty.{v + 1} (ChooseBasisIndex R M)
Tactic: rw [← Basis.mk_eq_rank'' (Module.Free.chooseBasis R M), Cardinal.mk_eq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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
⊢ Module.rank R M < ℵ₀ ↔ Module.Finite R M
have rw : Finite.{v + 1} (ChooseBasisIndex R M) ↔ Module.Finite R M
Tactic: rw [Free.rank_eq_card_chooseBasisIndex, mk_lt_aleph0_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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
h : ¬Module.Finite R M
⊢ finrank R M = 0
have rw : Module.rank R M = 0 ∨ ¬Module.Finite R M
Tactic: rw [finrank, toNat_eq_zero, ← not_lt, Module.rank_lt_aleph0_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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
h : 0 < finrank R M
⊢ Module.Finite R M
have contrapose : ∀ (h : ¬Module.Finite R M), ¬0 < finrank R M
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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
n : ℕ
hn : finrank R M = n.succ
⊢ 0 < finrank R M
have rw : 0 < n.succ
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
R : Type u
S : Type u_1
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Semiring S
inst_5 : StrongRankCondition S
inst_6 : Module S M
inst_7 : Module R S
inst_8 : FaithfulSMul R S
inst_9 : Module.Finite R S
inst_10 : IsScalarTower R S S
inst_11 : IsScalarTower R S M
inst_12 : Free S M
⊢ finrank S M ≤ finrank R M
have pos : ∀ (H : Module.Finite S M), finrank S M ≤ finrank R M
Tactic: by_cases H : Module.Finite S M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
R : Type u
S : Type u_1
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Semiring S
inst_5 : StrongRankCondition S
inst_6 : Module S M
inst_7 : Module R S
inst_8 : FaithfulSMul R S
inst_9 : Module.Finite R S
inst_10 : IsScalarTower R S S
inst_11 : IsScalarTower R S M
inst_12 : Free S M
pos : ∀ (H : Module.Finite S M), finrank S M ≤ finrank R M
⊢ finrank S M ≤ finrank R M
have neg : ∀ (H : ¬Module.Finite S M), finrank S M ≤ finrank R M
Tactic: by_cases H : Module.Finite S M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (hypothesis)
Goal:
R : Type u
S : Type u_1
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Semiring S
inst_5 : StrongRankCondition S
inst_6 : Module S M
inst_7 : Module R S
inst_8 : FaithfulSMul R S
inst_9 : Module.Finite R S
inst_10 : IsScalarTower R S S
inst_11 : IsScalarTower R S M
inst_12 : Free S M
H : Module.Finite S M
⊢ finrank S M ≤ finrank R M
have this : Module.Finite R M
Tactic: have := Module.Finite.trans (R := R) S M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
R : Type u
S : Type u_1
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Semiring S
inst_5 : StrongRankCondition S
inst_6 : Module S M
inst_7 : Module R S
inst_8 : FaithfulSMul R S
inst_9 : Module.Finite R S
inst_10 : IsScalarTower R S S
inst_11 : IsScalarTower R S M
inst_12 : Free S M
H : ¬Module.Finite S M
⊢ finrank S M ≤ finrank R M
have neg : 0 ≤ finrank R M
Tactic: rw [finrank, Cardinal.toNat_eq_zero.mpr (.inr _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
R : Type u
S : Type u_1
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Semiring S
inst_5 : StrongRankCondition S
inst_6 : Module S M
inst_7 : Module R S
inst_8 : FaithfulSMul R S
inst_9 : Module.Finite R S
inst_10 : IsScalarTower R S S
inst_11 : IsScalarTower R S M
inst_12 : Free S M
H : ¬Module.Finite S M
neg : 0 ≤ finrank R M
⊢ finrank S M ≤ finrank R M
have rw : ℵ₀ ≤ Module.rank S M
Tactic: rw [finrank, Cardinal.toNat_eq_zero.mpr (.inr _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
R : Type u
S : Type u_1
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Semiring S
inst_5 : StrongRankCondition S
inst_6 : Module S M
inst_7 : Module R S
inst_8 : FaithfulSMul R S
inst_9 : Module.Finite R S
inst_10 : IsScalarTower R S S
inst_11 : IsScalarTower R S M
inst_12 : Free S M
H : ¬Module.Finite S M
⊢ ℵ₀ ≤ Module.rank S M
have rwa : ¬Module.rank S M < ℵ₀
Tactic: rwa [← not_lt, Module.rank_lt_aleph0_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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
⊢ finrank R S ≤ finrank R T
have pos : ∀ (H : Module.Finite R S), finrank R S ≤ finrank R T
Tactic: by_cases H : Module.Finite R S
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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
pos : ∀ (H : Module.Finite R S), finrank R S ≤ finrank R T
⊢ finrank R S ≤ finrank R T
have neg : ∀ (H : ¬Module.Finite R S), finrank R S ≤ finrank R T
Tactic: by_cases H : Module.Finite R S
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (hypothesis)
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
⊢ finrank R S ≤ finrank R T
have this : Module.Finite R T
Tactic: have := Module.Finite.trans (R := R) S T
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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
⊢ finrank R S ≤ finrank R T
have neg : 0 ≤ finrank R T
Tactic: rw [finrank, Cardinal.toNat_eq_zero.mpr (.inr _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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
⊢ finrank R S ≤ finrank R T
have rw : ℵ₀ ≤ Module.rank R S
Tactic: rw [finrank, Cardinal.toNat_eq_zero.mpr (.inr _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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
⊢ ℵ₀ ≤ Module.rank R S
have rwa : ¬Module.rank R S < ℵ₀
Tactic: rwa [← not_lt, Module.rank_lt_aleph0_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (hypothesis)
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
⊢ Nonempty.{max 1 (u_2 + 1)} (Unique ι)
have this : Nontrivial R
Tactic: have : Nontrivial R := nontrivial_of_invariantBasisNumber R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (hypothesis)
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
⊢ Nonempty.{max 1 (u_2 + 1)} (Unique ι)
have this₁ : Module.Finite R M
Tactic: haveI : Module.Finite R M :=
    Module.finite_of_finrank_pos (Nat.lt_of_sub_eq_succ d1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (hypothesis)
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
⊢ Nonempty.{max 1 (u_2 + 1)} (Unique ι)
have this₁ : Finite ι
Tactic: have : Finite ι := Module.Finite.finite_basis b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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 ι
⊢ Nonempty.{max 1 (u_2 + 1)} (Unique ι)
have have : ∀ (this : Fintype ι), Nonempty.{max 1 (u_2 + 1)} (Unique ι)
Tactic: have : Fintype ι := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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 ι
⊢ Nonempty.{max 1 (u_2 + 1)} (Unique ι)
have rwa : ∀ (d1 : Fintype.card ι = 1), Nonempty.{max 1 (u_2 + 1)} (Unique ι)
Tactic: rwa [Module.finrank_eq_card_basis b, Fintype.card_eq_one_iff_nonempty_unique] at d1
Cleared hypotheses: d1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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 ι)
⊢ Nonempty.{max 1 (u_2 + 1)} (Unique ι)
have rwa₁ : ∀ (d1 : Nonempty.{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
Cleared hypotheses: d1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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
⊢ Nonempty (R ≃ₗ[R] M)
have let : ∀ (ι : Type v) (b : Basis ι R M), Nonempty (R ≃ₗ[R] M)
Tactic: let ⟨ι, b⟩ := (Module.Free.exists_basis R M).some
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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
⊢ Nonempty (R ≃ₗ[R] M)
have have : ∀ (this : Unique ι), Nonempty (R ≃ₗ[R] M)
Tactic: have : Unique ι := (b.nonempty_unique_index_of_finrank_eq_one d1).some
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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
⊢ Eq.{u + 1} (α := R) (((((basisUnique ι h).repr : (a : M) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
have rw : Eq.{u + 1} (α := R) ((((basisUnique ι h).repr : (a : M) → ι →₀ R) 0 : (a : ι) → R) i : R) (0 : R)
Tactic: rw [hv, map_zero, Finsupp.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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)
⊢ Eq.{u + 1} (α := R) (((((basisUnique ι h).repr : (a : M) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
have rw₁ : Eq.{u + 1} (α := R) ((0 : (a : ι) → R) i : R) (0 : R)
Tactic: rw [hv, map_zero, Finsupp.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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)
⊢ Eq.{u + 1} (α := R) (((((basisUnique ι h).repr : (a : M) → ι →₀ R) v : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
have rw₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [hv, map_zero, Finsupp.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (hypothesis)
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, u = HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id
have hc : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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
⊢ ∃! c : R, u = HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id
have 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
Tactic: use c
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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
⊢ (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
have h : ∀ (y : R), HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id = HSMul.hSMul (β := M →ₗ[R] M) y LinearMap.id → y = c
Tactic: simp only [this, true_and]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (hypothesis)
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
⊢ d = c
have 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)
Tactic: rw [LinearMap.ext_iff] at hcd
Cleared hypotheses: hcd
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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)
⊢ ∃! c : R, u = HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id
have suffices : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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)
⊢ u = HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id
have h : ∀ (x : M), Eq (α := M) ((u : (a : M) → M) x : M) ((HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id : (a : M) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (hypothesis)
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
⊢ Eq (α := M) ((u : (a : M) → M) x : M) ((HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id : (a : M) → M) x : M)
have 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)
Tactic: have (x : M) : x = (e.symm x) • (e 1) := by simp [← LinearEquiv.map_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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)
⊢ Eq (α := M) ((u : (a : M) → M) x : M) ((HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id : (a : M) → M) x : M)
have 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)
Tactic: rw [this x]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
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)
⊢ 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)
have 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))
Tactic: simp only [hc, map_smul, LinearMap.smul_apply, LinearMap.id_coe, id_eq]