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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this✝¹ : SigmaFinite (map f ν)
this✝ : SigmaFinite (map f (μ.singularPart ν))
this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν] fun x ↦
    ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)
⊢ (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᵐ[ν] fun x ↦
    ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)

Tactic:
refine Filter.EventuallyEq.add ?_ ?_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this✝¹ : SigmaFinite (map f ν)
this✝ : SigmaFinite (map f (μ.singularPart ν))
this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν] fun x ↦
    ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)
⊢ (μ.singularPart ν).rnDeriv ν =ᵐ[ν] fun x ↦ (map f (μ.singularPart ν)).rnDeriv (map f ν) (f x)

case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this✝¹ : SigmaFinite (map f ν)
this✝ : SigmaFinite (map f (μ.singularPart ν))
this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν] fun x ↦
    ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᵐ[ν] fun x ↦ (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)
Module: Mathlib.RingTheory.Algebraic.Cardinality

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
L : Type u
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : IsTorsionFree R L
inst✝ : Algebra.IsAlgebraic R L
⊢ #L ≤ #((p : R[X]) × { x // x ∈ p.aroots L })

Tactic:
by
  simpa only [lift_id] using lift_cardinalMk_le_sigma_polynomial R L

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ e.invLHom.comp ((e'.invLHom.comp e'.toLHom).comp e.toLHom) = LHom.id L

Tactic:
e'.left_inv,

