awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Algebraic.Cardinality
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

Tactic:
(Subtype.heq_iff_coe_eq ?_).1 h.2

Premises used: And.right, Iff.mp, Subtype.heq_iff_coe_eq
-- Module: Mathlib.RingTheory.Algebraic.Cardinality
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 ⋯)
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))
                ⋯) :
            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))
                ⋯) :
            R[X])
          L
⊢ x = y

Tactic:
refine (Subtype.heq_iff_coe_eq ?_).1 h.2

Premises used: And.right, Iff.mp, Subtype.heq_iff_coe_eq
-- Module: Mathlib.RingTheory.Algebraic.Cardinality
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_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_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))
                ⋯) :
            R[X])
          L

Tactic:
simp only [h.1, forall_true_iff]

Premises used: And.left, forall_true_iff
-- Module: Mathlib.RingTheory.Algebraic.Cardinality
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.{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]
-- Module: Mathlib.RingTheory.Algebraic.Cardinality
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 })
rwa₁ rwa₂ rwa₃ 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 })
⊢ lift.{u, v} #L ≤ #((p : R[X]) × { x : L // x ∈ p.aroots L })

Tactic:
rwa [lift_umax, lift_id'.{v}] at this

Premises used: Cardinal.lift_umax
-- Module: Mathlib.RingTheory.Algebraic.Cardinality
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 : #((p : R[X]) × { x : L // x ∈ p.aroots L }) = #((i : R[X]) × (↑{x : L | x ∈ i.aroots L} : Type v))
⊢ #((p : R[X]) × { x : L // x ∈ p.aroots L }) = sum.{u, v} fun (p : R[X]) ↦ #(↑{x : L | x ∈ p.aroots L} : Type v)

Tactic:
rw [← mk_sigma]

Premises used: Cardinal.mk_sigma
-- Module: Mathlib.RingTheory.Algebraic.Cardinality
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 }) = #((i : R[X]) × (↑{x : L | x ∈ i.aroots L} : Type v))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Algebraic.Cardinality
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] * ℵ₀
rw₁ rw₂ : lift.{v, u} #R[X] * ℵ₀ = lift.{v, u} #R[X] * ℵ₀
⊢ (sum.{u, v} fun (x : R[X]) ↦ ℵ₀) = lift.{v, u} #R[X] * ℵ₀

Tactic:
rw [sum_const, lift_aleph0]

