awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Morse
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
inst_7 : DecidableEq (↑(f.rootSet S) : Type u_2)
hf : Splits (map (algebraMap R S) f)
p : Ideal S
inst_8 : p.IsPrime
g : G
hg : Membership.mem (γ := Subgroup G) (Ideal.inertia G p) g
hfp : ¬Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S,
      ∀ c ∈ f.rootSet S,
        ∀ d ∈ f.rootSet S,
          Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) a : S ⧸ p) ((π : (a : S) → S ⧸ p) b : S ⧸ p) →
            Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) c : S ⧸ p) ((π : (a : S) → S ⧸ p) d : S ⧸ p) →
              a ≠ b → c ≠ d → Eq (α := Set S) {a, b} {c, d}
hπ : ∀ (x : S), Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) (g • x) : S ⧸ p) ((π : (a : S) → S ⧸ p) x : S ⧸ p)
x : (↑(f.rootSet S) : Type u_2)
hx : g • x ≠ x
z : (↑(f.rootSet S) : Type u_2)
neg : (↑(g • z) : S) = (↑(if z = g • x then x else if z = x then g • x else z) : S)
⊢ Eq.{u_2 + 1} (α := S)
    (↑((((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g :
              Equiv.Perm (↑(f.rootSet S) : Type u_2)) :
            (a : (↑(f.rootSet S) : Type u_2)) → (↑(f.rootSet S) : Type u_2))
          z) :
      S)
    (↑((Equiv.swap (g • x) x : (a : (↑(f.rootSet S) : Type u_2)) → (↑(f.rootSet S) : Type u_2)) z) : S)

Tactic:
simp only [Equiv.swap_apply_def, MulAction.toPermHom_apply, MulAction.toPerm_apply]

Premises used: MulAction.toPerm_apply, Equiv.swap_apply_def, MulAction.toPermHom_apply
-- Module: Mathlib.RingTheory.Polynomial.Morse
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
inst_7 : DecidableEq (↑(f.rootSet S) : Type u_2)
hf : Splits (map (algebraMap R S) f)
p : Ideal S
inst_8 : p.IsPrime
g : G
hg : Membership.mem (γ := Subgroup G) (Ideal.inertia G p) g
hfp : ¬Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S,
      ∀ c ∈ f.rootSet S,
        ∀ d ∈ f.rootSet S,
          Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) a : S ⧸ p) ((π : (a : S) → S ⧸ p) b : S ⧸ p) →
            Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) c : S ⧸ p) ((π : (a : S) → S ⧸ p) d : S ⧸ p) →
              a ≠ b → c ≠ d → Eq (α := Set S) {a, b} {c, d}
hπ : ∀ (x : S), Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) (g • x) : S ⧸ p) ((π : (a : S) → S ⧸ p) x : S ⧸ p)
x : (↑(f.rootSet S) : Type u_2)
hx : g • x ≠ x
z : (↑(f.rootSet S) : Type u_2)
pos : ∀ (hz : z = g • x), (↑(g • z) : S) = (↑x : S)
pos₁ : ∀ (hz : ¬z = g • x) (hz' : z = x), (↑(g • z) : S) = (↑(g • x) : S)
neg : ∀ (hz : ¬z = g • x) (hz' : ¬z = x), (↑(g • z) : S) = (↑z : S)
⊢ (↑(g • z) : S) = (↑(if z = g • x then x else if z = x then g • x else z) : S)

Tactic:
split_ifs with hz hz'
-- Module: Mathlib.RingTheory.Polynomial.Morse
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
inst_7 : DecidableEq (↑(f.rootSet S) : Type u_2)
hf : Splits (map (algebraMap R S) f)
p : Ideal S
inst_8 : p.IsPrime
g : G
hg : Membership.mem (γ := Subgroup G) (Ideal.inertia G p) g
hfp : ¬Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S,
      ∀ c ∈ f.rootSet S,
        ∀ d ∈ f.rootSet S,
          Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) a : S ⧸ p) ((π : (a : S) → S ⧸ p) b : S ⧸ p) →
            Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) c : S ⧸ p) ((π : (a : S) → S ⧸ p) d : S ⧸ p) →
              a ≠ b → c ≠ d → Eq (α := Set S) {a, b} {c, d}
