awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Unitization
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
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
⊢ Eq (α := Unitization R B →⋆ₐ[R] Unitization R B) (starMap (NonUnitalStarAlgHom.id R B))
    (StarAlgHom.id R (Unitization R B))

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Unitization
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
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:
simp
-- Module: Mathlib.Algebra.Algebra.Unitization
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
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:
simp
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarAddMonoid R
inst_2 : Star A
a : A
⊢ IsSelfAdjoint (R := Unitization R A) (↑a : Unitization R A) ↔ IsSelfAdjoint a

Tactic:
simp only [isSelfAdjoint_iff, ← inr_star, inr_injective.eq_iff]

Premises used: Unitization.inr_star, Function.Injective.eq_iff, Unitization.inr_injective, isSelfAdjoint_iff
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarAddMonoid R
inst_2 : Star A
a : A
ha : IsSelfAdjoint a
⊢ IsSelfAdjoint (R := Unitization R A) (↑a : Unitization R A)

Tactic:
isSelfAdjoint_inr.mpr ha

Premises used: Iff.mpr, Unitization.isSelfAdjoint_inr
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarAddMonoid R
inst_2 : Star A
a : A
inst_3 : AddCommMonoid A
inst_4 : Mul A
inst_5 : SMulWithZero R A
⊢ IsStarNormal (R := Unitization R A) (↑a : Unitization R A) ↔ IsStarNormal a

Tactic:
simp only [isStarNormal_iff, commute_iff_eq, ← inr_star, ← inr_mul, inr_injective.eq_iff]

Premises used: Unitization.inr_star, isStarNormal_iff, Function.Injective.eq_iff, commute_iff_eq, Unitization.inr_mul, Unitization.inr_injective
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarAddMonoid R
inst_2 : Star A
a_1 : A
inst_3 : AddCommMonoid A
inst_4 : Mul A
inst_5 : SMulWithZero R A
a : A
inst_6 : IsStarNormal a
⊢ IsStarNormal (R := Unitization R A) (↑a : Unitization R A)

Tactic:
isStarNormal_inr.mpr ‹_›

Premises used: Iff.mpr, Unitization.isStarNormal_inr
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : MulZeroClass R
inst_1 : AddZeroClass A
inst_2 : Mul A
inst_3 : SMulWithZero R A
a : A
⊢ IsIdempotentElem (M := Unitization R A) (↑a : Unitization R A) ↔ IsIdempotentElem a

Tactic:
simp only [IsIdempotentElem, ← inr_mul, inr_injective.eq_iff]

Premises used: Function.Injective.eq_iff, Unitization.inr_mul, Unitization.inr_injective, IsIdempotentElem
-- Module: Mathlib.Algebra.Algebra.Unitization
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
p : A
⊢ IsStarProjection (R := Unitization R A) (↑p : Unitization R A) ↔ IsStarProjection p

Tactic:
simp [isStarProjection_iff]

Premises used: isStarProjection_iff
-- Module: Mathlib.Algebra.Algebra.ZMod
Goal:
R : Type u_1
inst : Ring R
p : ℕ
⊢ Subsingleton.{max (u_1 + 1) 1} (Algebra (ZMod p) R)

Tactic:
⟨fun _ _ => Algebra.algebra_ext _ _ <| RingHom.congr_fun <| Subsingleton.elim _ _⟩

Premises used: Algebra.algebraMap, RingHom.congr_fun, ZMod, Subsingleton.intro, Algebra.algebra_ext, Subsingleton.elim
-- Module: Mathlib.Algebra.Algebra.ZMod
Goal:
R : Type u_1
inst : Ring R
n m : ℕ
inst_1 : CharP R m
h : m ∣ n
a : ZMod n
r : R
rcases : ∀ (k : ℤ), cast (n := n) (↑k : ZMod n) * r = r * cast (n := n) (↑k : ZMod n)
⊢ a.cast * r = r * a.cast

Tactic:
rcases ZMod.intCast_surjective a with ⟨k, rfl⟩

Premises used: ZMod.intCast_surjective, rfl
-- Module: Mathlib.Algebra.Algebra.ZMod
Goal:
R : Type u_1
inst : Ring R
n m : ℕ
inst_1 : CharP R m
h : m ∣ n
r : R
k : ℤ
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)
⊢ cast (n := n) (↑k : ZMod n) * r = r * cast (n := n) (↑k : ZMod n)

