awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p_1 p : K[X]
a : K
hp : p.coeff 0 = 0
ha : a ≠ 0
_ih :
  ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
_ne_zero : HAdd.hAdd (β := K[X]) p ((C : (a : K) → K[X]) a : K[X]) ≠ 0
aeval_eq :
  Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) (HAdd.hAdd (β := K[X]) p ((C : (a : K) → K[X]) a : K[X])) : ↥A)
    (0 : ↥A)
refine_2 : p.coeff 0 + coeff ((C : (a : K) → K[X]) a) 0 ≠ 0
refine_2₁ : HAdd.hAdd (α := K) 0 (coeff ((C : (a : K) → K[X]) a) 0) ≠ 0
⊢ (HAdd.hAdd (β := K[X]) p ((C : (a : K) → K[X]) a : K[X])).coeff 0 ≠ 0
have refine_2₂ : Ne.{u_1 + 1} (α := K) (coeff ((C : (a : K) → K[X]) a) 0) 0
Tactic: rwa [coeff_add, hp, zero_add, coeff_C, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p_1 p : K[X]
a : K
hp : p.coeff 0 = 0
ha : a ≠ 0
_ih :
  ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
_ne_zero : HAdd.hAdd (β := K[X]) p ((C : (a : K) → K[X]) a : K[X]) ≠ 0
aeval_eq :
  Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) (HAdd.hAdd (β := K[X]) p ((C : (a : K) → K[X]) a : K[X])) : ↥A)
    (0 : ↥A)
refine_2 : p.coeff 0 + coeff ((C : (a : K) → K[X]) a) 0 ≠ 0
refine_2₁ : HAdd.hAdd (α := K) 0 (coeff ((C : (a : K) → K[X]) a) 0) ≠ 0
refine_2₂ : Ne.{u_1 + 1} (α := K) (coeff ((C : (a : K) → K[X]) a) 0) 0
⊢ (HAdd.hAdd (β := K[X]) p ((C : (a : K) → K[X]) a : K[X])).coeff 0 ≠ 0
have refine_2₃ : (if Eq (α := ℕ) 0 0 then a else 0) ≠ 0
Tactic: rwa [coeff_add, hp, zero_add, coeff_C, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p_1 p : K[X]
hp : p ≠ 0
ih :
  ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) (p * X) : ↥A) (0 : ↥A)
⊢ (↑x : L)⁻¹ ∈ A
have aeval_eq₁ : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A) ∨ x = 0
Tactic: rw [map_mul, aeval_X, mul_eq_zero] at aeval_eq
Cleared hypotheses: aeval_eq
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p_1 p : K[X]
hp : p ≠ 0
ih :
  ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A) ∨ x = 0
⊢ (↑x : L)⁻¹ ∈ A
have refine_3 : ∀ (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
Tactic: rcases aeval_eq with aeval_eq | x_eq
Cleared hypotheses: aeval_eq
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p_1 p : K[X]
hp : p ≠ 0
ih :
  ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A) ∨ x = 0
