awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst_3 : Fintype α
IH :
  ∀ {f : MvPolynomial α S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
    (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial.{w, u_2} (Option α) S
H :
  RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R)
    (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) f
n : Option α →₀ ℕ
i : Option α
m : Option α →₀ ℕ
h :
  Eq.{u_2 + 1} (α := S)
    (coeff m
      ((RingHom.comp
            (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
              (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
            (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))) :
          (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
        (X none)))
    (coeff m
      ((algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S) :
          (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
        (X none)))
h₁ :
  ∀ (val : α),
    Eq.{u_2 + 1} (α := S)
      (coeff m
        ((RingHom.comp
              (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
                (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
              (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))) :
            (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
          (X (some val))))
      (coeff m
        ((algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S) :
            (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
          (X (some val))))
⊢ Eq.{u_2 + 1} (α := S)
    (coeff m
      ((RingHom.comp
            (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
              (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
            (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))) :
          (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
        (X i)))
    (coeff m
      ((algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S) :
          (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
        (X i)))

Tactic:
cases i
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst_3 : Fintype α
IH :
  ∀ {f : MvPolynomial α S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
    (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial.{w, u_2} (Option α) S
H :
  RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R)
    (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) f
n m : Option α →₀ ℕ
⊢ Eq.{u_2 + 1} (α := S)
    (coeff m
      ((RingHom.comp
            (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
              (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
            (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))) :
          (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
        (X none)))
    (coeff m
      ((algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S) :
          (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
        (X none)))

Tactic:
aesop
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst_3 : Fintype α
IH :
  ∀ {f : MvPolynomial α S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
    (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial.{w, u_2} (Option α) S
H :
  RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R)
    (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) f
n m : Option α →₀ ℕ
val : α
⊢ Eq.{u_2 + 1} (α := S)
    (coeff m
      ((RingHom.comp
            (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
              (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
            (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))) :
          (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
        (X (some val))))
    (coeff m
      ((algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S) :
          (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
        (X (some val))))

Tactic:
aesop
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst_3 : Fintype α
IH :
  ∀ {f : MvPolynomial α S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
    (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial.{w, u_2} (Option α) S
H :
  RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R)
    (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) f
n : Option α →₀ ℕ
⊢ (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))) :
        (a : Polynomial (MvPolynomial α S)) → MvPolynomial (Option α) S)
      ((optionEquivLeft S α : (a : MvPolynomial (Option α) S) → Polynomial (MvPolynomial α S)) f) =
    f

Tactic:
aesop
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst_3 : Fintype α
IH :
  ∀ {f : MvPolynomial α S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
    (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial.{w, u_2} (Option α) S
H :
  RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R)
    (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) f
n : Option α →₀ ℕ
⊢ IsIntegral.{u_1, u_2} R (A := S)
    (coeff n.some
      (Polynomial.coeff ((optionEquivLeft S α : (a : MvPolynomial (Option α) S) → Polynomial (MvPolynomial α S)) f)
        ((n : (a : Option α) → ℕ) none)))

Tactic:
have := IH (IsIntegral.coeff (R := MvPolynomial α R)
      (p := optionEquivLeft _ _ f) (.of_map
      (g := (optionEquivLeft _ _).symm.toRingHom) (optionEquivLeft _ _).symm.injective
      (.of_comp (f := (optionEquivLeft _ _).toRingHom) (by
        convert! H
        · ext i m
          · aesop
          · cases i <;> aesop
        · aesop))) (n .none)) n.some
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst_3 : Fintype α
IH :
  ∀ {f : MvPolynomial α S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
    (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial.{w, u_2} (Option α) S
H :
  RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R)
    (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) f
n : Option α →₀ ℕ
this :
  IsIntegral.{u_1, u_2} R (A := S)
    (coeff n.some
      (Polynomial.coeff ((optionEquivLeft S α : (a : MvPolynomial (Option α) S) → Polynomial (MvPolynomial α S)) f)
        ((n : (a : Option α) → ℕ) none)))
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : IsIntegral R (coeff n f)), IsIntegral R (coeff n f)
⊢ IsIntegral R (coeff n f)

Tactic:
rwa [optionEquivLeft_coeff_some_coeff_none] at this

Premises used: MvPolynomial.optionEquivLeft_coeff_some_coeff_none
-- 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
hp : (f.rootSet S).ncard ≤ Set.ncard.{u_2} (α := S ⧸ p) (f.rootSet (S ⧸ p)) + 1
g : G
hg : Membership.mem (γ := Subgroup G) (Ideal.inertia G p) g
pos :
  ∀ (hfp : Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0),
    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)) g :
          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)) g)
neg :
  ∀ (hfp : ¬Eq.{u_2 + 1} (α := (S ⧸ p)[X]) (map (algebraMap R (S ⧸ p)) f) 0),
    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)) g :
          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)) 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)) g :
        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)) g)

Tactic:
by_cases hfp : f.map (algebraMap R (S ⧸ p)) = 0

Premises used: Algebra.algebraMap, HasQuotient.Quotient, Polynomial.map
-- 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
hp : (f.rootSet S).ncard ≤ Set.ncard.{u_2} (α := S ⧸ p) (f.rootSet (S ⧸ p)) + 1
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
pos :
  ∀ (hp : Subsingleton.{u_2 + 1} (↑(f.rootSet S) : Type u_2)) (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),
    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)) g :
          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)) 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)) g :
        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)) g)

