awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
inst : CommRing R
R' : Type u_4
S : Type u
inst_1 : CommRing R'
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Algebra R R'
inst_5 : IsFractionRing R R'
inst_6 : FaithfulSMul R S
inst_7 : Algebra.IsAlgebraic R S
inst_8 : NoZeroDivisors S
S' : Type v
inst_9 : CommRing S'
inst_10 : Algebra R S'
inst_11 : Algebra S S'
inst_12 : Module R' S'
inst_13 : IsScalarTower R R' S'
inst_14 : IsScalarTower R S S'
inst_15 : IsFractionRing S S'
rw : Cardinal.lift.{u, v} (Module.rank R S') = Cardinal.lift.{v, u} (Module.rank R S)
rw₁ rw₂ : Cardinal.lift.{v, u} (Module.rank R S) = Cardinal.lift.{v, u} (Module.rank R S)
⊢ Cardinal.lift.{u, v} (Module.rank R' S') = Cardinal.lift.{v, u} (Module.rank R S)

Tactic:
rw [IsLocalization.rank_eq R' R⁰ le_rfl,
    IsLocalizedModule.lift_rank_eq R⁰ (IsScalarTower.toAlgHom R S S').toLinearMap le_rfl]

Premises used: AlgHom.toLinearMap, le_rfl, IsScalarTower.toAlgHom, nonZeroDivisors, IsLocalizedModule.lift_rank_eq, IsLocalization.rank_eq
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
inst : CommRing R
R' : Type u_4
S : Type u
inst_1 : CommRing R'
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Algebra R R'
inst_5 : IsFractionRing R R'
inst_6 : FaithfulSMul R S
inst_7 : Algebra.IsAlgebraic R S
inst_8 : NoZeroDivisors S
S' : Type v
inst_9 : CommRing S'
inst_10 : Algebra R S'
inst_11 : Algebra S S'
inst_12 : Module R' S'
inst_13 : IsScalarTower R R' S'
inst_14 : IsScalarTower R S S'
inst_15 : IsFractionRing S S'
⊢ Module.finrank R' S' = Module.finrank R S

Tactic:
simpa using congr_arg Cardinal.toNat (lift_rank_of_isFractionRing ..)

Premises used: Cardinal.toNat, congr_arg, Algebra.IsAlgebraic.lift_rank_of_isFractionRing, DFunLike.coe
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
inst : CommRing R
R' : Type u_4
S : Type u
inst_1 : CommRing R'
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Algebra R R'
inst_5 : IsFractionRing R R'
inst_6 : FaithfulSMul R S
inst_7 : Algebra.IsAlgebraic R S
inst_8 : NoZeroDivisors S
S' : Type u
inst_9 : CommRing S'
inst_10 : Algebra R S'
inst_11 : Algebra S S'
inst_12 : Module R' S'
inst_13 : IsScalarTower R R' S'
inst_14 : IsScalarTower R S S'
inst_15 : IsFractionRing S S'
⊢ Module.rank R' S' = Module.rank R S

Tactic:
simpa using lift_rank_of_isFractionRing R R' S S'

Premises used: Algebra.IsAlgebraic.lift_rank_of_isFractionRing
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : Algebra.IsAlgebraic R S
inst_5 : IsDomain S
⊢ Module.rank.{u_1, u} (FractionRing R) (FractionRing S) = Module.rank R S

Tactic:
rank_of_isFractionRing ..

Premises used: Algebra.IsAlgebraic.rank_of_isFractionRing
-- 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
⊢ Module.rank.{u_1, u_2} R[X] S[X] = Module.rank R S

Tactic:
((Algebra.isPushout_iff ..).mp inferInstance).rank_eq

Premises used: IsBaseChange.rank_eq
-- 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
σ : Type u
⊢ Cardinal.lift.{u_2, max u u_2} (Module.rank (MvPolynomial σ R) (MvPolynomial σ S)) =
    Cardinal.lift.{max u u_2, u_2} (Module.rank R S)

Tactic:
have := Algebra.isPushout_iff R (MvPolynomial σ R) S (MvPolynomial σ S)
    |>.mp inferInstance |>.lift_rank_eq
-- 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
σ : Type u
this :
  Cardinal.lift.{u_2, max u u_2} (Module.rank (MvPolynomial σ R) (MvPolynomial σ S)) =
    Cardinal.lift.{max u u_2, u_2} (Module.rank R S)
rwa :
  ∀ (this : Module.rank (MvPolynomial σ R) (MvPolynomial σ S) = Cardinal.lift.{max u u_2, u_2} (Module.rank R S)),
    Module.rank (MvPolynomial σ R) (MvPolynomial σ S) = Cardinal.lift.{u, u_2} (Module.rank R S)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : Module.rank (MvPolynomial σ R) (MvPolynomial σ S) = Cardinal.lift.{u, u_2} (Module.rank R S)),
    Module.rank (MvPolynomial σ R) (MvPolynomial σ S) = Cardinal.lift.{u, u_2} (Module.rank R S)
⊢ Module.rank (MvPolynomial σ R) (MvPolynomial σ S) = Cardinal.lift.{u, u_2} (Module.rank R S)

Tactic:
rwa [Cardinal.lift_id', Cardinal.lift_umax] at this

Premises used: Cardinal.lift_id', Cardinal.lift_umax
-- 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
alg : Algebra.IsAlgebraic R S
R' : Type u_4
inst_3 : CommRing R'
inst_4 : Algebra R R'
inst_5 : NoZeroDivisors R'
inst_6 : FaithfulSMul R R'
S' : Type u_5
inst_7 : CommRing S'
inst_8 : Algebra R S'
inst_9 : Algebra S S'
inst_10 : Algebra R' S'
inst_11 : IsScalarTower R R' S'
inst_12 : IsScalarTower R S S'
inst_13 : IsPushout R R' S S'
⊢ Algebra.IsAlgebraic R' S'

Tactic:
(equiv R R' S S').isAlgebraic

Premises used: AlgEquiv.isAlgebraic, Algebra.IsPushout.equiv
-- 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
alg : Algebra.IsAlgebraic R S
R' : Type u_4
inst_3 : CommRing R'
inst_4 : Algebra R R'
inst_5 : NoZeroDivisors R'
inst_6 : FaithfulSMul R R'
S' : Type u_5
inst_7 : CommRing S'
inst_8 : Algebra R S'
inst_9 : Algebra S S'
inst_10 : Algebra R' S'
inst_11 : IsScalarTower R R' S'
inst_12 : IsScalarTower R S S'
h : IsPushout R S R' S'
⊢ Algebra.IsAlgebraic R' S'

Tactic:
have := h.symm; (equiv R R' S S').isAlgebraic

Premises used: AlgEquiv.isAlgebraic, Algebra.IsPushout.equiv, Algebra.IsPushout.symm
-- 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
alg : Algebra.IsAlgebraic R S
inst_7 : NoZeroDivisors R
⊢ Algebra.IsAlgebraic.{u_1, u_2} R[X] S[X]

Tactic:
Algebra.IsPushout.isAlgebraic R S ..

Premises used: Algebra.IsPushout.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
z : A
z' : S
alg : Algebra.IsAlgebraic R S
inst_7 : NoZeroDivisors S
pos :
  ∀ (h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)),
    Algebra.IsAlgebraic.{u_1, u_2} R[X] S[X]
neg :
  ∀ (h : ¬Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)),
    Algebra.IsAlgebraic.{u_1, u_2} R[X] S[X]
⊢ Algebra.IsAlgebraic.{u_1, u_2} R[X] S[X]

Tactic:
by_cases h : Function.Injective (algebraMap R S)

Premises used: Algebra.algebraMap, Function.Injective, DFunLike.coe
-- 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
alg : Algebra.IsAlgebraic R S
inst_7 : NoZeroDivisors S
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ NoZeroDivisors R

Tactic:
have := h.noZeroDivisors _ (map_zero _) (map_mul _)
-- 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
alg : Algebra.IsAlgebraic R S
inst_7 : NoZeroDivisors S
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this : NoZeroDivisors R
⊢ Algebra.IsAlgebraic.{u_1, u_2} R[X] S[X]

Tactic:
infer_instance
-- 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
alg : Algebra.IsAlgebraic R S
inst_7 : NoZeroDivisors S
h : ¬Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ ¬Function.Injective (α := R[X]) (β := S[X]) (map (algebraMap R S))

Tactic:
rw [← Polynomial.map_injective_iff] at h

Premises used: Polynomial.map_injective_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
z : A
z' : S
alg : Algebra.IsAlgebraic R S
inst_7 : NoZeroDivisors S
h : ¬Function.Injective (α := R[X]) (β := S[X]) (map (algebraMap R S))
⊢ Algebra.IsAlgebraic.{u_1, u_2} R[X] S[X]

Tactic:
Algebra.isAlgebraic_of_not_injective h

Premises used: Algebra.isAlgebraic_of_not_injective
-- 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
alg : Algebra.IsAlgebraic R S
inst_7 : NoZeroDivisors S
h : ¬Function.Injective (α := R[X]) (β := S[X]) (map (algebraMap R S))
⊢ Algebra.IsAlgebraic.{u_1, u_2} R[X] S[X]

Tactic:
exact Algebra.isAlgebraic_of_not_injective h

Premises used: Algebra.isAlgebraic_of_not_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
alg : Algebra.IsAlgebraic R S
inst_3 : NoZeroDivisors S
f : S[X]
hf : f ≠ 0
⊢ ∃ (g : R[X]), g ≠ 0 ∧ f ∣ map (algebraMap R S) g

Tactic:
(Algebra.IsAlgebraic.isAlgebraic f).exists_nonzero_dvd (mem_nonZeroDivisors_of_ne_zero hf)

Premises used: IsAlgebraic.exists_nonzero_dvd, Algebra.IsAlgebraic.isAlgebraic, mem_nonZeroDivisors_of_ne_zero, Polynomial.map
-- 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
alg : Algebra.IsAlgebraic R S
σ : Type u_4
inst_7 : NoZeroDivisors R
⊢ Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)

