awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
alg : Algebra.IsAlgebraic R S
a : A
h : IsIntegral S a
inl : Subsingleton A → IsAlgebraic R a
⊢ IsAlgebraic R a
have inr : Nontrivial A → IsAlgebraic R a
Tactic: cases subsingleton_or_nontrivial A
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
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
alg : Algebra.IsAlgebraic R S
a : A
h : IsIntegral S a
h_1 : Subsingleton A
⊢ IsAlgebraic R a
have this : Nontrivial R
Tactic: have := Algebra.IsAlgebraic.nontrivial R S
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
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
alg : Algebra.IsAlgebraic R S
a : A
h : IsIntegral S a
h_1 : Nontrivial A
⊢ IsAlgebraic R a
have this : Nontrivial S
Tactic: have := Module.nontrivial S A
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
s : S
a : A
ha : IsAlgebraic R a
inst_5 : FaithfulSMul R S
⊢ IsAlgebraic S (A := TensorProduct R S A) (s ⊗ₜ[R] a)
have rw : IsAlgebraic S (HSMul.hSMul (β := TensorProduct R S A) s (1 ⊗ₜ[R] a))
Tactic: rw [← mul_one s, ← smul_eq_mul, ← TensorProduct.smul_tmul']
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
s : S
a : A
ha : IsAlgebraic R a
inst_5 : FaithfulSMul R S
⊢ IsAlgebraic S (HSMul.hSMul (β := TensorProduct R S A) s (1 ⊗ₜ[R] a))
have have : ∀ (p : R[X]) (h : p ≠ 0) (eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)),
  IsAlgebraic S (HSMul.hSMul (β := TensorProduct R S A) s (1 ⊗ₜ[R] a))
Tactic: have ⟨p, h, eval0⟩ := ha
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
s : S
a : A
ha : IsAlgebraic R a
inst_5 : FaithfulSMul R S
p : R[X]
h : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
⊢ IsAlgebraic S (HSMul.hSMul (β := TensorProduct R S A) s (1 ⊗ₜ[R] a))
have refine : Eq (α := TensorProduct R S A)
  ((aeval (1 ⊗ₜ[R] a) : (a : S[X]) → TensorProduct R S A) (map (algebraMap R S) p) : TensorProduct R S A)
  (0 : TensorProduct R S A)
Tactic: refine .smul ⟨p.map (algebraMap R S),
    (Polynomial.map_ne_zero_iff <| FaithfulSMul.algebraMap_injective ..).mpr h, ?_⟩ _
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
s : S
a : A
ha : IsAlgebraic R a
inst_5 : FaithfulSMul R S
p : R[X]
h : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
⊢ Eq (α := R →+* TensorProduct R S A)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (TensorProduct R S A)) (algebraMap R S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑Algebra.TensorProduct.includeRight : A →+* TensorProduct R S A) (algebraMap R A))
have a₁ : ∀ (x : R),
  Eq (α := TensorProduct R S A)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (TensorProduct R S A)) (algebraMap R S) :
          (a : R) → TensorProduct R S A)
        x :
      TensorProduct R S A)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑Algebra.TensorProduct.includeRight : A →+* TensorProduct R S A) (algebraMap R A) :
          (a : R) → TensorProduct R S A)
        x :
      TensorProduct R S A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
s : S
a : A
ha : IsAlgebraic R a
inst_5 : FaithfulSMul R S
p : R[X]
h : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
⊢ Eq (α := TensorProduct R S A)
    ((aeval (1 ⊗ₜ[R] a) : (a : S[X]) → TensorProduct R S A) (map (algebraMap R S) p) : TensorProduct R S A)
    (0 : TensorProduct R S A)
have rw : Eq (α := TensorProduct R S A)
  (((aeval ((Algebra.TensorProduct.includeRight : (a : A) → TensorProduct R S A) a) : S[X] →ₐ[S] TensorProduct R S A) :
        (a : S[X]) → TensorProduct R S A)
      (map (algebraMap R S) p) :
    TensorProduct R S A)
  (0 : TensorProduct R S A)
