mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
⊢ ∃ H, ↑H ⊆ W

Tactic:
by
  rcases exists_mulInvClosureNhd WClopen with ⟨V, hV⟩
  let S : Subgroup G := {
    carrier := ⋃ n, V ^ (n + 1)
    mul_mem' := fun ha hb ↦ by
      rcases mem_iUnion.mp ha with ⟨k, hk⟩
      rcases mem_iUnion.mp hb with ⟨l, hl⟩
      apply mem_iUnion.mpr
      use k + 1 + l
      rw [add_assoc, pow_add]
      exact Set.mul_mem_mul hk hl
    one_mem' := by
      apply mem_iUnion.mpr
      use 0
      simp [mem_of_mem_nhds hV.nhds]
    inv_mem' := fun ha ↦ by
      rcases mem_iUnion.mp ha with ⟨k, hk⟩
      apply mem_iUnion.mpr
      use k
      rw [← hV.inv]
      simpa only [inv_pow, Set.mem_inv, inv_inv] using hk }
  have : IsOpen (⋃ n, V ^ (n + 1)) := by
    refine isOpen_iUnion (fun n ↦ ?_)
    rw [pow_succ]
    exact hV.isOpen.mul_left
  use ⟨S, this⟩
  have mulVpow (n : ℕ) : W * V ^ (n + 1) ⊆ W := by
    induction n with
    | zero => simp [hV.mul]
    | succ n ih =>
      rw [pow_succ, ← mul_assoc]
      exact (Set.mul_subset_mul_right ih).trans hV.mul
  have (n : ℕ) : V ^ (n + 1) ⊆ W * V ^ (n + 1) := by
    intro x xin
    rw [Set.mem_mul]
    use 1, einW, x, xin
    rw [one_mul]
  apply iUnion_subset fun i _ a ↦ mulVpow i (this i a)

Goal state after:
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
E' : Type u_3
inst✝³ : Field F
inst✝² : Field E'
inst✝¹ : Algebra F E'
inst✝ : IsGalois F E'
L : IntermediateField F E'
hnfd : FiniteDimensional F ↥L
E : IntermediateField F E' := normalClosure F (↥L) E'
hle : L ≤ E
L' : IntermediateField F ↥E := restrict hle
h : finrank F ↥L' * finrank ↥L' ↥E = finrank F ↥E
⊢ finrank F ↥L = L.fixingSubgroup.index

Tactic:
← IsGalois.card_fixingSubgroup_eq_finrank L',

Goal state after:
F : Type u_1
E' : Type u_3
inst✝³ : Field F
inst✝² : Field E'
inst✝¹ : Algebra F E'
inst✝ : IsGalois F E'
L : IntermediateField F E'
hnfd : FiniteDimensional F ↥L
E : IntermediateField F E' := normalClosure F (↥L) E'
hle : L ≤ E
L' : IntermediateField F ↥E := restrict hle
h : finrank F ↥L' * Nat.card ↥L'.fixingSubgroup = finrank F ↥E
⊢ finrank F ↥L = L.fixingSubgroup.index
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: case a
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
i : ι
f : ι → R
hy : ∑ i, f i • b i ∈ Submodule.span R (Set.range ⇑b)
⊢ ∀ c ∈ Finset.univ, (B ((B.dualBasis hB b) i)) (f c • b c) ∈ 1

Tactic:
rintro j -

Goal state after:
case a
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
i : ι
f : ι → R
hy : ∑ i, f i • b i ∈ Submodule.span R (Set.range ⇑b)
j : ι
⊢ (B ((B.dualBasis hB b) i)) (f j • b j) ∈ 1
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ (X - C x) * (map (algebraMap R S) (minpoly R x) /ₘ (X - C x)) = map (algebraMap R S) (minpoly R x)

Tactic:
mul_divByMonic_eq_iff_isRoot,

Goal state after:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ (map (algebraMap R S) (minpoly R x)).IsRoot x
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ⇑φ
f : R[X]
hf : f.IsPrimitive
h_irr : Irreducible (map φ f)
⊢ Irreducible f

