awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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)
rw : support (Finsupp.embDomain ι c) = Finset.map ι c.support
rw₁ : (Finsupp.embDomain ι c).support = Finset.map ι c.support
rw₂ rw₃ : Finset.map ι c.support = Finset.map ι c.support
⊢ support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) = Finset.map ι c.support

Tactic:
rw [aux, support, Finsupp.support_embDomain]

Premises used: MvPolynomial.support, Finsupp.support_embDomain
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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)
⊢ support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c) = Finset.map ι c.support

Tactic:
have hsupp : (sumSMulXSMulY c).support = c.support.map ι := by
    rw [aux, support, Finsupp.support_embDomain]
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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
obtain :
  ∀ (a : n) (ha : a ∈ c.support),
    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)

Tactic:
obtain ⟨a, ha⟩ := hc.nonempty

Premises used: Finset.Nontrivial.nonempty
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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
nontrivial :
  Finset.Nontrivial.{u_1} (α := n ⊕ n →₀ ℕ)
    (support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c))
hd :
  Membership.mem (α := n ⊕ n →₀ ℕ) (γ := Finset (n ⊕ n →₀ ℕ))
    (support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c))
    ((ι : (a : n) → n ⊕ n →₀ ℕ) a : n ⊕ n →₀ ℕ)
hdi : Eq (α := ℕ) ((((ι : (a : n) → n ⊕ n →₀ ℕ) a : n ⊕ n →₀ ℕ) : (a : n ⊕ n) → ℕ) (Sum.inl a) : ℕ) (1 : ℕ)
disjoint :
  (↑(support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c)) :
        Set (n ⊕ n →₀ ℕ)).PairwiseDisjoint
    Finsupp.support
isPrimitive :
  ∀ (r : R), (∀ (d : n ⊕ n →₀ ℕ), r ∣ coeff d ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c)) → IsUnit 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:
apply irreducible_of_disjoint_support (d := ι a) (i := .inl a)

Premises used: MvPolynomial.irreducible_of_disjoint_support
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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
nontrivial : (Finset.map ι c.support).Nontrivial
nontrivial₁ nontrivial₂ nontrivial₃ nontrivial₄ : c.support.Nontrivial
⊢ Finset.Nontrivial.{u_1} (α := n ⊕ n →₀ ℕ)
    (support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c))

Tactic:
rwa [hsupp, Finset.map_nontrivial]

Premises used: Finset.map_nontrivial
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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
hd :
  Ne.{u_2 + 1} (α := R)
    (coeff.{u_2, u_1} (σ := n ⊕ n) ((ι : (a : n) → n ⊕ n →₀ ℕ) a)
      ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c))
    0
hd₁ : Ne.{u_2 + 1} (α := R) ((c : (a : n) → R) a : R) (0 : R)
hd₂ hd₃ hd₄ hd₅ : a ∈ c.support
⊢ Membership.mem (α := n ⊕ n →₀ ℕ) (γ := Finset (n ⊕ n →₀ ℕ))
    (support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c))
    ((ι : (a : n) → n ⊕ n →₀ ℕ) a : n ⊕ n →₀ ℕ)

Tactic:
rwa [MvPolynomial.mem_support_iff, hcoeff, ← Finsupp.mem_support_iff]

Premises used: Finsupp.mem_support_iff, MvPolynomial.mem_support_iff
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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
⊢ Eq (α := ℕ) ((((ι : (a : n) → n ⊕ n →₀ ℕ) a : n ⊕ n →₀ ℕ) : (a : n ⊕ n) → ℕ) (Sum.inl a) : ℕ) (1 : ℕ)

Tactic:
simp [ι]
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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
disjoint :
  (↑c.support : Set n).PairwiseDisjoint (α := Finset (n ⊕ n))
    (Function.comp (β := n ⊕ n →₀ ℕ) Finsupp.support (⇑ι : (a : n) → n ⊕ n →₀ ℕ))
