awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
have : ∀ (ra : R) (a0 : ra ≠ 0) (int_a : IsIntegral R (ra • a)), IsAlgebraic R (a + b)
⊢ IsAlgebraic R (a + b)

Tactic:
have ⟨ra, a0, int_a⟩ := ha.exists_integral_multiple
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
have : ∀ (rb : R) (b0 : rb ≠ 0) (int_b : IsIntegral R (rb • b)), IsAlgebraic R (a + b)
⊢ IsAlgebraic R (a + b)

Tactic:
have ⟨rb, b0, int_b⟩ := hb.exists_integral_multiple
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsAlgebraic R (a + b)

Tactic:
IsAlgebraic.iff_exists_smul_integral.mpr ⟨_, mul_ne_zero b0 a0, ?_⟩

Premises used: Iff.mpr, IsAlgebraic.iff_exists_smul_integral, And.intro, Exists.intro, mul_ne_zero
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
refine : IsIntegral R ((rb * ra) • (a + b))
⊢ IsAlgebraic R (a + b)

Tactic:
refine IsAlgebraic.iff_exists_smul_integral.mpr ⟨_, mul_ne_zero b0 a0, ?_⟩

Premises used: Iff.mpr, IsAlgebraic.iff_exists_smul_integral, And.intro, Exists.intro, mul_ne_zero
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
rw : IsIntegral R (rb • ra • a + ra • rb • b)
⊢ IsIntegral R ((rb * ra) • (a + b))

Tactic:
rw [smul_add, mul_smul, mul_comm, mul_smul]

Premises used: mul_comm, SemigroupAction.mul_smul, smul_add
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsIntegral R (rb • ra • a + ra • rb • b)

Tactic:
(int_a.smul _).add (int_b.smul _)

Premises used: IsIntegral.add, IsIntegral.smul
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsIntegral R (rb • ra • a + ra • rb • b)

Tactic:
exact (int_a.smul _).add (int_b.smul _)

Premises used: IsIntegral.add, IsIntegral.smul
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
⊢ IsAlgebraic R (a - b)

Tactic:
sub_eq_add_neg a b ▸ ha.add hb.neg

Premises used: sub_eq_add_neg, Eq.rec, IsAlgebraic.add, IsAlgebraic.neg, Eq.symm
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
a : S
ha : IsAlgebraic R a
n : ℕ
⊢ IsAlgebraic R (a ^ n)

Tactic:
have := ha.nontrivial
  n.rec (pow_zero a ▸ isAlgebraic_one) fun _ h ↦ pow_succ a _ ▸ h.mul ha

Premises used: Nat.rec, IsAlgebraic.nontrivial
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
alg : Algebra.IsAlgebraic S A
⊢ Algebra.IsAlgebraic R A

Tactic:
⟨fun _ ↦ (alg.1 _).restrictScalars _⟩

Premises used: Algebra.IsAlgebraic.isAlgebraic, IsAlgebraic.restrictScalars, Algebra.IsAlgebraic.mk
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsIntegral R S
alg : Algebra.IsAlgebraic S A
⊢ Algebra.IsAlgebraic R A

Tactic:
⟨fun _ ↦ (alg.1 _).restrictScalars_of_isIntegral _⟩

Premises used: Algebra.IsAlgebraic.isAlgebraic, IsAlgebraic.restrictScalars_of_isIntegral, Algebra.IsAlgebraic.mk
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
int : Algebra.IsIntegral S A
⊢ Algebra.IsAlgebraic R A

Tactic:
⟨fun _ ↦ (int.1 _).trans_isAlgebraic _⟩

Premises used: Algebra.IsIntegral.isIntegral, Algebra.IsAlgebraic.mk, IsIntegral.trans_isAlgebraic
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsIntegral R S
inst_9 : FaithfulSMul R S
a : A
⊢ IsAlgebraic R a ↔ IsAlgebraic S a

Tactic:
⟨.extendScalars (FaithfulSMul.algebraMap_injective ..), .restrictScalars_of_isIntegral _⟩

Premises used: IsAlgebraic.extendScalars, IsAlgebraic.restrictScalars_of_isIntegral, FaithfulSMul.algebraMap_injective, Iff.intro
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsIntegral R S
inst_9 : FaithfulSMul R S
simp_rw : (∀ (x : A), IsAlgebraic R x) ↔ ∀ (x : A), IsAlgebraic S x
⊢ Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic S A

Tactic:
simp_rw [Algebra.isAlgebraic_def, Algebra.IsIntegral.isAlgebraic_iff R S]

Premises used: Algebra.IsIntegral.isAlgebraic_iff, Algebra.isAlgebraic_def
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
inst_9 : FaithfulSMul R S
a : A
⊢ IsAlgebraic R a ↔ IsAlgebraic S a