Tactic: rw [← Algebra.TensorProduct.includeRight_apply, ← AlgHom.coe_toRingHom (A := A),
    ← map_aeval_eq_aeval_map (by ext; simp), eval0, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
s : S
a : A
ha : IsAlgebraic R a
inst_5 : FaithfulSMul R S
p : R[X]
h : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
rw :
  Eq (α := TensorProduct R S A)
    (((aeval ((Algebra.TensorProduct.includeRight : (a : A) → TensorProduct R S A) a) :
            S[X] →ₐ[S] TensorProduct R S A) :
          (a : S[X]) → TensorProduct R S A)
        (map (algebraMap R S) p) :
      TensorProduct R S A)
    (0 : TensorProduct R S A)
⊢ Eq (α := TensorProduct R S A)
    ((aeval (1 ⊗ₜ[R] a) : (a : S[X]) → TensorProduct R S A) (map (algebraMap R S) p) : TensorProduct R S A)
    (0 : TensorProduct R S A)
have rw₁ : Eq (α := TensorProduct R S A)
  (((aeval (((↑Algebra.TensorProduct.includeRight : A →+* TensorProduct R S A) : (a : A) → TensorProduct R S A) a) :
          S[X] →ₐ[S] TensorProduct R S A) :
        (a : S[X]) → TensorProduct R S A)
      (map (algebraMap R S) p) :
    TensorProduct R S A)
  (0 : TensorProduct R S A)
Tactic: rw [← Algebra.TensorProduct.includeRight_apply, ← AlgHom.coe_toRingHom (A := A),
    ← map_aeval_eq_aeval_map (by ext; simp), eval0, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
s : S
a : A
ha : IsAlgebraic R a
inst_5 : FaithfulSMul R S
p : R[X]
h : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
rw :
  Eq (α := TensorProduct R S A)
    (((aeval ((Algebra.TensorProduct.includeRight : (a : A) → TensorProduct R S A) a) :
            S[X] →ₐ[S] TensorProduct R S A) :
          (a : S[X]) → TensorProduct R S A)
        (map (algebraMap R S) p) :
      TensorProduct R S A)
    (0 : TensorProduct R S A)
rw₁ :
  Eq (α := TensorProduct R S A)
    (((aeval (((↑Algebra.TensorProduct.includeRight : A →+* TensorProduct R S A) : (a : A) → TensorProduct R S A) a) :
            S[X] →ₐ[S] TensorProduct R S A) :
          (a : S[X]) → TensorProduct R S A)
        (map (algebraMap R S) p) :
      TensorProduct R S A)
    (0 : TensorProduct R S A)
⊢ Eq (α := TensorProduct R S A)
    ((aeval (1 ⊗ₜ[R] a) : (a : S[X]) → TensorProduct R S A) (map (algebraMap R S) p) : TensorProduct R S A)
    (0 : TensorProduct R S A)
have rw₂ : Eq (α := TensorProduct R S A)
  (((↑Algebra.TensorProduct.includeRight : A →+* TensorProduct R S A) : (a : A) → TensorProduct R S A)
      ((aeval a : (a : R[X]) → A) p) :
    TensorProduct R S A)
  (0 : TensorProduct R S A)
Tactic: rw [← Algebra.TensorProduct.includeRight_apply, ← AlgHom.coe_toRingHom (A := A),
    ← map_aeval_eq_aeval_map (by ext; simp), eval0, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
s : S
a : A
ha : IsAlgebraic R a
inst_5 : FaithfulSMul R S
p : R[X]
h : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
rw :
  Eq (α := TensorProduct R S A)
    (((aeval ((Algebra.TensorProduct.includeRight : (a : A) → TensorProduct R S A) a) :
            S[X] →ₐ[S] TensorProduct R S A) :
          (a : S[X]) → TensorProduct R S A)
        (map (algebraMap R S) p) :
      TensorProduct R S A)
    (0 : TensorProduct R S A)
rw₁ :
  Eq (α := TensorProduct R S A)
    (((aeval (((↑Algebra.TensorProduct.includeRight : A →+* TensorProduct R S A) : (a : A) → TensorProduct R S A) a) :
            S[X] →ₐ[S] TensorProduct R S A) :
          (a : S[X]) → TensorProduct R S A)
        (map (algebraMap R S) p) :
      TensorProduct R S A)
    (0 : TensorProduct R S A)
rw₂ :
  Eq (α := TensorProduct R S A)
    (((↑Algebra.TensorProduct.includeRight : A →+* TensorProduct R S A) : (a : A) → TensorProduct R S A)
        ((aeval a : (a : R[X]) → A) p) :
      TensorProduct R S A)
    (0 : TensorProduct R S A)
⊢ Eq (α := TensorProduct R S A)
    ((aeval (1 ⊗ₜ[R] a) : (a : S[X]) → TensorProduct R S A) (map (algebraMap R S) p) : TensorProduct R S A)
    (0 : TensorProduct R S A)
have rw₃ : Eq (α := TensorProduct R S A)
  (((↑Algebra.TensorProduct.includeRight : A →+* TensorProduct R S A) : (a : A) → TensorProduct R S A) 0) 0
Tactic: rw [← Algebra.TensorProduct.includeRight_apply, ← AlgHom.coe_toRingHom (A := A),
    ← map_aeval_eq_aeval_map (by ext; simp), eval0, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
s : S
a : A
ha : IsAlgebraic R a
inst_5 : FaithfulSMul R S
p : R[X]
h : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
rw :
  Eq (α := TensorProduct R S A)
    (((aeval ((Algebra.TensorProduct.includeRight : (a : A) → TensorProduct R S A) a) :
            S[X] →ₐ[S] TensorProduct R S A) :
          (a : S[X]) → TensorProduct R S A)
        (map (algebraMap R S) p) :
      TensorProduct R S A)
    (0 : TensorProduct R S A)
rw₁ :
  Eq (α := TensorProduct R S A)
    (((aeval (((↑Algebra.TensorProduct.includeRight : A →+* TensorProduct R S A) : (a : A) → TensorProduct R S A) a) :
            S[X] →ₐ[S] TensorProduct R S A) :
          (a : S[X]) → TensorProduct R S A)
        (map (algebraMap R S) p) :
      TensorProduct R S A)
    (0 : TensorProduct R S A)
rw₂ :
  Eq (α := TensorProduct R S A)
    (((↑Algebra.TensorProduct.includeRight : A →+* TensorProduct R S A) : (a : A) → TensorProduct R S A)
        ((aeval a : (a : R[X]) → A) p) :
      TensorProduct R S A)
    (0 : TensorProduct R S A)
rw₃ :
  Eq (α := TensorProduct R S A)
    (((↑Algebra.TensorProduct.includeRight : A →+* TensorProduct R S A) : (a : A) → TensorProduct R S A) 0) 0
⊢ Eq (α := TensorProduct R S A)
    ((aeval (1 ⊗ₜ[R] a) : (a : S[X]) → TensorProduct R S A) (map (algebraMap R S) p) : TensorProduct R S A)
    (0 : TensorProduct R S A)
have rw₄ : Eq (α := TensorProduct R S A) 0 0
Tactic: rw [← Algebra.TensorProduct.includeRight_apply, ← AlgHom.coe_toRingHom (A := A),
    ← map_aeval_eq_aeval_map (by ext; simp), eval0, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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)
have have : ∀ (ra : R) (a0 : ra ≠ 0) (int_a : IsIntegral R (ra • a)), IsAlgebraic R (a * b)
Tactic: have ⟨ra, a0, int_a⟩ := ha.exists_integral_multiple
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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)
⊢ IsAlgebraic R (a * b)
have have : ∀ (rb : R) (b0 : rb ≠ 0) (int_b : IsIntegral R (rb • b)), IsAlgebraic R (a * b)
Tactic: have ⟨rb, b0, int_b⟩ := hb.exists_integral_multiple
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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)
have refine : IsIntegral R ((ra * rb) • (a * b))
Tactic: refine IsAlgebraic.iff_exists_smul_integral.mpr ⟨_, mul_ne_zero a0 b0, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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 ((ra * rb) • (a * b))
have simp_rw : IsIntegral R (ra • a * rb • b)
Tactic: simp_rw [Algebra.smul_def, map_mul, mul_mul_mul_comm, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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)
have have : ∀ (ra : R) (a0 : ra ≠ 0) (int_a : IsIntegral R (ra • a)), IsAlgebraic R (a + b)
Tactic: have ⟨ra, a0, int_a⟩ := ha.exists_integral_multiple
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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)
⊢ IsAlgebraic R (a + b)
have have : ∀ (rb : R) (b0 : rb ≠ 0) (int_b : IsIntegral R (rb • b)), IsAlgebraic R (a + b)
Tactic: have ⟨rb, b0, int_b⟩ := hb.exists_integral_multiple
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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)
have refine : IsIntegral R ((rb * ra) • (a + b))
Tactic: refine IsAlgebraic.iff_exists_smul_integral.mpr ⟨_, mul_ne_zero b0 a0, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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 + b))
have rw : IsIntegral R (rb • ra • a + ra • rb • b)
Tactic: rw [smul_add, mul_smul, mul_comm, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
⊢ Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic S A
have simp_rw : (∀ (x : A), IsAlgebraic R x) ↔ ∀ (x : A), IsAlgebraic S x
Tactic: simp_rw [Algebra.isAlgebraic_def, Algebra.IsIntegral.isAlgebraic_iff R S]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
⊢ Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic S A
have simp_rw : (∀ (x : A), IsAlgebraic R x) ↔ ∀ (x : A), IsAlgebraic S x
Tactic: simp_rw [Algebra.isAlgebraic_def, Algebra.IsAlgebraic.isAlgebraic_iff R S]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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)
⊢ IsAlgebraic R z
have 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
Tactic: have ⟨t, ht, r, hr, eq⟩ := alg_y.exists_nonzero_eq_adjoin_mul hy
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
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 z
have this : IsAlgebraic R (y * z * t)
Tactic: have := alg_yz.mul (Algebra.isAlgebraic_adjoin_singleton_iff.mpr alg_y _ ht)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
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 z
have this₁ : IsAlgebraic R (r • z)
Tactic: rw [mul_right_comm, eq, ← Algebra.smul_def] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
⊢ Transcendental S a
have contrapose : ∀ (ha : ¬Transcendental S a), ¬Transcendental R a
Tactic: contrapose ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
⊢ ¬Transcendental R a
have rw : ∀ (ha : IsAlgebraic S a), IsAlgebraic R a
Tactic: rw [Transcendental, not_not] at ha ⊢
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
⊢ Transcendental S a
have contrapose : ∀ (ha : ¬Transcendental S a), ¬Transcendental R a
Tactic: contrapose ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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
⊢ ¬Transcendental R a
have rw : ∀ (ha : IsAlgebraic S a), IsAlgebraic R a
Tactic: rw [Transcendental, not_not] at ha ⊢
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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'
⊢ Cardinal.lift.{u, v} (Module.rank R' S') = Cardinal.lift.{v, u} (Module.rank R S)
have rw : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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)
⊢ Cardinal.lift.{u, v} (Module.rank R' S') = Cardinal.lift.{v, u} (Module.rank R S)
have rw₁ : Cardinal.lift.{v, u} (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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
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
⊢ Module.rank (MvPolynomial σ R) (MvPolynomial σ S) = Cardinal.lift.{u, u_2} (Module.rank R S)
have 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)
Tactic: have := Algebra.isPushout_iff R (MvPolynomial σ R) S (MvPolynomial σ S)
    |>.mp inferInstance |>.lift_rank_eq
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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)
⊢ Module.rank (MvPolynomial σ R) (MvPolynomial σ S) = Cardinal.lift.{u, u_2} (Module.rank R S)
have 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)
Tactic: rwa [Cardinal.lift_id', Cardinal.lift_umax] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
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)
⊢ Module.rank (MvPolynomial σ R) (MvPolynomial σ S) = Cardinal.lift.{u, u_2} (Module.rank R S)
have 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)
Tactic: rwa [Cardinal.lift_id', Cardinal.lift_umax] at this
Cleared hypotheses: this