awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring S
inst_1 : CommSemiring R
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
B : Type u_4
inst_6 : Semiring B
inst_7 : Algebra S B
inst_8 : Algebra S R
inst_9 : DistribMulAction S A
inst_10 : IsScalarTower S R A
C : Type u_5
inst_11 : Semiring C
inst_12 : Algebra R C
φ : Unitization R A →ₐ[R] C
⊢ NonUnitalAlgHom.toAlgHom
      ((fun (φ : Unitization R A →ₐ[R] C) ↦ (↑φ : Unitization R A →ₙₐ[R] C).comp (inrNonUnitalAlgHom R A)) φ) =
    φ
have h : ∀ (x : A),
  Eq.{u_5 + 1} (α := C)
    ((NonUnitalAlgHom.comp
            (↑(NonUnitalAlgHom.toAlgHom
                  ((fun (φ : Unitization R A →ₐ[R] C) ↦ (↑φ : Unitization R A →ₙₐ[R] C).comp (inrNonUnitalAlgHom R A))
                    φ)) :
              Unitization R A →ₙₐ[R] C)
            (inrNonUnitalAlgHom R A) :
          (a : A) → C)
        x :
      C)
    (((↑φ : Unitization R A →ₙₐ[R] C).comp (inrNonUnitalAlgHom R A) : (a : A) → C) x : C)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
⊢ Eq (α := (a : Unitization R A) → R) (⇑(NonUnitalAlgHom.toAlgHom 0) : (a : Unitization R A) → R)
    fun (x : Unitization R A) ↦ x.toProd.1
