awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : { s : Set A // AlgebraicIndepOn R _root_.id s }
choose :
  ∀ (t : Set A)
    (ht :
      (↑s : Set A) ⊆ t ∧
        IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))),
    #(↑(↑s : Set A) : Type w) ≤
      ⨆ (ι :
        { s : Set A //
          IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s)) }),
        #(↑(↑ι : Set A) : Type w)
⊢ #(↑(↑s : Set A) : Type w) ≤
    ⨆ (ι :
      { s : Set A //
        IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s)) }),
      #(↑(↑ι : Set A) : Type w)

Tactic:
choose t ht using exists_isTranscendenceBasis_superset s.2

Premises used: exists_isTranscendenceBasis_superset, Subtype.property
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : { s : Set A // AlgebraicIndepOn R _root_.id s }
t : Set A
ht :
  (↑s : Set A) ⊆ t ∧
    IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))
⊢ #(↑(↑s : Set A) : Type w) ≤
    ⨆ (ι :
      { s : Set A //
        IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s)) }),
      #(↑(↑ι : Set A) : Type w)

Tactic:
le_ciSup_of_le bddAbove_of_small ⟨t, ht.2⟩ (mk_le_mk_of_subset ht.1)

Premises used: le_ciSup_of_le, Subtype.mk, Cardinal.mk_le_mk_of_subset, And.right, And.left, Cardinal.bddAbove_of_small
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : { s : Set A // AlgebraicIndepOn R _root_.id s }
t : Set A
ht :
  (↑s : Set A) ⊆ t ∧
    IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))
⊢ #(↑(↑s : Set A) : Type w) ≤
    ⨆ (ι :
      { s : Set A //
        IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s)) }),
      #(↑(↑ι : Set A) : Type w)

Tactic:
exact le_ciSup_of_le bddAbove_of_small ⟨t, ht.2⟩ (mk_le_mk_of_subset ht.1)

Premises used: le_ciSup_of_le, Cardinal.bddAbove_of_small
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
i : AlgebraicIndependent R x
mp :
  IsTranscendenceBasis R x →
    ∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
mpr :
  (∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j) →
    IsTranscendenceBasis R x
⊢ IsTranscendenceBasis R x ↔
    ∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j

Tactic:
fconstructor
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
κ : Type w
w : κ → A
i' : AlgebraicIndependent R w
j : ι → κ
i : AlgebraicIndependent R (w ∘ j)
p : IsTranscendenceBasis R (w ∘ j)
⊢ range (w ∘ j) = range w

Tactic:
have p := p.2 (range w) i'.coe_range (range_comp_subset_range _ _)
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
κ : Type w
w : κ → A
i' : AlgebraicIndependent R w
j : ι → κ
i : AlgebraicIndependent R (w ∘ j)
p_1 : IsTranscendenceBasis R (w ∘ j)
p : range (w ∘ j) = range w
⊢ w '' range j = w '' univ

Tactic:
rw [range_comp, ← @image_univ _ _ w] at p

Premises used: Set.range_comp, Set.image_univ
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
κ : Type w
w : κ → A
i' : AlgebraicIndependent R w
j : ι → κ
i : AlgebraicIndependent R (w ∘ j)
p_1 : IsTranscendenceBasis R (w ∘ j)
p : w '' range j = w '' univ
⊢ Surjective j