Tactic:
⟨.extendScalars (FaithfulSMul.algebraMap_injective ..), .restrictScalars _⟩

Premises used: IsAlgebraic.restrictScalars, IsAlgebraic.extendScalars, FaithfulSMul.algebraMap_injective, Iff.intro
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
inst_9 : FaithfulSMul R S
simp_rw : (∀ (x : A), IsAlgebraic R x) ↔ ∀ (x : A), IsAlgebraic S x
⊢ Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic S A

Tactic:
simp_rw [Algebra.isAlgebraic_def, Algebra.IsAlgebraic.isAlgebraic_iff R S]

Premises used: Algebra.isAlgebraic_def, Algebra.IsAlgebraic.isAlgebraic_iff
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic S A
inst_9 : FaithfulSMul S A
⊢ Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic R S

Tactic:
⟨fun _ ↦ .tower_bot_of_injective (FaithfulSMul.algebraMap_injective S A), fun _ ↦ .trans R S A⟩

Premises used: Algebra.IsAlgebraic.trans, FaithfulSMul.algebraMap_injective, Iff.intro, Algebra.IsAlgebraic.tower_bot_of_injective
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
x : S
⊢ Membership.mem (γ := Subalgebra R S) (algebraicClosure R S) x ↔ IsAlgebraic R x

Tactic:
Iff.rfl

Premises used: IsAlgebraic, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
⊢ LE.le (α := Subalgebra R S) (integralClosure R S) (Subalgebra.algebraicClosure R S)

Tactic:
fun _ ↦ IsIntegral.isAlgebraic

Premises used: IsAlgebraic, Set.Mem, setOf, IsIntegral.isAlgebraic, RingHom.IsIntegralElem, IsIntegral
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
inst_2 : Algebra K S
⊢ Eq (α := Subalgebra K S) (algebraicClosure K S) (integralClosure K S)

Tactic:
SetLike.ext fun _ ↦ isAlgebraic_iff_isIntegral

Premises used: SetLike.ext, isAlgebraic_iff_isIntegral
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
z : A
z' : S
inst_7 : IsDomain R
⊢ Algebra.IsAlgebraic.{u_1, u_2} R ↥(Subalgebra.algebraicClosure R S)

Tactic:
(Subalgebra.isAlgebraic_iff _).mp fun _ ↦ id

Premises used: Set.Mem, id, Iff.mp, Subalgebra.isAlgebraic_iff
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
s : Set S
⊢ Subalgebra.IsAlgebraic (adjoin R s) ↔ ∀ x ∈ s, IsAlgebraic R x

Tactic:
Algebra.adjoin_le_iff (S := Subalgebra.algebraicClosure R S)

Premises used: IsAlgebraic, Set.Mem, setOf, Set.Subset, Subalgebra.IsAlgebraic, Algebra.adjoin_le_iff
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
s : Set S
hs : s.Nonempty
⊢ Subalgebra.IsAlgebraic (adjoin R s) ↔ ∀ x ∈ s, IsAlgebraic R x

Tactic:
⟨fun h x hx ↦ h _ (subset_adjoin hx), fun h ↦
    have ⟨x, hx⟩ := hs
    have := (isDomain_iff_noZeroDivisors_and_nontrivial _).mpr ⟨‹_›, (h x hx).nontrivial⟩
    isAlgebraic_adjoin_iff.mpr h⟩

Premises used: Iff.mpr, Algebra.isAlgebraic_adjoin_iff, Algebra.subset_adjoin, Algebra.adjoin, _private.0.Algebra.isAlgebraic_adjoin_of_nonempty.match_1, Subalgebra.IsAlgebraic, IsAlgebraic.nontrivial, And.intro, Iff.intro, isDomain_iff_noZeroDivisors_and_nontrivial
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
s : S
⊢ Subalgebra.IsAlgebraic (A := S) R[s] ↔ IsAlgebraic R s

Tactic:
(isAlgebraic_adjoin_of_nonempty <| Set.singleton_nonempty s).trans forall_eq

Premises used: Set.singleton_nonempty, forall_eq, Iff.trans, Algebra.isAlgebraic_adjoin_of_nonempty
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
y z : S
hy : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) y
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
have :
  ∀ (t : S) (ht : Membership.mem (γ := Subalgebra R S) R[y] t) (r : R) (hr : r ≠ 0)
    (eq : y * t = (algebraMap R S : (a : R) → S) r), IsAlgebraic R z
⊢ IsAlgebraic R z

Tactic:
have ⟨t, ht, r, hr, eq⟩ := alg_y.exists_nonzero_eq_adjoin_mul hy
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
y z : S
hy : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) y
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : Membership.mem (γ := Subalgebra R S) R[y] t
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S : (a : R) → S) r
⊢ IsAlgebraic R (y * z * t)

