mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝² : μ.HaveLebesgueDecomposition ν
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
this : μ.withDensity (μ.rnDeriv ν)⁻¹ = μ.withDensity (ν.rnDeriv μ)
⊢ (μ.rnDeriv ν)⁻¹ =ᵐ[μ] ν.rnDeriv μ

Tactic:
calc (μ.rnDeriv ν)⁻¹ =ᵐ[μ] (μ.withDensity (μ.rnDeriv ν)⁻¹).rnDeriv μ :=
          (rnDeriv_withDensity _ (measurable_rnDeriv _ _).inv).symm
    _ = (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ := by rw [this]
    _ =ᵐ[μ] ν.rnDeriv μ := rnDeriv_withDensity _ (measurable_rnDeriv _ _)

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
U : Set (X × X)
U_uni : ∃ t ∈ 𝓤 Y, Prod.map φ φ ⁻¹' t ⊆ U
⊢ coverEntropyEntourage S F U ≤ coverEntropy T (φ '' F)

Tactic:
obtain ⟨V, V_uni, V_sub⟩ := U_uni

Goal state after:
case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
U : Set (X × X)
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
V_sub : Prod.map φ φ ⁻¹' V ⊆ U
⊢ coverEntropyEntourage S F U ≤ coverEntropy T (φ '' F)
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
U : Set (X × X)
U_uni : ∃ t ∈ 𝓤 Y, Prod.map φ φ ⁻¹' t ⊆ U
⊢ coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)

Tactic:
obtain ⟨V, V_uni, V_sub⟩ := U_uni

Goal state after:
case a
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
U : Set (X × X)
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
V_sub : Prod.map φ φ ⁻¹' V ⊆ U
⊢ coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝ : UniformSpace X
T : X → X
F : ι → Set X
s : Finset ι
this :
  { toFun := coverEntropy T, map_sup' := ⋯, map_bot' := ⋯ } (⋃ x ∈ s, F x) =
    ⨆ a ∈ s, (⇑{ toFun := coverEntropy T, map_sup' := ⋯, map_bot' := ⋯ } ∘ F) a
⊢ coverEntropy T (⋃ i ∈ s, F i) = ⨆ i ∈ s, coverEntropy T (F i)

Tactic:
SupBotHom.coe_mk,

