awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ :=
  { toFun := fun (i : n) ↦ HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl i) 1) (Finsupp.single (Sum.inr i) 1),
    inj' := ⋯ }
aux : (sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c = Finsupp.embDomain ι c
hcoeff :
  ∀ (i : n),
    Eq.{u_2 + 1} (α := R)
      (coeff.{u_2, u_1} (σ := n ⊕ n) ((ι : (a : n) → n ⊕ n →₀ ℕ) i)
          ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) :
        R)
      ((c : (a : n) → R) i : R)
hsupp : support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ (↑c.support : Set n).PairwiseDisjoint (α := Finset (n ⊕ n))
    (Function.comp (β := n ⊕ n →₀ ℕ) Finsupp.support (⇑ι : (a : n) → n ⊕ n →₀ ℕ))
have disjoint : (↑c.support : Set n).PairwiseDisjoint (α := Finset (n ⊕ n)) fun (x : n) ↦ {Sum.inl x, Sum.inr x}
Tactic: suffices (c.support : Set n).PairwiseDisjoint fun x ↦ {Sum.inl x, Sum.inr x} by
      simpa [ι, Function.comp_def, Finsupp.support_add_eq, Finsupp.support_single]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ :=
  { toFun := fun (i : n) ↦ HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl i) 1) (Finsupp.single (Sum.inr i) 1),
    inj' := ⋯ }
aux : (sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c = Finsupp.embDomain ι c
hcoeff :
  ∀ (i : n),
    Eq.{u_2 + 1} (α := R)
      (coeff.{u_2, u_1} (σ := n ⊕ n) ((ι : (a : n) → n ⊕ n →₀ ℕ) i)
          ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) :
        R)
      ((c : (a : n) → R) i : R)
hsupp : support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) = Finset.map ι c.support
a : n
ha : a ∈ c.support
r : R
hr : ∀ (d : n ⊕ n →₀ ℕ), r ∣ coeff d ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c)
⊢ IsUnit r
have isPrimitive : ∀ (i : n), r ∣ (c : (a : n) → R) i
Tactic: apply h_dvd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
let let₁ let₂ :
  Irreducible (M := MvPolynomial.{u_1, u_2} (n ⊕ n) R)
    ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c : MvPolynomial.{u_1, u_2} (n ⊕ n) R)
⊢ Irreducible (M := MvPolynomial.{u_1, u_2} (n ⊕ n) R)
    ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c : MvPolynomial.{u_1, u_2} (n ⊕ n) R)
have let₃ : let ι : n ↪ n ⊕ n →₀ ℕ :=
  { toFun := fun (i : n) ↦ HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl i) 1) (Finsupp.single (Sum.inr i) 1),
    inj' := sorry };
∀ (aux : (sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c = Finsupp.embDomain ι c),
  Irreducible (M := MvPolynomial.{u_1, u_2} (n ⊕ n) R)
    ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c : MvPolynomial.{u_1, u_2} (n ⊕ n) R)
Tactic: classical
  let ι : n ↪ ((n ⊕ n) →₀ ℕ) :=
    ⟨fun i ↦ .single (.inl i) 1 + .single (.inr i) 1,
     fun i j ↦ by simp +contextual [Finsupp.ext_iff, Finsupp.single_apply, ite_eq_iff']⟩
  -- unfortunate defeq abuse... we should have an `.embDomain`-like constructor for MvPolys
  have aux : sumSMulXSMulY c = c.embDomain ι := by
    rw [← Finsupp.sum_single (Finsupp.embDomain _ _)]
    simp [Finsupp.sum_embDomain, sumSMulXSMulY, X, monomial_mul,
      Finsupp.linearCombination_apply, smul_monomial, ι]
    rfl
  have hcoeff (i : n) : coeff (ι i) (sumSMulXSMulY c) = c i := by
    simp [aux, coeff, Finsupp.embDomain_apply]
  have hsupp : (sumSMulXSMulY c).support = c.support.map ι := by
    rw [aux, support, Finsupp.support_embDomain]
  obtain ⟨a, ha⟩ := hc.nonempty
  apply irreducible_of_disjoint_support (d := ι a) (i := .inl a)
  · rwa [hsupp, Finset.map_nontrivial]
  · rwa [MvPolynomial.mem_support_iff, hcoeff, ← Finsupp.mem_support_iff]
  · simp [ι]
  · rw [hsupp, Finset.coe_map, ι.injective.injOn.pairwiseDisjoint_image]
    suffices (c.support : Set n).PairwiseDisjoint fun x ↦ {Sum.inl x, Sum.inr x} by
      simpa [ι, Function.comp_def, Finsupp.support_add_eq, Finsupp.support_single]
    simp [Set.PairwiseDisjoint, Set.Pairwise, ne_comm]
  · intro r hr
    apply h_dvd
    intro i
    simpa [hcoeff] using hr (ι i)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic (goal)
Goal:
n : Type u_1
R : Type u_2
inst : CommRing R
c : n →₀ R
inst_1 : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ (c : (a : n) → R) i) → IsUnit r
let let₁ let₂ :
  Irreducible (M := MvPolynomial.{u_1, u_2} (n ⊕ n) R)
    ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c : MvPolynomial.{u_1, u_2} (n ⊕ n) R)