Tactic:
change ZMod.castHom h R k * r = r * ZMod.castHom h R k

Premises used: Int.cast, DFunLike.coe, ZMod.castHom
-- Module: Mathlib.Algebra.Algebra.ZMod
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)
rw₁ rw₂ : r * (↑k : 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)

Tactic:
rw [map_intCast, Int.cast_comm]

Premises used: map_intCast, Int.cast_comm
-- Module: Mathlib.Algebra.Algebra.ZMod
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
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
⊢ HSMul.hSMul (β := R) r 1 * x = r • x ∧ x * HSMul.hSMul (β := R) r 1 = r • x

Tactic:
obtain _ | n := n
-- Module: Mathlib.Algebra.Algebra.ZMod
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
⊢ inferInstance = inst_2

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Algebra.Algebra.ZMod
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
zero : 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

Tactic:
obtain rfl : ((inferInstance : Module ℤ R)) = ‹_› := Subsingleton.elim _ _

Premises used: inferInstance, Subsingleton.elim, rfl
-- Module: Mathlib.Algebra.Algebra.ZMod
Goal:
R_1 : Type u_1
inst : Ring R_1
R : Type u_2
inst_1 : Ring R
x : R
r : ZMod 0
⊢ HSMul.hSMul (β := R) r 1 * x = r • x ∧ x * HSMul.hSMul (β := R) r 1 = r • x

Tactic:
simp [ZMod, Int.cast_comm]

Premises used: ZMod, Int.cast_comm
-- Module: Mathlib.Algebra.Algebra.ZMod
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)
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
⊢ HSMul.hSMul (β := R) r 1 * x = r • x ∧ x * HSMul.hSMul (β := R) r 1 = r • x

Tactic:
obtain ⟨r, rfl⟩ := ZMod.natCast_zmod_surjective r

Premises used: ZMod.natCast_zmod_surjective, rfl
-- Module: Mathlib.Algebra.Algebra.ZMod
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 : ℕ
⊢ 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:
simp [Nat.cast_smul_eq_nsmul, Nat.cast_comm]

Premises used: Nat.cast_comm, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Algebra.Algebra.ZMod
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)
⊢ m₁ = m₂

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Algebra.Algebra.ZMod
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)
obtain : IsScalarTower (ZMod n) R M
⊢ IsScalarTower (ZMod n) R M

Tactic:
obtain rfl : m₁ = m₂ := Subsingleton.elim _ _

Premises used: Subsingleton.elim, rfl
-- Module: Mathlib.Algebra.Algebra.ZMod
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
rw : HSMul.hSMul (α := R) ((algebraMap (ZMod n) R : (a : ZMod n) → R) x : R) (y • z) = x • y • z
⊢ (x • y) • z = x • y • z

Tactic:
rw [Algebra.smul_def, mul_smul]

Premises used: Algebra.smul_def, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Algebra.ZMod
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
⊢ HSMul.hSMul (α := R) ((algebraMap (ZMod n) R : (a : ZMod n) → R) x : R) (y • z) = x • y • z

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.ZMod
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)
⊢ IsScalarTower (ZMod n) R M

Tactic:
exact ⟨fun x y z ↦ by rw [Algebra.smul_def, mul_smul]; rfl⟩
-- Module: Mathlib.Algebra.AlgebraicCard
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : CharZero A
this : Nontrivial R := ⋯
⊢ Set.Infinite.{u_2} (α := A) {x : A | IsAlgebraic R x}

Tactic:
infinite_of_injective_forall_mem Nat.cast_injective isAlgebraic_nat

Premises used: Set.infinite_of_injective_forall_mem, isAlgebraic_nat, Nat.cast_injective
-- Module: Mathlib.Algebra.AlgebraicCard
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : CharZero A
this : Nontrivial R := ⋯
⊢ Set.Infinite.{u_2} (α := A) {x : A | IsAlgebraic R x}

Tactic:
exact infinite_of_injective_forall_mem Nat.cast_injective isAlgebraic_nat

Premises used: Set.infinite_of_injective_forall_mem, Nat.cast_injective
-- Module: Mathlib.Algebra.AlgebraicCard
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : CharZero A
⊢ ℵ₀ ≤ #{ x : A // IsAlgebraic R x }

Tactic:
infinite_iff.1 (Set.infinite_coe_iff.2 <| infinite_of_charZero R A)