have h : ∀ (x : Unitization R A), (NonUnitalAlgHom.toAlgHom 0 : (a : Unitization R A) → R) x = x.toProd.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : StarRing C
inst_10 : StarModule R C
x : A →⋆ₙₐ[R] C
⊢ (fun (φ : Unitization R A →⋆ₐ[R] C) ↦ φ.toNonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom R A))
      ((fun (φ : A →⋆ₙₐ[R] C) ↦
          let __AlgHom : Unitization R A →ₐ[R] C :=
            (lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) φ.toNonUnitalAlgHom;
          ({ toAlgHom := __AlgHom, map_star' := ⋯ } : Unitization R A →⋆ₐ[R] C))
        x) =
    x
have h : ∀ (x_1 : A),
  Eq.{u_3 + 1} (α := C)
    (((fun (φ : Unitization R A →⋆ₐ[R] C) ↦ φ.toNonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom R A))
            ((fun (φ : A →⋆ₙₐ[R] C) ↦
                let __AlgHom : Unitization R A →ₐ[R] C :=
                  (lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) φ.toNonUnitalAlgHom;
                ({ toAlgHom := __AlgHom, map_star' := sorry } : Unitization R A →⋆ₐ[R] C))
              x) :
          (a : A) → C)
        x_1 :
      C)
    ((x : (a : A) → C) x_1 : C)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
R : Type u_1
A : Type u_2
C : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : StarRing C
inst_10 : StarModule R C
x : Unitization R A →⋆ₐ[R] C
⊢ (fun (φ : A →⋆ₙₐ[R] C) ↦
        let __AlgHom : Unitization R A →ₐ[R] C :=
          (lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) φ.toNonUnitalAlgHom;
        ({ toAlgHom := __AlgHom, map_star' := ⋯ } : Unitization R A →⋆ₐ[R] C))
      ((fun (φ : Unitization R A →⋆ₐ[R] C) ↦ φ.toNonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom R A)) x) =
    x
have h : ∀ (x_1 : A),
  Eq.{u_3 + 1} (α := C)
    ((NonUnitalStarAlgHom.comp
            (↑((fun (φ : A →⋆ₙₐ[R] C) ↦
                    let __AlgHom : Unitization R A →ₐ[R] C :=
                      (lift : (a : A →ₙₐ[R] C) → Unitization R A →ₐ[R] C) φ.toNonUnitalAlgHom;
                    ({ toAlgHom := __AlgHom, map_star' := sorry } : Unitization R A →⋆ₐ[R] C))
                  ((fun (φ : Unitization R A →⋆ₐ[R] C) ↦ φ.toNonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom R A))
                    x)) :
              Unitization R A →⋆ₙₐ[R] C)
            (inrNonUnitalStarAlgHom R A) :
          (a : A) → C)
        x_1 :
      C)
    ((NonUnitalStarAlgHom.comp (↑x : Unitization R A →⋆ₙₐ[R] C) (inrNonUnitalStarAlgHom R A) : (a : A) → C) x_1 : C)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : NonUnitalSemiring B
inst_8 : StarRing B
inst_9 : Module R B
inst_10 : SMulCommClass R B B
inst_11 : IsScalarTower R B B
inst_12 : StarModule R B
φ : A →⋆ₙₐ[R] B
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
x y : Unitization R A
h :
  Eq (α := Unitization R B) ((starMap φ : (a : Unitization R A) → Unitization R B) x : Unitization R B)
    ((starMap φ : (a : Unitization R A) → Unitization R B) y : Unitization R B)
⊢ x = y
have fst : x.toProd.1 = y.toProd.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : NonUnitalSemiring B
inst_8 : StarRing B
inst_9 : Module R B
inst_10 : SMulCommClass R B B
inst_11 : IsScalarTower R B B
inst_12 : StarModule R B
φ : A →⋆ₙₐ[R] B
hφ : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
x y : Unitization R A
h :
  Eq (α := Unitization R B) ((starMap φ : (a : Unitization R A) → Unitization R B) x : Unitization R B)
    ((starMap φ : (a : Unitization R A) → Unitization R B) y : Unitization R B)
fst : x.toProd.1 = y.toProd.1
⊢ x = y
have snd : x.toProd.2 = y.toProd.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : NonUnitalSemiring B
inst_8 : StarRing B
inst_9 : Module R B
inst_10 : SMulCommClass R B B
inst_11 : IsScalarTower R B B
inst_12 : StarModule R B
φ : A →⋆ₙₐ[R] B
hφ : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
r : R
b : B
⊢ ∃ (a : Unitization R A), (starMap φ : (a : Unitization R A) → Unitization R B) a = inl r + (↑b : Unitization R B)
have inl_add_inr : ∀ (a : A),
  ∃ (a_1 : Unitization R A),
    (starMap φ : (a : Unitization R A) → Unitization R B) a_1 =
      HAdd.hAdd (α := Unitization R B) (β := Unitization R B) (inl r : Unitization R B)
        ((↑((φ : (a : A) → B) a) : Unitization R B) : Unitization R B)
Tactic: obtain ⟨a, rfl⟩ := hφ b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : NonUnitalSemiring B
inst_8 : StarRing B
inst_9 : Module R B
inst_10 : SMulCommClass R B B
inst_11 : IsScalarTower R B B
inst_12 : StarModule R B
φ : A →⋆ₙₐ[R] B
hφ : Function.Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
x : Unitization R B
⊢ ∃ (a : Unitization R A), (starMap φ : (a : Unitization R A) → Unitization R B) a = x
have inl_add_inr : ∀ (r : R) (b : B),
  ∃ (a : Unitization R A), (starMap φ : (a : Unitization R A) → Unitization R B) a = inl r + (↑b : Unitization R B)
Tactic: induction x using Unitization.ind with
  | inl_add_inr r b =>
    obtain ⟨a, rfl⟩ := hφ b
    exact ⟨mk (r, a), by rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : NonUnitalSemiring B
inst_8 : StarRing B
inst_9 : Module R B
inst_10 : SMulCommClass R B B
inst_11 : IsScalarTower R B B
inst_12 : NonUnitalSemiring C
inst_13 : StarRing C
inst_14 : Module R C
inst_15 : SMulCommClass R C C
inst_16 : IsScalarTower R C C
inst_17 : StarModule R B
inst_18 : StarModule R C
φ : A →⋆ₙₐ[R] B
ψ : B →⋆ₙₐ[R] C
⊢ Eq (α := Unitization R A →⋆ₐ[R] Unitization R C) (starMap (ψ.comp φ)) (StarAlgHom.comp (starMap ψ) (starMap φ))
have h : ∀ (x : A),
  Eq.{u_1 + 1} (α := R)
    (toProd
        ((NonUnitalStarAlgHom.comp (↑(starMap (ψ.comp φ)) : Unitization R A →⋆ₙₐ[R] Unitization R C)
              (inrNonUnitalStarAlgHom R A) :
            (a : A) → Unitization R C)
          x)).1
    (toProd
        ((NonUnitalStarAlgHom.comp
              (↑(StarAlgHom.comp (starMap ψ) (starMap φ)) : Unitization R A →⋆ₙₐ[R] Unitization R C)
              (inrNonUnitalStarAlgHom R A) :
            (a : A) → Unitization R C)
          x)).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : SMulCommClass R A A
inst_6 : IsScalarTower R A A
inst_7 : NonUnitalSemiring B
inst_8 : StarRing B
inst_9 : Module R B
inst_10 : SMulCommClass R B B
inst_11 : IsScalarTower R B B
inst_12 : NonUnitalSemiring C
inst_13 : StarRing C
inst_14 : Module R C
inst_15 : SMulCommClass R C C
inst_16 : IsScalarTower R C C
inst_17 : StarModule R B
inst_18 : StarModule R C
φ : A →⋆ₙₐ[R] B
ψ : B →⋆ₙₐ[R] C
h :
  ∀ (x : A),
    Eq.{u_1 + 1} (α := R)
      (toProd
          ((NonUnitalStarAlgHom.comp (↑(starMap (ψ.comp φ)) : Unitization R A →⋆ₙₐ[R] Unitization R C)
                (inrNonUnitalStarAlgHom R A) :
              (a : A) → Unitization R C)
            x)).1
      (toProd
          ((NonUnitalStarAlgHom.comp
                (↑(StarAlgHom.comp (starMap ψ) (starMap φ)) : Unitization R A →⋆ₙₐ[R] Unitization R C)
                (inrNonUnitalStarAlgHom R A) :
              (a : A) → Unitization R C)
            x)).1
⊢ Eq (α := Unitization R A →⋆ₐ[R] Unitization R C) (starMap (ψ.comp φ)) (StarAlgHom.comp (starMap ψ) (starMap φ))
have h₁ : ∀ (x : A),
  Eq.{u_4 + 1} (α := C)
    (toProd
        ((NonUnitalStarAlgHom.comp (↑(starMap (ψ.comp φ)) : Unitization R A →⋆ₙₐ[R] Unitization R C)
              (inrNonUnitalStarAlgHom R A) :
            (a : A) → Unitization R C)
          x)).2
    (toProd
        ((NonUnitalStarAlgHom.comp
              (↑(StarAlgHom.comp (starMap ψ) (starMap φ)) : Unitization R A →⋆ₙₐ[R] Unitization R C)
              (inrNonUnitalStarAlgHom R A) :
            (a : A) → Unitization R C)
          x)).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
R : Type u_1
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring B
inst_3 : StarRing B
inst_4 : Module R B
inst_5 : SMulCommClass R B B
inst_6 : IsScalarTower R B B
inst_7 : StarModule R B
⊢ Eq (α := Unitization R B →⋆ₐ[R] Unitization R B) (starMap (NonUnitalStarAlgHom.id R B))
    (StarAlgHom.id R (Unitization R B))
have h : ∀ (x : B),
  Eq.{u_1 + 1} (α := R)
    (toProd
        ((NonUnitalStarAlgHom.comp (↑(starMap (NonUnitalStarAlgHom.id R B)) : Unitization R B →⋆ₙₐ[R] Unitization R B)
              (inrNonUnitalStarAlgHom R B) :
            (a : B) → Unitization R B)
          x)).1
    (toProd
        ((NonUnitalStarAlgHom.comp (↑(StarAlgHom.id R (Unitization R B)) : Unitization R B →⋆ₙₐ[R] Unitization R B)
              (inrNonUnitalStarAlgHom R B) :
            (a : B) → Unitization R B)
          x)).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
R : Type u_1
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring B
inst_3 : StarRing B
inst_4 : Module R B
inst_5 : SMulCommClass R B B
inst_6 : IsScalarTower R B B
inst_7 : StarModule R B
h :
  ∀ (x : B),
    Eq.{u_1 + 1} (α := R)
      (toProd
          ((NonUnitalStarAlgHom.comp (↑(starMap (NonUnitalStarAlgHom.id R B)) : Unitization R B →⋆ₙₐ[R] Unitization R B)
                (inrNonUnitalStarAlgHom R B) :
              (a : B) → Unitization R B)
            x)).1
      (toProd
          ((NonUnitalStarAlgHom.comp (↑(StarAlgHom.id R (Unitization R B)) : Unitization R B →⋆ₙₐ[R] Unitization R B)
                (inrNonUnitalStarAlgHom R B) :
              (a : B) → Unitization R B)
            x)).1
⊢ Eq (α := Unitization R B →⋆ₐ[R] Unitization R B) (starMap (NonUnitalStarAlgHom.id R B))
    (StarAlgHom.id R (Unitization R B))
have h₁ : ∀ (x : B),
  Eq.{u_3 + 1} (α := B)
    (toProd
        ((NonUnitalStarAlgHom.comp (↑(starMap (NonUnitalStarAlgHom.id R B)) : Unitization R B →⋆ₙₐ[R] Unitization R B)
              (inrNonUnitalStarAlgHom R B) :
            (a : B) → Unitization R B)
          x)).2
    (toProd
        ((NonUnitalStarAlgHom.comp (↑(StarAlgHom.id R (Unitization R B)) : Unitization R B →⋆ₙₐ[R] Unitization R B)
              (inrNonUnitalStarAlgHom R B) :
            (a : B) → Unitization R B)
          x)).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.ZMod (goal)
Goal:
R : Type u_1
inst : Ring R
n m : ℕ
inst_1 : CharP R m
h : m ∣ n
a : ZMod n
r : R
⊢ a.cast * r = r * a.cast
have rcases : ∀ (k : ℤ), cast (n := n) (↑k : ZMod n) * r = r * cast (n := n) (↑k : ZMod n)
Tactic: rcases ZMod.intCast_surjective a with ⟨k, rfl⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Algebra.ZMod (goal)
Goal:
R : Type u_1
inst : Ring R
n m : ℕ
inst_1 : CharP R m
h : m ∣ n
r : R
k : ℤ
⊢ cast (n := n) (↑k : ZMod n) * r = r * cast (n := n) (↑k : ZMod n)
have change : HMul.hMul (α := R) ((castHom h R : (a : ZMod n) → R) (↑k : ZMod n) : R) r =
  HMul.hMul (β := R) r ((castHom h R : (a : ZMod n) → R) (↑k : ZMod n) : R)
Tactic: change ZMod.castHom h R k * r = r * ZMod.castHom h R k
-- Lean 4 proof step from Mathlib.Algebra.Algebra.ZMod (goal)
Goal:
R : Type u_1
inst : Ring R
n m : ℕ
inst_1 : CharP R m
h : m ∣ n
r : R
k : ℤ
⊢ HMul.hMul (α := R) ((castHom h R : (a : ZMod n) → R) (↑k : ZMod n) : R) r =
    HMul.hMul (β := R) r ((castHom h R : (a : ZMod n) → R) (↑k : ZMod n) : R)
have rw : (↑k : R) * r = r * (↑k : R)
Tactic: rw [map_intCast, Int.cast_comm]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.ZMod (goal)
Goal:
R : Type u_1
inst : Ring R
n m : ℕ
inst_1 : CharP R m
h : m ∣ n
r : R
k : ℤ
rw : (↑k : R) * r = r * (↑k : R)
⊢ HMul.hMul (α := R) ((castHom h R : (a : ZMod n) → R) (↑k : ZMod n) : R) r =
    HMul.hMul (β := R) r ((castHom h R : (a : ZMod n) → R) (↑k : ZMod n) : R)
have rw₁ : r * (↑k : R) = r * (↑k : R)
Tactic: rw [map_intCast, Int.cast_comm]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.ZMod (goal)
Goal:
R_1 : Type u_1
inst : Ring R_1
n : ℕ
R : Type u_2
inst_1 : Ring R
inst_2 : Module (ZMod n) R
r : ZMod n
x : R
⊢ HSMul.hSMul (β := R) r 1 * x = r • x ∧ x * HSMul.hSMul (β := R) r 1 = r • x
have zero : ∀ [inst : Module (ZMod 0) R] (r : ZMod 0), HSMul.hSMul (β := R) r 1 * x = r • x ∧ x * HSMul.hSMul (β := R) r 1 = r • x
Tactic: obtain _ | n := n
Cleared hypotheses: n, inst_2, r
-- Lean 4 proof step from Mathlib.Algebra.Algebra.ZMod (goal)
Goal:
R_1 : Type u_1
inst : Ring R_1
n : ℕ
R : Type u_2
inst_1 : Ring R
inst_2 : Module (ZMod n) R
r : ZMod n
x : R
zero :
  ∀ [inst : Module (ZMod 0) R] (r : ZMod 0), HSMul.hSMul (β := R) r 1 * x = r • x ∧ x * HSMul.hSMul (β := R) r 1 = r • x
⊢ HSMul.hSMul (β := R) r 1 * x = r • x ∧ x * HSMul.hSMul (β := R) r 1 = r • x
have succ : ∀ (n : ℕ) [inst : Module (ZMod (n + 1)) R] (r : ZMod (n + 1)),
  HSMul.hSMul (β := R) r 1 * x = r • x ∧ x * HSMul.hSMul (β := R) r 1 = r • x
Tactic: obtain _ | n := n
Cleared hypotheses: n, inst_2, r
-- Lean 4 proof step from Mathlib.Algebra.Algebra.ZMod (goal)
Goal:
R_1 : Type u_1
inst : Ring R_1
R : Type u_2
inst_1 : Ring R
x : R
inst_2 : Module (ZMod 0) R
r : ZMod 0
⊢ HSMul.hSMul (β := R) r 1 * x = r • x ∧ x * HSMul.hSMul (β := R) r 1 = r • x
have zero : HSMul.hSMul (β := R) r 1 * x = r • x ∧ x * HSMul.hSMul (β := R) r 1 = r • x
Tactic: obtain rfl : ((inferInstance : Module ℤ R)) = ‹_› := Subsingleton.elim _ _
Cleared hypotheses: inst_2
-- Lean 4 proof step from Mathlib.Algebra.Algebra.ZMod (goal)
Goal:
R_1 : Type u_1
inst : Ring R_1
R : Type u_2
inst_1 : Ring R
x : R
n : ℕ
inst_2 : Module (ZMod (n + 1)) R
r : ZMod (n + 1)
⊢ HSMul.hSMul (β := R) r 1 * x = r • x ∧ x * HSMul.hSMul (β := R) r 1 = r • x
have succ : ∀ (r : ℕ),
  HSMul.hSMul (α := ZMod (n + 1)) (β := R) (↑r : ZMod (n + 1)) 1 * x =
      HSMul.hSMul (α := ZMod (n + 1)) (↑r : ZMod (n + 1)) x ∧
    x * HSMul.hSMul (α := ZMod (n + 1)) (β := R) (↑r : ZMod (n + 1)) 1 =
      HSMul.hSMul (α := ZMod (n + 1)) (↑r : ZMod (n + 1)) x
Tactic: obtain ⟨r, rfl⟩ := ZMod.natCast_zmod_surjective r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Algebra.ZMod (goal)
Goal:
R_1 : Type u_1
inst : Ring R_1
n : ℕ
R : Type u_2
M : Type u_3
inst_1 : Ring R
inst_2 : AddCommGroup M
inst_3 : Module (ZMod n) R
m₁ : Module (ZMod n) M
inst_4 : Module R M
this : Algebra (ZMod n) R := algebraOfModule n R
m₂ : Module (ZMod n) M := Module.compHom M (algebraMap (ZMod n) R)
⊢ IsScalarTower (ZMod n) R M
have obtain : IsScalarTower (ZMod n) R M
Tactic: obtain rfl : m₁ = m₂ := Subsingleton.elim _ _
Cleared hypotheses: m₁
-- Lean 4 proof step from Mathlib.Algebra.Algebra.ZMod (goal)
Goal:
R_1 : Type u_1
inst : Ring R_1
n : ℕ
R : Type u_2
M : Type u_3
inst_1 : Ring R
inst_2 : AddCommGroup M
inst_3 : Module (ZMod n) R
inst_4 : Module R M
this : Algebra (ZMod n) R := algebraOfModule n R
m₂ : Module (ZMod n) M := Module.compHom M (algebraMap (ZMod n) R)
x : ZMod n
y : R
z : M
⊢ (x • y) • z = x • y • z
have rw : HSMul.hSMul (α := R) ((algebraMap (ZMod n) R : (a : ZMod n) → R) x : R) (y • z) = x • y • z
Tactic: rw [Algebra.smul_def, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.AlgebraicCard (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Algebra R A
inst_5 : Module.IsTorsionFree R A
⊢ #(ULift.{u, v} { x : A // IsAlgebraic R x }) ≤ #(ULift.{v, u} R[X]) * ℵ₀
have choose : ∀ (g : (x : (↑{x : A | IsAlgebraic R x} : Type v)) → R[X])
  (hg₁ : ∀ (x : (↑{x : A | IsAlgebraic R x} : Type v)), g x ≠ 0)
  (hg₂ :
    ∀ (x : (↑{x : A | IsAlgebraic R x} : Type v)),
      Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) (g x) : A) (0 : A)),
  #(ULift.{u, v} { x : A // IsAlgebraic R x }) ≤ #(ULift.{v, u} R[X]) * ℵ₀
Tactic: choose g hg₁ hg₂ using fun x : { x : A | IsAlgebraic R x } => x.coe_prop
-- Lean 4 proof step from Mathlib.Algebra.AlgebraicCard (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Algebra R A
inst_5 : Module.IsTorsionFree R A
g : (x : (↑{x : A | IsAlgebraic R x} : Type v)) → R[X]
hg₁ : ∀ (x : (↑{x : A | IsAlgebraic R x} : Type v)), g x ≠ 0
hg₂ :
  ∀ (x : (↑{x : A | IsAlgebraic R x} : Type v)),
    Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) (g x) : A) (0 : A)
⊢ #(ULift.{u, v} { x : A // IsAlgebraic R x }) ≤ #(ULift.{v, u} R[X]) * ℵ₀
have refine : ∀ (f : R[X]), lift.{u, v} #(↑(g ⁻¹' {f}) : Type v) ≤ ℵ₀
Tactic: refine lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le g fun f => ?_
-- Lean 4 proof step from Mathlib.Algebra.AlgebraicCard (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Algebra R A
inst_5 : Module.IsTorsionFree R A
g : (x : (↑{x : A | IsAlgebraic R x} : Type v)) → R[X]
hg₁ : ∀ (x : (↑{x : A | IsAlgebraic R x} : Type v)), g x ≠ 0
hg₂ :
  ∀ (x : (↑{x : A | IsAlgebraic R x} : Type v)),
    Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) (g x) : A) (0 : A)
f : R[X]
⊢ lift.{u, v} #(↑(g ⁻¹' {f}) : Type v) ≤ ℵ₀
have rw : (g ⁻¹' {f}).Countable
Tactic: rw [lift_le_aleph0, le_aleph0_iff_set_countable]
-- Lean 4 proof step from Mathlib.Algebra.AlgebraicCard (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Algebra R A
inst_5 : Module.IsTorsionFree R A
g : (x : (↑{x : A | IsAlgebraic R x} : Type v)) → R[X]
hg₁ : ∀ (x : (↑{x : A | IsAlgebraic R x} : Type v)), g x ≠ 0
hg₂ :
  ∀ (x : (↑{x : A | IsAlgebraic R x} : Type v)),
    Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) (g x) : A) (0 : A)
f : R[X]
⊢ (g ⁻¹' {f}).Countable
have suffices : MapsTo (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Set A) {x : A | IsAlgebraic R x} x)) (g ⁻¹' {f})
  (f.rootSet A)
Tactic: suffices MapsTo (↑) (g ⁻¹' {f}) (f.rootSet A) from
    this.countable_of_injOn Subtype.coe_injective.injOn (f.rootSet_finite A).countable
-- Lean 4 proof step from Mathlib.Algebra.AlgebraicCard (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Algebra R A
inst_5 : Module.IsTorsionFree R A
⊢ lift.{v, u} #R[X] * ℵ₀ ≤ max (lift.{v, u} #R) ℵ₀
have grw : lift.{v, u} (max #R ℵ₀) * ℵ₀ ≤ max (lift.{v, u} #R) ℵ₀
Tactic: grw [lift_le.2 cardinalMk_le_max]
-- Lean 4 proof step from Mathlib.Algebra.AlgebraicCard (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Algebra R A
inst_5 : Module.IsTorsionFree R A
inst_6 : Countable R
⊢ Set.Countable.{v} (α := A) {x : A | IsAlgebraic R x}
have rw : lift.{u, v} #(↑{x : A | IsAlgebraic R x} : Type v) ≤ ℵ₀
Tactic: rw [← le_aleph0_iff_set_countable, ← lift_le_aleph0]
-- Lean 4 proof step from Mathlib.Algebra.AlgebraicCard (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Algebra R A
inst_5 : Module.IsTorsionFree R A
inst_6 : Countable R
⊢ lift.{u, v} #(↑{x : A | IsAlgebraic R x} : Type v) ≤ ℵ₀
have apply : max (lift.{v, u} #R) ℵ₀ ≤ ℵ₀
Tactic: apply (cardinalMk_lift_le_max R A).trans
-- Lean 4 proof step from Mathlib.Algebra.AlgebraicCard (goal)
Goal:
R A : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Algebra R A
inst_5 : Module.IsTorsionFree R A
⊢ #{ x : A // IsAlgebraic R x } ≤ #R[X] * ℵ₀
have rw : lift.{u, u} #{ x : A // IsAlgebraic R x } ≤ lift.{u, u} #R[X] * ℵ₀
Tactic: rw [← lift_id #_, ← lift_id #R[X]]
-- Lean 4 proof step from Mathlib.Algebra.AlgebraicCard (goal)
Goal:
R A : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Algebra R A
inst_5 : Module.IsTorsionFree R A
⊢ #{ x : A // IsAlgebraic R x } ≤ max #R ℵ₀
have rw : lift.{u, u} #{ x : A // IsAlgebraic R x } ≤ max (lift.{u, u} #R) ℵ₀
Tactic: rw [← lift_id #_, ← lift_id #R]
-- Lean 4 proof step from Mathlib.Algebra.Azumaya.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
⊢ Function.Bijective (α := R ⊗[R] Rᵐᵒᵖ) (β := Module.End R R)
    (⇑(AlgHom.mulLeftRight R R) : (a : R ⊗[R] Rᵐᵒᵖ) → Module.End R R)
have rw : Function.Bijective (α := R ⊗[R] Rᵐᵒᵖ) (β := Module.End R R)
  (⇑(↑(tensorEquivEnd R) : R ⊗[R] Rᵐᵒᵖ →ₐ[R] Module.End R R) : (a : R ⊗[R] Rᵐᵒᵖ) → Module.End R R)
Tactic: rw [← coe_tensorEquivEnd]