awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set A
his : ∀ (x : A), Membership.mem (γ := Set A) ∅ x → IsIntegral R x
x : A
empty :
  Membership.mem (γ := Submodule R A) (span R (↑{1} : Set A)) x ↔
    Membership.mem (γ := Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) ⊥ : Submodule R A) x
empty₁ :
  Membership.mem (γ := Submodule R A) (R ∙ 1) x ↔
    Membership.mem (γ := Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) ⊥ : Submodule R A) x
⊢ Membership.mem (γ := Submodule R A) (span R (↑{1} : Set A)) x ↔
    Membership.mem (γ := Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[] : Submodule R A) x
have empty₂ : Membership.mem (γ := Submodule R A) 1 x ↔
  Membership.mem (γ := Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) ⊥ : Submodule R A) x
Tactic: rw [Algebra.adjoin_empty, Finset.coe_singleton, ← one_eq_span, Algebra.toSubmodule_bot]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set A
his : ∀ (x : A), Membership.mem (γ := Set A) ∅ x → IsIntegral R x
x : A
empty :
  Membership.mem (γ := Submodule R A) (span R (↑{1} : Set A)) x ↔
    Membership.mem (γ := Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) ⊥ : Submodule R A) x
empty₁ :
  Membership.mem (γ := Submodule R A) (R ∙ 1) x ↔
    Membership.mem (γ := Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) ⊥ : Submodule R A) x
empty₂ :
  Membership.mem (γ := Submodule R A) 1 x ↔
    Membership.mem (γ := Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) ⊥ : Submodule R A) x
⊢ Membership.mem (γ := Submodule R A) (span R (↑{1} : Set A)) x ↔
    Membership.mem (γ := Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[] : Submodule R A) x
have empty₃ : Membership.mem (γ := Submodule R A) 1 x ↔ Membership.mem (γ := Submodule R A) 1 x
Tactic: rw [Algebra.adjoin_empty, Finset.coe_singleton, ← one_eq_span, Algebra.toSubmodule_bot]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s_1 : Set A
a : A
s : Set A
h : a ∉ s
hs : s.Finite
ih :
  ∀ (his : ∀ x ∈ s, IsIntegral R x),
    FG.{u_1, u_2} (R := R) (M := A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R s))
his : ∀ x ∈ insert a s, IsIntegral R x
⊢ FG.{u_1, u_2} (R := R) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R (insert a s)))
have insert : (HMul.hMul (α := Submodule R A) (β := Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R s) : Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[a] : Submodule R A)).FG
Tactic: rw [← Set.union_singleton, Algebra.adjoin_union_coe_submodule]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set A
hfs : s.Finite
his : ∀ x ∈ s, IsIntegral R x
⊢ FG.{u_1, u_2} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R s))
have empty : ∀ (his : ∀ (x : A), Membership.mem (γ := Set A) ∅ x → IsIntegral R x),
  FG.{u_1, u_2} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[])
Tactic: induction s, hfs using Set.Finite.induction_on with
  | empty =>
    refine ⟨{1}, Submodule.ext fun x => ?_⟩
    rw [Algebra.adjoin_empty, Finset.coe_singleton, ← one_eq_span, Algebra.toSubmodule_bot]
  | @insert a s _ _ ih =>
    rw [← Set.union_singleton, Algebra.adjoin_union_coe_submodule]
    exact FG.mul
      (ih fun i hi => his i <| Set.mem_insert_of_mem a hi)
      (his a <| Set.mem_insert a s).fg_adjoin_singleton
Cleared hypotheses: hfs, his
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set A
hfs : s.Finite
his : ∀ x ∈ s, IsIntegral R x
empty :
  ∀ (his : ∀ (x : A), Membership.mem (γ := Set A) ∅ x → IsIntegral R x),
    FG.{u_1, u_2} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[])
⊢ FG.{u_1, u_2} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R s))
have insert : ∀ {a : A} {s : Set A},
  a ∉ s →
    s.Finite →
      ∀
        (ih :
          ∀ (his : ∀ x ∈ s, IsIntegral R x),
            FG.{u_1, u_2} (R := R) (M := A)
              ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R s)))
        (his : ∀ x ∈ insert a s, IsIntegral R x),
        FG.{u_1, u_2} (R := R) (M := A)
          ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R (insert a s)))