hπ : ∀ (x : S), Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) (g • x) : S ⧸ p) ((π : (a : S) → S ⧸ p) x : S ⧸ p)
x : (↑(f.rootSet S) : Type u_2)
hx : g • x ≠ x
z : (↑(f.rootSet S) : Type u_2)
hz : z = g • x
pos : (↑(g • g • x) : S) = (↑x : S)
⊢ (↑(g • z) : S) = (↑x : S)

Tactic:
subst hz
-- Module: Mathlib.RingTheory.Polynomial.Morse
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
inst_7 : DecidableEq (↑(f.rootSet S) : Type u_2)
hf : Splits (map (algebraMap R S) f)
p : Ideal S
inst_8 : p.IsPrime
g : G
hg : Membership.mem (γ := Subgroup G) (Ideal.inertia G p) g
hfp : ¬Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S,
      ∀ c ∈ f.rootSet S,
        ∀ d ∈ f.rootSet S,
          Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) a : S ⧸ p) ((π : (a : S) → S ⧸ p) b : S ⧸ p) →
            Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) c : S ⧸ p) ((π : (a : S) → S ⧸ p) d : S ⧸ p) →
              a ≠ b → c ≠ d → Eq (α := Set S) {a, b} {c, d}
hπ : ∀ (x : S), Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) (g • x) : S ⧸ p) ((π : (a : S) → S ⧸ p) x : S ⧸ p)
x : (↑(f.rootSet S) : Type u_2)
hx : g • x ≠ x
⊢ Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) (g • g • (↑x : S)) : S ⧸ p) ((π : (a : S) → S ⧸ p) (g • (↑x : S)) : S ⧸ p)

Tactic:
simp [hπ]
-- Module: Mathlib.RingTheory.Polynomial.Morse
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
inst_7 : DecidableEq (↑(f.rootSet S) : Type u_2)
hf : Splits (map (algebraMap R S) f)
p : Ideal S
inst_8 : p.IsPrime
g : G
hg : Membership.mem (γ := Subgroup G) (Ideal.inertia G p) g
hfp : ¬Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S,
      ∀ c ∈ f.rootSet S,
        ∀ d ∈ f.rootSet S,
          Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) a : S ⧸ p) ((π : (a : S) → S ⧸ p) b : S ⧸ p) →
            Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) c : S ⧸ p) ((π : (a : S) → S ⧸ p) d : S ⧸ p) →
              a ≠ b → c ≠ d → Eq (α := Set S) {a, b} {c, d}
hπ : ∀ (x : S), Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) (g • x) : S ⧸ p) ((π : (a : S) → S ⧸ p) x : S ⧸ p)
x : (↑(f.rootSet S) : Type u_2)
hx : g • x ≠ x
⊢ Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) (g • (↑x : S)) : S ⧸ p) ((π : (a : S) → S ⧸ p) (↑x : S) : S ⧸ p)

Tactic:
simp [hπ]
-- Module: Mathlib.RingTheory.Polynomial.Morse
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
inst_7 : DecidableEq (↑(f.rootSet S) : Type u_2)
hf : Splits (map (algebraMap R S) f)
p : Ideal S
inst_8 : p.IsPrime
g : G
hg : Membership.mem (γ := Subgroup G) (Ideal.inertia G p) g
hfp : ¬Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S,
      ∀ c ∈ f.rootSet S,
        ∀ d ∈ f.rootSet S,
          Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) a : S ⧸ p) ((π : (a : S) → S ⧸ p) b : S ⧸ p) →
            Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) c : S ⧸ p) ((π : (a : S) → S ⧸ p) d : S ⧸ p) →
              a ≠ b → c ≠ d → Eq (α := Set S) {a, b} {c, d}
hπ : ∀ (x : S), Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) (g • x) : S ⧸ p) ((π : (a : S) → S ⧸ p) x : S ⧸ p)
x : (↑(f.rootSet S) : Type u_2)
hx : g • x ≠ x
⊢ g • g • (↑x : S) ≠ g • (↑x : S)