Tactic:
rw [rootSet_def f (S ⧸ p), aroots_def, hfp, roots_zero, Multiset.toFinset_zero,
      Finset.coe_empty, Set.ncard_empty, zero_add, Set.ncard_le_one_iff_subsingleton,
      ← Set.subsingleton_coe] at hp

Premises used: Finset.coe_empty, Polynomial.roots_zero, Set.ncard_empty, Set.ncard_le_one_iff_subsingleton, Polynomial.rootSet_def, zero_add, HasQuotient.Quotient, Multiset.toFinset_zero, Set.subsingleton_coe, Polynomial.aroots_def
-- 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
hp : Subsingleton.{u_2 + 1} (↑(f.rootSet S) : Type u_2)
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
⊢ 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)) g :
        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)) g)

Tactic:
Or.inl (Subsingleton.elim _ _)

Premises used: Or.inl, Subsingleton.elim
-- 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
hp : Subsingleton.{u_2 + 1} (↑(f.rootSet S) : Type u_2)
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
⊢ 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)) g :
        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)) g)

Tactic:
exact Or.inl (Subsingleton.elim _ _)

Premises used: Or.inl, Subsingleton.elim
-- 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
hp : (f.rootSet S).ncard ≤ Set.ncard.{u_2} (α := S ⧸ p) (f.rootSet (S ⧸ p)) + 1
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
⊢ ∀ 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}

Tactic:
rw [← hf.image_rootSet_of_map_ne_zero π hfp, Set.ncard_le_ncard_image_add_one_iff] at hp

Premises used: Set.ncard_le_ncard_image_add_one_iff, Polynomial.Splits.image_rootSet_of_map_ne_zero
-- 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}
⊢ ∀ (x : S), Eq (α := S ⧸ p) ((π : (a : S) → S ⧸ p) (g • x) : S ⧸ p) ((π : (a : S) → S ⧸ p) x : S ⧸ p)

Tactic:
have hπ (x : S) : π (g • x) = π x := (Ideal.Quotient.mk_eq_mk_iff_sub_mem (g • x) x).mpr (hg x)
-- 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)
neg :
  (∃ (x : (↑(f.rootSet S) : Type u_2)),
      ¬Eq (α := (↑(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)) g :
                  Equiv.Perm (↑(f.rootSet S) : Type u_2)) :
                (a : (↑(f.rootSet S) : Type u_2)) → (↑(f.rootSet S) : Type u_2))
              x :
            (↑(f.rootSet S) : Type u_2))
          ((1 : (a : (↑(f.rootSet S) : Type u_2)) → (↑(f.rootSet S) : Type u_2)) x : (↑(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)) 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)) g :
        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)) g)

Tactic:
rw [or_iff_not_imp_left, Equiv.ext_iff, not_forall]

Premises used: Equiv.ext_iff, Classical.or_iff_not_imp_left, Classical.not_forall
-- 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
⊢ 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)) g)

Tactic:
⟨g • x, x, hx, ?_⟩

Premises used: Equiv.Perm.IsSwap, And.intro, Exists.intro, HSMul.hSMul
-- 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
neg :
  (MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g =
    Equiv.swap (g • x) x
⊢ 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)) g)

Tactic:
refine ⟨g • x, x, hx, ?_⟩
-- 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
neg :
  ∀ (z : (↑(f.rootSet S) : Type u_2)),
    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)
⊢ (MulAction.toPermHom G (↑(f.rootSet S) : Type u_2) : (a : G) → Equiv.Perm (↑(f.rootSet S) : Type u_2)) g =
    Equiv.swap (g • x) x

Tactic:
ext z