Tactic: induction s, hfs using Set.Finite.induction_on with
  | empty =>
    refine ⟨{1}, Submodule.ext fun x => ?_⟩
    rw [Algebra.adjoin_empty, Finset.coe_singleton, ← one_eq_span, Algebra.toSubmodule_bot]
  | @insert a s _ _ ih =>
    rw [← Set.union_singleton, Algebra.adjoin_union_coe_submodule]
    exact FG.mul
      (ih fun i hi => his i <| Set.mem_insert_of_mem a hi)
      (his a <| Set.mem_insert a s).fg_adjoin_singleton
Cleared hypotheses: hfs, his
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A × B
hx₁ : IsIntegral R x.1
hx₂ : IsIntegral R x.2
⊢ IsIntegral R x
have obtain : ∀ (p₁ : R[X]) (hp₁Monic : p₁.Monic) (hp₁Eval : eval₂ (algebraMap R A) x.1 p₁ = 0), IsIntegral R x
Tactic: obtain ⟨p₁, ⟨hp₁Monic, hp₁Eval⟩⟩ := hx₁
Cleared hypotheses: hx₁
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A × B
hx₂ : IsIntegral R x.2
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : eval₂ (algebraMap R A) x.1 p₁ = 0
⊢ IsIntegral R x
have obtain : ∀ (p₂ : R[X]) (hp₂Monic : p₂.Monic) (hp₂Eval : eval₂ (algebraMap R B) x.2 p₂ = 0), IsIntegral R x
Tactic: obtain ⟨p₂, ⟨hp₂Monic, hp₂Eval⟩⟩ := hx₂
Cleared hypotheses: hx₂
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : eval₂ (algebraMap R A) x.1 p₁ = 0
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : eval₂ (algebraMap R B) x.2 p₂ = 0
⊢ IsIntegral R x
have refine : eval₂ (algebraMap R (A × B)) x (p₁ * p₂) = 0
Tactic: refine ⟨p₁ * p₂, ⟨hp₁Monic.mul hp₂Monic, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : eval₂ (algebraMap R A) x.1 p₁ = 0
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : eval₂ (algebraMap R B) x.2 p₂ = 0
⊢ eval₂ (algebraMap R (A × B)) x (p₁ * p₂) = 0
have rw : ∀ (hp₁Eval : Eq.{u_2 + 1} (α := A) ((aeval x.1 : (a : R[X]) → A) p₁ : A) (0 : A)) (p₂ : R[X]) (hp₂Monic : p₂.Monic)
  (hp₂Eval : Eq.{u_3 + 1} (α := B) ((aeval x.2 : (a : R[X]) → B) p₂ : B) (0 : B)),
  Eq (α := A × B) ((aeval x : (a : R[X]) → A × B) (p₁ * p₂) : A × B) (0 : A × B)