Tactic:
simpa [← rootSet.coe_smul]

Premises used: Polynomial.rootSet.coe_smul
-- Module: Mathlib.RingTheory.Polynomial.Morse
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
inst_7 : DecidableEq (↑(f.rootSet S) : Type u_2)
hf : Splits (map (algebraMap R S) f)
p : Ideal S
inst_8 : p.IsPrime
g : G
hg : Membership.mem (γ := Subgroup G) (Ideal.inertia G p) g
hfp : ¬Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S,
      ∀ c ∈ f.rootSet S,
        ∀ d ∈ f.rootSet S,
          Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) a : S ⧸ p) ((π : (a : S) → S ⧸ p) b : S ⧸ p) →
            Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) c : S ⧸ p) ((π : (a : S) → S ⧸ p) d : S ⧸ p) →
              a ≠ b → c ≠ d → Eq (α := Set S) {a, b} {c, d}
hπ : ∀ (x : S), Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) (g • x) : S ⧸ p) ((π : (a : S) → S ⧸ p) x : S ⧸ p)
x : (↑(f.rootSet S) : Type u_2)
hx : g • x ≠ x
⊢ g • (↑x : S) ≠ (↑x : S)

Tactic:
simpa [← rootSet.coe_smul]

Premises used: Polynomial.rootSet.coe_smul
-- Module: Mathlib.RingTheory.Polynomial.Morse
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
inst_7 : DecidableEq (↑(f.rootSet S) : Type u_2)
hf : Splits (map (algebraMap R S) f)
p : Ideal S
inst_8 : p.IsPrime
g : G
hg : Membership.mem (γ := Subgroup G) (Ideal.inertia G p) g
hfp : ¬Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S,
      ∀ c ∈ f.rootSet S,
        ∀ d ∈ f.rootSet S,
          Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) a : S ⧸ p) ((π : (a : S) → S ⧸ p) b : S ⧸ p) →
            Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) c : S ⧸ p) ((π : (a : S) → S ⧸ p) d : S ⧸ p) →
              a ≠ b → c ≠ d → Eq (α := Set S) {a, b} {c, d}
hπ : ∀ (x : S), Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) (g • x) : S ⧸ p) ((π : (a : S) → S ⧸ p) x : S ⧸ p)
x : (↑(f.rootSet S) : Type u_2)
hx : g • x ≠ x
⊢ Eq (α := Set S) {g • g • (↑x : S), g • (↑x : S)} {g • (↑x : S), (↑x : S)}

Tactic:
have key := hp (g • g • x) (g • g • x).2 (g • x) (g • x).2 (g • x) (g • x).2 x x.2
      (by simp [hπ]) (by simp [hπ]) (by simpa [← rootSet.coe_smul]) (by simpa [← rootSet.coe_smul])
-- Module: Mathlib.RingTheory.Polynomial.Morse
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
inst_7 : DecidableEq (↑(f.rootSet S) : Type u_2)
hf : Splits (map (algebraMap R S) f)
p : Ideal S
inst_8 : p.IsPrime
g : G
hg : Membership.mem (γ := Subgroup G) (Ideal.inertia G p) g
hfp : ¬Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S,
      ∀ c ∈ f.rootSet S,
        ∀ d ∈ f.rootSet S,
          Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) a : S ⧸ p) ((π : (a : S) → S ⧸ p) b : S ⧸ p) →
            Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) c : S ⧸ p) ((π : (a : S) → S ⧸ p) d : S ⧸ p) →
              a ≠ b → c ≠ d → Eq (α := Set S) {a, b} {c, d}
hπ : ∀ (x : S), Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) (g • x) : S ⧸ p) ((π : (a : S) → S ⧸ p) x : S ⧸ p)
x : (↑(f.rootSet S) : Type u_2)
hx : g • x ≠ x
key : Eq (α := Set S) {g • g • (↑x : S), g • (↑x : S)} {g • (↑x : S), (↑x : S)}
⊢ (↑(g • g • x) : S) = (↑x : S)