Tactic:
Algebra.IsPushout.isAlgebraic R S ..

Premises used: Algebra.IsPushout.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
z : A
z' : S
alg : Algebra.IsAlgebraic R S
σ : Type u_4
inst_7 : NoZeroDivisors S
pos :
  ∀ (h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)),
    Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)
neg :
  ∀ (h : ¬Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)),
    Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)
⊢ Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)

Tactic:
by_cases h : Function.Injective (algebraMap R S)

Premises used: Algebra.algebraMap, Function.Injective, DFunLike.coe
-- 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
alg : Algebra.IsAlgebraic R S
σ : Type u_4
inst_7 : NoZeroDivisors S
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ NoZeroDivisors R

Tactic:
have := h.noZeroDivisors _ (map_zero _) (map_mul _)
-- 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
alg : Algebra.IsAlgebraic R S
σ : Type u_4
inst_7 : NoZeroDivisors S
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this : NoZeroDivisors R
⊢ Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)

Tactic:
infer_instance
-- 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
alg : Algebra.IsAlgebraic R S
σ : Type u_4
inst_7 : NoZeroDivisors S
h : ¬Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
neg :
  ∀
    (h :
      ¬Function.Injective (α := MvPolynomial σ R) (β := MvPolynomial σ S)
          (⇑(MvPolynomial.map (algebraMap R S)) : (a : MvPolynomial σ R) → MvPolynomial σ S)),
    Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)