Tactic: rw [← aeval_def] at *
Cleared hypotheses: hp₁Eval, p₂, hp₂Monic, hp₂Eval
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : Eq.{u_2 + 1} (α := A) ((aeval x.1 : (a : R[X]) → A) p₁ : A) (0 : A)
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : Eq.{u_3 + 1} (α := B) ((aeval x.2 : (a : R[X]) → B) p₂ : B) (0 : B)
⊢ Eq (α := A × B) ((aeval x : (a : R[X]) → A × B) (p₁ * p₂) : A × B) (0 : A × B)
have rw : Eq (α := A × B) (((aeval x.1 : (a : R[X]) → A) (p₁ * p₂), (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) : A × B) (0 : A × B)
Tactic: rw [aeval_prod_apply, aeval_mul, hp₁Eval, zero_mul, aeval_mul, hp₂Eval, mul_zero,
    Prod.zero_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : Eq.{u_2 + 1} (α := A) ((aeval x.1 : (a : R[X]) → A) p₁ : A) (0 : A)
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : Eq.{u_3 + 1} (α := B) ((aeval x.2 : (a : R[X]) → B) p₂ : B) (0 : B)
rw :
  Eq (α := A × B) (((aeval x.1 : (a : R[X]) → A) (p₁ * p₂), (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) : A × B) (0 : A × B)
⊢ Eq (α := A × B) ((aeval x : (a : R[X]) → A × B) (p₁ * p₂) : A × B) (0 : A × B)
have rw₁ : Eq (α := A × B)
  ((HMul.hMul (α := A) (β := A) ((aeval x.1 : (a : R[X]) → A) p₁ : A) ((aeval x.1 : (a : R[X]) → A) p₂ : A),
      (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) :
    A × B)
  (0 : A × B)
Tactic: rw [aeval_prod_apply, aeval_mul, hp₁Eval, zero_mul, aeval_mul, hp₂Eval, mul_zero,
    Prod.zero_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : Eq.{u_2 + 1} (α := A) ((aeval x.1 : (a : R[X]) → A) p₁ : A) (0 : A)
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : Eq.{u_3 + 1} (α := B) ((aeval x.2 : (a : R[X]) → B) p₂ : B) (0 : B)
rw :
  Eq (α := A × B) (((aeval x.1 : (a : R[X]) → A) (p₁ * p₂), (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) : A × B) (0 : A × B)
rw₁ :
  Eq (α := A × B)
    ((HMul.hMul (α := A) (β := A) ((aeval x.1 : (a : R[X]) → A) p₁ : A) ((aeval x.1 : (a : R[X]) → A) p₂ : A),
        (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) :
      A × B)
    (0 : A × B)
⊢ Eq (α := A × B) ((aeval x : (a : R[X]) → A × B) (p₁ * p₂) : A × B) (0 : A × B)
have rw₂ : Eq (α := A × B)
  ((HMul.hMul (α := A) (β := A) (0 : A) ((aeval x.1 : (a : R[X]) → A) p₂ : A), (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) :
    A × B)
  (0 : A × B)
Tactic: rw [aeval_prod_apply, aeval_mul, hp₁Eval, zero_mul, aeval_mul, hp₂Eval, mul_zero,
    Prod.zero_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : Eq.{u_2 + 1} (α := A) ((aeval x.1 : (a : R[X]) → A) p₁ : A) (0 : A)
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : Eq.{u_3 + 1} (α := B) ((aeval x.2 : (a : R[X]) → B) p₂ : B) (0 : B)
rw :
  Eq (α := A × B) (((aeval x.1 : (a : R[X]) → A) (p₁ * p₂), (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) : A × B) (0 : A × B)
rw₁ :
  Eq (α := A × B)
    ((HMul.hMul (α := A) (β := A) ((aeval x.1 : (a : R[X]) → A) p₁ : A) ((aeval x.1 : (a : R[X]) → A) p₂ : A),
        (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) :
      A × B)
    (0 : A × B)
rw₂ :
  Eq (α := A × B)
    ((HMul.hMul (α := A) (β := A) (0 : A) ((aeval x.1 : (a : R[X]) → A) p₂ : A),
        (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) :
      A × B)
    (0 : A × B)
⊢ Eq (α := A × B) ((aeval x : (a : R[X]) → A × B) (p₁ * p₂) : A × B) (0 : A × B)
have rw₃ : Eq (α := A × B) ((0, (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) : A × B) (0 : A × B)
Tactic: rw [aeval_prod_apply, aeval_mul, hp₁Eval, zero_mul, aeval_mul, hp₂Eval, mul_zero,
    Prod.zero_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : Eq.{u_2 + 1} (α := A) ((aeval x.1 : (a : R[X]) → A) p₁ : A) (0 : A)
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : Eq.{u_3 + 1} (α := B) ((aeval x.2 : (a : R[X]) → B) p₂ : B) (0 : B)
rw :
  Eq (α := A × B) (((aeval x.1 : (a : R[X]) → A) (p₁ * p₂), (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) : A × B) (0 : A × B)
rw₁ :
  Eq (α := A × B)
    ((HMul.hMul (α := A) (β := A) ((aeval x.1 : (a : R[X]) → A) p₁ : A) ((aeval x.1 : (a : R[X]) → A) p₂ : A),
        (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) :
      A × B)
    (0 : A × B)
rw₂ :
  Eq (α := A × B)
    ((HMul.hMul (α := A) (β := A) (0 : A) ((aeval x.1 : (a : R[X]) → A) p₂ : A),
        (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) :
      A × B)
    (0 : A × B)
rw₃ : Eq (α := A × B) ((0, (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) : A × B) (0 : A × B)
⊢ Eq (α := A × B) ((aeval x : (a : R[X]) → A × B) (p₁ * p₂) : A × B) (0 : A × B)
have rw₄ : Eq (α := A × B)
  (0, HMul.hMul (α := B) (β := B) ((aeval x.2 : (a : R[X]) → B) p₁ : B) ((aeval x.2 : (a : R[X]) → B) p₂ : B)) 0
Tactic: rw [aeval_prod_apply, aeval_mul, hp₁Eval, zero_mul, aeval_mul, hp₂Eval, mul_zero,
    Prod.zero_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : Eq.{u_2 + 1} (α := A) ((aeval x.1 : (a : R[X]) → A) p₁ : A) (0 : A)
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : Eq.{u_3 + 1} (α := B) ((aeval x.2 : (a : R[X]) → B) p₂ : B) (0 : B)
rw :
  Eq (α := A × B) (((aeval x.1 : (a : R[X]) → A) (p₁ * p₂), (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) : A × B) (0 : A × B)
rw₁ :
  Eq (α := A × B)
    ((HMul.hMul (α := A) (β := A) ((aeval x.1 : (a : R[X]) → A) p₁ : A) ((aeval x.1 : (a : R[X]) → A) p₂ : A),
        (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) :
      A × B)
    (0 : A × B)
rw₂ :
  Eq (α := A × B)
    ((HMul.hMul (α := A) (β := A) (0 : A) ((aeval x.1 : (a : R[X]) → A) p₂ : A),
        (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) :
      A × B)
    (0 : A × B)
rw₃ : Eq (α := A × B) ((0, (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) : A × B) (0 : A × B)
rw₄ :
  Eq (α := A × B)
    (0, HMul.hMul (α := B) (β := B) ((aeval x.2 : (a : R[X]) → B) p₁ : B) ((aeval x.2 : (a : R[X]) → B) p₂ : B)) 0
⊢ Eq (α := A × B) ((aeval x : (a : R[X]) → A × B) (p₁ * p₂) : A × B) (0 : A × B)
have rw₅ : Eq (α := A × B) (0, HMul.hMul (α := B) (β := B) ((aeval x.2 : (a : R[X]) → B) p₁ : B) (0 : B)) 0
Tactic: rw [aeval_prod_apply, aeval_mul, hp₁Eval, zero_mul, aeval_mul, hp₂Eval, mul_zero,
    Prod.zero_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : Eq.{u_2 + 1} (α := A) ((aeval x.1 : (a : R[X]) → A) p₁ : A) (0 : A)
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : Eq.{u_3 + 1} (α := B) ((aeval x.2 : (a : R[X]) → B) p₂ : B) (0 : B)
rw :
  Eq (α := A × B) (((aeval x.1 : (a : R[X]) → A) (p₁ * p₂), (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) : A × B) (0 : A × B)
rw₁ :
  Eq (α := A × B)
    ((HMul.hMul (α := A) (β := A) ((aeval x.1 : (a : R[X]) → A) p₁ : A) ((aeval x.1 : (a : R[X]) → A) p₂ : A),
        (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) :
      A × B)
    (0 : A × B)
rw₂ :
  Eq (α := A × B)
    ((HMul.hMul (α := A) (β := A) (0 : A) ((aeval x.1 : (a : R[X]) → A) p₂ : A),
        (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) :
      A × B)
    (0 : A × B)
rw₃ : Eq (α := A × B) ((0, (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) : A × B) (0 : A × B)
rw₄ :
  Eq (α := A × B)
    (0, HMul.hMul (α := B) (β := B) ((aeval x.2 : (a : R[X]) → B) p₁ : B) ((aeval x.2 : (a : R[X]) → B) p₂ : B)) 0
rw₅ : Eq (α := A × B) (0, HMul.hMul (α := B) (β := B) ((aeval x.2 : (a : R[X]) → B) p₁ : B) (0 : B)) 0
⊢ Eq (α := A × B) ((aeval x : (a : R[X]) → A × B) (p₁ * p₂) : A × B) (0 : A × B)
have rw₆ : Eq (α := A × B) (0, 0) 0
Tactic: rw [aeval_prod_apply, aeval_mul, hp₁Eval, zero_mul, aeval_mul, hp₂Eval, mul_zero,
    Prod.zero_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : Eq.{u_2 + 1} (α := A) ((aeval x.1 : (a : R[X]) → A) p₁ : A) (0 : A)
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : Eq.{u_3 + 1} (α := B) ((aeval x.2 : (a : R[X]) → B) p₂ : B) (0 : B)
rw :
  Eq (α := A × B) (((aeval x.1 : (a : R[X]) → A) (p₁ * p₂), (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) : A × B) (0 : A × B)
rw₁ :
  Eq (α := A × B)
    ((HMul.hMul (α := A) (β := A) ((aeval x.1 : (a : R[X]) → A) p₁ : A) ((aeval x.1 : (a : R[X]) → A) p₂ : A),
        (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) :
      A × B)
    (0 : A × B)
rw₂ :
  Eq (α := A × B)
    ((HMul.hMul (α := A) (β := A) (0 : A) ((aeval x.1 : (a : R[X]) → A) p₂ : A),
        (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) :
      A × B)
    (0 : A × B)
rw₃ : Eq (α := A × B) ((0, (aeval x.2 : (a : R[X]) → B) (p₁ * p₂)) : A × B) (0 : A × B)
rw₄ :
  Eq (α := A × B)
    (0, HMul.hMul (α := B) (β := B) ((aeval x.2 : (a : R[X]) → B) p₁ : B) ((aeval x.2 : (a : R[X]) → B) p₂ : B)) 0
rw₅ : Eq (α := A × B) (0, HMul.hMul (α := B) (β := B) ((aeval x.2 : (a : R[X]) → B) p₁ : B) (0 : B)) 0
rw₆ : Eq (α := A × B) (0, 0) 0
⊢ Eq (α := A × B) ((aeval x : (a : R[X]) → A × B) (p₁ * p₂) : A × B) (0 : A × B)
have rw₇ : Eq (α := A × B) (0, 0) (0, 0)
Tactic: rw [aeval_prod_apply, aeval_mul, hp₁Eval, zero_mul, aeval_mul, hp₂Eval, mul_zero,
    Prod.zero_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
inst_4 : Algebra.IsIntegral R S
hR : IsField R
x : S
hx : x ≠ 0
this : Field R := hR.toField
⊢ ∃ (b : S), x * b = 1
have obtain : ∀ (y : Sˣ) (hx : (↑y : S) ≠ 0), ∃ (b : S), (↑y : S) * b = 1
Tactic: obtain ⟨y, rfl⟩ := (Algebra.IsIntegral.isIntegral (R := R) x).isUnit hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : DivisionRing S
inst_2 : Algebra R S
x : S
int : IsIntegral R x
⊢ Membership.mem (γ := Subalgebra R S) R[x] x⁻¹
have inl : ∀ (int : IsIntegral.{u_1, u_2} R (A := S) 0), Membership.mem (γ := Subalgebra R S) R[0] 0⁻¹
Tactic: obtain rfl | h0 := eq_or_ne x 0
Cleared hypotheses: x, int
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : DivisionRing S
inst_2 : Algebra R S
x : S
int : IsIntegral R x
inl : ∀ (int : IsIntegral.{u_1, u_2} R (A := S) 0), Membership.mem (γ := Subalgebra R S) R[0] 0⁻¹
⊢ Membership.mem (γ := Subalgebra R S) R[x] x⁻¹
have inr : ∀ (h0 : x ≠ 0), Membership.mem (γ := Subalgebra R S) R[x] x⁻¹
Tactic: obtain rfl | h0 := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : DivisionRing S
inst_2 : Algebra R S
int : IsIntegral.{u_1, u_2} R (A := S) 0
⊢ Membership.mem (γ := Subalgebra R S) R[0] 0⁻¹
have inl : Membership.mem (γ := Subalgebra R S) R[0] 0
Tactic: rw [inv_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : DivisionRing S
inst_2 : Algebra R S
x : S
int : IsIntegral R x
h0 : x ≠ 0
⊢ Membership.mem (γ := Subalgebra R S) R[x] x⁻¹
have this : FiniteDimensional.{u_1, u_2} R ↥R[x]
Tactic: have : FiniteDimensional R (R[x]) := .of_fg int.fg_adjoin_singleton
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : DivisionRing S
inst_2 : Algebra R S
x : S
int : IsIntegral R x
h0 : x ≠ 0
this : FiniteDimensional.{u_1, u_2} R ↥R[x]
⊢ Membership.mem (γ := Subalgebra R S) R[x] x⁻¹
have inr : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: obtain ⟨⟨y, hy⟩, h1⟩ := FiniteDimensional.exists_mul_eq_one R
    (K := R[x]) (x := ⟨x, subset_adjoin rfl⟩) (mt Subtype.ext_iff.mp h0)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : DivisionRing S
inst_2 : Algebra R S
x : S
int : IsIntegral R x
h0 : x ≠ 0
this : FiniteDimensional.{u_1, u_2} R ↥R[x]
y : S
hy : Membership.mem (γ := Subalgebra R S) R[x] y
h1 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Membership.mem (γ := Subalgebra R S) R[x] x⁻¹
have inr : Membership.mem (γ := Subalgebra R S) R[x]
  (↑(Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) y hy) : S)
Tactic: rwa [← mul_left_cancel₀ h0 ((Subtype.ext_iff.mp h1).trans (mul_inv_cancel₀ h0).symm)]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : DivisionRing S
inst_2 : Algebra R S
x : S
A : Subalgebra R S
int : IsIntegral R x
inv_mem : x⁻¹ ∈ A
⊢ x ∈ A
have rw : x⁻¹⁻¹ ∈ A
Tactic: rw [← inv_inv x]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
x : A
hx : IsIntegral R x
⊢ LE.le (α := Subalgebra R A) R[x] (integralClosure R A)
have rw : {x} ⊆ (↑(integralClosure R A) : Set A)
Tactic: rw [Algebra.adjoin_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
x : A
hx : IsIntegral R x
⊢ {x} ⊆ (↑(integralClosure R A) : Set A)
have simp : Membership.mem (γ := Subalgebra R A) (integralClosure R A) x
Tactic: simp only [SetLike.mem_coe, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ Eq (α := Subalgebra R A) (integralClosure R A) ⊤ ↔ Algebra.IsIntegral R A
have rw : LE.le (α := Subalgebra R A) ⊤ (integralClosure R A) ↔ Algebra.IsIntegral R A
Tactic: rw [← top_le_iff, le_integralClosure_iff_isIntegral,
      (Subalgebra.topEquiv (R := R) (A := A)).isIntegral_iff]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
rw : LE.le (α := Subalgebra R A) ⊤ (integralClosure R A) ↔ Algebra.IsIntegral R A
⊢ Eq (α := Subalgebra R A) (integralClosure R A) ⊤ ↔ Algebra.IsIntegral R A
have rw₁ : Algebra.IsIntegral.{u_1, u_2} R ↥⊤ ↔ Algebra.IsIntegral R A
Tactic: rw [← top_le_iff, le_integralClosure_iff_isIntegral,
      (Subalgebra.topEquiv (R := R) (A := A)).isIntegral_iff]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
rw : LE.le (α := Subalgebra R A) ⊤ (integralClosure R A) ↔ Algebra.IsIntegral R A
rw₁ : Algebra.IsIntegral.{u_1, u_2} R ↥⊤ ↔ Algebra.IsIntegral R A
⊢ Eq (α := Subalgebra R A) (integralClosure R A) ⊤ ↔ Algebra.IsIntegral R A
have rw₂ : Algebra.IsIntegral R A ↔ Algebra.IsIntegral R A
Tactic: rw [← top_le_iff, le_integralClosure_iff_isIntegral,
      (Subalgebra.topEquiv (R := R) (A := A)).isIntegral_iff]