awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
inst : CommRing B
G : Type u_3
inst_1 : Group G
inst_2 : Finite G
inst_3 : MulSemiringAction G B
Q : Ideal B
inst_4 : Q.IsPrime
val : Fintype G
P : Ideal B := Finset.inf {g : G | g • Q ≠ Q} fun (g : G) ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq :
  map (algebraMap B (B ⧸ Q)) f =
    HPow.hPow (α := (B ⧸ Q)[X]) X (rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i : (a : B) → B[X]) (f.coeff (i + j))
hr_1 : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
h : G
refine_2 : (a - eval b r - h⁻¹ • if h • Q = Q then a else 0) ∈ h⁻¹ • Q
⊢ Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (h • (a - eval b r)) : B ⧸ Q)
    ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if h • Q = Q then a else 0) : B ⧸ Q)

Tactic:
rw [← sub_eq_zero, ← map_sub, Ideal.Quotient.algebraMap_eq, Ideal.Quotient.eq_zero_iff_mem,
      ← Ideal.smul_mem_pointwise_smul_iff (a := h⁻¹), smul_sub, inv_smul_smul]

Premises used: map_sub, sub_eq_zero, Ideal.Quotient.algebraMap_eq, inv_smul_smul, Ideal.Quotient.eq_zero_iff_mem, smul_sub, Ideal.smul_mem_pointwise_smul_iff
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
inst : CommRing B
G : Type u_3
inst_1 : Group G
inst_2 : Finite G
inst_3 : MulSemiringAction G B
Q : Ideal B
inst_4 : Q.IsPrime
val : Fintype G
P : Ideal B := Finset.inf {g : G | g • Q ≠ Q} fun (g : G) ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq :
  map (algebraMap B (B ⧸ Q)) f =
    HPow.hPow (α := (B ⧸ Q)[X]) X (rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i : (a : B) → B[X]) (f.coeff (i + j))
hr_1 : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
h : G
refine_2 : (a - eval b r - h⁻¹ • if h⁻¹ • Q = Q then a else 0) ∈ h⁻¹ • Q
⊢ (a - eval b r - h⁻¹ • if h • Q = Q then a else 0) ∈ h⁻¹ • Q

Tactic:
simp only [← eq_inv_smul_iff (g := h), eq_comm (a := Q)]

Premises used: eq_comm, eq_inv_smul_iff
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
inst : CommRing B
G : Type u_3
inst_1 : Group G
inst_2 : Finite G
inst_3 : MulSemiringAction G B
Q : Ideal B
inst_4 : Q.IsPrime
val : Fintype G
P : Ideal B := Finset.inf {g : G | g • Q ≠ Q} fun (g : G) ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq :
  map (algebraMap B (B ⧸ Q)) f =
    HPow.hPow (α := (B ⧸ Q)[X]) X (rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i : (a : B) → B[X]) (f.coeff (i + j))
hr_1 : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
h : G
pos : ∀ (hh : h⁻¹ • Q = Q), a - eval b r - h⁻¹ • a ∈ h⁻¹ • Q
neg : ∀ (hh : ¬h⁻¹ • Q = Q), a - eval b r - HSMul.hSMul (β := B) h⁻¹ 0 ∈ h⁻¹ • Q
⊢ (a - eval b r - h⁻¹ • if h⁻¹ • Q = Q then a else 0) ∈ h⁻¹ • Q

Tactic:
split_ifs with hh
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
inst : CommRing B
G : Type u_3
inst_1 : Group G
inst_2 : Finite G
inst_3 : MulSemiringAction G B
Q : Ideal B
inst_4 : Q.IsPrime
val : Fintype G
P : Ideal B := Finset.inf {g : G | g • Q ≠ Q} fun (g : G) ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq :
  map (algebraMap B (B ⧸ Q)) f =
    HPow.hPow (α := (B ⧸ Q)[X]) X (rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i : (a : B) → B[X]) (f.coeff (i + j))