Tactic:
refine
    ⟨fun h => h_irr.not_isUnit (IsUnit.map (mapRingHom φ) h), fun a b h =>
      (h_irr.isUnit_or_isUnit <| by rw [h, Polynomial.map_mul]).imp ?_ ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ⇑φ
f : R[X]
hf : f.IsPrimitive
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ IsUnit (map φ a) → IsUnit a

case refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ⇑φ
f : R[X]
hf : f.IsPrimitive
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ IsUnit (map φ b) → IsUnit b
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
x : S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
y : S
hy : (aeval y) (minpoly R x) = 0
⊢ eval y (minpolyDiv R x) = if x = y then (aeval x) (derivative (minpoly R x)) else 0

Tactic:
eval,

Goal state after:
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
x : S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
y : S
hy : (aeval y) (minpoly R x) = 0
⊢ eval₂ (RingHom.id S) y (minpolyDiv R x) = if x = y then (aeval x) (derivative (minpoly R x)) else 0
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
⊢ σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ

Tactic:
rintro φ ⟨τ, hτ, muleq⟩

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
φ τ : Gal(K/k)
hτ : τ ∈ L'.fixingSubgroup.carrier
muleq : (fun x ↦ σ • x) τ = φ
⊢ φ ∈ (↑H).carrierᶜ
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
b : Basis ι R S
c : Basis κ S T
x✝ : T
⊢ (trace R S) ((↑R (trace S T)) x✝) = (trace R T) x✝

Tactic:
LinearMap.restrictScalars_apply,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
b : Basis ι R S
c : Basis κ S T
x✝ : T
⊢ (trace R S) ((trace S T) x✝) = (trace R T) x✝
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁷ : Group G
inst✝⁶ : CommSemiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
inst✝³ : MulSemiringAction G B
hG : IsGaloisGroup G A B
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
x' : B'
hx' : ∀ (g : G), g • x' = x'
g : G
⊢ g • e.symm x' = e.symm x'