Tactic:
grind [rootSet.coe_smul]

Premises used: Polynomial.rootSet.coe_smul
-- Module: Mathlib.RingTheory.Polynomial.Morse
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
inst_7 : DecidableEq (↑(f.rootSet S) : Type u_2)
hf : Splits (map (algebraMap R S) f)
p : Ideal S
inst_8 : p.IsPrime
g : G
hg : Membership.mem (γ := Subgroup G) (Ideal.inertia G p) g
hfp : ¬Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S,
      ∀ c ∈ f.rootSet S,
        ∀ d ∈ f.rootSet S,
          Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) a : S ⧸ p) ((π : (a : S) → S ⧸ p) b : S ⧸ p) →
            Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) c : S ⧸ p) ((π : (a : S) → S ⧸ p) d : S ⧸ p) →
              a ≠ b → c ≠ d → Eq (α := Set S) {a, b} {c, d}
hπ : ∀ (x : S), Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) (g • x) : S ⧸ p) ((π : (a : S) → S ⧸ p) x : S ⧸ p)
x : (↑(f.rootSet S) : Type u_2)
hx : g • x ≠ x
z : (↑(f.rootSet S) : Type u_2)
hz : ¬z = g • x
hz' : z = x
⊢ (↑(g • z) : S) = (↑(g • x) : S)

Tactic:
simp [hz']
-- Module: Mathlib.RingTheory.Polynomial.Morse
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
inst_7 : DecidableEq (↑(f.rootSet S) : Type u_2)
hf : Splits (map (algebraMap R S) f)
p : Ideal S
inst_8 : p.IsPrime
g : G
hg : Membership.mem (γ := Subgroup G) (Ideal.inertia G p) g
hfp : ¬Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S,
      ∀ c ∈ f.rootSet S,
        ∀ d ∈ f.rootSet S,
          Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) a : S ⧸ p) ((π : (a : S) → S ⧸ p) b : S ⧸ p) →
            Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) c : S ⧸ p) ((π : (a : S) → S ⧸ p) d : S ⧸ p) →
              a ≠ b → c ≠ d → Eq (α := Set S) {a, b} {c, d}
hπ : ∀ (x : S), Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) (g • x) : S ⧸ p) ((π : (a : S) → S ⧸ p) x : S ⧸ p)
x : (↑(f.rootSet S) : Type u_2)
hx : g • x ≠ x
z : (↑(f.rootSet S) : Type u_2)
hz : ¬z = g • x
hz' : ¬z = x
⊢ (↑(g • z) : S) = (↑z : S)

Tactic:
grind [rootSet.coe_smul, SetLike.coe_eq_coe]

Premises used: SetLike.coe_eq_coe, Polynomial.rootSet.coe_smul
-- Module: Mathlib.RingTheory.Polynomial.Morse
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
hf : Splits (map (algebraMap R S) f)
inst_7 : MulAction.IsPretransitive.{u_3, u_2} G (↑(f.rootSet S) : Type u_2)
h :
  ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ Set.ncard.{u_2} (α := S ⧸ m.asIdeal) (f.rootSet (S ⧸ m.asIdeal)) + 1
hG : Eq.{u_3 + 1} (α := Subgroup G) (⨆ (m : MaximalSpectrum S), Ideal.inertia G m.asIdeal) ⊤
hS1 :
  ∀ (σ : G),
    Membership.mem (γ := Set G) (⋃ (m : MaximalSpectrum S), (↑(Ideal.inertia G m.asIdeal) : Set G)) σ →
      Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
          ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ :
            Equiv.Perm (↑(f.rootSet S) : Type u_2))
          (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
        Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
          ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ)
hS2 :
  Eq.{u_3 + 1} (α := Subgroup G) (Subgroup.closure (⋃ (m : MaximalSpectrum S), (↑(Ideal.inertia G m.asIdeal) : Set G)))
    ⊤