Goal state after:
X : Type u_1
ι : Type u_2
inst✝ : UniformSpace X
T : X → X
F : ι → Set X
s : Finset ι
this :
  { toFun := coverEntropy T, map_sup' := ⋯ } (⋃ x ∈ s, F x) =
    ⨆ a ∈ s, (⇑{ toFun := coverEntropy T, map_sup' := ⋯ } ∘ F) a
⊢ coverEntropy T (⋃ i ∈ s, F i) = ⨆ i ∈ s, coverEntropy T (F i)
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ∈ (X ^ n - C a).rootSet (X ^ n - C a).SplittingField
⊢ (σ * τ) b = (τ * σ) b

Tactic:
mem_rootSet_of_ne hn'',

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : (aeval b) (X ^ n - C a) = 0
⊢ (σ * τ) b = (τ * σ) b
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
f : M ≃[L] N
n : ℕ
r : L.Relations n
x : Fin n → N
⊢ RelMap r (f.symm.toFun ∘ x) ↔ RelMap r x

Tactic:
by
      simp only [Equiv.toFun_as_coe]
      refine (f.map_rel' r (f.toEquiv.symm ∘ x)).symm.trans ?_
      rw [← Function.comp_assoc, Equiv.toFun_as_coe, Equiv.self_comp_symm, Function.id_comp]

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_1
L : Language
α : Type u'
i : ℕ
⊢ max ℵ₀ #((α ⊕ Fin i) ⊕ (i : ℕ) × L.Functions i) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i)

Tactic:
refine max_le (le_max_left _ _) ?_

Goal state after:
case refine_1
L : Language
α : Type u'
i : ℕ
⊢ #((α ⊕ Fin i) ⊕ (i : ℕ) × L.Functions i) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i)
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L.Formula (↑A ⊕ α)
A0 : Finset M := Finset.image Subtype.val (BoundedFormula.freeVarFinset φ).toLeft
⊢ ↑A0 ⊆ A

Tactic:
simp [A0]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.e__v.inr.refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
x : Fin (n✝ + 1)
⊢ ∀ (i : Fin n✝),
    Sum.elim v (fun x ↦ snoc default a (castAdd 0 x))
        (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) (fun x ↦ Sum.map Sum.inr id (finSumFinEquiv.symm x))
          (Sum.inr i.castSucc)) =
      Sum.elim (fun x ↦ v (Sum.inl x)) (snoc (fun x ↦ v (Sum.inr x)) a) (Sum.inr i.castSucc)

Tactic:
simp only [castSucc, Sum.elim_inr,
            finSumFinEquiv_symm_apply_castAdd, Sum.map_inl, Sum.elim_inl]
          rw [← castSucc]
          simp

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable L[[α]].Symbols

Tactic:
simp only [← mk_le_aleph0_iff]

Goal state after:
L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ #L[[α]].Symbols ≤ ℵ₀
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
φ : L.Sentence
⊢ M ⊨ φ ↔ N ⊨ φ

Tactic:
rw [Sentence.Realize, Sentence.Realize, ← realize_formula g,
    Unique.eq_default (g ∘ default)]

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
f : M → M
⊢ TermDefinable₁ L f ↔ ∃ φ, f = (fun v ↦ Term.realize v φ) ∘ Function.const Unit

Tactic:
refine exists_congr fun φ ↦ ?_
  rw [funext_iff, funext_iff, (Equiv.funUnique Unit M).forall_congr']
  simp only [Equiv.funUnique_symm_apply, uniqueElim_const, Function.comp_apply]
  congr!

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case h2
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ Cardinal.lift.{0, 0} Language.ring.card ≤ Cardinal.lift.{0, 0} (Order.succ ℵ₀)

Tactic:
simp only [card_ring, lift_id']
    exact le_trans (le_of_lt (lt_aleph0_of_finite _)) (Order.le_succ _)

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
φ : L.Formula α
⊢ T ⊨ᵇ φ ↔ (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ

Tactic:
by
  refine ⟨fun h => models_sentence_iff.2 (fun M => ?_),
    fun h => models_formula_iff.2 (fun M v => ?_)⟩
  · let := (L.lhomWithConstants α).reduct M
    rw [Formula.realize_equivSentence]
    have : M ⊨ T := (LHom.onTheory_model _ _).1 M.is_model -- why isn't M.is_model inferInstance?
    let M' := Theory.ModelType.of T M
    exact h M' (fun a => (L.con a : M)) _
  · let : (constantsOn α).Structure M := constantsOn.structure v
    have : M ⊨ (L.lhomWithConstants α).onTheory T := (LHom.onTheory_model _ _).2 inferInstance
    exact (Formula.realize_equivSentence _ _).1 (h.realize_sentence M)

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)

Tactic:
rcases finite_or_infinite X with _ | _
  · have := lift_mk_le_lift_mk_of_surjective (oreDiv_one_surjective_of_finite_right S X)
    rw [lift_umax.{v, u}, lift_id'] at this
    exact le_max_of_le_right this
  rcases finite_or_infinite S with _ | _
  · have := lift_mk_le_lift_mk_of_surjective (oreDiv_one_surjective_of_finite_left S X)
    rw [lift_umax.{v, u}, lift_id'] at this
    exact le_max_of_le_right this
  convert! ←
    mk_le_of_surjective (show Surjective fun x : X × S ↦ x.1 /ₒ x.2 from Quotient.mk''_surjective)
  rw [mk_prod, mul_comm]
  refine mul_eq_max ?_ ?_ <;> simp

Goal state after:
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: K : Type u_1
ι : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Finite ι
p : ι → MvPolynomial ι K
this : CompatibleRing K := compatibleRingOfRing K
s : Finset (MvPolynomial ι K)
S : Set (ι → K) := zeroLocus K (Ideal.span ↑s)
⊢ Set.MapsTo (fun v i ↦ (eval v) (p i)) S S →
    Set.InjOn (fun v i ↦ (eval v) (p i)) S → Set.SurjOn (fun v i ↦ (eval v) (p i)) S S

Tactic:
exact ax_grothendieck_of_definable S (mvPolynomial_zeroLocus_definable s) p

Goal state after:
Module: Mathlib.FieldTheory.FinTrdeg

Goal state before:
pp: case mpr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : Algebra.trdeg K L < Cardinal.aleph0
⊢ FinTrdeg K L

Tactic:
obtain ⟨s, hs⟩ := exists_isTranscendenceBasis K L

Goal state after:
case mpr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : Algebra.trdeg K L < Cardinal.aleph0
s : Set L
hs : IsTranscendenceBasis K Subtype.val
⊢ FinTrdeg K L
Module: Mathlib.FieldTheory.FinTrdeg

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FinTrdeg K L
⊢ ∃ s, IsTranscendenceBasis K Subtype.val

Tactic:
obtain ⟨s, hs⟩ := exists_isTranscendenceBasis K L

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FinTrdeg K L
s : Set L
hs : IsTranscendenceBasis K Subtype.val
⊢ ∃ s, IsTranscendenceBasis K Subtype.val
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : Finite k
f : k[X]
hi : Irreducible f
n : ℕ
hdvd : f.natDegree ∣ n
a : AdjoinRoot f := AdjoinRoot.root f
this✝² : NeZero f.natDegree
this✝¹ : Fact (Irreducible f)
p : ℕ
hp : CharP k p
this✝ : Fact (Nat.Prime p)
e : AdjoinRoot f ≃ₐ[k] Extension k p f.natDegree := algEquivExtension k p f.natDegree (AdjoinRoot f) ⋯
this : Fintype (Extension k p f.natDegree)
⊢ e a ^ Fintype.card (Extension k p f.natDegree) - e a = 0

pp: k : Type u_1
inst✝¹ : Field k
inst✝ : Finite k
f : k[X]
hi : Irreducible f
n : ℕ
hdvd : f.natDegree ∣ n
a : AdjoinRoot f := ⋯
this✝² : NeZero f.natDegree
this✝¹ : Fact (Irreducible f)
p : ℕ
hp : CharP k p
this✝ : Fact (Nat.Prime p)
e : AdjoinRoot f ≃ₐ[k] Extension k p f.natDegree := ⋯
this : Fintype (Extension k p f.natDegree)
⊢ Fintype (Extension k p f.natDegree)

Tactic:
pow_card (e a),

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : Finite k
f : k[X]
hi : Irreducible f
n : ℕ
hdvd : f.natDegree ∣ n
a : AdjoinRoot f := AdjoinRoot.root f
this✝² : NeZero f.natDegree
this✝¹ : Fact (Irreducible f)
p : ℕ
hp : CharP k p
this✝ : Fact (Nat.Prime p)
e : AdjoinRoot f ≃ₐ[k] Extension k p f.natDegree := algEquivExtension k p f.natDegree (AdjoinRoot f) ⋯
this : Fintype (Extension k p f.natDegree)
⊢ e a - e a = 0
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case refine_2
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 j : (Module.rank F E).ord.ToType
hj : j ∈ Iio (φ i)
⊢ b j ∈ ↑(adjoin F (⇑b ∘ φ '' Iio i))

Tactic:
contrapose hj

Goal state after:
case refine_2
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 j : (Module.rank F E).ord.ToType
hj : b j ∉ ↑(adjoin F (⇑b ∘ φ '' Iio i))
⊢ j ∉ Iio (φ i)
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 : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f : ↑(limit (embFunctor F E) i)
j : ↑(Iio i)
this : Nonempty ↑(Iio i)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp_rw [dif_pos this]

Goal state after:
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 : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f : ↑(limit (embFunctor F E) i)
j : ↑(Iio i)
this : Nonempty ↑(Iio i)
⊢ embFunctor F E ⋯ (Subalgebra.iSupLift (fun x ↦ (filtration ↑x).toSubalgebra) ⋯ ↑f ⋯ (filtration i).toSubalgebra ⋯) =
    ↑f j
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: k✝ : Type u_1
K✝ : Type u_2
inst✝⁵ : Field k✝
inst✝⁴ : Field K✝
inst✝³ : Algebra k✝ K✝
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
⊢ ⟨fun L ↦ (AlgEquiv.restrictNormalHom ↥(unop L).toIntermediateField) 1, ⋯⟩ = 1

Tactic:
by
    simp only [map_one]
    rfl

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ x ∈ ↑∅, g x • ↑H = Set.univ
hind : H.index = s.card
h : s = ∅
⊢ False

Tactic:
Finset.coe_empty,

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ x ∈ ∅, g x • ↑H = Set.univ
hind : H.index = s.card
h : s = ∅
⊢ False
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
hcovers : ⋃ x ∈ ↑∅, g x • ↑(H x) = Set.univ
⊢ False

Tactic:
Finset.coe_empty,

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
hcovers : ⋃ x ∈ ∅, g x • ↑(H x) = Set.univ
⊢ False
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: 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 : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
c_eq : a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c
eq1 : c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1
⊢ a * d - d * a = a

Tactic:
← mul_one a

Goal state after:
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 : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
c_eq : a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c
eq1 : c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1
⊢ a * d - d * a = a * 1
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case prime_mul
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K],
    Odd n → ∀ {a : K}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (X ^ n - C a)
K : Type u
inst✝ : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
⊢ Irreducible (X ^ (n * p) - C a)

Tactic:
apply X_pow_mul_sub_C_irreducible
      (X_pow_sub_C_irreducible_of_prime hp (ha p hp (dvd_mul_right _ _)))

Goal state after:
case prime_mul
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K],
    Odd n → ∀ {a : K}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (X ^ n - C a)
K : Type u
inst✝ : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
⊢ ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ p - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case adjoin_rootSet'
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
⊢ ⊤ ≤ Algebra.adjoin K ((X ^ n - C a).rootSet K[n√a])

Tactic:
← AdjoinRoot.adjoinRoot_eq_top

Goal state after:
case adjoin_rootSet'
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
⊢ K [root (X ^ n - C a)] ≤ Algebra.adjoin K ((X ^ n - C a).rootSet K[n√a])
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case refine_1
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
hσ'✝ : orderOf σ = Nat.card Gal(L/K)
this : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n) v = ζ ^ n • v
σ' : Gal(L/K)
hσ' : σ' ∈ OrderDual.ofDual ⊥
⊢ ⟨σ', hσ'⟩ • v ^ finrank K L = v ^ finrank K L

Tactic:
obtain ⟨n, rfl : σ ^ n = σ'⟩ := mem_powers_iff_mem_zpowers.mpr (hσ σ')

Goal state after:
case refine_1
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
hσ'✝ : orderOf σ = Nat.card Gal(L/K)
this : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n) v = ζ ^ n • v
n : ℕ
hσ' : σ ^ n ∈ OrderDual.ofDual ⊥
⊢ ⟨σ ^ n, hσ'⟩ • v ^ finrank K L = v ^ finrank K L
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case refine_2
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
hσ'✝ : orderOf σ = Nat.card Gal(L/K)
this : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n) v = ζ ^ n • v
σ' : Gal(L/K)
hσ' : σ' ∈ IsGalois.intermediateFieldEquivSubgroup K⟮v⟯
⊢ σ' ∈ ⊤

Tactic:
obtain ⟨n, rfl : σ ^ n = σ'⟩ := mem_powers_iff_mem_zpowers.mpr (hσ σ')