Tactic:
apply e.injective
      simp [he, hx']

Goal state after:
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case inl
a : ZMod 0
ha : 2 * a.val ≠ 0
⊢ (-a).valMinAbs = -a.valMinAbs

pp: case inr
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ (-a).valMinAbs = -a.valMinAbs

Tactic:
· rfl

Goal state after:
case inr
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ (-a).valMinAbs = -a.valMinAbs
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case mpr.inl
n : ℕ
a : ZMod n
⊢ a.valMinAbs.natAbs = a.valMinAbs.natAbs

pp: case mpr.inr
n : ℕ
b : ZMod n
⊢ (-b).valMinAbs.natAbs = b.valMinAbs.natAbs

Tactic:
· rfl

Goal state after:
case mpr.inr
n : ℕ
b : ZMod n
⊢ (-b).valMinAbs.natAbs = b.valMinAbs.natAbs
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case mpr
n : ℕ
a b : ZMod n
⊢ a = b ∨ a = -b → a.valMinAbs.natAbs = b.valMinAbs.natAbs

Tactic:
rintro (rfl | rfl)
    · rfl
    · rw [natAbs_valMinAbs_neg]

Goal state after:
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case zero
a b : ZMod 0
⊢ (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs

pp: case succ
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs

Tactic:
· rfl

Goal state after:
case succ
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: ι : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : Basis ι A B
z : B
i : ι
⊢ replicateCol (Fin 1) (traceMatrix A ⇑b *ᵥ b.equivFun z) i 0 = (trace A B) (z * b i)

Tactic:
replicateCol_mulVec,

Goal state after:
ι : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : Basis ι A B
z : B
i : ι
⊢ (traceMatrix A ⇑b * replicateCol (Fin 1) (b.equivFun z)) i 0 = (trace A B) (z * b i)
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
inst✝ : SMulCommClass G K L
⊢ fixingSubgroup G ↑⊥ = ⊤

Tactic:
by
  simp [Subgroup.ext_iff, mem_fixingSubgroup_iff, IntermediateField.mem_bot]

Goal state after:
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Fintype.card ↥G
⊢ ∑ x, ↑↑x ^ k = 0

Tactic:
rw [← Nat.card_eq_fintype_card] at k_lt_card_G
  nontriviality K
  have := NoZeroDivisors.to_isDomain K
  rcases (exists_pow_ne_one_of_isCyclic k_pos k_lt_card_G) with ⟨a, ha⟩
  rw [Finset.sum_eq_multiset_sum]
  have h_multiset_map :
    Finset.univ.val.map (fun x : G => ((x : Kˣ) : K) ^ k) =
      Finset.univ.val.map (fun x : G => ((x : Kˣ) : K) ^ k * ((a : Kˣ) : K) ^ k) := by
    simp_rw [← mul_pow]
    have as_comp :
      (fun x : ↥G => (((x : Kˣ) : K) * ((a : Kˣ) : K)) ^ k)
        = (fun x : ↥G => ((x : Kˣ) : K) ^ k) ∘ fun x : ↥G => x * a := by
      funext x
      simp only [Function.comp_apply, Subgroup.coe_mul, Units.val_mul]
    rw [as_comp, ← Multiset.map_map]
    congr
    rw [eq_comm]
    exact Multiset.map_univ_val_equiv (Equiv.mulRight a)
  have h_multiset_map_sum : (Multiset.map (fun x : G => ((x : Kˣ) : K) ^ k) Finset.univ.val).sum =
    (Multiset.map (fun x : G => ((x : Kˣ) : K) ^ k * ((a : Kˣ) : K) ^ k) Finset.univ.val).sum := by
    rw [h_multiset_map]
  rw [Multiset.sum_map_mul_right] at h_multiset_map_sum
  have hzero : (((a : Kˣ) : K) ^ k - 1 : K)
                  * (Multiset.map (fun i : G => (i.val : K) ^ k) Finset.univ.val).sum = 0 := by
    rw [sub_mul, mul_comm, ← h_multiset_map_sum, one_mul, sub_self]
  rw [mul_eq_zero] at hzero
  refine hzero.resolve_left fun h => ha ?_
  ext
  rw [← sub_eq_zero]
  simp_rw [SubmonoidClass.coe_pow, Units.val_pow_eq_pow_val, OneMemClass.coe_one, Units.val_one, h]

Goal state after:
Module: Mathlib.Data.Int.Associated

Goal state before:
pp: case mp.inl
a : ℤ
⊢ Associated a a

pp: case mp.inr
b : ℤ
⊢ Associated (-b) b

Tactic:
· rfl

Goal state after:
case mp.inr
b : ℤ
⊢ Associated (-b) b
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
inst✝¹⁹ : Group G
A : Type u_5
B : Type u_6
C : Type u_7
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : IsDomain C
inst✝¹⁴ : Algebra A B
inst✝¹³ : Algebra A C
inst✝¹² : Algebra B C
inst✝¹¹ : FaithfulSMul A B
inst✝¹⁰ : FaithfulSMul B C
inst✝⁹ : IsScalarTower A B C
inst✝⁸ : Finite G
N : Subgroup G
inst✝⁷ : N.Normal
inst✝⁶ : MulSemiringAction G C
hG : IsGaloisGroup G A C
inst✝⁵ : MulSemiringAction G B
inst✝⁴ : MulSemiringAction (G ⧸ N) B
inst✝³ : SMulCommClass (G ⧸ N) A B
inst✝² : SMulDistribClass G B C
inst✝¹ : IsScalarTower G (G ⧸ N) B
inst✝ : IsGaloisGroup (↥N) B C
g₁✝ g₂✝ : G ⧸ N
g₁ g₂ : G
h : ∀ (a : B), Quotient.mk'' g₁ • a = Quotient.mk'' g₂ • a
⊢ Quotient.mk'' g₁ = Quotient.mk'' g₂

Tactic:
by
    have : FaithfulSMul A C := FaithfulSMul.trans A B C
    have h' : ∀ g : G, (∀ x : B, g • x = x) → g ∈ N := by
      simp [← fixingSubgroup_range_algebraMap G A B C N, mem_fixingSubgroup_iff, ← algebraMap.smul',
        (FaithfulSMul.algebraMap_injective B C).eq_iff]
    have {g : G} : Quotient.mk'' g = QuotientGroup.mk' N g := rfl
    simp_rw [← inv_smul_eq_iff, this, ← map_inv, smul_smul, ← map_mul,
      QuotientGroup.mk'_apply, MulAction.coe_quotient_smul] at h
    have := h' _ h
    rwa [QuotientGroup.eq, ← Subgroup.inv_mem_iff, mul_inv_rev, inv_inv]

Goal state after:
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x ↦ ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ : φ = 1
⊢ ↑q - ↑1 = -1

pp: case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x ↦ ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ : φ = 1
⊢ 1 ≤ q

Tactic:
cast_card_eq_zero,

Goal state after:
case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x ↦ ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ : φ = 1
⊢ 0 - ↑1 = -1

case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x ↦ ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ : φ = 1
⊢ 1 ≤ q
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case intro
A : Type u_1
B : Type u_2
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
G : Type u_3
inst✝¹⁵ : Group G
inst✝¹⁴ : Finite G
inst✝¹³ : MulSemiringAction G B
inst✝¹² : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹¹ : Q.IsPrime
inst✝¹⁰ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra (A ⧸ P) K
inst✝⁶ : Algebra (B ⧸ Q) L
inst✝⁵ : Algebra (A ⧸ P) L
inst✝⁴ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝³ : Algebra K L
inst✝² : IsScalarTower (A ⧸ P) K L
inst✝¹ : Algebra.IsInvariant A B G
inst✝ : Module.IsTorsionFree (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((Ideal.Quotient.stabilizerHom Q P G) g) ((Ideal.Quotient.mk Q) b₀) = (Ideal.Quotient.mk Q) b₀
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb : ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a * b₀ else 0)
M : A[X]
key₀ :
  ∀ (g : G),
    map (algebraMap B (B ⧸ Q)) (X - C (g • b)) = if g • Q = Q then X - C ((algebraMap B (B ⧸ Q)) (a * b₀)) else X
key :
  f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) a)) * f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) =
    (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) a) * (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)
