mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
inst✝⁶ : CharZero F
K' : Type u_3
inst✝⁵ : Field K'
inst✝⁴ : Differential K'
inst✝³ : Algebra F K'
inst✝² : DifferentialAlgebra F K'
inst✝¹ : Algebra.IsAlgebraic F K'
inst : IsLiouville F K
e : K ≃ₐ[F] K'
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K'
v : K'
h : e.symm ↑a = e.symm (∑ x, ↑(c x) * logDeriv (u x) + v′)
⊢ ↑a = ∑ x, ↑(c x) * logDeriv ((⇑e.symm ∘ u) x) + (e.symm v)′

Tactic:
simpa using

Goal state after:
F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
inst✝⁶ : CharZero F
K' : Type u_3
inst✝⁵ : Field K'
inst✝⁴ : Differential K'
inst✝³ : Algebra F K'
inst✝² : DifferentialAlgebra F K'
inst✝¹ : Algebra.IsAlgebraic F K'
inst : IsLiouville F K
e : K ≃ₐ[F] K'
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K'
v : K'
h : e.symm ↑a = e.symm (∑ x, ↑(c x) * logDeriv (u x) + v′)
⊢ ↑a = ∑ x, ↑(c x) * ((e.symm (u x))′ / e.symm (u x)) + (e.symm v)′
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: case e'_4
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this✝ : Finite K
this : Fintype K
x : L
hx :
  Ideal.span {X ^ finrank K L - 1} =
    (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
        ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x)).ker
e_1✝ : Fin (X ^ finrank K L - C 1).natDegree = Fin (AdjoinRoot.powerBasis ⋯).dim
i : Fin (X ^ finrank K L - C 1).natDegree
⊢ (⇑(frobeniusAlgEquivOfAlgebraic K L))^[↑(Fin.cast ⋯ i)] x =
    (⇑(AEval'.of (frobeniusAlgHom K L).toLinearMap).symm ∘
        ⇑(↑K
            (liftQ (Ideal.span {X ^ finrank K L - 1})
              (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
                ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x))
              ⋯)))
      (AdjoinRoot.root (X ^ finrank K L - C 1) ^ ↑i)

Tactic:
LinearMap.coe_restrictScalars

Goal state after:
case e'_4
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this✝ : Finite K
this : Fintype K
x : L
hx :
  Ideal.span {X ^ finrank K L - 1} =
    (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
        ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x)).ker
e_1✝ : Fin (X ^ finrank K L - C 1).natDegree = Fin (AdjoinRoot.powerBasis ⋯).dim
i : Fin (X ^ finrank K L - C 1).natDegree
⊢ (⇑(frobeniusAlgEquivOfAlgebraic K L))^[↑(Fin.cast ⋯ i)] x =
    (⇑(AEval'.of (frobeniusAlgHom K L).toLinearMap).symm ∘
        ⇑(liftQ (Ideal.span {X ^ finrank K L - 1})
            (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
              ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x))
            ⋯))
      (AdjoinRoot.root (X ^ finrank K L - C 1) ^ ↑i)
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ ∑ x, ↑a = ∑ x, (∑ x_1, ↑(c x_1) * logDeriv (x (u x_1)) + (x v)′)