Tactic:
have := alg_yz.mul (Algebra.isAlgebraic_adjoin_singleton_iff.mpr alg_y _ ht)
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
y z : S
hy : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) y
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : Membership.mem (γ := Subalgebra R S) R[y] t
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S : (a : R) → S) r
this : IsAlgebraic R (y * z * t)
⊢ IsAlgebraic R (r • z)

Tactic:
rw [mul_right_comm, eq, ← Algebra.smul_def] at this

Premises used: mul_right_comm, Algebra.smul_def
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
y z : S
hy : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) y
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : Membership.mem (γ := Subalgebra R S) R[y] t
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S : (a : R) → S) r
this : IsAlgebraic R (r • z)
⊢ IsAlgebraic R z

Tactic:
this.of_smul (mem_nonZeroDivisors_of_ne_zero hr)

Premises used: IsAlgebraic.of_smul, mem_nonZeroDivisors_of_ne_zero
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors R
y z : S
hy : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) y
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : Membership.mem (γ := Subalgebra R S) R[y] t
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S : (a : R) → S) r
this : IsAlgebraic R (r • z)
⊢ IsAlgebraic R z

Tactic:
exact this.of_smul (mem_nonZeroDivisors_of_ne_zero hr)

Premises used: IsAlgebraic.of_smul, mem_nonZeroDivisors_of_ne_zero
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
a : A
ha : Transcendental R a
inst_8 : Algebra.IsIntegral R S
contrapose : ∀ (ha : ¬Transcendental S a), ¬Transcendental R a
⊢ Transcendental S a

Tactic:
contrapose ha
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
a : A
inst_8 : Algebra.IsIntegral R S
ha : ¬Transcendental S a
rw : ∀ (ha : IsAlgebraic S a), IsAlgebraic R a
⊢ ¬Transcendental R a

Tactic:
rw [Transcendental, not_not] at ha ⊢

Premises used: Classical.not_not, Transcendental
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
a : A
inst_8 : Algebra.IsIntegral R S
ha : IsAlgebraic S a
⊢ IsAlgebraic R a

Tactic:
ha.restrictScalars_of_isIntegral _

Premises used: IsAlgebraic.restrictScalars_of_isIntegral
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
a : A
inst_8 : Algebra.IsIntegral R S
ha : IsAlgebraic S a
⊢ IsAlgebraic R a

Tactic:
exact ha.restrictScalars_of_isIntegral _

Premises used: IsAlgebraic.restrictScalars_of_isIntegral
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
a : A
ha : Transcendental R a
inst_8 : Algebra.IsAlgebraic R S
contrapose : ∀ (ha : ¬Transcendental S a), ¬Transcendental R a
⊢ Transcendental S a

Tactic:
contrapose ha
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
a : A
inst_8 : Algebra.IsAlgebraic R S
ha : ¬Transcendental S a
rw : ∀ (ha : IsAlgebraic S a), IsAlgebraic R a
⊢ ¬Transcendental R a

Tactic:
rw [Transcendental, not_not] at ha ⊢

Premises used: Classical.not_not, Transcendental
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
a : A
inst_8 : Algebra.IsAlgebraic R S
ha : IsAlgebraic S a
⊢ IsAlgebraic R a

Tactic:
ha.restrictScalars _

Premises used: IsAlgebraic.restrictScalars
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
a : A
inst_8 : Algebra.IsAlgebraic R S
ha : IsAlgebraic S a
⊢ IsAlgebraic R a

Tactic:
exact ha.restrictScalars _

Premises used: IsAlgebraic.restrictScalars
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors S
a : S
ha : Transcendental R a
⊢ Transcendental (↥(integralClosure R S)) a

Tactic:
ha.extendScalars_of_isIntegral _

Premises used: Transcendental.extendScalars_of_isIntegral
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors S
a : S
ha : Transcendental R a
inst_4 : IsDomain R
⊢ Transcendental (↥(Subalgebra.algebraicClosure R S)) a

Tactic:
ha.extendScalars _

Premises used: Transcendental.extendScalars
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : FaithfulSMul R S
a : A
inst_9 : Algebra.IsIntegral R S
⊢ Transcendental R a ↔ Transcendental S a

Tactic:
⟨(·.extendScalars_of_isIntegral _), (·.restrictScalars (FaithfulSMul.algebraMap_injective R S))⟩

Premises used: Transcendental.extendScalars_of_isIntegral, FaithfulSMul.algebraMap_injective, Transcendental.restrictScalars, Iff.intro
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : FaithfulSMul R S
a : A
inst_9 : Algebra.IsAlgebraic R S
⊢ Transcendental R a ↔ Transcendental S a

Tactic:
⟨(·.extendScalars _), (·.restrictScalars (FaithfulSMul.algebraMap_injective R S))⟩