⊢ f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) = (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)

Tactic:
obtain ⟨a, rfl⟩ := Algebra.IsInvariant.isInvariant (A := A) a ha1

Goal state after:
case intro
A : Type u_1
B : Type u_2
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
G : Type u_3
inst✝¹⁵ : Group G
inst✝¹⁴ : Finite G
inst✝¹³ : MulSemiringAction G B
inst✝¹² : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹¹ : Q.IsPrime
inst✝¹⁰ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra (A ⧸ P) K
inst✝⁶ : Algebra (B ⧸ Q) L
inst✝⁵ : Algebra (A ⧸ P) L
inst✝⁴ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝³ : Algebra K L
inst✝² : IsScalarTower (A ⧸ P) K L
inst✝¹ : Algebra.IsInvariant A B G
inst✝ : Module.IsTorsionFree (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((Ideal.Quotient.stabilizerHom Q P G) g) ((Ideal.Quotient.mk Q) b₀) = (Ideal.Quotient.mk Q) b₀
b : B
M : A[X]
a : A
ha1 : ∀ (g : G), g • (algebraMap A B) a = (algebraMap A B) a
ha2 : (algebraMap A B) a ∉ Q
hb :
  ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then (algebraMap A B) a * b₀ else 0)
key₀ :
  ∀ (g : G),
    map (algebraMap B (B ⧸ Q)) (X - C (g • b)) =
      if g • Q = Q then X - C ((algebraMap B (B ⧸ Q)) ((algebraMap A B) a * b₀)) else X