⊢ (↑(support.{u_2, u_1} (R := R) ((sumSMulXSMulY : (a : n →₀ R) → MvPolynomial (n ⊕ n) R) c)) :
        Set (n ⊕ n →₀ ℕ)).PairwiseDisjoint
    Finsupp.support

Tactic:
rw [hsupp, Finset.coe_map, ι.injective.injOn.pairwiseDisjoint_image]

Premises used: Function.Injective.injOn, Set.InjOn.pairwiseDisjoint_image, Function.Embedding.injective, Finset.coe_map
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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
this : (↑c.support : Set n).PairwiseDisjoint (α := Finset (n ⊕ n)) fun (x : n) ↦ {Sum.inl x, Sum.inr x}
⊢ (↑c.support : Set n).PairwiseDisjoint (α := Finset (n ⊕ n))
    (Function.comp (β := n ⊕ n →₀ ℕ) Finsupp.support (⇑ι : (a : n) → n ⊕ n →₀ ℕ))

Tactic:
simpa [ι, Function.comp_def, Finsupp.support_add_eq, Finsupp.support_single]

Premises used: Finsupp.support_single, Finsupp.support_add_eq, Function.comp_def
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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
disjoint : (↑c.support : Set n).PairwiseDisjoint (α := Finset (n ⊕ n)) fun (x : n) ↦ {Sum.inl x, Sum.inr x}
⊢ (↑c.support : Set n).PairwiseDisjoint (α := Finset (n ⊕ n))
    (Function.comp (β := n ⊕ n →₀ ℕ) Finsupp.support (⇑ι : (a : n) → n ⊕ n →₀ ℕ))

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]
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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)) fun (x : n) ↦ {Sum.inl x, Sum.inr x}

Tactic:
simp [Set.PairwiseDisjoint, Set.Pairwise, ne_comm]

Premises used: Set.PairwiseDisjoint, Set.Pairwise, ne_comm
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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)
isPrimitive : ∀ (i : n), r ∣ (c : (a : n) → R) i
⊢ IsUnit r

Tactic:
apply h_dvd
-- Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
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)
i : n
⊢ r ∣ (c : (a : n) → R) i

Tactic:
simpa [hcoeff] using hr (ι i)

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.MvPolynomial.Localization
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
x : MvPolynomial σ R
⊢ Eq (α := MvPolynomial σ S)
    (((↑(algebraTensorAlgEquiv R S) : TensorProduct R S (MvPolynomial σ R) ≃ₗ[S] MvPolynomial σ S) :
          (a : TensorProduct R S (MvPolynomial σ R)) → MvPolynomial σ S)
        (1 ⊗ₜ[R] x) :
      MvPolynomial σ S)
    ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R (MvPolynomial σ R) (MvPolynomial σ S)) :
          (a : MvPolynomial σ R) → MvPolynomial σ S)
        x :
      MvPolynomial σ S)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Localization
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)
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)
⊢ 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)

Tactic:
simp_rw [IsLocalization.eq_mk'_iff_mul_eq, algebraMap_def, map_C, ← map_mul,
    IsLocalization.mk'_spec]

Premises used: map_mul, MvPolynomial.map_C, IsLocalization.eq_mk'_iff_mul_eq, MvPolynomial.algebraMap_def, IsLocalization.mk'_spec
-- Module: Mathlib.RingTheory.MvPolynomial.Localization
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)

Tactic:
Submodule.span_induction ?_ ?_ ?_ ?_ hp

Premises used: Submodule.span_induction
-- Module: Mathlib.RingTheory.MvPolynomial.Localization
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)
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)
⊢ Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) p : S) (0 : S)

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ hp
-- Module: Mathlib.RingTheory.MvPolynomial.Localization
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)
        (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
          1) :
      S)
    (0 : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Localization
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) 0 : S) (0 : S)

Tactic:
simp