Tactic:
· rcongr e
        apply_fun e at h
        simp only [AlgEquiv.commutes, map_add, map_sum, map_mul] at h
        convert! h using 2
        · rcongr x
          simp [logDeriv, algEquiv_deriv']
        · rw [algEquiv_deriv']

Goal state after:
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case inl
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
eq : ℵ₀ = Module.rank F E
this : Finite ↑(Iio i)
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E

Tactic:
have : FiniteDimensional F (adjoin F s) :=
          finiteDimensional_adjoin fun x _ ↦ (IsAlgebraic.isAlgebraic x).isIntegral

Goal state after:
case inl
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝² : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝¹ : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
eq : ℵ₀ = Module.rank F E
this✝ : Finite ↑(Iio i)
this : FiniteDimensional F ↥(adjoin F s)
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)

Tactic:
by
  rw [image_eq_range, leastExt, wellFounded_lt.fix_eq]
  exact ⟨wellFounded_lt.min_mem _ _, fun _ ↦ (wellFounded_lt.min_le ·)⟩

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
n : ℕ
h : x ^ p ^ n = 0
⊢ i x ^ p ^ n = 0

Tactic:
simpa using

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : K
n : ℕ
h : x ^ p ^ n = 0
⊢ i x ^ p ^ n = 0
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst✝¹ : IsPRadical i p
inst✝ : IsPRadical f p
x : K
h : i x ∈ RingHom.ker f
⊢ x ∈ pNilradical K p

Tactic:
simpa using

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst✝¹ : IsPRadical i p
inst✝ : IsPRadical f p
x : K
h : i x ∈ RingHom.ker f
⊢ x ∈ pNilradical K p
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: case h
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
H : Set Gal(K/k)
L : FiniteGaloisIntermediateField k K
le : ↑L.fixingSubgroup ⊆ H
⊢ (fun a ↦ (mulEquivToLimit k K) a) '' ↑L.fixingSubgroup ⊆ (fun a ↦ (mulEquivToLimit k K).toEquiv a) '' H ∧
    True ∧ 1 ∈ (fun a ↦ (mulEquivToLimit k K) a) '' ↑L.fixingSubgroup

Tactic:
simpa using

Goal state after:
case h
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
H : Set Gal(K/k)
L : FiniteGaloisIntermediateField k K
le : ↑L.fixingSubgroup ⊆ H
⊢ ↑L.fixingSubgroup ⊆ (fun a ↦ (mulEquivToLimit k K) a) ⁻¹' (fun a ↦ (mulEquivToLimit k K) a) '' H
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
n : ℕ
ih : mk K p x ^ n = mk K p (x.1, x.2 ^ n)
⊢ (⇑(frobenius K p))^[(x.1, x.2 ^ n * x.2).1 + 0]
      ((x.1, x.2 ^ n).1 + x.1,
          (⇑(frobenius K p))^[x.1] (x.1, x.2 ^ n).2 * (⇑(frobenius K p))^[(x.1, x.2 ^ n).1] x.2).2 =
    (⇑(frobenius K
            p))^[((x.1, x.2 ^ n).1 + x.1,
              (⇑(frobenius K p))^[x.1] (x.1, x.2 ^ n).2 * (⇑(frobenius K p))^[(x.1, x.2 ^ n).1] x.2).1 +
          0]
      (x.1, x.2 ^ n * x.2).2

Tactic:
simp_rw [iterate_frobenius, add_zero, mul_pow, ← pow_mul,
      ← pow_add, mul_assoc, ← pow_add]

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hn : Odd n
r : R
hr : (X ^ n - C x).IsRoot r
⊢ r ^ n - x = 0

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hn : Odd n
r : R
hr : (X ^ n - C x).IsRoot r
⊢ r ^ n - x = 0
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hk : Odd ↑n
⊢ ∃ r, x = r ^ ↑n

Tactic:
simpa using

Goal state after:
case inl
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hk : Odd ↑n
⊢ ∃ r, x = r ^ n
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hk : Odd ↑n
⊢ Odd n

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hk : Odd ↑n
⊢ Odd n
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hk : Odd (-↑n)
⊢ Odd ?m.72

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hk : Odd (-↑n)
⊢ Odd ?m.72
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hk : Odd (-↑n)
r : R
hr : x = r ^ n
⊢ x = r⁻¹ ^ (-↑n)

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hk : Odd (-↑n)
r : R
hr : x = r ^ n
⊢ x = r ^ n
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y z : ℕ
H : (⇑(frobenius K p))^[(0, ↑y).1 + z] (0, ↑x).2 = (⇑(frobenius K p))^[(0, ↑x).1 + z] (0, ↑y).2
⊢ ↑x = ↑y

Tactic:
simpa using

Goal state after:
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y z : ℕ
H : (⇑(frobenius K p))^[(0, ↑y).1 + z] (0, ↑x).2 = (⇑(frobenius K p))^[(0, ↑x).1 + z] (0, ↑y).2
⊢ ↑x = ↑y
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝¹ : PerfectClosure K p
x : ℕ × K
x✝ : IsNilpotent (mk K p x)
n m : ℕ
h : (iterateFrobenius K p m) (x.2 ^ p ^ n) = 0
⊢ (iterateFrobenius K p (n + m)) x.2 = 0

Tactic:
simpa using

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝¹ : PerfectClosure K p
x : ℕ × K
x✝ : IsNilpotent (mk K p x)
n m : ℕ
h : (iterateFrobenius K p m) (x.2 ^ p ^ n) = 0
⊢ (x.2 ^ p ^ n) ^ p ^ m = 0
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : ↑n ≠ 0
⊢ ∃ r, x = r ^ ↑n

Tactic:
simpa using

Goal state after:
case inl
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : ↑n ≠ 0
⊢ ∃ r, x = r ^ n
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : ↑n ≠ 0
⊢ n ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : ↑n ≠ 0
⊢ ¬n = 0
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : -↑n ≠ 0
⊢ ?m.78 ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : -↑n ≠ 0
⊢ ¬?m.78 = 0
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : -↑n ≠ 0
r : R
hr : x = r ^ n
⊢ x = r⁻¹ ^ (-↑n)

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : -↑n ≠ 0
r : R
hr : x = r ^ n
⊢ x = r ^ n
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
⊢ ∃ x, ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
⊢ ∃ x, ∀ i ∈ s, H i = H j → ¬↑(g i) = ↑x
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x
y z : G
hz : z ∈ y • ↑(H j)
⊢ ∃ i ∈ s, x * (y⁻¹ * z) ∈ g i • ↑(H i)

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x
y z : G
hz : z ∈ y • ↑(H j)
⊢ ∃ i ∈ s, x * (y⁻¹ * z) ∈ g i • ↑(H i)
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x
y z : G
hz : z ∈ y • ↑(H j)
i : ι
hi : i ∈ s
hmem : ↑(g i) = ↑(x * (y⁻¹ * z))
⊢ z ∈ (y * x⁻¹ * g i) • ↑(H i)

Tactic:
simpa using

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x
y z : G
hz : z ∈ y • ↑(H j)
i : ι
hi : i ∈ s
hmem : ↑(g i) = ↑(x * (y⁻¹ * z))
⊢ (g i)⁻¹ * (x * (y⁻¹ * z)) ∈ H i
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
j : ι
hcovers : (⋃ x ∈ {x ∈ s | H x = H j}, g x • ↑(H x)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • ↑(H x) = Set.univ
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun x_1 ↦
    match x_1 with
    | (k₁, some k₂) => g ↑k₂ * x⁻¹ * g ↑k₁
    | (k₁, none) => g ↑k₁
K : κ → Subgroup G := fun k ↦ H ↑k.1
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
hK : ∀ (k : κ), K k ≠ H j
y : G
hy✝ : y ∈ ⋃ x ∈ {x ∈ s | H x = H j}, g x • ↑(H x)
k : ι
hk : k ∈ {x ∈ s | H x = H j}
hy : y ∈ g k • ↑(H k)
⊢ ?m.560 ∧ H k = H j

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
j : ι
hcovers : (⋃ x ∈ {x ∈ s | H x = H j}, g x • ↑(H x)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • ↑(H x) = Set.univ
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun x_1 ↦
    match x_1 with
    | (k₁, some k₂) => g ↑k₂ * x⁻¹ * g ↑k₁
    | (k₁, none) => g ↑k₁
K : κ → Subgroup G := fun k ↦ H ↑k.1
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
hK : ∀ (k : κ), K k ≠ H j
y : G
hy✝ : y ∈ ⋃ x ∈ {x ∈ s | H x = H j}, g x • ↑(H x)
k : ι
hk : k ∈ {x ∈ s | H x = H j}
hy : y ∈ g k • ↑(H k)
⊢ ?m.560 ∧ H k = H j
Module: Mathlib.FieldTheory.Laurent

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
r : R
inst✝ : IsDomain R
x✝¹ x✝ : R⟮X⟯
h : (laurent r) x✝¹ = (laurent r) x✝
⊢ x✝¹ = x✝

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : CommRing R
r : R
inst✝ : IsDomain R
x✝¹ x✝ : R⟮X⟯
h : (laurent r) x✝¹ = (laurent r) x✝
⊢ x✝¹ = x✝
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: case h
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : ∃ x, ¬x * a = a * x
ha₀ : a ≠ 0
⊢ a * ha.choose - ha.choose * a ≠ 0

Tactic:
simpa using

Goal state after:
case h
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : ∃ x, ¬x * a = a * x
ha₀ : a ≠ 0
⊢ ¬a * ha.choose = ha.choose * a
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: F : Type u
E : Type v
inst✝⁵ : CommRing F
inst✝⁴ : Nontrivial F
inst✝³ : CommRing E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
K : Subalgebra F E := adjoin F (range x)
this✝ : Algebra.IsAlgebraic (↥K) E
this : Infinite ↥K
⊢ #E ≤ #↥K

Tactic:
simpa using

Goal state after:
F : Type u
E : Type v
inst✝⁵ : CommRing F
inst✝⁴ : Nontrivial F
inst✝³ : CommRing E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
K : Subalgebra F E := adjoin F (range x)
this✝ : Algebra.IsAlgebraic (↥K) E
this : Infinite ↥K
⊢ #E ≤ #↥K
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Nonempty ι
⊢ Module.rank F E = #E

Tactic:
simpa using

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Nonempty ι
⊢ Module.rank F E = #E
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
hn : 0 < n
e : α ^ n = a
K : Type u_1 := FractionRing R
i : R →+* K := algebraMap R K
h : Function.Injective ⇑(algebraMap R K)
⊢ Polynomial.map i (X ^ n - C a) = Polynomial.map i (∏ i ∈ Finset.range n, (X - C (ζ ^ i * α)))

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
hn : 0 < n
e : α ^ n = a
K : Type u_1 := FractionRing R
i : R →+* K := algebraMap R K
h : Function.Injective ⇑(algebraMap R K)
⊢ X ^ n - C (i a) = ∏ x ∈ Finset.range n, (X - C (i ζ) ^ x * C (i α))
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
n m : ℕ
a : K
hm : Irreducible (X ^ m - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ m - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
hm' : m ≠ 0
⊢ Irreducible (X ^ (n * m) - C a)

Tactic:
simpa using

Goal state after:
K : Type u
inst✝ : Field K
n m : ℕ
a : K
hm : Irreducible (X ^ m - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ m - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
hm' : m ≠ 0
⊢ Irreducible ((X ^ n) ^ m - C a)
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
n m : ℕ
a : K
hm : Irreducible (X ^ m - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ m - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
hm' : m ≠ 0
⊢ ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ m - C a → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) (X ^ n) - C (AdjoinSimple.gen K x))

Tactic:
simpa using

Goal state after:
K : Type u
inst✝ : Field K
n m : ℕ
a : K
hm : Irreducible (X ^ m - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ m - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
hm' : m ≠ 0
⊢ ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ m - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case one
K : Type u
inst✝ : Field K
hn : Odd 1
a : K
ha : ∀ (p : ℕ), Nat.Prime p → p ∣ 1 → ∀ (b : K), b ^ p ≠ a
⊢ Irreducible (X ^ 1 - C a)

Tactic:
simpa using

Goal state after:
case one
K : Type u
inst✝ : Field K
hn : Odd 1
a : K
ha : ∀ (p : ℕ), Nat.Prime p → p ∣ 1 → ∀ (b : K), b ^ p ≠ a
⊢ Irreducible (X - C a)