awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
⊢ IsIntegral (MvPolynomial σ R) f ↔ ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
have mp : ∀ (H : IsIntegral (MvPolynomial σ R) f) (n : σ →₀ ℕ), IsIntegral R (coeff n f)
Tactic: classical
  refine ⟨fun H n ↦ ?mp, fun H ↦ ?mpr⟩
  case mpr =>
    rw [← f.support_sum_monomial_coeff]
    simp_rw [monomial_eq]
    refine IsIntegral.sum _ fun n _ ↦ .mul ((H n).map (Algebra.ofId _ _)).tower_top
      (.prod _ fun i _ ↦ .pow ?_ _)
    convert! isIntegral_algebraMap (x := MvPolynomial.X i)
    simp only [algebraMap_def, map_X]
  unfold IsIntegral at H
  wlog hσ : Finite σ generalizing σ
  · obtain ⟨g, hg⟩ := MvPolynomial.exists_rename_eq_of_vars_subset_range (τ := f.vars) f _
      Subtype.val_injective (by simp)
    by_cases hn : n ∈ Set.range (Finsupp.mapDomain ((↑) : f.vars → σ))
    · obtain ⟨n, rfl⟩ := hn
      simp_rw [← hg, coeff_rename_mapDomain _ Subtype.val_injective]
      exact this (f := g) (RingHom.IsIntegralElem.of_map
        (g := (rename ((↑) : f.vars → σ)).toRingHom) (rename_injective _ Subtype.val_injective)
        (.of_comp (f := (killCompl (f := ((↑) : f.vars → σ)) Subtype.val_injective).toRingHom) <| by
        simp only [AlgHom.toRingHom_eq_coe, algebraMap_def, RingHom.coe_coe, hg]
        convert!
          H.map
            ((rename Subtype.val).comp
                (killCompl (f := ((↑) : f.vars → σ)) Subtype.val_injective)).toRingHom
        · exact RingHom.ext (by simp [MvPolynomial.killCompl_map])
        · nth_rw 1 12 [← hg]; simp)) n (.of_fintype _)
    · rw [← hg, coeff_rename_eq_zero _ _ _ (by grind)]
      exact isIntegral_zero
  revert f n
  apply Finite.induction_empty_option _ _ _ σ
  · intro α β e IH f H n
    have := @IH (rename e.symm f) (.of_map (g := (rename e).toRingHom)
      (rename_injective _ e.injective) <| .of_comp (f := (rename e.symm).toRingHom)
        (by convert! H <;> aesop)) (n.embDomain e.symm)
    simpa [Finsupp.embDomain_eq_mapDomain, coeff_rename_mapDomain _ e.symm.injective] using this
  · intro f H n
    refine .of_map (g := (isEmptyAlgEquiv _ PEmpty).symm.toRingHom)
      (isEmptyAlgEquiv _ PEmpty).symm.injective
      (.of_comp (f := (isEmptyAlgEquiv _ PEmpty).toRingHom) ?_)
    convert! H
    · aesop (add simp MvPolynomial.isEmptyAlgEquiv)
    · obtain rfl := Subsingleton.elim n 0
      have : constantCoeff = (isEmptyAlgEquiv S PEmpty).toRingHom := by aesop
      simpa [-EmbeddingLike.apply_eq_iff_eq, -isEmptyAlgEquiv_apply] using
        congr((isEmptyAlgEquiv S PEmpty.{w + 1}).symm ($this f))
  · intro α _ IH f H n
    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
    rwa [optionEquivLeft_coeff_some_coeff_none] at this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (goal)
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
⊢ 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)
have 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)
Tactic: by_cases hfp : f.map (algebraMap R (S ⧸ p)) = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hfp : f.map (algebraMap R (S ⧸ p)) = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (goal)
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
⊢ 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)
have 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)
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
Cleared hypotheses: hp, g, hg, hfp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (hypothesis)
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
⊢ 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)
have 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}
Tactic: rw [← hf.image_rootSet_of_map_ne_zero π hfp, Set.ncard_le_ncard_image_add_one_iff] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (hypothesis)
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}
⊢ 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)
have hπ : ∀ (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)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (goal)
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)
⊢ 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)
have 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)
Tactic: rw [or_iff_not_imp_left, Equiv.ext_iff, not_forall]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (goal)
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)
have 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
Tactic: refine ⟨g • x, x, hx, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (goal)
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
⊢ (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
have 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)
Tactic: ext z
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (goal)
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)
⊢ 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)
have neg : (↑(g • z) : S) = (↑(if z = g • x then x else if z = x then g • x else z) : S)
Tactic: simp only [Equiv.swap_apply_def, MulAction.toPermHom_apply, MulAction.toPerm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (goal)
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)
⊢ (↑(g • z) : S) = (↑(if z = g • x then x else if z = x then g • x else z) : S)
have pos : ∀ (hz : z = g • x), (↑(g • z) : S) = (↑x : S)
Tactic: split_ifs with hz hz'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (goal)
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)
⊢ (↑(g • z) : S) = (↑(if z = g • x then x else if z = x then g • x else z) : S)
have pos₁ : ∀ (hz : ¬z = g • x) (hz' : z = x), (↑(g • z) : S) = (↑(g • x) : S)
Tactic: split_ifs with hz hz'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (goal)
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)
⊢ (↑(g • z) : S) = (↑(if z = g • x then x else if z = x then g • x else z) : S)
have neg : ∀ (hz : ¬z = g • x) (hz' : ¬z = x), (↑(g • z) : S) = (↑z : S)
Tactic: split_ifs with hz hz'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Morse (goal)
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
⊢ (↑(g • z) : S) = (↑x : S)
have pos : (↑(g • g • x) : S) = (↑x : S)
Tactic: subst hz
Cleared hypotheses: z, hz