⊢ Function.Surjective.{u_3 + 1, u_2 + 1} (α := G) (β := Equiv.Perm (↑(f.rootSet S) : Type u_2))
    (⇑(MulAction.toPermHom G (↑(f.rootSet S) : Type u_2)) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2))

Tactic:
apply surjective_of_isSwap_of_isPretransitive'
      (⋃ m : MaximalSpectrum S, m.asIdeal.inertia G)

Premises used: surjective_of_isSwap_of_isPretransitive', Set.iUnion
-- Module: Mathlib.RingTheory.Polynomial.Morse
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
hf : Splits (map (algebraMap R S) f)
inst_7 : MulAction.IsPretransitive.{u_3, u_2} G (↑(f.rootSet S) : Type u_2)
h :
  ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ Set.ncard.{u_2} (α := S ⧸ m.asIdeal) (f.rootSet (S ⧸ m.asIdeal)) + 1
hG : Eq.{u_3 + 1} (α := Subgroup G) (⨆ (m : MaximalSpectrum S), Ideal.inertia G m.asIdeal) ⊤
σ : G
hσ : Membership.mem (γ := Set G) (⋃ (m : MaximalSpectrum S), (↑(Ideal.inertia G m.asIdeal) : Set G)) σ
hS1 :
  ∀ (m : MaximalSpectrum S) (hm : σ ∈ (↑(Ideal.inertia G m.asIdeal) : Set G)),
    Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
        ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ :
          Equiv.Perm (↑(f.rootSet S) : Type u_2))
        (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
      Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
        ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ)
⊢ Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
      ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ :
        Equiv.Perm (↑(f.rootSet S) : Type u_2))
      (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
    Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
      ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ)

Tactic:
obtain ⟨m, hm⟩ := Set.mem_iUnion.mp hσ

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Morse
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
hf : Splits (map (algebraMap R S) f)
inst_7 : MulAction.IsPretransitive.{u_3, u_2} G (↑(f.rootSet S) : Type u_2)
h :
  ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ Set.ncard.{u_2} (α := S ⧸ m.asIdeal) (f.rootSet (S ⧸ m.asIdeal)) + 1
hG : Eq.{u_3 + 1} (α := Subgroup G) (⨆ (m : MaximalSpectrum S), Ideal.inertia G m.asIdeal) ⊤
σ : G
hσ : Membership.mem (γ := Set G) (⋃ (m : MaximalSpectrum S), (↑(Ideal.inertia G m.asIdeal) : Set G)) σ
m : MaximalSpectrum S
hm : σ ∈ (↑(Ideal.inertia G m.asIdeal) : Set G)
⊢ Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
      ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ :
        Equiv.Perm (↑(f.rootSet S) : Type u_2))
      (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
    Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
      ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ)

Tactic:
hf.toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia m.asIdeal (h m) σ hm

Premises used: MaximalSpectrum.asIdeal, Polynomial.Splits.toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia
-- Module: Mathlib.RingTheory.Polynomial.Morse
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
hf : Splits (map (algebraMap R S) f)
inst_7 : MulAction.IsPretransitive.{u_3, u_2} G (↑(f.rootSet S) : Type u_2)
h :
  ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ Set.ncard.{u_2} (α := S ⧸ m.asIdeal) (f.rootSet (S ⧸ m.asIdeal)) + 1
hG : Eq.{u_3 + 1} (α := Subgroup G) (⨆ (m : MaximalSpectrum S), Ideal.inertia G m.asIdeal) ⊤
σ : G
hσ : Membership.mem (γ := Set G) (⋃ (m : MaximalSpectrum S), (↑(Ideal.inertia G m.asIdeal) : Set G)) σ
m : MaximalSpectrum S
hm : σ ∈ (↑(Ideal.inertia G m.asIdeal) : Set G)
⊢ Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
      ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ :
        Equiv.Perm (↑(f.rootSet S) : Type u_2))
      (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
    Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
      ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ)

Tactic:
exact hf.toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia m.asIdeal (h m) σ hm