Premises used: Transcendental.extendScalars, FaithfulSMul.algebraMap_injective, Transcendental.restrictScalars, Iff.intro
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
z : A
z' : S
R' : Type u_4
S' : Type u_5
inst_7 : CommRing S'
inst_8 : FaithfulSMul R S
alg : Algebra.IsAlgebraic R S
inst_9 : NoZeroDivisors S
inst_10 : Algebra S S'
inst_11 : IsFractionRing S S'
⊢ IsLocalization (algebraMapSubmonoid.{u_1, u_2} (R := R) S R⁰) S'

Tactic:
have := (FaithfulSMul.algebraMap_injective R S).noZeroDivisors _ (map_zero _) (map_mul _)
  (IsLocalization.iff_of_le_of_exists_dvd _ S⁰
    (map_le_nonZeroDivisors_of_injective _ (FaithfulSMul.algebraMap_injective ..) le_rfl)
    fun s hs ↦ have ⟨r, ne, eq⟩ := (alg.1 s).exists_nonzero_dvd hs
    ⟨_, ⟨r, mem_nonZeroDivisors_of_ne_zero ne, rfl⟩, eq⟩).mpr inferInstance

Premises used: IsAlgebraic.exists_nonzero_dvd, Iff.mpr, Algebra.IsAlgebraic.isAlgebraic, Dvd.dvd, le_rfl, Algebra.algebraMap, Membership.mem, nonZeroDivisors, Exists, inferInstance, map_zero, map_le_nonZeroDivisors_of_injective, Submonoid.map, map_mul, And, _private.0.Algebra.IsAlgebraic.instIsLocalizationAlgebraMapSubmonoidNonZeroDivisors.match_1, FaithfulSMul.algebraMap_injective, And.intro, Exists.intro, mem_nonZeroDivisors_of_ne_zero, Algebra.algebraMapSubmonoid, IsLocalization.iff_of_le_of_exists_dvd, Function.Injective.noZeroDivisors, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
z : A
z' : S
R' : Type u_4
S' : Type u_5
inst_7 : CommRing S'
inst_8 : FaithfulSMul R S
alg : Algebra.IsAlgebraic R S
inst_9 : NoZeroDivisors S
inst_10 : Algebra S S'
inst_11 : IsFractionRing S S'
inst_12 : Algebra R S'
inst_13 : IsScalarTower R S S'
⊢ IsLocalizedModule R⁰ (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S'))

Tactic:
isLocalizedModule_iff_isLocalization.mpr inferInstance

Premises used: Iff.mpr, inferInstance, isLocalizedModule_iff_isLocalization
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' : Type u_4
S' : Type u_5
inst_3 : CommRing S'
inst_4 : FaithfulSMul R S
alg : Algebra.IsAlgebraic R S
inst_5 : NoZeroDivisors S
inst_6 : Algebra S S'
inst_7 : IsFractionRing S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R S S'
inst_10 : CommRing R'
inst_11 : Algebra R R'
inst_12 : IsFractionRing R R'
inst_13 : Module R' S'
inst_14 : IsScalarTower R R' S'
⊢ IsBaseChange R' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S'))

Tactic:
(isLocalizedModule_iff_isBaseChange R⁰ ..).mp inferInstance

Premises used: isLocalizedModule_iff_isBaseChange, nonZeroDivisors, inferInstance, Iff.mp
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
z : A
z' : S
R' : Type u_4
S' : Type u_5
inst_7 : CommRing S'
inst_8 : FaithfulSMul R S
alg : Algebra.IsAlgebraic R S
inst_9 : NoZeroDivisors S
inst_10 : Algebra S S'
inst_11 : IsFractionRing S S'
inst_12 : Algebra R S'
inst_13 : IsScalarTower R S S'
inst_14 : CommRing R'
inst_15 : Algebra R R'
inst_16 : IsFractionRing R R'
inst_17 : Algebra R' S'
inst_18 : IsScalarTower R R' S'
⊢ IsPushout R R' S S'

Tactic:
(isPushout_iff ..).mpr <| isBaseChange_of_isFractionRing ..

Premises used: Iff.mpr, Algebra.isPushout_iff, Algebra.IsAlgebraic.isBaseChange_of_isFractionRing
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
z : A
z' : S
R' : Type u_4
S' : Type u_5
inst_7 : CommRing S'
inst_8 : FaithfulSMul R S
alg : Algebra.IsAlgebraic R S
inst_9 : NoZeroDivisors S
inst_10 : Algebra S S'
inst_11 : IsFractionRing S S'
inst_12 : Algebra R S'
inst_13 : IsScalarTower R S S'
inst_14 : CommRing R'
inst_15 : Algebra R R'
inst_16 : IsFractionRing R R'
inst_17 : Algebra R' S'
inst_18 : IsScalarTower R R' S'
⊢ IsPushout R S R' S'

Tactic:
.symm inferInstance

Premises used: inferInstance, Algebra.IsPushout.symm