Tactic:
range_eq_univ.mp (image_injective.mpr i'.injective p)

Premises used: Iff.mpr, Set.range_eq_univ, Set.image_injective, Iff.mp, AlgebraicIndependent.injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
κ : Type w
w : κ → A
i' : AlgebraicIndependent R w
j : ι → κ
i : AlgebraicIndependent R (w ∘ j)
p_1 : IsTranscendenceBasis R (w ∘ j)
p : w '' range j = w '' univ
⊢ Surjective j

Tactic:
exact range_eq_univ.mp (image_injective.mpr i'.injective p)

Premises used: Iff.mpr, Set.range_eq_univ, Set.image_injective, Iff.mp, AlgebraicIndependent.injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
i : AlgebraicIndependent R x
p : ∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
right : ∀ (s : Set A), AlgebraicIndepOn R _root_.id s → range x ⊆ s → range x = s
⊢ IsTranscendenceBasis R x

Tactic:
use i
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
i : AlgebraicIndependent R x
p : ∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
w : Set A
i' : AlgebraicIndepOn R _root_.id w
h : range x ⊆ w
h₁ :
  ∀ (x_1 : ι),
    Function.comp (β := (↑w : Type w)) (Subtype.val (p := fun (x : A) ↦ x ∈ w))
        (fun (i : ι) ↦ Subtype.mk (p := fun (x : A) ↦ x ∈ w) (x i) ⋯) x_1 =
      x x_1
⊢ (Function.comp (β := (↑w : Type w)) (Subtype.val (p := fun (x : A) ↦ x ∈ w)) fun (i : ι) ↦
      Subtype.mk (p := fun (x : A) ↦ x ∈ w) (x i) ⋯) =
    x

Tactic:
ext
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
i : AlgebraicIndependent R x
p : ∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
w : Set A
i' : AlgebraicIndepOn R _root_.id w
h : range x ⊆ w
x_1 : ι
⊢ Function.comp (β := (↑w : Type w)) (Subtype.val (p := fun (x : A) ↦ x ∈ w))
      (fun (i : ι) ↦ Subtype.mk (p := fun (x : A) ↦ x ∈ w) (x i) ⋯) x_1 =
    x x_1

Tactic:
simp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
i : AlgebraicIndependent R x
p : ∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
w : Set A
i' : AlgebraicIndepOn R _root_.id w
h : range x ⊆ w
⊢ Surjective.{u + 1, w + 1} (β := (↑w : Type w)) fun (i : ι) ↦ Subtype.mk (p := fun (x : A) ↦ x ∈ w) (x i) ⋯

Tactic:
specialize p w ((↑) : w → A) i' (fun i => ⟨x i, range_subset_iff.mp h i⟩) (by ext; simp)

Premises used: Set.Elem, Subtype.mk, Iff.mp, Set.range_subset_iff, Subtype.val
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndepOn R _root_.id w
h : range x ⊆ w
p : Surjective.{u + 1, w + 1} (β := (↑w : Type w)) fun (i : ι) ↦ Subtype.mk (p := fun (x : A) ↦ x ∈ w) (x i) ⋯
⊢ Eq.{w + 1} (α := Set A)
    ((fun (s : Set { x : A // x ∈ w }) ↦ Subtype.val (p := fun (x : A) ↦ x ∈ w) '' s)
      (range fun (i : ι) ↦ Subtype.mk (p := fun (x : A) ↦ x ∈ w) (x i) ⋯))
    ((fun (s : Set { x : A // x ∈ w }) ↦ Subtype.val (p := fun (x : A) ↦ x ∈ w) '' s) univ)

Tactic:
have q := congr_arg (fun s => ((↑) : w → A) '' s) p.range_eq
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndepOn R _root_.id w
h : range x ⊆ w
p : Surjective.{u + 1, w + 1} (β := (↑w : Type w)) fun (i : ι) ↦ Subtype.mk (p := fun (x : A) ↦ x ∈ w) (x i) ⋯
q :
  Eq.{w + 1} (α := Set A)
    (Set.image (α := { x : A // x ∈ w }) (Subtype.val (p := fun (x : A) ↦ x ∈ w))
      (range fun (i : ι) ↦ Subtype.mk (p := fun (x : A) ↦ x ∈ w) (x i) ⋯))
    (Set.image (α := { x : A // x ∈ w }) (Subtype.val (p := fun (x : A) ↦ x ∈ w)) univ)
⊢ Eq.{w + 1} (α := Set A) ((fun (x_1 : ι) ↦ (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ w) (x x_1) ⋯) : A)) '' univ)
    (Set.image (α := { x : A // x ∈ w }) (Subtype.val (p := fun (x : A) ↦ x ∈ w)) univ)

Tactic:
rw [← image_univ, image_image] at q

Premises used: Set.image_image, Set.image_univ
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndepOn R _root_.id w
h : range x ⊆ w
p : Surjective.{u + 1, w + 1} (β := (↑w : Type w)) fun (i : ι) ↦ Subtype.mk (p := fun (x : A) ↦ x ∈ w) (x i) ⋯
q :
  Eq.{w + 1} (α := Set A) ((fun (x_1 : ι) ↦ (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ w) (x x_1) ⋯) : A)) '' univ)
    (Set.image (α := { x : A // x ∈ w }) (Subtype.val (p := fun (x : A) ↦ x ∈ w)) univ)
⊢ range x = w

Tactic:
simpa using q
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
hx : IsTranscendenceBasis R x
isAlgebraic₁ : ∀ (x_1 : A), IsAlgebraic (↥(adjoin R (range x))) x_1
⊢ Algebra.IsAlgebraic (↥(adjoin R (range x))) A

Tactic:
constructor
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
isAlgebraic₁ : ¬AlgebraicIndependent.{u, u_1, w} R (A := A) fun (o : Option ι) ↦ o.elim a x
⊢ IsAlgebraic (↥(adjoin R (range x))) a

Tactic:
rw [← not_iff_comm.1 (hx.1.option_iff_transcendental _).symm]

Premises used: AlgebraicIndependent.option_iff_transcendental, And.left, Iff.mp, Iff.symm, not_iff_comm
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent.{u, u_1, w} R (A := A) fun (o : Option ι) ↦ o.elim a x
y : ι
⊢ Membership.mem (γ := Set A) (range fun (o : Option ι) ↦ o.elim a x) (x y)

Tactic:
⟨some y, rfl⟩

Premises used: Set.Mem, setOf, Option.some, Exists.intro, Set.range, rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent.{u, u_1, w} R (A := A) fun (o : Option ι) ↦ o.elim a x
y : ι
⊢ Membership.mem (γ := Set A) (range fun (o : Option ι) ↦ o.elim a x) (x y)

Tactic:
exact ⟨some y, rfl⟩
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent.{u, u_1, w} R (A := A) fun (o : Option ι) ↦ o.elim a x
⊢ range x ⊆ range fun (o : Option ι) ↦ o.elim a x

Tactic:
have h₁ : range x ⊆ range fun o : Option ι => o.elim a x := by
    rintro x ⟨y, rfl⟩
    exact ⟨some y, rfl⟩
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent.{u, u_1, w} R (A := A) fun (o : Option ι) ↦ o.elim a x
h₁ : range x ⊆ range fun (o : Option ι) ↦ o.elim a x
h : range x = range fun (o : Option ι) ↦ o.elim a x
rw : Membership.mem (γ := Set A) (range fun (o : Option ι) ↦ o.elim a x) a
⊢ a ∈ range x

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent.{u, u_1, w} R (A := A) fun (o : Option ι) ↦ o.elim a x
h₁ : range x ⊆ range fun (o : Option ι) ↦ o.elim a x
h : range x = range fun (o : Option ι) ↦ o.elim a x
⊢ Membership.mem (γ := Set A) (range fun (o : Option ι) ↦ o.elim a x) a

Tactic:
⟨none, rfl⟩

Premises used: Set.Mem, setOf, Option.none, Exists.intro, Set.range, rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent.{u, u_1, w} R (A := A) fun (o : Option ι) ↦ o.elim a x
h₁ : range x ⊆ range fun (o : Option ι) ↦ o.elim a x
h : range x = range fun (o : Option ι) ↦ o.elim a x
⊢ Membership.mem (γ := Set A) (range fun (o : Option ι) ↦ o.elim a x) a

Tactic:
exact ⟨none, rfl⟩
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent.{u, u_1, w} R (A := A) fun (o : Option ι) ↦ o.elim a x
h₁ : range x ⊆ range fun (o : Option ι) ↦ o.elim a x
h : range x = range fun (o : Option ι) ↦ o.elim a x
⊢ a ∈ range x

Tactic:
have : a ∈ range x := by
      rw [h]
      exact ⟨none, rfl⟩
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent.{u, u_1, w} R (A := A) fun (o : Option ι) ↦ o.elim a x
h₁ : range x ⊆ range fun (o : Option ι) ↦ o.elim a x
h : range x = range fun (o : Option ι) ↦ o.elim a x
this : a ∈ range x
rcases :
  ∀ (b : ι) (ai : AlgebraicIndependent.{u, u_1, w} R (A := A) fun (o : Option ι) ↦ o.elim (x b) x)
    (h₁ : range x ⊆ range fun (o : Option ι) ↦ o.elim (x b) x)
    (h : range x = range fun (o : Option ι) ↦ o.elim (x b) x), False
⊢ False

Tactic:
rcases this with ⟨b, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
hx : IsTranscendenceBasis R x
b : ι
ai : AlgebraicIndependent.{u, u_1, w} R (A := A) fun (o : Option ι) ↦ o.elim (x b) x
h₁ : range x ⊆ range fun (o : Option ι) ↦ o.elim (x b) x
h : range x = range fun (o : Option ι) ↦ o.elim (x b) x
⊢ some b = none

Tactic:
have : some b = none := ai.injective rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
hx : IsTranscendenceBasis R x
b : ι
ai : AlgebraicIndependent.{u, u_1, w} R (A := A) fun (o : Option ι) ↦ o.elim (x b) x
h₁ : range x ⊆ range fun (o : Option ι) ↦ o.elim (x b) x
h : range x = range fun (o : Option ι) ↦ o.elim (x b) x
this : some b = none
⊢ False

Tactic:
simpa
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent.{u, u_1, w} R (A := A) fun (o : Option ι) ↦ o.elim a x
h₁ : range x ⊆ range fun (o : Option ι) ↦ o.elim a x
⊢ range x ≠ range fun (o : Option ι) ↦ o.elim a x

Tactic:
have h₂ : range x ≠ range fun o : Option ι => o.elim a x := by
    intro h
    have : a ∈ range x := by
      rw [h]
      exact ⟨none, rfl⟩
    rcases this with ⟨b, rfl⟩
    have : some b = none := ai.injective rfl
    simpa
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent.{u, u_1, w} R (A := A) fun (o : Option ι) ↦ o.elim a x
h₁ : range x ⊆ range fun (o : Option ι) ↦ o.elim a x
h₂ : range x ≠ range fun (o : Option ι) ↦ o.elim a x
⊢ False

Tactic:
h₂ (hx.2 (Set.range fun o : Option ι => o.elim a x)
    ((algebraicIndependent_subtype_range ai.injective).2 ai) h₁)

Premises used: Iff.mpr, algebraicIndependent_subtype_range, And.right, Set.range, AlgebraicIndependent.injective, Option.elim
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent.{u, u_1, w} R (A := A) fun (o : Option ι) ↦ o.elim a x
h₁ : range x ⊆ range fun (o : Option ι) ↦ o.elim a x
h₂ : range x ≠ range fun (o : Option ι) ↦ o.elim a x
⊢ False

Tactic:
exact h₂ (hx.2 (Set.range fun o : Option ι => o.elim a x)
    ((algebraicIndependent_subtype_range ai.injective).2 ai) h₁)

Premises used: Iff.mpr, algebraicIndependent_subtype_range, And.right, Set.range, AlgebraicIndependent.injective, Option.elim
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
ind : AlgebraicIndependent R x
⊢ IsTranscendenceBasis R x ↔ Algebra.IsAlgebraic (↥(adjoin R (range x))) A

Tactic:
⟨(·.isAlgebraic), fun alg ↦ ⟨ind, fun s ind_s hxs ↦ of_not_not fun hxs' ↦ ?_⟩⟩

Premises used: And.intro, Iff.intro, of_not_not, IsTranscendenceBasis.isAlgebraic
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
ind : AlgebraicIndependent R x
refine :
  ∀ (alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A) (s : Set A) (ind_s : AlgebraicIndepOn R _root_.id s)
    (hxs : range x ⊆ s) (hxs' : ¬range x = s), False
⊢ IsTranscendenceBasis R x ↔ Algebra.IsAlgebraic (↥(adjoin R (range x))) A

Tactic:
refine ⟨(·.isAlgebraic), fun alg ↦ ⟨ind, fun s ind_s hxs ↦ of_not_not fun hxs' ↦ ?_⟩⟩
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
ind : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
hxs' : ¬range x = s
⊢ ¬s ⊆ range x

Tactic:
have : ¬ s ⊆ range x := (hxs' <| hxs.antisymm ·)
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
ind : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
hxs' : ¬range x = s
this : ¬s ⊆ range x
have : ∀ (a : A) (has : a ∈ s) (hax : a ∉ range x), False
⊢ False

Tactic:
have ⟨a, has, hax⟩ := not_subset.mp this
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
ind : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
hxs' : ¬range x = s
this : ¬s ⊆ range x
a : A
has : a ∈ s
hax : a ∉ range x
rw : range x = range (Subtype.val (p := fun (x : A) ↦ x ∈ s) ∘ Set.inclusion (s := range x) (t := s) hxs)
rw₁ : range x = range (ι := (↑(range x) : Type w)) (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))
rw₂ rw₃ : range x = range x
⊢ range x = Subtype.val (p := fun (x : A) ↦ x ∈ s) '' range (Set.inclusion (s := range x) (t := s) hxs)

Tactic:
rw [← range_comp, val_comp_inclusion, Subtype.range_val]

Premises used: Set.range_comp, Set.val_comp_inclusion, Subtype.range_val
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
ind : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
hxs' : ¬range x = s
this : ¬s ⊆ range x
a : A
has : a ∈ s
hax : a ∉ range x
rw :
  ∀
    (alg :
      Algebra.IsAlgebraic
        (↥(adjoin R (Subtype.val (p := fun (x : A) ↦ x ∈ s) '' range (Set.inclusion (s := range x) (t := s) hxs)))) A)
    (hxs' : ¬range x = s) (this : ¬s ⊆ range x) (a : A) (has : a ∈ s) (hax : a ∉ range x), False
⊢ False

Tactic:
rw [show range x = Subtype.val '' range (Set.inclusion hxs) by
    rw [← range_comp, val_comp_inclusion, Subtype.range_val]] at alg
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
ind : AlgebraicIndependent R x
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
alg :
  Algebra.IsAlgebraic
    (↥(adjoin R (Subtype.val (p := fun (x : A) ↦ x ∈ s) '' range (Set.inclusion (s := range x) (t := s) hxs)))) A
hxs' : ¬range x = s
this : ¬s ⊆ range x
a : A
has : a ∈ s
hax : a ∉ range x
⊢ False

Tactic:
ind_s.transcendental_adjoin (s := range (inclusion hxs)) (i := ⟨a, has⟩) ?_ (alg.1 _)

Premises used: Algebra.IsAlgebraic.isAlgebraic, AlgebraicIndependent.transcendental_adjoin
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
ind : AlgebraicIndependent R x
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
alg :
  Algebra.IsAlgebraic
    (↥(adjoin R (Subtype.val (p := fun (x : A) ↦ x ∈ s) '' range (Set.inclusion (s := range x) (t := s) hxs)))) A
hxs' : ¬range x = s
this : ¬s ⊆ range x
a : A
has : a ∈ s
hax : a ∉ range x
refine : Subtype.mk (p := fun (x : A) ↦ x ∈ s) a has ∉ range (Set.inclusion (s := range x) (t := s) hxs)
⊢ False

Tactic:
refine ind_s.transcendental_adjoin (s := range (inclusion hxs)) (i := ⟨a, has⟩) ?_ (alg.1 _)

Premises used: Algebra.IsAlgebraic.isAlgebraic, AlgebraicIndependent.transcendental_adjoin
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
ind : AlgebraicIndependent R x
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
alg :
  Algebra.IsAlgebraic
    (↥(adjoin R (Subtype.val (p := fun (x : A) ↦ x ∈ s) '' range (Set.inclusion (s := range x) (t := s) hxs)))) A
hxs' : ¬range x = s
this : ¬s ⊆ range x
a : A
has : a ∈ s
hax : a ∉ range x
⊢ Subtype.mk (p := fun (x : A) ↦ x ∈ s) a has ∉ range (Set.inclusion (s := range x) (t := s) hxs)

Tactic:
simpa using hax