rw : Type u_4
⊢ Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)

Tactic:
rw [← MvPolynomial.map_injective_iff] at h

Premises used: MvPolynomial.map_injective_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
z : A
z' : S
alg : Algebra.IsAlgebraic R S
σ : Type u_4
inst_7 : NoZeroDivisors S
h_1 : ¬Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h :
  ¬Function.Injective (α := MvPolynomial σ R) (β := MvPolynomial σ S)
      (⇑(MvPolynomial.map (algebraMap R S)) : (a : MvPolynomial σ R) → MvPolynomial σ S)
⊢ Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)

Tactic:
Algebra.isAlgebraic_of_not_injective h

Premises used: Algebra.isAlgebraic_of_not_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
alg : Algebra.IsAlgebraic R S
σ : Type u_4
inst_3 : NoZeroDivisors S
f : MvPolynomial σ S
hf : f ≠ 0
⊢ ∃ (g : MvPolynomial σ R), g ≠ 0 ∧ f ∣ (map (algebraMap R S) : (a : MvPolynomial σ R) → MvPolynomial σ S) g

Tactic:
(Algebra.IsAlgebraic.isAlgebraic f).exists_nonzero_dvd (mem_nonZeroDivisors_of_ne_zero hf)

Premises used: IsAlgebraic.exists_nonzero_dvd, Algebra.IsAlgebraic.isAlgebraic, 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
z : A
z' : S
alg : Algebra.IsAlgebraic R S
inst_7 : IsDomain S
inst_8 : FaithfulSMul R S
⊢ Algebra.IsPushout R (FractionRing R[X]) S (FractionRing S[X])