refine_3 : ∀ (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
⊢ (↑x : L)⁻¹ ∈ A
have refine_3₁ : ∀ (x_eq : x = 0), (↑x : L)⁻¹ ∈ A
Tactic: rcases aeval_eq with aeval_eq | x_eq
Cleared hypotheses: aeval_eq
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p_1 p : K[X]
hp : p ≠ 0
ih :
  ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
x_eq : x = 0
⊢ (↑x : L)⁻¹ ∈ A
have refine_3 : 0 ∈ A
Tactic: rw [x_eq, Subalgebra.coe_zero, inv_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Cardinality (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : Type v
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra R L
inst_5 : IsTorsionFree R L
inst_6 : Algebra.IsAlgebraic R L
x : L
p : { x_1 : R[X] // x_1 ≠ 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) x_1 : L) (0 : L) } :=
  Classical.indefiniteDescription
    (fun (x_1 : R[X]) ↦ x_1 ≠ 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) x_1 : L) (0 : L)) ⋯
⊢ x ∈ (↑p : R[X]).aroots L
have this : Ne (α := L[X]) (Polynomial.map (algebraMap R L) (↑p : R[X])) 0
Tactic: have := (Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective R L)).2 p.2.1
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Cardinality (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : Type v
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra R L
inst_5 : IsTorsionFree R L
inst_6 : Algebra.IsAlgebraic R L
x : L
p : { x_1 : R[X] // x_1 ≠ 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) x_1 : L) (0 : L) } :=
  Classical.indefiniteDescription
    (fun (x_1 : R[X]) ↦ x_1 ≠ 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) x_1 : L) (0 : L)) ⋯
this : Ne (α := L[X]) (Polynomial.map (algebraMap R L) (↑p : R[X])) 0
⊢ x ∈ (↑p : R[X]).aroots L
have rw : Polynomial.IsRoot (Polynomial.map (algebraMap R L) (↑p : R[X])) x
Tactic: rw [Polynomial.mem_roots this, Polynomial.IsRoot, Polynomial.eval_map,
          ← Polynomial.aeval_def, p.2.2]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Cardinality (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : Type v
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra R L
inst_5 : IsTorsionFree R L
inst_6 : Algebra.IsAlgebraic R L
x : L
p : { x_1 : R[X] // x_1 ≠ 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) x_1 : L) (0 : L) } :=
  Classical.indefiniteDescription
    (fun (x_1 : R[X]) ↦ x_1 ≠ 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) x_1 : L) (0 : L)) ⋯
this : Ne (α := L[X]) (Polynomial.map (algebraMap R L) (↑p : R[X])) 0
rw : Polynomial.IsRoot (Polynomial.map (algebraMap R L) (↑p : R[X])) x
⊢ x ∈ (↑p : R[X]).aroots L
have rw₁ : Polynomial.eval x (Polynomial.map (algebraMap R L) (↑p : R[X])) = 0
Tactic: rw [Polynomial.mem_roots this, Polynomial.IsRoot, Polynomial.eval_map,
          ← Polynomial.aeval_def, p.2.2]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Cardinality (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : Type v
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra R L
inst_5 : IsTorsionFree R L
inst_6 : Algebra.IsAlgebraic R L
x : L
p : { x_1 : R[X] // x_1 ≠ 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) x_1 : L) (0 : L) } :=
  Classical.indefiniteDescription
    (fun (x_1 : R[X]) ↦ x_1 ≠ 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) x_1 : L) (0 : L)) ⋯
this : Ne (α := L[X]) (Polynomial.map (algebraMap R L) (↑p : R[X])) 0
rw : Polynomial.IsRoot (Polynomial.map (algebraMap R L) (↑p : R[X])) x
rw₁ : Polynomial.eval x (Polynomial.map (algebraMap R L) (↑p : R[X])) = 0
⊢ x ∈ (↑p : R[X]).aroots L
have rw₂ : Polynomial.eval₂ (algebraMap R L) x (↑p : R[X]) = 0
Tactic: rw [Polynomial.mem_roots this, Polynomial.IsRoot, Polynomial.eval_map,
          ← Polynomial.aeval_def, p.2.2]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Cardinality (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : Type v
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra R L
inst_5 : IsTorsionFree R L
inst_6 : Algebra.IsAlgebraic R L
x : L
p : { x_1 : R[X] // x_1 ≠ 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) x_1 : L) (0 : L) } :=
  Classical.indefiniteDescription
    (fun (x_1 : R[X]) ↦ x_1 ≠ 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) x_1 : L) (0 : L)) ⋯
this : Ne (α := L[X]) (Polynomial.map (algebraMap R L) (↑p : R[X])) 0
rw : Polynomial.IsRoot (Polynomial.map (algebraMap R L) (↑p : R[X])) x
rw₁ : Polynomial.eval x (Polynomial.map (algebraMap R L) (↑p : R[X])) = 0
rw₂ : Polynomial.eval₂ (algebraMap R L) x (↑p : R[X]) = 0
⊢ x ∈ (↑p : R[X]).aroots L
have rw₃ : Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) (↑p : R[X]) : L) (0 : L)
Tactic: rw [Polynomial.mem_roots this, Polynomial.IsRoot, Polynomial.eval_map,
          ← Polynomial.aeval_def, p.2.2]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Cardinality (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : Type v
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra R L
inst_5 : IsTorsionFree R L
inst_6 : Algebra.IsAlgebraic R L
x : L
p : { x_1 : R[X] // x_1 ≠ 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) x_1 : L) (0 : L) } :=
  Classical.indefiniteDescription
    (fun (x_1 : R[X]) ↦ x_1 ≠ 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) x_1 : L) (0 : L)) ⋯