Goal state after:
L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ e.invLHom.comp ((LHom.id L').comp e.toLHom) = LHom.id L
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
α : Type w'
β : Type u_1
f : α → β
⊢ (L.lhomWithConstantsMap f).comp LHom.sumInl = L.lhomWithConstants β

Tactic:
ext <;> rfl

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case pos
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : x = 0
⊢ Group.IsSolvable (X ^ n - C x).Gal

Tactic:
rw [hx, C_0, sub_zero]

Goal state after:
case pos
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : x = 0
⊢ Group.IsSolvable (X ^ n).Gal
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
⊢ (φ ⊓ ψ).Realize v xs ↔ φ.Realize v xs ∧ ψ.Realize v xs

Tactic:
simp [Realize, Min.min]

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case e'_3.e'_3.func
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
β : Type u_3
x : β → (a : α) → M a
a : α
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term β
t_ih : ∀ (a_1 : Fin l✝), Term.realize (fun i ↦ x i a) (_ts✝ a_1) = Term.realize x (_ts✝ a_1) a
⊢ Term.realize (fun i ↦ x i a) (func _f✝ _ts✝) = Term.realize x (func _f✝ _ts✝) a

Tactic:
simp only [Term.realize, t_ih]; rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : L.Term (α ⊕ Fin n)
xs : Fin n → M
⊢ realize (Sum.elim v xs ∘ ⇑(g.sumCongr (_root_.Equiv.refl (Fin n)))) t = realize (Sum.elim (v ∘ ⇑g) xs) t

Tactic:
refine congr (congr rfl ?_) rfl

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : L.Term (α ⊕ Fin n)
xs : Fin n → M
⊢ Sum.elim v xs ∘ ⇑(g.sumCongr (_root_.Equiv.refl (Fin n))) = Sum.elim (v ∘ ⇑g) xs
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case equal.hc
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ ⟨n✝, equal t₁✝ t₂✝⟩.fst = ⟨n✝, equal t₁✝ t₂✝⟩.fst

Tactic:
· simp only

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (s.inf f)

Tactic:
refine Finset.induction definable_univ (fun i s _ h => ?_) s
    rw [Finset.inf_insert]
    exact (hf i).inter h

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case imp
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ {xs : Fin n✝ → M}, f₁✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f₁✝.Realize v xs
ih2 : ∀ {xs : Fin n✝ → M}, f₂✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f₂✝.Realize v xs
xs : Fin n✝ → M
⊢ (f₁✝ ⟹ f₂✝).Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ (f₁✝ ⟹ f₂✝).Realize v xs

Tactic:
BoundedFormula.Realize,

Goal state after:
case imp
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ {xs : Fin n✝ → M}, f₁✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f₁✝.Realize v xs
ih2 : ∀ {xs : Fin n✝ → M}, f₂✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f₂✝.Realize v xs
xs : Fin n✝ → M
⊢ f₁✝.Realize (⇑g ∘ v) (⇑g ∘ xs) → f₂✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ (f₁✝ ⟹ f₂✝).Realize v xs
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
⊢ (∀' f✝).Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ (∀' f✝).Realize v xs

Tactic:
BoundedFormula.Realize,

Goal state after:
case all
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
⊢ (∀ (x : N), f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) x)) ↔ (∀' f✝).Realize v xs
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case refine_2
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
⊢ Set.InjOn (fun i ↦ ↑(L.con i)) s →
    ∀ (φ : L[[α]].Sentence) (x x_1 : α),
      (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → ((L.con x).term.equal (L.con x_1).term).not = φ → M ⊨ φ

Tactic:
· rintro h φ a b ⟨⟨as, bs⟩, ab⟩ rfl
    simp only [Sentence.Realize, Formula.realize_not, Formula.realize_equal, Term.realize_constants]
    exact fun contra => ab (h as bs contra)

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
f : M → M
h✝ : TermDefinable₁ L f
t : L[[↑A]].Formula (Option Unit)
h : (Function.tupleGraph fun v ↦ f (v ())) = ofPred t.Realize
v : Fin 2 → M
⊢ v ∈ {x | (x 0, x 1) ∈ Function.graph f} ↔ v ∈ ofPred (Formula.relabel (fun x ↦ x.elim 1 fun x ↦ 0) t).Realize

Tactic:
convert! Set.ext_iff.1 h (v ∘ (Option.elim · 1 (fun _ ↦ 0)))

Goal state after:
case e'_2
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
f : M → M
h✝ : TermDefinable₁ L f
t : L[[↑A]].Formula (Option Unit)
h : (Function.tupleGraph fun v ↦ f (v ())) = ofPred t.Realize
v : Fin 2 → M
⊢ v ∈ ofPred (Formula.relabel (fun x ↦ x.elim 1 fun x ↦ 0) t).Realize ↔
    (v ∘ fun x ↦ x.elim 1 fun x ↦ 0) ∈ ofPred t.Realize
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {n : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ↑n ∣ c * b

pp: n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {n : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℵ₀ ≤ c * b

pp: n✝ n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
hℵ₀b : ℵ₀ ≤ b
⊢ ↑n ∣ b ∨ ↑n ∣ c

Tactic:
· rwa [mul_comm] at hbc

Goal state after:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {n : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℵ₀ ≤ c * b

n✝ n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
hℵ₀b : ℵ₀ ≤ b
⊢ ↑n ∣ b ∨ ↑n ∣ c
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case pos
a : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ IsPrimePow a ↔ ℵ₀ ≤ a ∨ ∃ n, a = ↑n ∧ IsPrimePow n

Tactic:
simp [h, (prime_of_aleph0_le h).isPrimePow]

Goal state after:
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
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
x✝ : ι₀
⊢ ↑(c₀ x✝)′ = ↑0

Tactic:
simp only [coe_deriv, hc, algebraMap.coe_zero]

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
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
x✝ : ι₀
⊢ (c₀✝ x✝)′ = 0
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case intro.refine_2
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ ∑ x, e x * (eval n) (indicator x) = e n

Tactic:
rw [Finset.sum_eq_single n]

Goal state after:
case intro.refine_2
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ e n * (eval n) (indicator n) = e n

case intro.refine_2.h₀
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ ∀ b ∈ Finset.univ, b ≠ n → e b * (eval n) (indicator b) = 0

case intro.refine_2.h₁
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ n ∉ Finset.univ → e n * (eval n) (indicator n) = 0
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case intro
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ Module.finrank K (R σ K) = Fintype.card (σ → K)

Tactic:
finrank_R

Goal state after:
case intro
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ Fintype.card (σ → K) = Fintype.card (σ → K)
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
⊢ (AEval'.of (frobeniusAlgHom K L).toLinearMap) ((frobeniusAlgHom K L).toLinearMap ^ ↑i • x) =
    (AEval'.of (frobeniusAlgHom K L).toLinearMap) ((⇑(frobeniusAlgEquivOfAlgebraic K L))^[↑(Fin.cast ⋯ i)] x)

Tactic:
End.smul_def,

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
⊢ (AEval'.of (frobeniusAlgHom K L).toLinearMap) (((frobeniusAlgHom K L).toLinearMap ^ ↑i) x) =
    (AEval'.of (frobeniusAlgHom K L).toLinearMap) ((⇑(frobeniusAlgEquivOfAlgebraic K L))^[↑(Fin.cast ⋯ i)] x)
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
f : ↥(adjoin F (⇑b ∘ φ '' Iio (i⁺))) →ₐ[F] Ē
⊢ ((succEquiv i) f).1 = f.comp (Subalgebra.inclusion ⋯)

Tactic:
by
  ext
  rfl

Goal state after:
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 j : WithTop (Module.rank F E).ord.ToType
h : i < j
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
    cases j
    · obtain ⟨i, rfl⟩ := ne_top_iff_exists.mp h.ne
      exact ⟨le_top, fun incl ↦ (isLeast_leastExt i).1 (incl trivial)⟩
    · obtain ⟨i, rfl⟩ := ne_top_iff_exists.mp (h.trans <| coe_lt_top _).ne
      exact strictMono_filtration (coe_lt_coe.mp h)

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

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

Tactic:
simp only [iterate_map_one, iterate_zero_apply, mul_one, add_zero]

Goal state after:
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:
by simp_rw [iterate_frobenius, add_zero, mul_pow, ← pow_mul,
      ← pow_add, mul_assoc, ← pow_add]

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case hx
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
inst✝ : DecidablePred FiniteIndex
hcovers : ⋃ i ∈ {i ∈ s | (H i).FiniteIndex} ∪ {a ∈ s | ¬(H a).FiniteIndex}, g i • ↑(H i) = Set.univ
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
i : ι
⊢ ⋃ (hx : i ∈ s), ⋃ a, ⋃ (_ : ⟨⟨i, hx⟩, a⟩ ∈ {k | (H ↑k.fst).FiniteIndex}), f ⟨⟨i, hx⟩, a⟩ • ↑(K ⟨⟨i, hx⟩, a⟩) =
    ⋃ (_ : i ∈ {i ∈ s | (H i).FiniteIndex}), g i • ↑(H i)

pp: case hy
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
inst✝ : DecidablePred FiniteIndex
hcovers : ⋃ i ∈ {i ∈ s | (H i).FiniteIndex} ∪ {a ∈ s | ¬(H a).FiniteIndex}, g i • ↑(H i) = Set.univ
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
i : ι
⊢ ⋃ (hx : i ∈ s), ⋃ a, ⋃ (_ : ⟨⟨i, hx⟩, a⟩ ∈ {a | ¬(H ↑a.fst).FiniteIndex}), f ⟨⟨i, hx⟩, a⟩ • ↑(K ⟨⟨i, hx⟩, a⟩) =
    ⋃ (_ : i ∈ {a ∈ s | ¬(H a).FiniteIndex}), g i • ↑(H i)

Tactic:
· by_cases hfi : (H i).FiniteIndex <;>
        simp [← Set.smul_set_iUnion₂, Set.iUnion_subtype, ← leftCoset_assoc, f, K, ht, hfi]

Goal state after:
case hy
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
inst✝ : DecidablePred FiniteIndex
hcovers : ⋃ i ∈ {i ∈ s | (H i).FiniteIndex} ∪ {a ∈ s | ¬(H a).FiniteIndex}, g i • ↑(H i) = Set.univ
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
i : ι
⊢ ⋃ (hx : i ∈ s), ⋃ a, ⋃ (_ : ⟨⟨i, hx⟩, a⟩ ∈ {a | ¬(H ↑a.fst).FiniteIndex}), f ⟨⟨i, hx⟩, a⟩ • ↑(K ⟨⟨i, hx⟩, a⟩) =
    ⋃ (_ : i ∈ {a ∈ s | ¬(H a).FiniteIndex}), g i • ↑(H i)
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
inst✝¹ : IsGalois F ↥A
inst✝ : FiniteDimensional F E
h₁ : A ⊔ B = ⊤
h₂ : A ⊓ B = ⊥
⊢ finrank F E = finrank F ↥A * finrank F ↥B

Tactic:
← Module.finrank_mul_finrank F B E,

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
inst✝¹ : IsGalois F ↥A
inst✝ : FiniteDimensional F E
h₁ : A ⊔ B = ⊤
h₂ : A ⊓ B = ⊥
⊢ finrank F ↥B * finrank (↥B) E = finrank F ↥A * finrank F ↥B
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
⊢ (X ^ ringExpChar K ^ elemExponent K a).natDegree = ringExpChar K ^ elemExponent K a

Tactic:
natDegree_pow,

Goal state after:
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
⊢ ringExpChar K ^ elemExponent K a * X.natDegree = ringExpChar K ^ elemExponent K a
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
n : ℕ
h : a ^ ringExpChar K ^ n ∈ (algebraMap K L).range
p : ℕ
h✝ : ExpChar K p
hp : Nat.Prime p
hchar✝ : CharP K p
y : K
hy : (algebraMap K L) y = a ^ ringExpChar K ^ n
f : K[X] := X ^ ringExpChar K ^ n - C y
hf₁ : (aeval a) f = 0
hf₂ : f.Monic
⊢ (X ^ ringExpChar K ^ n).natDegree = ringExpChar K ^ n

Tactic:
natDegree_pow,

Goal state after:
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
n : ℕ
h : a ^ ringExpChar K ^ n ∈ (algebraMap K L).range
p : ℕ
h✝ : ExpChar K p
hp : Nat.Prime p
hchar✝ : CharP K p
y : K
hy : (algebraMap K L) y = a ^ ringExpChar K ^ n
f : K[X] := X ^ ringExpChar K ^ n - C y
hf₁ : (aeval a) f = 0
hf₂ : f.Monic
⊢ ringExpChar K ^ n * X.natDegree = ringExpChar K ^ n
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: case zero
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : IsPurelyInseparable K L
inst✝¹ : FiniteDimensional K L
inst✝ : CharZero K
h✝ : ExpChar K 1
⊢ HasExponent K L

pp: case prime
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsPurelyInseparable K L
inst✝ : FiniteDimensional K L
p : ℕ
h✝ : ExpChar K p
hp : Nat.Prime p
hchar✝ : CharP K p
⊢ HasExponent K L

Tactic:
· exact ⟨0, fun a ↦ surjective_algebraMap_of_isSeparable K L _⟩

Goal state after:
case prime
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsPurelyInseparable K L
inst✝ : FiniteDimensional K L
p : ℕ
h✝ : ExpChar K p
hp : Nat.Prime p
hchar✝ : CharP K p
⊢ HasExponent K L
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
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
x : E
n : ℕ
hx : x ^ ringExpChar F ^ n ∈ (algebraMap F E).rangeS
⊢ x⁻¹ ∈
    (have this := ⋯;
      Subalgebra.perfectClosure F E (ringExpChar F)).carrier

Tactic:
use n

Goal state after:
case h
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
x : E
n : ℕ
hx : x ^ ringExpChar F ^ n ∈ (algebraMap F E).rangeS
⊢ x⁻¹ ^ ringExpChar F ^ n ∈ (algebraMap F E).rangeS