hr_1 : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
h : G
hh : h⁻¹ • Q = Q
pos : a - eval b r - a ∈ h⁻¹ • Q
pos₁ : -eval b r ∈ h⁻¹ • Q
pos₂ : -eval b r ∈ Q
pos₃ pos₄ pos₅ pos₆ : eval b r ∈ Q
⊢ a - eval b r - h⁻¹ • a ∈ h⁻¹ • Q

Tactic:
rwa [ha, sub_sub_cancel_left, hh, Q.neg_mem_iff]

Premises used: sub_sub_cancel_left, Ideal.neg_mem_iff
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
inst : CommRing B
G : Type u_3
inst_1 : Group G
inst_2 : Finite G
inst_3 : MulSemiringAction G B
Q : Ideal B
inst_4 : Q.IsPrime
val : Fintype G
P : Ideal B := Finset.inf {g : G | g • Q ≠ Q} fun (g : G) ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq :
  map (algebraMap B (B ⧸ Q)) f =
    HPow.hPow (α := (B ⧸ Q)[X]) X (rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i : (a : B) → B[X]) (f.coeff (i + j))
hr_1 : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
h : G
hh : ¬h⁻¹ • Q = Q
neg : a - eval b r ∈ h⁻¹ • Q
⊢ a - eval b r - HSMul.hSMul (β := B) h⁻¹ 0 ∈ h⁻¹ • Q

Tactic:
rw [smul_zero, sub_zero]

Premises used: sub_zero, smul_zero
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
inst : CommRing B
G : Type u_3
inst_1 : Group G
inst_2 : Finite G
inst_3 : MulSemiringAction G B
Q : Ideal B
inst_4 : Q.IsPrime
val : Fintype G
P : Ideal B := Finset.inf {g : G | g • Q ≠ Q} fun (g : G) ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq :
  map (algebraMap B (B ⧸ Q)) f =
    HPow.hPow (α := (B ⧸ Q)[X]) X (rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i : (a : B) → B[X]) (f.coeff (i + j))
hr_1 : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
h : G
hh : ¬h⁻¹ • Q = Q
⊢ a - eval b r ∈ h⁻¹ • Q

Tactic:
hr' h⁻¹ hh

Premises used: Inv.inv
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
inst : CommRing B
G : Type u_3
inst_1 : Group G
inst_2 : Finite G
inst_3 : MulSemiringAction G B
Q : Ideal B
inst_4 : Q.IsPrime
val : Fintype G
P : Ideal B := Finset.inf {g : G | g • Q ≠ Q} fun (g : G) ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq :
  map (algebraMap B (B ⧸ Q)) f =
    HPow.hPow (α := (B ⧸ Q)[X]) X (rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity (R := B ⧸ Q) 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i : (a : B) → B[X]) (f.coeff (i + j))
hr_1 : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
h : G
hh : ¬h⁻¹ • Q = Q
⊢ a - eval b r ∈ h⁻¹ • Q

Tactic:
exact hr' h⁻¹ hh

Premises used: Inv.inv
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
inst : CommRing B
G : Type u_3
inst_1 : Group G
inst_2 : Finite G
inst_3 : MulSemiringAction G B
Q : Ideal B
inst_4 : Q.IsPrime
b₀ : B
hx :
  ∀ (g : G),
    g • Q = Q →
      Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b₀) : B ⧸ Q)
        ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
obtain :
  ∀ (a b : B) (ha1 : ∀ (g : G), g • a = a) (ha2 : a ∉ Q)
    (hb :
      ∀ (g : G),
        Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
          ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a else 0) : B ⧸ Q)),
    ∃ (a : B) (b : B),
      (∀ (g : G), g • a = a) ∧
        a ∉ Q ∧
          ∀ (g : G),
            Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
              ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)
⊢ ∃ (a : B) (b : B),
    (∀ (g : G), g • a = a) ∧
      a ∉ Q ∧
        ∀ (g : G),
          Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
            ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)

Tactic:
obtain ⟨a, b, ha1, ha2, hb⟩ := fixed_of_fixed1_aux1 G Q

Premises used: _private.0.fixed_of_fixed1_aux1
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
inst : CommRing B
G : Type u_3
inst_1 : Group G
inst_2 : Finite G
inst_3 : MulSemiringAction G B
Q : Ideal B
inst_4 : Q.IsPrime
b₀ : B
hx :
  ∀ (g : G),
    g • Q = Q →
      Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b₀) : B ⧸ Q)
        ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb :
  ∀ (g : G),
    Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a else 0) : B ⧸ Q)