Premises used: Cardinal.lift_aleph0, Cardinal.sum_const
-- Module: Mathlib.RingTheory.Algebraic.Cardinality
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
h₁ : lift.{v, u} #R[X] ≤ lift.{v, u} (max #R ℵ₀)
⊢ max (max (lift.{v, u} #R[X]) ℵ₀) ℵ₀ ≤ max (max (lift.{v, u} (max #R ℵ₀)) ℵ₀) ℵ₀

Tactic:
gcongr
-- Module: Mathlib.RingTheory.Algebraic.Cardinality
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.{v, u} #R[X] ≤ lift.{v, u} (max #R ℵ₀)

Tactic:
simp only [lift_le, Polynomial.cardinalMk_le_max]

Premises used: Polynomial.cardinalMk_le_max, Cardinal.lift_le
-- Module: Mathlib.RingTheory.Algebraic.Cardinality
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} (max #R ℵ₀)) ℵ₀) ℵ₀ = max (lift.{v, u} #R) ℵ₀

Tactic:
simp
-- Module: Mathlib.RingTheory.Algebraic.Cardinality
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : Type u
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra R L
inst_5 : IsTorsionFree R L
inst_6 : Algebra.IsAlgebraic R L
⊢ #L ≤ #((p : R[X]) × { x : L // x ∈ p.aroots L })

Tactic:
simpa only [lift_id] using lift_cardinalMk_le_sigma_polynomial R L

Premises used: Algebra.IsAlgebraic.lift_cardinalMk_le_sigma_polynomial, Cardinal.lift_id
-- Module: Mathlib.RingTheory.Algebraic.Cardinality
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : Type u
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra R L
inst_5 : IsTorsionFree R L
inst_6 : Algebra.IsAlgebraic R L
⊢ #L ≤ max #R ℵ₀

Tactic:
simpa only [lift_id] using lift_cardinalMk_le_max R L

Premises used: Algebra.IsAlgebraic.lift_cardinalMk_le_max, Cardinal.lift_id
-- Module: Mathlib.RingTheory.Algebraic.Defs
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
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
⊢ Transcendental R x ↔ ∀ (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]

Premises used: IsAlgebraic, not_exists, Transcendental
-- Module: Mathlib.RingTheory.Algebraic.Defs
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
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
⊢ (∀ (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:
congr! 1
-- Module: Mathlib.RingTheory.Algebraic.Defs
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₉ : a_1 = 0 → ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
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₁₁ : a_1 = 0 → ¬(a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A))
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) → False
a₁₃ : a_1 = 0 → a_1 ≠ 0 ∧ Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → False
a₁₄ 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₁₈ :
  ¬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) → False
a₁₉ : a_1 = 0 → a_1 ≠ 0 → Eq.{v + 1} (α := A) ((aeval x : (a : R[X]) → A) a_1 : A) (0 : A) → False
⊢ ¬(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

Tactic:
tauto
-- Module: Mathlib.RingTheory.Algebraic.Defs
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Algebra.IsAlgebraic R A
obtain : ∀ (p : R[X]) (hp : p ≠ 0), Nontrivial R
⊢ Nontrivial R

Tactic:
obtain ⟨p, hp, -⟩ := Algebra.IsAlgebraic.isAlgebraic (R := R) (0 : A)

Premises used: Algebra.IsAlgebraic.isAlgebraic, OfNat.ofNat
-- Module: Mathlib.RingTheory.Algebraic.Defs
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Algebra.IsAlgebraic R A
p : R[X]
hp : p ≠ 0
⊢ Nontrivial R

Tactic:
.of_polynomial_ne hp

Premises used: Polynomial.Nontrivial.of_polynomial_ne
-- Module: Mathlib.RingTheory.Algebraic.Defs
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Algebra.IsAlgebraic R A
p : R[X]
hp : p ≠ 0
⊢ Nontrivial R

Tactic:
exact .of_polynomial_ne hp
-- Module: Mathlib.RingTheory.Algebraic.Defs
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
⊢ Algebra.IsAlgebraic R A ↔ ∀ (x : A), IsAlgebraic R x

Tactic:
⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Premises used: Algebra.IsAlgebraic.mk, _private.0.Algebra.isAlgebraic_def.match_1, Iff.intro
-- Module: Mathlib.RingTheory.Algebraic.Defs
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
⊢ Algebra.Transcendental R A ↔ ∃ (x : A), Transcendental R x

Tactic:
⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Premises used: Exists, Algebra.Transcendental.mk, Transcendental, Iff.intro, _private.0.Algebra.transcendental_def.match_1
-- Module: Mathlib.RingTheory.Algebraic.Defs
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
⊢ Algebra.Transcendental R A ↔ ¬Algebra.IsAlgebraic R A

Tactic:
simp [isAlgebraic_def, transcendental_def, Transcendental]

Premises used: Transcendental, Algebra.isAlgebraic_def, Algebra.transcendental_def
-- Module: Mathlib.RingTheory.Algebraic.Defs
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
rw : (∀ (x : ↥S), IsAlgebraic R (↑x : A)) ↔ ∀ (x : ↥S), IsAlgebraic R x
⊢ (∀ x ∈ S, IsAlgebraic R x) ↔ Algebra.IsAlgebraic.{u, v} R ↥S

Tactic:
rw [Subtype.forall', Algebra.isAlgebraic_def]

Premises used: Algebra.isAlgebraic_def, Subtype.forall'
-- Module: Mathlib.RingTheory.Algebraic.Defs
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ (∀ (x : ↥S), IsAlgebraic R (↑x : A)) ↔ ∀ (x : ↥S), IsAlgebraic R x

Tactic:
forall_congr' fun x => exists_congr fun p => and_congr Iff.rfl ?_

Premises used: Iff.rfl, exists_congr, forall_congr', and_congr
-- Module: Mathlib.RingTheory.Algebraic.Defs
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
refine :
  ∀ (x : ↥S) (p : R[X]),
    Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A) ↔
      Eq.{v + 1} (α := ↥S) ((aeval x : (a : R[X]) → ↥S) p : ↥S) (0 : ↥S)
⊢ (∀ (x : ↥S), IsAlgebraic R (↑x : A)) ↔ ∀ (x : ↥S), IsAlgebraic R x

Tactic:
refine forall_congr' fun x => exists_congr fun p => and_congr Iff.rfl ?_

Premises used: Iff.rfl, exists_congr, forall_congr', and_congr
-- Module: Mathlib.RingTheory.Algebraic.Defs
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
⊢ Function.Injective (α := ↥S) (β := A) (⇑S.val : (a : ↥S) → A)

Tactic:
have h : Function.Injective S.val := Subtype.val_injective
-- Module: Mathlib.RingTheory.Algebraic.Defs
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
h : Function.Injective (α := ↥S) (β := A) (⇑S.val : (a : ↥S) → A)
rw : Eq (α := A) ((S.val : (a : ↥S) → A) ((aeval x : (a : R[X]) → ↥S) p : ↥S) : A) (0 : A)
| Eq.{v + 1} (α := ↥S) ((aeval x : (a : R[X]) → ↥S) p : ↥S) (0 : ↥S)

Tactic:
rw [← h.eq_iff, map_zero]

Premises used: Function.Injective.eq_iff, map_zero
-- Module: Mathlib.RingTheory.Algebraic.Defs
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
h : Function.Injective (α := ↥S) (β := A) (⇑S.val : (a : ↥S) → A)
conv_rhs :
  Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A) ↔
    Eq (α := A) ((S.val : (a : ↥S) → A) ((aeval x : (a : R[X]) → ↥S) p : ↥S) : A) (0 : A)
⊢ Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A) ↔
    Eq.{v + 1} (α := ↥S) ((aeval x : (a : R[X]) → ↥S) p : ↥S) (0 : ↥S)