this : Ne (α := L[X]) (Polynomial.map (algebraMap R L) (↑p : R[X])) 0
rw : Polynomial.IsRoot (Polynomial.map (algebraMap R L) (↑p : R[X])) x
rw₁ : Polynomial.eval x (Polynomial.map (algebraMap R L) (↑p : R[X])) = 0
rw₂ : Polynomial.eval₂ (algebraMap R L) x (↑p : R[X]) = 0
rw₃ : Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) (↑p : R[X]) : L) (0 : L)
⊢ x ∈ (↑p : R[X]).aroots L
have rw₄ : Eq.{v + 1} (α := L) 0 0
Tactic: rw [Polynomial.mem_roots this, Polynomial.IsRoot, Polynomial.eval_map,
          ← Polynomial.aeval_def, p.2.2]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Cardinality (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : Type v
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra R L
inst_5 : IsTorsionFree R L
inst_6 : Algebra.IsAlgebraic R L
x y : L
h :
  Eq.{u + 1} (α := R[X])
      (↑(Classical.indefiniteDescription
            (fun (x_1 : R[X]) ↦ ¬x_1 = 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) x_1 : L) (0 : L))
            ⋯) :
        R[X])
      (↑(Classical.indefiniteDescription
            (fun (x : R[X]) ↦ ¬x = 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval y : (a : R[X]) → L) x : L) (0 : L)) ⋯) :
        R[X]) ∧
    HEq (α :=
      { x_1 : L //
        x_1 ∈
          Polynomial.aroots.{u, v} (T := R)
            (↑(Classical.indefiniteDescription
                  (fun (x_2 : R[X]) ↦
                    ¬x_2 = 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) x_2 : L) (0 : L))
                  ⋯) :
              R[X])
            L })
      (Subtype.mk (p := fun (x_1 : L) ↦
        x_1 ∈
          Polynomial.aroots.{u, v} (T := R)
            (↑(Classical.indefiniteDescription
                  (fun (x_2 : R[X]) ↦
                    ¬x_2 = 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) x_2 : L) (0 : L))
                  ⋯) :
              R[X])
            L)
        x ⋯)
      (β :=
      { x : L //
        x ∈
          Polynomial.aroots.{u, v} (T := R)
            (↑(Classical.indefiniteDescription
                  (fun (x : R[X]) ↦ ¬x = 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval y : (a : R[X]) → L) x : L) (0 : L))
                  ⋯) :
              R[X])
            L })
      (Subtype.mk (p := fun (x : L) ↦
        x ∈
          Polynomial.aroots.{u, v} (T := R)
            (↑(Classical.indefiniteDescription
                  (fun (x : R[X]) ↦ ¬x = 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval y : (a : R[X]) → L) x : L) (0 : L))
                  ⋯) :
              R[X])
            L)
        y ⋯)