key :
  f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) ((algebraMap A B) a))) *
      f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) =
    (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) ((algebraMap A B) a)) *
      (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)
⊢ f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) = (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹⁷ : Group G
inst✝¹⁶ : Group G'
A : Type u_5
B : Type u_6
C : Type u_7
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : CommRing C
inst✝¹² : IsDomain C
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Algebra A C
inst✝⁹ : Algebra B C
inst✝⁸ : FaithfulSMul A B
inst✝⁷ : FaithfulSMul B C
inst✝⁶ : IsScalarTower A B C
inst✝⁵ : Finite G
inst✝⁴ : Finite G'
inst✝³ : MulSemiringAction G C
inst✝² : IsGaloisGroup G A C
inst✝¹ : MulSemiringAction G' B
inst✝ : IsGaloisGroup G' A B
g : G
x : B
⊢ (algebraMap B C) ((restrictHom G G' A B C) g • x) = g • (algebraMap B C) x

Tactic:
have : IsDomain B := IsDomain.of_faithfulSMul B C
  have : IsDomain A := IsDomain.of_faithfulSMul A B
  have : FaithfulSMul A C := FaithfulSMul.trans A B C
  let : MulSemiringAction G (FractionRing C) :=
    IsFractionRing.mulSemiringAction G C (FractionRing C)
  let : MulSemiringAction G' (FractionRing B) :=
    IsFractionRing.mulSemiringAction G' B (FractionRing B)
  apply FaithfulSMul.algebraMap_injective C (FractionRing C)
  rw [← IsScalarTower.algebraMap_apply,
    IsScalarTower.algebraMap_apply B (FractionRing B) (FractionRing C)]
  simp only [restrictHom, MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_comp, MonoidHom.coe_coe,
    QuotientGroup.coe_mk', Function.comp_apply]
  rw [algebraMap.smul', algebraMap_quotientMulEquiv_smul, ← IsScalarTower.algebraMap_apply,
    algebraMap.smul', ← IsScalarTower.algebraMap_apply]

Goal state after:
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
⊢ ∃ a b, a ^ 2 + b ^ 2 = x

Tactic:
rcases hp.1.eq_two_or_odd with rfl | hp_odd

Goal state after:
case inl
hp : Fact (Nat.Prime 2)
x : ZMod 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x

case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case inl.«1»
hp : Fact (Nat.Prime 2)
⊢ ∃ a b, a ^ 2 + b ^ 2 = (fun i ↦ i) ⟨1, ⋯⟩

Tactic:
use 0, 1

Goal state after:
case h
hp : Fact (Nat.Prime 2)
⊢ 0 ^ 2 + 1 ^ 2 = (fun i ↦ i) ⟨1, ⋯⟩
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
n : ZMod p
x✝ : n ∈ ⊤
this : ↑n.val • 1 ∈ ⊥
⊢ n ∈ ⊥

Tactic:
rwa [natCast_zsmul, Nat.smul_one_eq_cast, ZMod.natCast_zmod_val] at this

Goal state after:
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
k : Type u_3
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u_4
inst✝¹⁰ : Finite G
inst✝⁹ : Group G
inst✝⁸ : MulSemiringAction G B
inst✝⁷ : Algebra.IsInvariant A B G
P✝ : Ideal A
Q : Ideal B
inst✝⁶ : Q.LiesOver P✝
inst✝⁵ : CommRing k
inst✝⁴ : Algebra (A ⧸ P✝) k
inst✝³ : Algebra (B ⧸ Q) k
inst✝² : IsScalarTower (A ⧸ P✝) (B ⧸ Q) k
inst✝¹ : IsDomain k
inst✝ : FaithfulSMul (B ⧸ Q) k
σ : k →ₐ[A ⧸ P✝] k
f : B ⧸ Q →ₐ[A ⧸ P✝] k := IsScalarTower.toAlgHom (A ⧸ P✝) (B ⧸ Q) k
hf : Function.Injective ⇑f
x : B
val✝ : Fintype G
algInst✝¹ : Algebra A k := ((algebraMap (A ⧸ P✝) k).comp (algebraMap A (A ⧸ P✝))).toAlgebra
algInst✝ : Algebra B k := ((algebraMap (B ⧸ Q) k).comp (algebraMap B (B ⧸ Q))).toAlgebra
scalarTowerInst✝¹ : IsScalarTower A (A ⧸ P✝) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A k))
scalarTowerInst✝ : IsScalarTower B (B ⧸ Q) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap B k))
this✝ : IsScalarTower A (B ⧸ Q) k
this : IsScalarTower A B k
P : Polynomial A
hp : (Polynomial.mapRingHom (algebraMap A B)) P = MulSemiringAction.charpoly G x
⊢ Polynomial.eval₂ (algebraMap A B) x P = 0

Tactic:
← Polynomial.eval_map,

Goal state after:
A : Type u_1
B : Type u_2
k : Type u_3
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u_4
inst✝¹⁰ : Finite G
inst✝⁹ : Group G
inst✝⁸ : MulSemiringAction G B
inst✝⁷ : Algebra.IsInvariant A B G
P✝ : Ideal A
Q : Ideal B
inst✝⁶ : Q.LiesOver P✝
inst✝⁵ : CommRing k
inst✝⁴ : Algebra (A ⧸ P✝) k
inst✝³ : Algebra (B ⧸ Q) k
inst✝² : IsScalarTower (A ⧸ P✝) (B ⧸ Q) k
inst✝¹ : IsDomain k
inst✝ : FaithfulSMul (B ⧸ Q) k
σ : k →ₐ[A ⧸ P✝] k
f : B ⧸ Q →ₐ[A ⧸ P✝] k := IsScalarTower.toAlgHom (A ⧸ P✝) (B ⧸ Q) k
hf : Function.Injective ⇑f
x : B
val✝ : Fintype G
algInst✝¹ : Algebra A k := ((algebraMap (A ⧸ P✝) k).comp (algebraMap A (A ⧸ P✝))).toAlgebra
algInst✝ : Algebra B k := ((algebraMap (B ⧸ Q) k).comp (algebraMap B (B ⧸ Q))).toAlgebra
scalarTowerInst✝¹ : IsScalarTower A (A ⧸ P✝) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A k))
scalarTowerInst✝ : IsScalarTower B (B ⧸ Q) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap B k))
this✝ : IsScalarTower A (B ⧸ Q) k
this : IsScalarTower A B k
P : Polynomial A
hp : (Polynomial.mapRingHom (algebraMap A B)) P = MulSemiringAction.charpoly G x
⊢ Polynomial.eval x (Polynomial.map (algebraMap A B) P) = 0
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝³ : CommRing S₁
inst✝² : Algebra R S₁
P : Ideal S
E : Type u_2
inst✝¹ : EquivLike E S S₁
inst✝ : AlgEquivClass E R S S₁
e : E
⊢ p.inertiaDeg' (map e P) = p.inertiaDeg' P

Tactic:
rw [show P.map e = _ from map_comap_of_equiv (RingEquivClass.toRingEquiv e : S ≃+* S₁)]
  exact p.inertiaDeg'_comap_eq (AlgEquivClass.toAlgEquiv e).symm P

Goal state after:
Module: Mathlib.RingTheory.Finiteness.NilpotentKer

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this✝ : Module.Finite R (S ⧸ I)
this : ∀ (i : ℕ), Module.Finite R (S ⧸ I ^ i)
⊢ Module.Finite R S

Tactic:
obtain ⟨n, hn : _ = ⊥⟩ := hf₃.isNilpotent_iff_le_nilradical.mpr hf₂

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this✝ : Module.Finite R (S ⧸ I)
this : ∀ (i : ℕ), Module.Finite R (S ⧸ I ^ i)
n : ℕ
hn : I ^ n = ⊥
⊢ Module.Finite R S