awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.FixedSubmodule (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e : V →ₗ[R] V).fixedSubmodule
x : V
hx : x ∈ W
⊢ x ∈ map (DistribSMul.toLinearMap R V e) W
have a : (DistribSMul.toLinearMap R V e : (a : V) → V) x = x
Tactic: refine ⟨x, hx, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FixedSubmodule (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e : V →ₗ[R] V).fixedSubmodule
x : V
hx : x ∈ W
⊢ (DistribSMul.toLinearMap R V e : (a : V) → V) x = x
have a : (e : (a : V) → V) x = x
Tactic: simp only [DistribSMul.toLinearMap_apply, LinearEquiv.smul_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FixedSubmodule (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
he : Membership.mem (γ := Subgroup (V ≃ₗ[R] V)) (fixingSubgroup (V ≃ₗ[R] V) W.carrier) e
⊢ map (↑e : V →ₗ[R] V) W = W
have h : ∀ (v : V), v ∈ map (↑e : V →ₗ[R] V) W ↔ v ∈ W
Tactic: ext v
-- Lean 4 proof step from Mathlib.LinearAlgebra.FixedSubmodule (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
he : Membership.mem (γ := Subgroup (V ≃ₗ[R] V)) (fixingSubgroup (V ≃ₗ[R] V) W.carrier) e
v : V
⊢ v ∈ map (↑e : V →ₗ[R] V) W ↔ v ∈ W
have he₁ : ∀ y ∈ W, (e : (a : V) → V) y = y
Tactic: simp only [mem_fixingSubgroup_iff, carrier_eq_coe, SetLike.mem_coe, LinearEquiv.smul_def] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.LinearAlgebra.FixedSubmodule (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
v : V
he : ∀ y ∈ W, (e : (a : V) → V) y = y
⊢ v ∈ map (↑e : V →ₗ[R] V) W ↔ v ∈ W
have h : v ∈ map (↑e : V →ₗ[R] V) W → ∀ (w : V) (hv : w ∈ (↑W : Set V)) (hv' : ((↑e : V →ₗ[R] V) : (a : V) → V) w = v), v ∈ W
Tactic: refine ⟨fun ⟨w, hv, hv'⟩ ↦ ?_, fun hv ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FixedSubmodule (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
v : V
he : ∀ y ∈ W, (e : (a : V) → V) y = y
h : v ∈ map (↑e : V →ₗ[R] V) W → ∀ (w : V) (hv : w ∈ (↑W : Set V)) (hv' : ((↑e : V →ₗ[R] V) : (a : V) → V) w = v), v ∈ W
⊢ v ∈ map (↑e : V →ₗ[R] V) W ↔ v ∈ W
have h₁ : ∀ (hv : v ∈ W), v ∈ map (↑e : V →ₗ[R] V) W
Tactic: refine ⟨fun ⟨w, hv, hv'⟩ ↦ ?_, fun hv ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FixedSubmodule (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
v : V
he : ∀ y ∈ W, (e : (a : V) → V) y = y
h : v ∈ map (↑e : V →ₗ[R] V) W
w : V
hv : w ∈ (↑W : Set V)
hv' : ((↑e : V →ₗ[R] V) : (a : V) → V) w = v
⊢ v ∈ W
have hv₁ : w ∈ W
Tactic: simp only [SetLike.mem_coe, coe_coe] at hv hv'
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.FixedSubmodule (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_3
inst_1 : AddCommMonoid V
inst_2 : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
v : V
he : ∀ y ∈ W, (e : (a : V) → V) y = y
h : v ∈ map (↑e : V →ₗ[R] V) W
w : V
hv' : (e : (a : V) → V) w = v
hv : w ∈ W
⊢ v ∈ W
have h : Membership.mem (α := V) W ((e : (a : V) → V) w : V)
Tactic: rwa [← hv', he w hv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FixedSubmodule (goal)
Goal:
R_1 : Type u_1
inst : Semiring R_1
U : Type u_2
V_1 : Type u_3
inst_1 : AddCommMonoid U
inst_2 : AddCommMonoid V_1
inst_3 : Module R_1 U
inst_4 : Module R_1 V_1
e : V_1 ≃ₗ[R_1] V_1
P : Submodule R_1 U
Q : Submodule R_1 V_1
R : Type u_4
V : Type u_5
inst_5 : Ring R
inst_6 : AddCommGroup V
inst_7 : Module R V
W : Submodule R V
u v : ↥(stabilizer (V ≃ₗ[R] V) W)
⊢ Quotient.equiv W W (↑(u * v) : V ≃ₗ[R] V) ⋯ =
    Quotient.equiv W W (↑u : V ≃ₗ[R] V) ⋯ * Quotient.equiv W W (↑v : V ≃ₗ[R] V) ⋯
have h : ∀ (x : V ⧸ W),
  Eq (α := V ⧸ W) ((Quotient.equiv W W (↑(u * v) : V ≃ₗ[R] V) sorry : (a : V ⧸ W) → V ⧸ W) x : V ⧸ W)
    ((Quotient.equiv W W (↑u : V ≃ₗ[R] V) sorry * Quotient.equiv W W (↑v : V ≃ₗ[R] V) sorry : (a : V ⧸ W) → V ⧸ W) x : V ⧸ W)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.FixedSubmodule (goal)
Goal:
R_1 : Type u_1
inst : Semiring R_1
U : Type u_2
V_1 : Type u_3
inst_1 : AddCommMonoid U
inst_2 : AddCommMonoid V_1
inst_3 : Module R_1 U
inst_4 : Module R_1 V_1
e : V_1 ≃ₗ[R_1] V_1
P : Submodule R_1 U
Q : Submodule R_1 V_1
R : Type u_4
V : Type u_5
inst_5 : Ring R
inst_6 : AddCommGroup V
inst_7 : Module R V
W : Submodule R V
u v : ↥(stabilizer (V ≃ₗ[R] V) W)
x : V ⧸ W
⊢ Eq (α := V ⧸ W) ((Quotient.equiv W W (↑(u * v) : V ≃ₗ[R] V) ⋯ : (a : V ⧸ W) → V ⧸ W) x : V ⧸ W)
    ((Quotient.equiv W W (↑u : V ≃ₗ[R] V) ⋯ * Quotient.equiv W W (↑v : V ≃ₗ[R] V) ⋯ : (a : V ⧸ W) → V ⧸ W) x : V ⧸ W)
have h : ∀ (y : V),
  Eq (α := V ⧸ W)
    ((Quotient.equiv W W (↑(u * v) : V ≃ₗ[R] V) sorry : (a : V ⧸ W) → V ⧸ W) ((W.mkQ : (a : V) → V ⧸ W) y) : V ⧸ W)
    ((Quotient.equiv W W (↑u : V ≃ₗ[R] V) sorry * Quotient.equiv W W (↑v : V ≃ₗ[R] V) sorry : (a : V ⧸ W) → V ⧸ W)
        ((W.mkQ : (a : V) → V ⧸ W) y) :
      V ⧸ W)
Tactic: obtain ⟨y, rfl⟩ := W.mkQ_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.FixedSubmodule (goal)
Goal:
R : Type u_4
V : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
a : R
⊢ (∀ (x : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule),
      (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x = a • x) ↔
    ∀ (v : V), HSub.hSub (α := V) ((e : (a : V) → V) v : V) (a • v) ∈ (↑e : V →ₗ[R] V).fixedSubmodule
have simp : (∀ (x : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule),
    (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x = a • x) ↔
  ∀ (v : V),
    Eq (α := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
      ((e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
          (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) v) :
        V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
      (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) (a • v) :
        V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
Tactic: simp only [← e.fixedSubmodule.ker_mkQ, mem_ker, map_sub, ← fixedReduce_mkQ, sub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FixedSubmodule (goal)
Goal:
R : Type u_4
V : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
a : R
⊢ (∀ (x : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule),
      (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x = a • x) ↔
    ∀ (v : V),
      Eq (α := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
        ((e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
            (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) v) :
          V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
        (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) (a • v) :
          V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
have mp : (∀ (x : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule),
    (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x = a • x) →
  ∀ (v : V),
    Eq (α := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
      ((e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
          (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) v) :
        V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
      (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) (a • v) :
        V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.FixedSubmodule (goal)
Goal:
R : Type u_4
V : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
a : R
mp :
  (∀ (x : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule),
      (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x = a • x) →
    ∀ (v : V),
      Eq (α := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
        ((e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
            (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) v) :
          V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
        (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) (a • v) :
          V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
⊢ (∀ (x : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule),
      (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x = a • x) ↔
    ∀ (v : V),
      Eq (α := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
        ((e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
            (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) v) :
          V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
        (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) (a • v) :
          V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
have mpr : (∀ (v : V),
    Eq (α := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
      ((e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
          (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) v) :
        V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
      (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) (a • v) :
        V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)) →
  ∀ (x : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule),
    (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x = a • x
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.FixedSubmodule (goal)
Goal:
R : Type u_4
V : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
a : R
H :
  ∀ (v : V),
    Eq (α := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
      ((e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
          (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) v) :
        V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
      (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) (a • v) :
        V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
x : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule
⊢ (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x = a • x
have mpr : ∀ (y : V) (hy : ((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) y = x),
  (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x = a • x
Tactic: have ⟨y, hy⟩ := e.fixedSubmodule.mkQ_surjective x
-- Lean 4 proof step from Mathlib.LinearAlgebra.FixedSubmodule (goal)
Goal:
R : Type u_4
V : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
e : V ≃ₗ[R] V
a : R
H :
  ∀ (v : V),
    Eq (α := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
      ((e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
          (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) v) :
        V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
      (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) (a • v) :
        V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
x : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule
y : V
hy : ((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) y = x
⊢ (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) x = a • x
have mpr : (e.fixedReduce : (a : V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
    (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) y) =
  HSMul.hSMul (β := V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) a
    (((↑e : V →ₗ[R] V).fixedSubmodule.mkQ : (a : V) → V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule) y :
      V ⧸ (↑e : V →ₗ[R] V).fixedSubmodule)
Tactic: rw [← hy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeAlgebra (goal)
Goal:
R : Type u
X : Type v
inst : CommRing R
inst_1 : Nontrivial R
⊢ Module.rank R (FreeAlgebra R X) = Cardinal.lift.{u, v} (Cardinal.mk (List X))
have rw : Cardinal.lift.{max u v, v} (Cardinal.mk (FreeMonoid X)) = Cardinal.lift.{u, v} (Cardinal.mk (List X))
Tactic: rw [← (Basis.mk_eq_rank'.{_, _, _, u} (basisFreeMonoid R X)).trans (Cardinal.lift_id _),
    Cardinal.lift_umax.{v, u}, FreeMonoid]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeAlgebra (goal)
Goal:
R : Type u
X : Type v
inst : CommRing R
inst_1 : Nontrivial R
rw : Cardinal.lift.{max u v, v} (Cardinal.mk (FreeMonoid X)) = Cardinal.lift.{u, v} (Cardinal.mk (List X))
⊢ Module.rank R (FreeAlgebra R X) = Cardinal.lift.{u, v} (Cardinal.mk (List X))
have rw₁ : Cardinal.lift.{u, v} (Cardinal.mk (FreeMonoid X)) = Cardinal.lift.{u, v} (Cardinal.mk (List X))
Tactic: rw [← (Basis.mk_eq_rank'.{_, _, _, u} (basisFreeMonoid R X)).trans (Cardinal.lift_id _),
    Cardinal.lift_umax.{v, u}, FreeMonoid]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeAlgebra (goal)
Goal:
R : Type u
X : Type v
inst : CommRing R
inst_1 : Nontrivial R
rw : Cardinal.lift.{max u v, v} (Cardinal.mk (FreeMonoid X)) = Cardinal.lift.{u, v} (Cardinal.mk (List X))
rw₁ : Cardinal.lift.{u, v} (Cardinal.mk (FreeMonoid X)) = Cardinal.lift.{u, v} (Cardinal.mk (List X))
⊢ Module.rank R (FreeAlgebra R X) = Cardinal.lift.{u, v} (Cardinal.mk (List X))
have rw₂ : Cardinal.lift.{u, v} (Cardinal.mk (List X)) = Cardinal.lift.{u, v} (Cardinal.mk (List X))
Tactic: rw [← (Basis.mk_eq_rank'.{_, _, _, u} (basisFreeMonoid R X)).trans (Cardinal.lift_id _),
    Cardinal.lift_umax.{v, u}, FreeMonoid]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeAlgebra (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : Set S
⊢ Module.rank R ↥(adjoin R s) ≤ max #(↑s : Type v) ℵ₀
have rw : Module.rank R
    ↥(AlgHom.range (A := FreeAlgebra.{u, v} R { x : S // x ∈ s })
        ((FreeAlgebra.lift R : (a : { x : S // x ∈ s } → S) → FreeAlgebra R { x : S // x ∈ s } →ₐ[R] S)
          (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) ≤
  max #(↑s : Type v) ℵ₀
Tactic: rw [adjoin_eq_range_freeAlgebra_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeAlgebra (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : Set S
⊢ Module.rank R
      ↥(AlgHom.range (A := FreeAlgebra.{u, v} R { x : S // x ∈ s })
          ((FreeAlgebra.lift R : (a : { x : S // x ∈ s } → S) → FreeAlgebra R { x : S // x ∈ s } →ₐ[R] S)
            (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) ≤
    max #(↑s : Type v) ℵ₀
have inl : Subsingleton R →
  Module.rank R
      ↥(AlgHom.range (A := FreeAlgebra.{u, v} R { x : S // x ∈ s })
          ((FreeAlgebra.lift R : (a : { x : S // x ∈ s } → S) → FreeAlgebra R { x : S // x ∈ s } →ₐ[R] S)
            (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) ≤
    max #(↑s : Type v) ℵ₀
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeAlgebra (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : Set S
inl :
  Subsingleton R →
    Module.rank R
        ↥(AlgHom.range (A := FreeAlgebra.{u, v} R { x : S // x ∈ s })
            ((FreeAlgebra.lift R : (a : { x : S // x ∈ s } → S) → FreeAlgebra R { x : S // x ∈ s } →ₐ[R] S)
              (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) ≤
      max #(↑s : Type v) ℵ₀
⊢ Module.rank R
      ↥(AlgHom.range (A := FreeAlgebra.{u, v} R { x : S // x ∈ s })
          ((FreeAlgebra.lift R : (a : { x : S // x ∈ s } → S) → FreeAlgebra R { x : S // x ∈ s } →ₐ[R] S)
            (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) ≤
    max #(↑s : Type v) ℵ₀
have inr : Nontrivial R →
  Module.rank R
      ↥(AlgHom.range (A := FreeAlgebra.{u, v} R { x : S // x ∈ s })
          ((FreeAlgebra.lift R : (a : { x : S // x ∈ s } → S) → FreeAlgebra R { x : S // x ∈ s } →ₐ[R] S)
            (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) ≤
    max #(↑s : Type v) ℵ₀
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeAlgebra (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : Set S
h : Subsingleton R
⊢ Module.rank R
      ↥(AlgHom.range (A := FreeAlgebra.{u, v} R { x : S // x ∈ s })
          ((FreeAlgebra.lift R : (a : { x : S // x ∈ s } → S) → FreeAlgebra R { x : S // x ∈ s } →ₐ[R] S)
            (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) ≤
    max #(↑s : Type v) ℵ₀
have inl : 1 ≤ max #(↑s : Type v) ℵ₀
Tactic: rw [rank_subsingleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeAlgebra (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : Set S
h : Nontrivial R
⊢ Module.rank R
      ↥(AlgHom.range (A := FreeAlgebra.{u, v} R { x : S // x ∈ s })
          ((FreeAlgebra.lift R : (a : { x : S // x ∈ s } → S) → FreeAlgebra R { x : S // x ∈ s } →ₐ[R] S)
            (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) ≤
    max #(↑s : Type v) ℵ₀
have inr : lift.{max u v, v}
    (Module.rank R
      ↥(AlgHom.range (A := FreeAlgebra.{u, v} R { x : S // x ∈ s })
          ((FreeAlgebra.lift R : (a : { x : S // x ∈ s } → S) → FreeAlgebra R { x : S // x ∈ s } →ₐ[R] S)
            (Subtype.val (p := fun (x : S) ↦ x ∈ s))))) ≤
  lift.{max u v, v} (max #(↑s : Type v) ℵ₀)
Tactic: rw [← lift_le.{max u v}]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeAlgebra (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : Set S
h : Nontrivial R
⊢ lift.{max u v, v}
      (Module.rank R
        ↥(AlgHom.range (A := FreeAlgebra.{u, v} R { x : S // x ∈ s })
            ((FreeAlgebra.lift R : (a : { x : S // x ∈ s } → S) → FreeAlgebra R { x : S // x ∈ s } →ₐ[R] S)
              (Subtype.val (p := fun (x : S) ↦ x ∈ s))))) ≤
    lift.{max u v, v} (max #(↑s : Type v) ℵ₀)
have inr : lift.{v, max u v} (Module.rank R (FreeAlgebra.{u, v} R { x : S // x ∈ s })) ≤ lift.{max u v, v} (max #(↑s : Type v) ℵ₀)
Tactic: refine (lift_rank_range_le (FreeAlgebra.lift R ((↑) : s → S)).toLinearMap).trans ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeAlgebra (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : Set S
h : Nontrivial R
⊢ lift.{v, max u v} (Module.rank R (FreeAlgebra.{u, v} R { x : S // x ∈ s })) ≤
    lift.{max u v, v} (max #(↑s : Type v) ℵ₀)
have inr : #(List { x : S // x ∈ s }) ≤ max ℵ₀ #(↑s : Type v)
Tactic: rw [FreeAlgebra.rank_eq, lift_id'.{v, u}, lift_umax.{v, u}, lift_le, max_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Basic (goal)
Goal:
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
σ : R →+* R'
σ' : R' →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] M'
inst_8 : Free R M
e₁ : R ≃+* R' := RingHomInvPair.toRingEquiv σ σ'
I : Type u_4 := ChooseBasisIndex R M
⊢ Free R' M'
have obtain : ∀ (e₃ : M ≃ₗ[R] I →₀ R), Free R' M'
Tactic: obtain ⟨e₃ : M ≃ₗ[R] I →₀ R⟩ := Module.Free.chooseBasis R M
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Basic (hypothesis)
Goal:
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
σ : R →+* R'
σ' : R' →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] M'
inst_8 : Free R M
e₁ : R ≃+* R' := RingHomInvPair.toRingEquiv σ σ'
I : Type u_4 := ChooseBasisIndex R M
e₃ : M ≃ₗ[R] I →₀ R
e : M' ≃+ (I →₀ R') := (LinearEquiv.toAddEquiv (e₂.symm.trans e₃)).trans (Finsupp.mapRange.addEquiv e₁.toAddEquiv)
⊢ Free R' M'
have he : ∀ (x : M'),
  Eq (α := I →₀ R') ((e : (a : M') → I →₀ R') x : I →₀ R')
    ((Finsupp.mapRange.addEquiv e₁.toAddEquiv : (a : I →₀ R) → I →₀ R')
        ((e₃ : (a : M) → I →₀ R) ((e₂.symm : (a : M') → M) x)) :
      I →₀ R')
Tactic: have he (x) : e x = Finsupp.mapRange.addEquiv (ι := I) e₁.toAddEquiv (e₃ (e₂.symm x)) := rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Basic (goal)
Goal:
R : Type u
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
ι : Type u_3
B : Basis ι R S
i : ι
hBi : Eq.{u_2 + 1} (α := S) ((B : (a : ι) → S) i : S) (1 : S)
r : R
⊢ Eq (α := ι →₀ R) ((B.repr : (a : S) → ι →₀ R) ((algebraMap R S : (a : R) → S) r) : ι →₀ R)
    (Finsupp.single i r : ι →₀ R)
have h : ∀ (j : ι),
  Eq.{u + 1} (α := R) ((((B.repr : (a : S) → ι →₀ R) ((algebraMap R S : (a : R) → S) r) : ι →₀ R) : (a : ι) → R) j : R)
    ((Finsupp.single i r : (a : ι) → R) j : R)
Tactic: ext j
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
f : End R M
⊢ Membership.mem (γ := Set (End R M)) (Set.center (End R M)) f ↔ ∃ (α : R) (hα : α ∈ Set.center R), f = smulLeft α hα
have simp : (∀ (g : End R M) (x : M),
    Eq (α := M) ((g : (a : M) → M) ((f : (a : M) → M) x : M) : M) ((f : (a : M) → M) ((g : (a : M) → M) x : M) : M)) ↔
  ∃ (α : R) (h : ∀ (g : R), g * α = α * g),
    ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((smulLeft α sorry : (a : M) → M) x : M)
Tactic: simp only [Semigroup.mem_center_iff, LinearMap.ext_iff, mul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
f : End R M
⊢ (∀ (g : End R M) (x : M),
      Eq (α := M) ((g : (a : M) → M) ((f : (a : M) → M) x : M) : M) ((f : (a : M) → M) ((g : (a : M) → M) x : M) : M)) ↔
    ∃ (α : R) (h : ∀ (g : R), g * α = α * g),
      ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((smulLeft α ⋯ : (a : M) → M) x : M)
have refine : ∀
  (h :
    ∀ (g : End R M) (x : M),
      Eq (α := M) ((g : (a : M) → M) ((f : (a : M) → M) x : M) : M) ((f : (a : M) → M) ((g : (a : M) → M) x : M) : M)),
  ∃ (α : R) (h : ∀ (g : R), g * α = α * g),
    ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((smulLeft α sorry : (a : M) → M) x : M)
Tactic: refine ⟨fun h ↦ ?_, by simp_all⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
f : End R M
h :
  ∀ (g : End R M) (x : M),
    Eq (α := M) ((g : (a : M) → M) ((f : (a : M) → M) x : M) : M) ((f : (a : M) → M) ((g : (a : M) → M) x : M) : M)
⊢ ∃ (α : R) (h : ∀ (g : R), g * α = α * g),
    ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((smulLeft α ⋯ : (a : M) → M) x : M)
have pos : Subsingleton M →
  ∃ (α : R) (h : ∀ (g : R), g * α = α * g),
    ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((smulLeft α sorry : (a : M) → M) x : M)
Tactic: by_cases! Subsingleton M
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
f : End R M
h :
  ∀ (g : End R M) (x : M),
    Eq (α := M) ((g : (a : M) → M) ((f : (a : M) → M) x : M) : M) ((f : (a : M) → M) ((g : (a : M) → M) x : M) : M)
pos :
  Subsingleton M →
    ∃ (α : R) (h : ∀ (g : R), g * α = α * g),
      ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((smulLeft α ⋯ : (a : M) → M) x : M)
⊢ ∃ (α : R) (h : ∀ (g : R), g * α = α * g),
    ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((smulLeft α ⋯ : (a : M) → M) x : M)
have neg : Nontrivial M →
  ∃ (α : R) (h : ∀ (g : R), g * α = α * g),
    ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((smulLeft α sorry : (a : M) → M) x : M)
Tactic: by_cases! Subsingleton M