Premises used: MaximalSpectrum.asIdeal, Polynomial.Splits.toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia
-- Module: Mathlib.RingTheory.Polynomial.Morse
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
hf : Splits (map (algebraMap R S) f)
inst_7 : MulAction.IsPretransitive.{u_3, u_2} G (↑(f.rootSet S) : Type u_2)
h :
  ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ Set.ncard.{u_2} (α := S ⧸ m.asIdeal) (f.rootSet (S ⧸ m.asIdeal)) + 1
hG : Eq.{u_3 + 1} (α := Subgroup G) (⨆ (m : MaximalSpectrum S), Ideal.inertia G m.asIdeal) ⊤
⊢ Eq.{u_3 + 1} (α := Subgroup G) (Subgroup.closure (⋃ (m : MaximalSpectrum S), (↑(Ideal.inertia G m.asIdeal) : Set G)))
    ⊤

Tactic:
simpa [Subgroup.closure_iUnion]

Premises used: Subgroup.closure_iUnion
-- Module: Mathlib.RingTheory.Polynomial.Morse
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
G : Type u_3
inst_4 : Group G
inst_5 : MulSemiringAction G S
inst_6 : SMulCommClass G R S
f : R[X]
hf : Splits (map (algebraMap R S) f)
inst_7 : MulAction.IsPretransitive.{u_3, u_2} G (↑(f.rootSet S) : Type u_2)
h :
  ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ Set.ncard.{u_2} (α := S ⧸ m.asIdeal) (f.rootSet (S ⧸ m.asIdeal)) + 1
hG : Eq.{u_3 + 1} (α := Subgroup G) (⨆ (m : MaximalSpectrum S), Ideal.inertia G m.asIdeal) ⊤
hS1 :
  ∀ (σ : G),
    Membership.mem (γ := Set G) (⋃ (m : MaximalSpectrum S), (↑(Ideal.inertia G m.asIdeal) : Set G)) σ →
      Eq.{u_2 + 1} (α := Equiv.Perm (↑(f.rootSet S) : Type u_2))
          ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ :
            Equiv.Perm (↑(f.rootSet S) : Type u_2))
          (1 : Equiv.Perm (↑(f.rootSet S) : Type u_2)) ∨
        Equiv.Perm.IsSwap.{u_2} (α := (↑(f.rootSet S) : Type u_2))
          ((MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) σ)
hS2 hS2₁ :
  Eq.{u_3 + 1} (α := Subgroup G) (Subgroup.closure (⋃ (m : MaximalSpectrum S), (↑(Ideal.inertia G m.asIdeal) : Set G)))
    ⊤
⊢ Function.Surjective.{u_3 + 1, u_2 + 1} (α := G) (β := Equiv.Perm (↑(f.rootSet S) : Type u_2))
    (⇑(MulAction.toPermHom G (↑(f.rootSet S) : Type u_2)) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2))

Tactic:
classical
  apply surjective_of_isSwap_of_isPretransitive'
      (⋃ m : MaximalSpectrum S, m.asIdeal.inertia G)
  · intro σ hσ
    obtain ⟨m, hm⟩ := Set.mem_iUnion.mp hσ
    exact hf.toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia m.asIdeal (h m) σ hm
  · simpa [Subgroup.closure_iUnion]

Premises used: Subgroup.closure_iUnion, surjective_of_isSwap_of_isPretransitive', Set.iUnion
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
r : R
inst : Semiring R
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))

Tactic:
Commute.isNilpotent_mul_right (commute_X_pow _ _).symm ?_

Premises used: Commute.symm, Commute.isNilpotent_mul_right, Polynomial.commute_X_pow
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
r : R
inst : Semiring R
n : ℕ
hnil : IsNilpotent r
refine : IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])
⊢ IsNilpotent (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))

Tactic:
refine Commute.isNilpotent_mul_right (commute_X_pow _ _).symm ?_

Premises used: Commute.symm, Commute.isNilpotent_mul_right, Polynomial.commute_X_pow
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
r : R
inst : Semiring R
n : ℕ
hnil : IsNilpotent r
obtain : ∀ (m : ℕ) (hm : r ^ m = 0), IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])
⊢ IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])

Tactic:
obtain ⟨m, hm⟩ := hnil