Goal state after:
case refine_2
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
hσ'✝ : orderOf σ = Nat.card Gal(L/K)
this : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n) v = ζ ^ n • v
n : ℕ
hσ' : σ ^ n ∈ IsGalois.intermediateFieldEquivSubgroup K⟮v⟯
⊢ σ ^ n ∈ ⊤
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
i : ι
⊢ ⋃ (_ : i ∈ s), ⋃ (_ : (H i).FiniteIndex), g i • ↑(H i) =
    ⋃ (hx : i ∈ s), ⋃ a, ⋃ (_ : ⟨⟨i, hx⟩, a⟩ ∈ {x | K x = D}), f ⟨⟨i, hx⟩, a⟩ • ↑D

Tactic:
refine Set.iUnion_congr fun hi => ?_

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
i : ι
hi : i ∈ s
⊢ ⋃ (_ : (H i).FiniteIndex), g i • ↑(H i) = ⋃ a, ⋃ (_ : ⟨⟨i, hi⟩, a⟩ ∈ {x | K x = D}), f ⟨⟨i, hi⟩, a⟩ • ↑D
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
⊢ IsPurelyInseparable F ↥F⟮x⟯ ↔ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Tactic:
by
  rw [← le_perfectClosure_iff, adjoin_simple_le_iff, mem_perfectClosure_iff_pow_mem q]

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: case refine_1
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
inst✝¹ : Algebra.IsSeparable F ↥(adjoin F S)
q : ℕ
inst✝ : ExpChar F q
n : ℕ
M : IntermediateField F E := adjoin F ((fun x ↦ x ^ q ^ n) '' S)
this : ExpChar (↥M) q
x : E
hx : x ∈ S
⊢ x ∈ ↑M

Tactic:
have : Algebra.IsSeparable M M⟮x⟯ :=
      (isSeparable_adjoin_simple_iff_isSeparable M E).2 <|
        ((isSeparable_adjoin_iff_isSeparable F E).1 inferInstance x hx).tower_top M

Goal state after:
case refine_1
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
inst✝¹ : Algebra.IsSeparable F ↥(adjoin F S)
q : ℕ
inst✝ : ExpChar F q
n : ℕ
M : IntermediateField F E := adjoin F ((fun x ↦ x ^ q ^ n) '' S)
this✝ : ExpChar (↥M) q
x : E
hx : x ∈ S
this : Algebra.IsSeparable ↥M ↥(↥M)⟮x⟯
⊢ x ∈ ↑M