Tactic:
(Algebra.IsPushout.comp_iff _ R[X] _ S[X]).mpr inferInstance

Premises used: Iff.mpr, inferInstance, Algebra.IsPushout.comp_iff, Polynomial
-- 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
alg : Algebra.IsAlgebraic R S
inst_7 : IsDomain S
inst_8 : FaithfulSMul R S
⊢ Algebra.IsPushout R S (FractionRing R[X]) (FractionRing S[X])

Tactic:
.symm inferInstance

Premises used: inferInstance, Algebra.IsPushout.symm
-- 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
alg : Algebra.IsAlgebraic R S
inst_7 : IsDomain S
inst_8 : FaithfulSMul R S
σ : Type u_4
⊢ Algebra.IsPushout R (FractionRing (MvPolynomial σ R)) S (FractionRing (MvPolynomial σ S))

Tactic:
(Algebra.IsPushout.comp_iff _ (MvPolynomial σ R) _ (MvPolynomial σ S)).mpr inferInstance

Premises used: Iff.mpr, inferInstance, Algebra.IsPushout.comp_iff, MvPolynomial
-- 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
alg : Algebra.IsAlgebraic R S
inst_7 : IsDomain S
inst_8 : FaithfulSMul R S
σ : Type u_4
⊢ Algebra.IsPushout R S (FractionRing (MvPolynomial σ R)) (FractionRing (MvPolynomial σ S))

Tactic:
.symm inferInstance

Premises used: inferInstance, Algebra.IsPushout.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
alg : Algebra.IsAlgebraic R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
⊢ IsDomain R

Tactic:
have := IsDomain.of_faithfulSMul R S
-- 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
alg : Algebra.IsAlgebraic R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
this : IsDomain R
rw : Module.rank.{u_1, u_2} R[X] S[X] = Module.rank R S
rw₁ rw₂ : Module.rank R S = Module.rank R S
⊢ Module.rank.{u_1, u_2} (FractionRing R[X]) (FractionRing S[X]) = Module.rank R S

Tactic:
rw [rank_fractionRing, rank_polynomial_polynomial]

Premises used: rank_polynomial_polynomial, Algebra.IsAlgebraic.rank_fractionRing
-- 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
alg : Algebra.IsAlgebraic R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
σ : Type u
⊢ IsDomain R

Tactic:
have := IsDomain.of_faithfulSMul R S
-- 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
alg : Algebra.IsAlgebraic R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
σ : Type u
this : IsDomain R
rw : Module.rank (MvPolynomial σ R) (MvPolynomial σ S) = lift.{u, u_2} (Module.rank R S)
rw₁ rw₂ : lift.{u, u_2} (Module.rank R S) = lift.{u, u_2} (Module.rank R S)
⊢ Module.rank (FractionRing (MvPolynomial σ R)) (FractionRing (MvPolynomial σ S)) = lift.{u, u_2} (Module.rank R S)