Premises used: Iff.mpr, Cardinal.infinite_iff, Set.infinite_coe_iff, Iff.mp, Algebraic.infinite_of_charZero
-- Module: Mathlib.Algebra.AlgebraicCard
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
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]) * ℵ₀
⊢ #(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

Premises used: Subtype.coe_prop
-- Module: Mathlib.Algebra.AlgebraicCard
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]) * ℵ₀

Tactic:
lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le g fun f => ?_

Premises used: Cardinal.lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le
-- Module: Mathlib.Algebra.AlgebraicCard
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)
refine : ∀ (f : R[X]), lift.{u, v} #(↑(g ⁻¹' {f}) : Type v) ≤ ℵ₀
⊢ #(ULift.{u, v} { x : A // IsAlgebraic R x }) ≤ #(ULift.{v, u} R[X]) * ℵ₀

Tactic:
refine lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le g fun f => ?_

Premises used: Cardinal.lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le
-- Module: Mathlib.Algebra.AlgebraicCard
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]
rw : (g ⁻¹' {f}).Countable
⊢ lift.{u, v} #(↑(g ⁻¹' {f}) : Type v) ≤ ℵ₀

Tactic:
rw [lift_le_aleph0, le_aleph0_iff_set_countable]

Premises used: Cardinal.lift_le_aleph0, Cardinal.le_aleph0_iff_set_countable
-- Module: Mathlib.Algebra.AlgebraicCard
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]
suffices :
  MapsTo (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Set A) {x : A | IsAlgebraic R x} x)) (g ⁻¹' {f})
    (f.rootSet A)
⊢ (g ⁻¹' {f}).Countable

Tactic:
suffices MapsTo (↑) (g ⁻¹' {f}) (f.rootSet A) from
    this.countable_of_injOn Subtype.coe_injective.injOn (f.rootSet_finite A).countable
-- Module: Mathlib.Algebra.AlgebraicCard
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)
x : (↑{x : A | IsAlgebraic R x} : Type v)
⊢ (↑x : A) ∈ (g x).rootSet A

Tactic:
mem_rootSet.2 ⟨hg₁ x, hg₂ x⟩

Premises used: Iff.mpr, And.intro, Polynomial.mem_rootSet
-- Module: Mathlib.Algebra.AlgebraicCard
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)
x : (↑{x : A | IsAlgebraic R x} : Type v)
⊢ (↑x : A) ∈ (g x).rootSet A

Tactic:
exact mem_rootSet.2 ⟨hg₁ x, hg₂ x⟩

Premises used: Iff.mpr, And.intro, Polynomial.mem_rootSet
-- Module: Mathlib.Algebra.AlgebraicCard
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
grw : lift.{v, u} (max #R ℵ₀) * ℵ₀ ≤ max (lift.{v, u} #R) ℵ₀
⊢ lift.{v, u} #R[X] * ℵ₀ ≤ max (lift.{v, u} #R) ℵ₀

Tactic:
grw [lift_le.2 cardinalMk_le_max]

Premises used: Iff.mpr, Polynomial.cardinalMk_le_max, Cardinal.lift_le
-- Module: Mathlib.Algebra.AlgebraicCard
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} (max #R ℵ₀) * ℵ₀ ≤ max (lift.{v, u} #R) ℵ₀

Tactic:
simp
-- Module: Mathlib.Algebra.AlgebraicCard
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 : Infinite R
⊢ lift.{u, v} #{ x : A // IsAlgebraic R x } = lift.{v, u} #R

Tactic:
((cardinalMk_lift_le_max R A).trans_eq (max_eq_left <| aleph0_le_mk _)).antisymm <|
    lift_mk_le'.2 ⟨⟨fun x => ⟨algebraMap R A x, isAlgebraic_algebraMap _⟩, fun _ _ h =>
      FaithfulSMul.algebraMap_injective R A (Subtype.ext_iff.1 h)⟩⟩

Premises used: Iff.mpr, LE.le.trans_eq, Algebra.algebraMap, Function.Embedding.mk, LE.le.antisymm, max_eq_left, Nonempty.intro, Subtype.ext_iff, Subtype.mk, FaithfulSMul.algebraMap_injective, Iff.mp, Cardinal.lift_mk_le', isAlgebraic_algebraMap, DFunLike.coe, Cardinal.aleph0_le_mk, Algebraic.cardinalMk_lift_le_max
-- Module: Mathlib.Algebra.AlgebraicCard
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
rw : lift.{u, v} #(↑{x : A | IsAlgebraic R x} : Type v) ≤ ℵ₀
⊢ Set.Countable.{v} (α := A) {x : A | IsAlgebraic R x}

Tactic:
rw [← le_aleph0_iff_set_countable, ← lift_le_aleph0]

Premises used: Cardinal.lift_le_aleph0, Cardinal.le_aleph0_iff_set_countable
-- Module: Mathlib.Algebra.AlgebraicCard
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
apply : max (lift.{v, u} #R) ℵ₀ ≤ ℵ₀
⊢ lift.{u, v} #(↑{x : A | IsAlgebraic R x} : Type v) ≤ ℵ₀

Tactic:
apply (cardinalMk_lift_le_max R A).trans

Premises used: LE.le.trans, Algebraic.cardinalMk_lift_le_max
-- Module: Mathlib.Algebra.AlgebraicCard
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
⊢ max (lift.{v, u} #R) ℵ₀ ≤ ℵ₀

Tactic:
simp
-- Module: Mathlib.Algebra.AlgebraicCard
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
inst_7 : CharZero A
⊢ #{ x : A // IsAlgebraic R x } = ℵ₀

Tactic:
(Algebraic.countable R A).le_aleph0.antisymm (aleph0_le_cardinalMk_of_charZero R A)

Premises used: IsAlgebraic, Set.Mem, setOf, LE.le.antisymm, Set.Countable.le_aleph0, Algebraic.aleph0_le_cardinalMk_of_charZero, Algebraic.countable
-- Module: Mathlib.Algebra.AlgebraicCard
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
rw : lift.{u, u} #{ x : A // IsAlgebraic R x } ≤ lift.{u, u} #R[X] * ℵ₀
⊢ #{ x : A // IsAlgebraic R x } ≤ #R[X] * ℵ₀

Tactic:
rw [← lift_id #_, ← lift_id #R[X]]

Premises used: Cardinal.mk, Polynomial, Cardinal.lift_id
-- Module: Mathlib.Algebra.AlgebraicCard
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
⊢ lift.{u, u} #{ x : A // IsAlgebraic R x } ≤ lift.{u, u} #R[X] * ℵ₀

Tactic:
cardinalMk_lift_le_mul R A

Premises used: Algebraic.cardinalMk_lift_le_mul
-- Module: Mathlib.Algebra.AlgebraicCard
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
⊢ lift.{u, u} #{ x : A // IsAlgebraic R x } ≤ lift.{u, u} #R[X] * ℵ₀

Tactic:
exact cardinalMk_lift_le_mul R A

Premises used: Algebraic.cardinalMk_lift_le_mul
-- Module: Mathlib.Algebra.AlgebraicCard
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
rw : lift.{u, u} #{ x : A // IsAlgebraic R x } ≤ max (lift.{u, u} #R) ℵ₀
⊢ #{ x : A // IsAlgebraic R x } ≤ max #R ℵ₀

Tactic:
rw [← lift_id #_, ← lift_id #R]

Premises used: Cardinal.mk, Cardinal.lift_id
-- Module: Mathlib.Algebra.AlgebraicCard
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
⊢ lift.{u, u} #{ x : A // IsAlgebraic R x } ≤ max (lift.{u, u} #R) ℵ₀

Tactic:
cardinalMk_lift_le_max R A

Premises used: Algebraic.cardinalMk_lift_le_max
-- Module: Mathlib.Algebra.AlgebraicCard
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
⊢ lift.{u, u} #{ x : A // IsAlgebraic R x } ≤ max (lift.{u, u} #R) ℵ₀

Tactic:
exact cardinalMk_lift_le_max R A

Premises used: Algebraic.cardinalMk_lift_le_max
-- Module: Mathlib.Algebra.AlgebraicCard
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
inst_6 : Infinite R
⊢ #{ x : A // IsAlgebraic R x } = #R

Tactic:
lift_inj.1 <| cardinalMk_lift_of_infinite R A

Premises used: Cardinal.lift_inj, Iff.mp, Algebraic.cardinalMk_lift_of_infinite
-- Module: Mathlib.Algebra.Azumaya.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
h : IsAzumaya R A
⊢ Function.Bijective (α := A ⊗[R] Aᵐᵒᵖ) (β := Module.End R A)
    (⇑(AlgHom.mulLeftRight R A) : (a : A ⊗[R] Aᵐᵒᵖ) → Module.End R A)

Tactic:
h.bij

Premises used: IsAzumaya.bij