⊢ ∃ (a : B) (b : B),
    (∀ (g : G), g • a = a) ∧
      a ∉ Q ∧
        ∀ (g : G),
          Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
            ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)

Tactic:
⟨a, b * b₀, ha1, ha2, fun g ↦ ?_⟩

Premises used: HMul.hMul, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
inst : CommRing B
G : Type u_3
inst_1 : Group G
inst_2 : Finite G
inst_3 : MulSemiringAction G B
Q : Ideal B
inst_4 : Q.IsPrime
b₀ : B
hx :
  ∀ (g : G),
    g • Q = Q →
      Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b₀) : B ⧸ Q)
        ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb :
  ∀ (g : G),
    Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a else 0) : B ⧸ Q)
refine :
  ∀ (g : G),
    Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • (b * b₀)) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)
⊢ ∃ (a : B) (b : B),
    (∀ (g : G), g • a = a) ∧
      a ∉ Q ∧
        ∀ (g : G),
          Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
            ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)

Tactic:
refine ⟨a, b * b₀, ha1, ha2, fun g ↦ ?_⟩
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
inst : CommRing B
G : Type u_3
inst_1 : Group G
inst_2 : Finite G
inst_3 : MulSemiringAction G B
Q : Ideal B
inst_4 : Q.IsPrime
b₀ : B
hx :
  ∀ (g : G),
    g • Q = Q →
      Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b₀) : B ⧸ Q)
        ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb :
  ∀ (g : G),
    Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a else 0) : B ⧸ Q)
g : G
rw :
  HMul.hMul (α := B ⧸ Q) (β := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a else 0) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b₀) : B ⧸ Q) =
    (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0)
⊢ Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • (b * b₀)) : B ⧸ Q)
    ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)

Tactic:
rw [smul_mul', map_mul, hb]

Premises used: map_mul, smul_mul'
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
inst : CommRing B
G : Type u_3
inst_1 : Group G
inst_2 : Finite G
inst_3 : MulSemiringAction G B
Q : Ideal B
inst_4 : Q.IsPrime
b₀ : B
hx :
  ∀ (g : G),
    g • Q = Q →
      Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b₀) : B ⧸ Q)
        ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb :
  ∀ (g : G),
    Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a else 0) : B ⧸ Q)
g : G
⊢ Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
    ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a else 0) : B ⧸ Q)

Tactic:
specialize hb g
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
inst : CommRing B
G : Type u_3
inst_1 : Group G
inst_2 : Finite G
inst_3 : MulSemiringAction G B
Q : Ideal B
inst_4 : Q.IsPrime
b₀ : B
hx :
  ∀ (g : G),
    g • Q = Q →
      Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b₀) : B ⧸ Q)
        ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
g : G
hb :
  Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
    ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a else 0) : B ⧸ Q)
pos :
  ∀ (hg : g • Q = Q),
    HMul.hMul (α := B ⧸ Q) (β := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) a : B ⧸ Q)
        ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b₀) : B ⧸ Q) =
      (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)
neg :
  ∀ (hg : ¬g • Q = Q),
    HMul.hMul (α := B ⧸ Q) (β := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0 : B ⧸ Q)
        ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b₀) : B ⧸ Q) =
      (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0
⊢ HMul.hMul (α := B ⧸ Q) (β := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a else 0) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b₀) : B ⧸ Q) =
    (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0)

Tactic:
split_ifs with hg
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
inst : CommRing B
G : Type u_3
inst_1 : Group G
inst_2 : Finite G
inst_3 : MulSemiringAction G B
Q : Ideal B
inst_4 : Q.IsPrime
b₀ : B
hx :
  ∀ (g : G),
    g • Q = Q →
      Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b₀) : B ⧸ Q)
        ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
g : G
hb :
  Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
    ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a else 0) : B ⧸ Q)
hg : g • Q = Q
pos :
  HMul.hMul (α := B ⧸ Q) (β := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) a : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b₀) : B ⧸ Q) =
    HMul.hMul (α := B ⧸ Q) (β := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) a : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