Tactic:
rw [rank_fractionRing, rank_mvPolynomial_mvPolynomial]

Premises used: Algebra.IsAlgebraic.rank_fractionRing, rank_mvPolynomial_mvPolynomial
-- 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
inst_8 : IsDomain S
inst_9 : IsTorsionFree R S
inst_10 : Module.Finite R S
obtain :
  ∀ (w : ℕ) (s : Fin w → S) (hs : Eq (α := Submodule R S) (Submodule.span R (Set.range s)) ⊤),
    FiniteDimensional.{u_1, u_2} (FractionRing R) (FractionRing S)
⊢ FiniteDimensional.{u_1, u_2} (FractionRing R) (FractionRing S)

Tactic:
obtain ⟨_, s, hs⟩ := Module.Finite.exists_fin (R := R) (M := S)

Premises used: Module.Finite.exists_fin
-- 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
inst_8 : IsDomain S
inst_9 : IsTorsionFree R S
inst_10 : Module.Finite R S
w : ℕ
s : Fin w → S
hs : Eq (α := Submodule R S) (Submodule.span R (Set.range s)) ⊤
⊢ FiniteDimensional.{u_1, u_2} (FractionRing R) (FractionRing S)

Tactic:
Module.finite_def.mpr <|
    (span_eq_top_localization_localization (FractionRing R) R⁰ (FractionRing S) hs) ▸
      Submodule.fg_span (Set.toFinite _)

Premises used: Iff.mpr, span_eq_top_localization_localization, FractionRing, nonZeroDivisors, Eq.rec, Set.toFinite, Module.finite_def, Submodule.fg_span
-- 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
inst_8 : IsDomain S
inst_9 : IsTorsionFree R S
inst_10 : Module.Finite R S
w : ℕ
s : Fin w → S
hs : Eq (α := Submodule R S) (Submodule.span R (Set.range s)) ⊤
⊢ FiniteDimensional.{u_1, u_2} (FractionRing R) (FractionRing S)

Tactic:
exact Module.finite_def.mpr <|
    (span_eq_top_localization_localization (FractionRing R) R⁰ (FractionRing S) hs) ▸
      Submodule.fg_span (Set.toFinite _)

Premises used: Iff.mpr, Module.finite_def
-- Module: Mathlib.RingTheory.Algebraic.LinearIndependent
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : Transcendental F x
⊢ ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0

Tactic:
rw [transcendental_iff] at H

Premises used: transcendental_iff
-- Module: Mathlib.RingTheory.Algebraic.LinearIndependent
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
⊢ LinearIndependent.{u_1, u_1, u_2} F (M := E) fun (a : F) ↦
    (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E))⁻¹

Tactic:
linearIndependent_iff'.2 fun s m hm i hi ↦ ?_

Premises used: Iff.mpr, linearIndependent_iff'
-- Module: Mathlib.RingTheory.Algebraic.LinearIndependent
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
refine :
  ∀ (s : Finset F) (m : F → F)
    (hm : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, m i • (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) 0)
    (i : F) (hi : i ∈ s), m i = 0
⊢ LinearIndependent.{u_1, u_1, u_2} F (M := E) fun (a : F) ↦
    (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E))⁻¹

Tactic:
refine linearIndependent_iff'.2 fun s m hm i hi ↦ ?_

Premises used: Iff.mpr, linearIndependent_iff'
-- Module: Mathlib.RingTheory.Algebraic.LinearIndependent
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
hm : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, m i • (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) 0
i : F
hi : i ∈ s
a : F
h : HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) = 0
⊢ Eq.{u_2 + 1} (α := E)
    ((aeval x : (a : F[X]) → E) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) a : F[X])) : E) (0 : E)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Algebraic.LinearIndependent
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
hm : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, m i • (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) 0
i : F
hi : i ∈ s
⊢ ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0

Tactic:
have hnz (a : F) : x - algebraMap F E a ≠ 0 := fun h ↦
    X_sub_C_ne_zero a <| H (.X - .C a) (by simp [h])