⊢ x = y
have refine : ∀ (x_1 : L),
  x_1 ∈
      Polynomial.aroots.{u, v} (T := R)
        (↑(Classical.indefiniteDescription
              (fun (x_2 : R[X]) ↦
                ¬x_2 = 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) x_2 : L) (0 : L))
              sorry) :
          R[X])
        L ↔
    x_1 ∈
      Polynomial.aroots.{u, v} (T := R)
        (↑(Classical.indefiniteDescription
              (fun (x : R[X]) ↦ ¬x = 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval y : (a : R[X]) → L) x : L) (0 : L)) sorry) :
          R[X])
        L
Tactic: refine (Subtype.heq_iff_coe_eq ?_).1 h.2
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Cardinality (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : Type v
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra R L
inst_5 : IsTorsionFree R L
inst_6 : Algebra.IsAlgebraic R L
⊢ lift.{u, v} #L ≤ #((p : R[X]) × { x : L // x ∈ p.aroots L })
have this : lift.{max v u, v} #L ≤ lift.{v, max v u} #((p : R[X]) × (↑{x : L | x ∈ p.aroots L} : Type v))
Tactic: have := @lift_mk_le_lift_mk_of_injective L (Σ p : R[X], {x : L | x ∈ p.aroots L})
    (fun x : L =>
      let p := Classical.indefiniteDescription _ (Algebra.IsAlgebraic.isAlgebraic x)
      ⟨p.1, x, by
        dsimp
        have := (Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective R L)).2 p.2.1
        rw [Polynomial.mem_roots this, Polynomial.IsRoot, Polynomial.eval_map,
          ← Polynomial.aeval_def, p.2.2]⟩)
    fun x y => by
      intro h
      simp only [Set.coe_setOf, ne_eq, Set.mem_setOf_eq, Sigma.mk.inj_iff] at h
      refine (Subtype.heq_iff_coe_eq ?_).1 h.2
      simp only [h.1, forall_true_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Cardinality (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : Type v
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra R L
inst_5 : IsTorsionFree R L
inst_6 : Algebra.IsAlgebraic R L
this : lift.{max v u, v} #L ≤ lift.{v, max v u} #((p : R[X]) × (↑{x : L | x ∈ p.aroots L} : Type v))
⊢ lift.{u, v} #L ≤ #((p : R[X]) × { x : L // x ∈ p.aroots L })
have rwa : ∀ (this : lift.{u, v} #L ≤ lift.{v, max v u} #((p : R[X]) × (↑{x : L | x ∈ p.aroots L} : Type v))),
  lift.{u, v} #L ≤ #((p : R[X]) × { x : L // x ∈ p.aroots L })
Tactic: rwa [lift_umax, lift_id'.{v}] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Cardinality (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : Type v
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra R L
inst_5 : IsTorsionFree R L
inst_6 : Algebra.IsAlgebraic R L
this : lift.{max v u, v} #L ≤ lift.{v, max v u} #((p : R[X]) × (↑{x : L | x ∈ p.aroots L} : Type v))
rwa :
  ∀ (this : lift.{u, v} #L ≤ lift.{v, max v u} #((p : R[X]) × (↑{x : L | x ∈ p.aroots L} : Type v))),
    lift.{u, v} #L ≤ #((p : R[X]) × { x : L // x ∈ p.aroots L })
⊢ lift.{u, v} #L ≤ #((p : R[X]) × { x : L // x ∈ p.aroots L })
have rwa₁ : ∀ (this : lift.{u, v} #L ≤ #((p : R[X]) × (↑{x : L | x ∈ p.aroots L} : Type v))),
  lift.{u, v} #L ≤ #((p : R[X]) × { x : L // x ∈ p.aroots L })
Tactic: rwa [lift_umax, lift_id'.{v}] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Cardinality (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : Type v
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra R L
inst_5 : IsTorsionFree R L
inst_6 : Algebra.IsAlgebraic R L
⊢ #((p : R[X]) × { x : L // x ∈ p.aroots L }) = sum.{u, v} fun (p : R[X]) ↦ #(↑{x : L | x ∈ p.aroots L} : Type v)
have rw : #((p : R[X]) × { x : L // x ∈ p.aroots L }) = #((i : R[X]) × (↑{x : L | x ∈ i.aroots L} : Type v))
Tactic: rw [← mk_sigma]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Cardinality (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : Type v
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra R L
inst_5 : IsTorsionFree R L
inst_6 : Algebra.IsAlgebraic R L
⊢ (sum.{u, v} fun (x : R[X]) ↦ ℵ₀) = lift.{v, u} #R[X] * ℵ₀
have rw : lift.{v, u} #R[X] * lift.{u, v} ℵ₀ = lift.{v, u} #R[X] * ℵ₀
Tactic: rw [sum_const, lift_aleph0]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Cardinality (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : Type v
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra R L
inst_5 : IsTorsionFree R L
inst_6 : Algebra.IsAlgebraic R L
rw : lift.{v, u} #R[X] * lift.{u, v} ℵ₀ = lift.{v, u} #R[X] * ℵ₀
⊢ (sum.{u, v} fun (x : R[X]) ↦ ℵ₀) = lift.{v, u} #R[X] * ℵ₀
have rw₁ : lift.{v, u} #R[X] * ℵ₀ = lift.{v, u} #R[X] * ℵ₀
Tactic: rw [sum_const, lift_aleph0]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Cardinality (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : Type v
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra R L
inst_5 : IsTorsionFree R L
inst_6 : Algebra.IsAlgebraic R L
⊢ max (max (lift.{v, u} #R[X]) ℵ₀) ℵ₀ ≤ max (max (lift.{v, u} (max #R ℵ₀)) ℵ₀) ℵ₀
have h₁ : lift.{v, u} #R[X] ≤ lift.{v, u} (max #R ℵ₀)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Defs (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
⊢ Transcendental R x ↔ ∀ (p : R[X]), Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A) → p = 0
have rw : (∀ (x_1 : R[X]), ¬(x_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) x_1 : A) (0 : A))) ↔
  ∀ (p : R[X]), Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A) → p = 0
Tactic: rw [Transcendental, IsAlgebraic, not_exists]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Defs (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
⊢ (∀ (x_1 : R[X]), ¬(x_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) x_1 : A) (0 : A))) ↔
    ∀ (p : R[X]), Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A) → p = 0
have a : ∀ (a : R[X]),
  ¬(a ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a : A) (0 : A)) ↔
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a : A) (0 : A) → a = 0
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Defs (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
a : R[X]
⊢ ¬(a ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a : A) (0 : A)) ↔
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a : A) (0 : A) → a = 0
have a : ¬(a ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a : A) (0 : A)) →
  Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a : A) (0 : A) → a = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Defs (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
a_1 : R[X]
a :
  ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A)) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
⊢ ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A)) ↔
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
have a₁ : (Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0) →
  ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Defs (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
a_1 : R[X]
a :
  ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A)) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₁ :
  (Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0) →
    ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
⊢ ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A)) ↔
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
have a₂ : ¬a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Defs (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
a_1 : R[X]
a :
  ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A)) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₁ :
  (Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0) →
    ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
a₂ : ¬a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
⊢ ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A)) ↔
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
have a₃ : ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
  Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Defs (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
a_1 : R[X]
a :
  ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A)) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₁ :
  (Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0) →
    ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
a₂ : ¬a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₃ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₄ : ¬a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₅ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₆ : ¬a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₇ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
⊢ ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A)) ↔
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
have a₈ : ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
  ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Defs (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
a_1 : R[X]
a :
  ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A)) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₁ :
  (Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0) →
    ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
a₂ : ¬a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₃ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₄ : ¬a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₅ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₆ : ¬a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₇ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
a₈ :
  ¬Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) →
    ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
⊢ ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A)) ↔
    Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → a_1 = 0
have a₉ : a_1 = 0 → ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
Tactic: tauto