pos₁ pos₂ :
  HMul.hMul (α := B ⧸ Q) (β := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) a : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) =
    HMul.hMul (α := B ⧸ Q) (β := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) a : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
⊢ HMul.hMul (α := B ⧸ Q) (β := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) a : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b₀) : B ⧸ Q) =
    (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)

Tactic:
rw [map_mul, hx g hg]

Premises used: map_mul
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
B : Type u_2
inst : CommRing B
G : Type u_3
inst_1 : Group G
inst_2 : Finite G
inst_3 : MulSemiringAction G B
Q : Ideal B
inst_4 : Q.IsPrime
b₀ : B
hx :
  ∀ (g : G),
    g • Q = Q →
      Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b₀) : B ⧸ Q)
        ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
g : G
hb :
  Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
    ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a else 0) : B ⧸ Q)
hg : ¬g • Q = Q
neg : HMul.hMul (α := B ⧸ Q) (β := B ⧸ Q) (0 : B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b₀) : B ⧸ Q) = 0
neg₁ neg₂ : Eq.{u_2 + 1} (α := B ⧸ Q) 0 0
⊢ HMul.hMul (α := B ⧸ Q) (β := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0 : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b₀) : B ⧸ Q) =
    (algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0

Tactic:
rw [map_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, map_zero
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : NoZeroDivisors B
b : B
i j : ℕ
p : A[X]
h :
  map (algebraMap A B) p =
    HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) b : B[X]) ^ i * HPow.hPow (α := B[X]) X j
f : B ≃ₐ[A] B
hi : i ≠ 0
pos : ∀ (ha : b = 0), (f : (a : B) → B) b = b
neg : ∀ (ha : ¬b = 0), (f : (a : B) → B) b = b
⊢ (f : (a : B) → B) b = b

Tactic:
by_cases ha : b = 0
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : NoZeroDivisors B
b : B
i j : ℕ
p : A[X]
h :
  map (algebraMap A B) p =
    HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) b : B[X]) ^ i * HPow.hPow (α := B[X]) X j
f : B ≃ₐ[A] B
hi : i ≠ 0
ha : b = 0
pos : Eq (α := B) ((f : (a : B) → B) 0 : B) (0 : B)
pos₁ pos₂ : Eq.{u_2 + 1} (α := B) 0 0
⊢ (f : (a : B) → B) b = b

Tactic:
rw [ha, map_zero]

Premises used: map_zero
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : NoZeroDivisors B
b : B
i j : ℕ
p : A[X]
h :
  map (algebraMap A B) p =
    HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) b : B[X]) ^ i * HPow.hPow (α := B[X]) X j
f : B ≃ₐ[A] B
hi : i ≠ 0
ha : ¬b = 0
⊢ eval b ((mapAlgHom (↑f : B →ₐ[A] B) : (a : B[X]) → B[X]) (map (algebraMap A B) p)) =
    eval b
      ((mapAlgHom (↑f : B →ₐ[A] B) : (a : B[X]) → B[X])
        (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) b : B[X]) ^ i * HPow.hPow (α := B[X]) X j))

Tactic:
have hf := congrArg (eval b) (congrArg (Polynomial.mapAlgHom f.toAlgHom) h)
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : NoZeroDivisors B
b : B
i j : ℕ
p : A[X]
h :
  map (algebraMap A B) p =
    HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) b : B[X]) ^ i * HPow.hPow (α := B[X]) X j
f : B ≃ₐ[A] B
hi : i ≠ 0
ha : ¬b = 0
hf :
  eval b ((mapAlgHom (↑f : B →ₐ[A] B) : (a : B[X]) → B[X]) (map (algebraMap A B) p)) =
    eval b
      ((mapAlgHom (↑f : B →ₐ[A] B) : (a : B[X]) → B[X])
        (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) b : B[X]) ^ i * HPow.hPow (α := B[X]) X j))
⊢ eval b (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) b : B[X]) ^ i * HPow.hPow (α := B[X]) X j) =
    eval b
      (map (↑(↑f : B →ₐ[A] B) : B →+* B)
        (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) b : B[X]) ^ i * HPow.hPow (α := B[X]) X j))