let₃ :
  let ι : n ↪ n ⊕ n →₀ ℕ :=
    { toFun := fun (i : n) ↦ HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl i) 1) (Finsupp.single (Sum.inr i) 1),
      inj' := ⋯ };
  ∀ (aux : (sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c = Finsupp.embDomain ι c),
    Irreducible (M := MvPolynomial.{u_1, u_2} (n ⊕ n) R)
      ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c : MvPolynomial.{u_1, u_2} (n ⊕ n) R)
⊢ Irreducible (M := MvPolynomial.{u_1, u_2} (n ⊕ n) R)
    ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c : MvPolynomial.{u_1, u_2} (n ⊕ n) R)
have let₄ : let ι : n ↪ n ⊕ n →₀ ℕ :=
  { toFun := fun (i : n) ↦ HAdd.hAdd (α := n ⊕ n →₀ ℕ) (Finsupp.single (Sum.inl i) 1) (Finsupp.single (Sum.inr i) 1),
    inj' := sorry };
∀ (aux : (sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c = Finsupp.embDomain ι c)
  (hcoeff :
    ∀ (i : n),
      Eq.{u_2 + 1} (α := R)
        (coeff.{u_2, u_1} (σ := n ⊕ n) ((ι : (a : n) → n ⊕ n →₀ ℕ) i)
            ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) :
          R)
        ((c : (a : n) → R) i : R)),
  Irreducible (M := MvPolynomial.{u_1, u_2} (n ⊕ n) R)
    ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c : MvPolynomial.{u_1, u_2} (n ⊕ n) R)