Tactic:
conv_rhs => rw [← h.eq_iff, map_zero]

Premises used: Function.Injective.eq_iff, map_zero
-- Module: Mathlib.RingTheory.Algebraic.Defs
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
h : Function.Injective (α := ↥S) (β := A) (⇑S.val : (a : ↥S) → A)
rw :
  Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A) ↔
    Eq.{v + 1} (α := A) (((aeval ((S.val : (a : ↥S) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
rw₁ rw₂ :
  Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A) ↔
    Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A)
⊢ Eq.{v + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) (0 : A) ↔
    Eq (α := A) ((S.val : (a : ↥S) → A) ((aeval x : (a : R[X]) → ↥S) p : ↥S) : A) (0 : A)

Tactic:
rw [← aeval_algHom_apply, S.val_apply]

Premises used: Subalgebra.val_apply, Polynomial.aeval_algHom_apply
-- Module: Mathlib.RingTheory.Algebraic.Defs
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
⊢ Algebra.IsAlgebraic R A ↔ ∀ (x : A), Membership.mem (γ := Subalgebra R A) ⊤ x → IsAlgebraic R x

Tactic:
simp only [Algebra.isAlgebraic_def, Algebra.mem_top, forall_prop_of_true]

Premises used: Algebra.mem_top, Algebra.isAlgebraic_def, forall_prop_of_true
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial R
x : A
⊢ IsIntegral R x → IsAlgebraic R x

Tactic:
fun ⟨p, hp, hpx⟩ => ⟨p, hp.ne_zero, hpx⟩

Premises used: IsAlgebraic, _private.0.IsIntegral.isAlgebraic.match_1, And.intro, Exists.intro, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u
S : Type u_1
A : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R A
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
inst_8 : Algebra.IsIntegral R A
⊢ Algebra.IsAlgebraic R A

Tactic:
⟨fun a ↦ (Algebra.IsIntegral.isIntegral a).isAlgebraic⟩

Premises used: Algebra.IsIntegral.isIntegral, IsIntegral.isAlgebraic, Algebra.IsAlgebraic.mk
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
K : Type u
A : Type v
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
x : A
⊢ IsAlgebraic K x ↔ IsIntegral K x

Tactic:
⟨?_, IsIntegral.isAlgebraic⟩

Premises used: IsIntegral.isAlgebraic, Iff.intro
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
K : Type u
A : Type v
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
x : A
refine : IsAlgebraic K x → IsIntegral K x
⊢ IsAlgebraic K x ↔ IsIntegral K x

Tactic:
refine ⟨?_, IsIntegral.isAlgebraic⟩
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
K : Type u
A : Type v
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
x : A
p : K[X]
hp : p ≠ 0
hpx : Eq.{v + 1} (α := A) ((aeval x : (a : K[X]) → A) p : A) (0 : A)
⊢ IsIntegral K x

Tactic:
⟨_, monic_mul_leadingCoeff_inv hp, ?_⟩

Premises used: RingHom.IsIntegralElem, IsIntegral, Polynomial.monic_mul_leadingCoeff_inv, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
K : Type u
A : Type v
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
x : A
p : K[X]
hp : p ≠ 0
hpx : Eq.{v + 1} (α := A) ((aeval x : (a : K[X]) → A) p : A) (0 : A)
refine : eval₂ (algebraMap K A) x (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) = 0
⊢ IsIntegral K x

Tactic:
refine ⟨_, monic_mul_leadingCoeff_inv hp, ?_⟩