Tactic:
rw [coe_mapAlgHom, map_map, f.toAlgHom.comp_algebraMap, h] at hf

Premises used: AlgHom.comp_algebraMap, AlgEquiv.toAlgHom, Polynomial.map_map, Polynomial.coe_mapAlgHom
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : NoZeroDivisors B
b : B
i j : ℕ
p : A[X]
h :
  map (algebraMap A B) p =
    HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) b : B[X]) ^ i * HPow.hPow (α := B[X]) X j
f : B ≃ₐ[A] B
hi : i ≠ 0
ha : ¬b = 0
hf :
  eval b (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) b : B[X]) ^ i * HPow.hPow (α := B[X]) X j) =
    eval b
      (map (↑(↑f : B →ₐ[A] B) : B →+* B)
        (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) b : B[X]) ^ i * HPow.hPow (α := B[X]) X j))
⊢ b = ((↑(↑f : B →ₐ[A] B) : B →+* B) : (a : B) → B) b

Tactic:
simp_rw [Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_sub, map_X, map_C,
    eval_mul, eval_pow, eval_sub, eval_X, eval_C, sub_self, zero_pow hi, zero_mul,
    zero_eq_mul, or_iff_left (pow_ne_zero j ha), pow_eq_zero_iff hi, sub_eq_zero] at hf

Premises used: Polynomial.map_mul, pow_eq_zero_iff, Polynomial.eval_C, sub_self, sub_eq_zero, Polynomial.eval_X, Polynomial.eval_pow, MulZeroClass.zero_mul, zero_eq_mul, Polynomial.map_pow, pow_ne_zero, Polynomial.map_X, Polynomial.eval_mul, Polynomial.map_sub, or_iff_left, Polynomial.map_C, Polynomial.eval_sub, zero_pow
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : NoZeroDivisors B
b : B
i j : ℕ
p : A[X]
h :
  map (algebraMap A B) p =
    HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) b : B[X]) ^ i * HPow.hPow (α := B[X]) X j
f : B ≃ₐ[A] B
hi : i ≠ 0
ha : ¬b = 0
hf : b = ((↑(↑f : B →ₐ[A] B) : B →+* B) : (a : B) → B) b
⊢ (f : (a : B) → B) b = b

Tactic:
hf.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : NoZeroDivisors B
b : B
i j : ℕ
p : A[X]
h :
  map (algebraMap A B) p =
    HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) b : B[X]) ^ i * HPow.hPow (α := B[X]) X j
f : B ≃ₐ[A] B
hi : i ≠ 0
ha : ¬b = 0
hf : b = ((↑(↑f : B →ₐ[A] B) : B →+* B) : (a : B) → B) b
⊢ (f : (a : B) → B) b = b

Tactic:
exact hf.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver P
K : Type u_4
L : Type u_5
inst_9 : Field K
inst_10 : Field L
inst_11 : Algebra.{u_1, u_4} (A ⧸ P) K
inst_12 : Algebra.{u_2, u_5} (B ⧸ Q) L
inst_13 : Algebra.{u_1, u_5} (A ⧸ P) L
inst_14 : IsScalarTower.{u_1, u_2, u_5} (A ⧸ P) (B ⧸ Q) L
inst_15 : Algebra K L
inst_16 : IsScalarTower.{u_1, u_4, u_5} (A ⧸ P) K L
inst_17 : Algebra.IsInvariant A B G
inst_18 : Module.IsTorsionFree.{u_2, u_5} (B ⧸ Q) L
f : Gal(L/K)
b : B ⧸ Q
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((((Ideal.Quotient.stabilizerHom Q P G :
                  MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q))
                    (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
                (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
              g :
            AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)) :
          (a : B ⧸ Q) → B ⧸ Q)
        b =
      b
intro :
  ∀ (val : Fintype G),
    Eq (α := L) ((f : (a : L) → L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) b : L) : L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) b : L)
⊢ Eq (α := L) ((f : (a : L) → L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) b : L) : L)
    ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) b : L)

Tactic:
cases nonempty_fintype G

Premises used: nonempty_fintype