Tactic: classical
  let ι : n ↪ ((n ⊕ n) →₀ ℕ) :=
    ⟨fun i ↦ .single (.inl i) 1 + .single (.inr i) 1,
     fun i j ↦ by simp +contextual [Finsupp.ext_iff, Finsupp.single_apply, ite_eq_iff']⟩
  -- unfortunate defeq abuse... we should have an `.embDomain`-like constructor for MvPolys
  have aux : sumSMulXSMulY c = c.embDomain ι := by
    rw [← Finsupp.sum_single (Finsupp.embDomain _ _)]
    simp [Finsupp.sum_embDomain, sumSMulXSMulY, X, monomial_mul,
      Finsupp.linearCombination_apply, smul_monomial, ι]
    rfl
  have hcoeff (i : n) : coeff (ι i) (sumSMulXSMulY c) = c i := by
    simp [aux, coeff, Finsupp.embDomain_apply]
  have hsupp : (sumSMulXSMulY c).support = c.support.map ι := by
    rw [aux, support, Finsupp.support_embDomain]
  obtain ⟨a, ha⟩ := hc.nonempty
  apply irreducible_of_disjoint_support (d := ι a) (i := .inl a)
  · rwa [hsupp, Finset.map_nontrivial]
  · rwa [MvPolynomial.mem_support_iff, hcoeff, ← Finsupp.mem_support_iff]
  · simp [ι]
  · rw [hsupp, Finset.coe_map, ι.injective.injOn.pairwiseDisjoint_image]
    suffices (c.support : Set n).PairwiseDisjoint fun x ↦ {Sum.inl x, Sum.inr x} by
      simpa [ι, Function.comp_def, Finsupp.support_add_eq, Finsupp.support_single]
    simp [Set.PairwiseDisjoint, Set.Pairwise, ne_comm]
  · intro r hr
    apply h_dvd
    intro i
    simpa [hcoeff] using hr (ι i)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Localization (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
M : Submonoid R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
a : R
m : ↥M
⊢ Eq (α := MvPolynomial σ S) ((C : (a : S) → MvPolynomial σ S) (IsLocalization.mk' S a m) : MvPolynomial σ S)
    (IsLocalization.mk' (R := MvPolynomial σ R) (M :=
        (Submonoid.map (F := R →+* MvPolynomial σ R) C M : Submonoid (MvPolynomial σ R))) (MvPolynomial σ S)
        ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
        (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
            Membership.mem (γ := Submonoid (MvPolynomial σ R)) (Submonoid.map (F := R →+* MvPolynomial σ R) C M) x)
            ((C : (a : R) → MvPolynomial σ R) (↑m : R)) ⋯ :
          ↥(Submonoid.map (F := R →+* MvPolynomial σ R) C M)) :
      MvPolynomial σ S)
have simp_rw : HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
    ((C : (a : S) → MvPolynomial σ S) (IsLocalization.mk' S a m) : MvPolynomial σ S)
    ((algebraMap (MvPolynomial σ R) (MvPolynomial σ S) : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((C : (a : R) → MvPolynomial σ R) (↑m : R)) :
      MvPolynomial σ S) =
  (algebraMap (MvPolynomial σ R) (MvPolynomial σ S) : (a : MvPolynomial σ R) → MvPolynomial σ S)
    ((C : (a : R) → MvPolynomial σ R) a)
Tactic: simp_rw [IsLocalization.eq_mk'_iff_mul_eq, algebraMap_def, map_C, ← map_mul,
    IsLocalization.mk'_spec]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Localization (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
M : Submonoid R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
a : R
m : ↥M
simp_rw :
  HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
      ((C : (a : S) → MvPolynomial σ S) (IsLocalization.mk' S a m) : MvPolynomial σ S)
      ((algebraMap (MvPolynomial σ R) (MvPolynomial σ S) : (a : MvPolynomial σ R) → MvPolynomial σ S)
          ((C : (a : R) → MvPolynomial σ R) (↑m : R)) :
        MvPolynomial σ S) =
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S) : (a : MvPolynomial σ R) → MvPolynomial σ S)
      ((C : (a : R) → MvPolynomial σ R) a)
⊢ Eq (α := MvPolynomial σ S) ((C : (a : S) → MvPolynomial σ S) (IsLocalization.mk' S a m) : MvPolynomial σ S)
    (IsLocalization.mk' (R := MvPolynomial σ R) (M :=
        (Submonoid.map (F := R →+* MvPolynomial σ R) C M : Submonoid (MvPolynomial σ R))) (MvPolynomial σ S)
        ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
        (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
            Membership.mem (γ := Submonoid (MvPolynomial σ R)) (Submonoid.map (F := R →+* MvPolynomial σ R) C M) x)
            ((C : (a : R) → MvPolynomial σ R) (↑m : R)) ⋯ :
          ↥(Submonoid.map (F := R →+* MvPolynomial σ R) C M)) :
      MvPolynomial σ S)
have simp_rw₁ : HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
    ((C : (a : S) → MvPolynomial σ S) (IsLocalization.mk' S a m) : MvPolynomial σ S)
    ((map (algebraMap R S) : (a : MvPolynomial σ R) → MvPolynomial σ S) ((C : (a : R) → MvPolynomial σ R) (↑m : R)) :
      MvPolynomial σ S) =
  (map (algebraMap R S) : (a : MvPolynomial σ R) → MvPolynomial σ S) ((C : (a : R) → MvPolynomial σ R) a)
Tactic: simp_rw [IsLocalization.eq_mk'_iff_mul_eq, algebraMap_def, map_C, ← map_mul,
    IsLocalization.mk'_spec]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Localization (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
M : Submonoid R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
a : R
m : ↥M
simp_rw :
  HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
      ((C : (a : S) → MvPolynomial σ S) (IsLocalization.mk' S a m) : MvPolynomial σ S)
      ((algebraMap (MvPolynomial σ R) (MvPolynomial σ S) : (a : MvPolynomial σ R) → MvPolynomial σ S)
          ((C : (a : R) → MvPolynomial σ R) (↑m : R)) :
        MvPolynomial σ S) =
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S) : (a : MvPolynomial σ R) → MvPolynomial σ S)
      ((C : (a : R) → MvPolynomial σ R) a)
simp_rw₁ :
  HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
      ((C : (a : S) → MvPolynomial σ S) (IsLocalization.mk' S a m) : MvPolynomial σ S)
      ((map (algebraMap R S) : (a : MvPolynomial σ R) → MvPolynomial σ S) ((C : (a : R) → MvPolynomial σ R) (↑m : R)) :
        MvPolynomial σ S) =
    (map (algebraMap R S) : (a : MvPolynomial σ R) → MvPolynomial σ S) ((C : (a : R) → MvPolynomial σ R) a)
⊢ Eq (α := MvPolynomial σ S) ((C : (a : S) → MvPolynomial σ S) (IsLocalization.mk' S a m) : MvPolynomial σ S)
    (IsLocalization.mk' (R := MvPolynomial σ R) (M :=
        (Submonoid.map (F := R →+* MvPolynomial σ R) C M : Submonoid (MvPolynomial σ R))) (MvPolynomial σ S)
        ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
        (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
            Membership.mem (γ := Submonoid (MvPolynomial σ R)) (Submonoid.map (F := R →+* MvPolynomial σ R) C M) x)
            ((C : (a : R) → MvPolynomial σ R) (↑m : R)) ⋯ :
          ↥(Submonoid.map (F := R →+* MvPolynomial σ R) C M)) :
      MvPolynomial σ S)
have simp_rw₂ : HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
    ((C : (a : S) → MvPolynomial σ S) (IsLocalization.mk' S a m) : MvPolynomial σ S)
    ((C : (a : S) → MvPolynomial σ S) ((algebraMap R S : (a : R) → S) (↑m : R)) : MvPolynomial σ S) =
  (C : (a : S) → MvPolynomial σ S) ((algebraMap R S : (a : R) → S) a)
Tactic: simp_rw [IsLocalization.eq_mk'_iff_mul_eq, algebraMap_def, map_C, ← map_mul,
    IsLocalization.mk'_spec]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Localization (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
M : Submonoid R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
a : R
m : ↥M
simp_rw :
  HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
      ((C : (a : S) → MvPolynomial σ S) (IsLocalization.mk' S a m) : MvPolynomial σ S)
      ((algebraMap (MvPolynomial σ R) (MvPolynomial σ S) : (a : MvPolynomial σ R) → MvPolynomial σ S)
          ((C : (a : R) → MvPolynomial σ R) (↑m : R)) :
        MvPolynomial σ S) =
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S) : (a : MvPolynomial σ R) → MvPolynomial σ S)
      ((C : (a : R) → MvPolynomial σ R) a)
simp_rw₁ :
  HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
      ((C : (a : S) → MvPolynomial σ S) (IsLocalization.mk' S a m) : MvPolynomial σ S)
      ((map (algebraMap R S) : (a : MvPolynomial σ R) → MvPolynomial σ S) ((C : (a : R) → MvPolynomial σ R) (↑m : R)) :
        MvPolynomial σ S) =
    (map (algebraMap R S) : (a : MvPolynomial σ R) → MvPolynomial σ S) ((C : (a : R) → MvPolynomial σ R) a)
simp_rw₂ :
  HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
      ((C : (a : S) → MvPolynomial σ S) (IsLocalization.mk' S a m) : MvPolynomial σ S)
      ((C : (a : S) → MvPolynomial σ S) ((algebraMap R S : (a : R) → S) (↑m : R)) : MvPolynomial σ S) =
    (C : (a : S) → MvPolynomial σ S) ((algebraMap R S : (a : R) → S) a)
⊢ Eq (α := MvPolynomial σ S) ((C : (a : S) → MvPolynomial σ S) (IsLocalization.mk' S a m) : MvPolynomial σ S)
    (IsLocalization.mk' (R := MvPolynomial σ R) (M :=
        (Submonoid.map (F := R →+* MvPolynomial σ R) C M : Submonoid (MvPolynomial σ R))) (MvPolynomial σ S)
        ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
        (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
            Membership.mem (γ := Submonoid (MvPolynomial σ R)) (Submonoid.map (F := R →+* MvPolynomial σ R) C M) x)
            ((C : (a : R) → MvPolynomial σ R) (↑m : R)) ⋯ :
          ↥(Submonoid.map (F := R →+* MvPolynomial σ R) C M)) :
      MvPolynomial σ S)
have simp_rw₃ : Eq (α := MvPolynomial σ S)
  ((C : (a : S) → MvPolynomial σ S)
      (HMul.hMul (β := S) (IsLocalization.mk' S a m) ((algebraMap R S : (a : R) → S) (↑m : R) : S)) :
    MvPolynomial σ S)
  ((C : (a : S) → MvPolynomial σ S) ((algebraMap R S : (a : R) → S) a) : MvPolynomial σ S)
Tactic: simp_rw [IsLocalization.eq_mk'_iff_mul_eq, algebraMap_def, map_C, ← map_mul,
    IsLocalization.mk'_spec]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Localization (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
M : Submonoid R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : Away r S
p : MvPolynomial Unit R
hp :
  Membership.mem (γ := Ideal (MvPolynomial Unit R))
    (Ideal.span
      {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
          1})
    p
⊢ Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) p : S) (0 : S)
have refine_1 : ∀ (x : MvPolynomial Unit R)
  (h :
    Membership.mem (γ := Set (MvPolynomial Unit R))
      {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
          1}
      x),
  Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) x : S) (0 : S)
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hp
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Localization (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
M : Submonoid R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : Away r S
p : MvPolynomial Unit R
hp :
  Membership.mem (γ := Ideal (MvPolynomial Unit R))
    (Ideal.span
      {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
          1})
    p
refine_1 :
  ∀ (x : MvPolynomial Unit R)
    (h :
      Membership.mem (γ := Set (MvPolynomial Unit R))
        {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
              ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
            1}
        x),
    Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) x : S) (0 : S)
⊢ Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) p : S) (0 : S)
have refine_2 : Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) 0 : S) (0 : S)
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hp
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Localization (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
M : Submonoid R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : Away r S
p : MvPolynomial Unit R
hp :
  Membership.mem (γ := Ideal (MvPolynomial Unit R))
    (Ideal.span
      {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
          1})
    p
refine_1 :
  ∀ (x : MvPolynomial Unit R)
    (h :
      Membership.mem (γ := Set (MvPolynomial Unit R))
        {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
              ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
            1}
        x),
    Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) x : S) (0 : S)
refine_2 : Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) 0 : S) (0 : S)
⊢ Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) p : S) (0 : S)
have refine_3 : ∀ (x y : MvPolynomial Unit R)
  (hx :
    Membership.mem (γ := Submodule (MvPolynomial Unit R) (MvPolynomial Unit R))
      (MvPolynomial Unit R ∙
        (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
          1))
      x)
  (hy :
    Membership.mem (γ := Submodule (MvPolynomial Unit R) (MvPolynomial Unit R))
      (MvPolynomial Unit R ∙
        (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
          1))
      y),
  Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) x : S) (0 : S) →
    Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) y : S) (0 : S) →
      Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) (x + y) : S) (0 : S)
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hp
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Localization (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
M : Submonoid R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : Away r S
p : MvPolynomial Unit R
hp :
  Membership.mem (γ := Ideal (MvPolynomial Unit R))
    (Ideal.span
      {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
          1})
    p
refine_1 :
  ∀ (x : MvPolynomial Unit R)
    (h :
      Membership.mem (γ := Set (MvPolynomial Unit R))
        {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
              ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
            1}
        x),
    Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) x : S) (0 : S)
refine_2 : Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) 0 : S) (0 : S)
refine_3 :
  ∀ (x y : MvPolynomial Unit R)
    (hx :
      Membership.mem (γ := Submodule (MvPolynomial Unit R) (MvPolynomial Unit R))
        (MvPolynomial Unit R ∙
          (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
              ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
            1))
        x)
    (hy :
      Membership.mem (γ := Submodule (MvPolynomial Unit R) (MvPolynomial Unit R))
        (MvPolynomial Unit R ∙
          (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
              ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
            1))
        y),
    Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) x : S) (0 : S) →
      Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) y : S) (0 : S) →
        Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) (x + y) : S) (0 : S)
⊢ Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) p : S) (0 : S)
have refine_4 : ∀ (a x : MvPolynomial Unit R)
  (hx :
    Membership.mem (γ := Submodule (MvPolynomial Unit R) (MvPolynomial Unit R))
      (MvPolynomial Unit R ∙
        (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
          1))
      x),
  Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) x : S) (0 : S) →
    Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) (a • x) : S) (0 : S)
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hp