mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
s : WSeq α
⊢ ∀ {s t : WSeq α},
    (fun s1 s2 ↦ (map ret s2).join = s1) s t →
      Computation.LiftRel (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1) s.destruct t.destruct

Tactic:
intro s' s h

Goal state after:
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ Computation.LiftRel (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1) s'.destruct s.destruct
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: α : Type u_1
k : ℕ
⊢ Nat.card (Sym α k) = (Nat.card α + k - 1).choose k

Tactic:
rw [natCard_sym_eq_multichoose, Nat.multichoose_eq]

Goal state after:
Module: Mathlib.Data.W.Constructions

Goal state before:
pp: n : ℕ
⊢ (ofNat n.succ).toNat = n.succ

Tactic:
ofNat,

Goal state after:
n : ℕ
⊢ (mk Natα.succ fun x ↦ ofNat n).toNat = n.succ
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace X
inst✝⁸ : BorelSpace X
inst✝⁷ : R1Space X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : BorelSpace Y
inst✝³ : R1Space Y
inst✝² : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst✝², _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z)) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : ν t ≠ ∞
z : Z
hz : z ∈ {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}ᶜ
⊢ 0 < μ ((⇑(f z) ⁻¹' t) ∆ s)

Tactic:
pos_iff_ne_zero,

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace X
inst✝⁸ : BorelSpace X
inst✝⁷ : R1Space X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : BorelSpace Y
inst✝³ : R1Space Y
inst✝² : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst✝², _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z)) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : ν t ≠ ∞
z : Z
hz : z ∈ {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}ᶜ
⊢ μ ((⇑(f z) ⁻¹' t) ∆ s) ≠ 0
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: case e'_6
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ f ⁻¹' s ∈ ae (μ.singularPart ν)

Tactic:
← Filter.eventuallyEq_univ,

Goal state after:
case e'_6
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ f ⁻¹' s =ᵐ[μ.singularPart ν] univ
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
key : ⨅ s, ↑(#↑s) ∈ range fun s ↦ ↑(#↑s)
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ #s = k

Tactic:
rw [coverMincard, iInf_subtype'] at k_min

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = ⨅ x, ↑(#↑x)
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
key : ⨅ s, ↑(#↑s) ∈ range fun s ↦ ↑(#↑s)
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ #s = k
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ coverMincard T F U n ≠ 0 ↔ F ≠ ∅

Tactic:
not_iff_not

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ coverMincard T F U n = 0 ↔ F = ∅
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
⊢ coverEntropy (MapsTo.restrict T G G hG) (val ⁻¹' F) = coverEntropy T F

Tactic:
by
  rw [← coverEntropy_image_of_comap _ hG.val_restrict_apply (val ⁻¹' F), image_preimage_coe G F,
    inter_eq_right.2 hF]

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

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
⊢ coverEntropyInf (MapsTo.restrict T G G hG) (val ⁻¹' F) = coverEntropyInf T F

Tactic:
by
  rw [← coverEntropyInf_image_of_comap _ hG.val_restrict_apply (val ⁻¹' F), image_preimage_coe G F,
    inter_eq_right.2 hF]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ.rnDeriv ν ≤ᵐ[ν] 1 ↔ μ ≤ ν

Tactic:
refine ⟨fun h s ↦ ?_, fun h ↦ rnDeriv_le_one_of_le h⟩
  rw [← withDensity_rnDeriv_eq _ _ hμν, withDensity_apply', ← setLIntegral_one]
  exact setLIntegral_mono_ae aemeasurable_const (h.mono fun _ hh _ ↦ hh)

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

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n_pos : n ≠ 0
s : Finset X
h : IsDynCoverOf T F U n ↑s
⊢ (↑(coverMincard T F U n)).log / ↑n ≤ (↑(#s)).log / ↑n

Tactic:
apply monotone_div_right_of_nonneg n.cast_nonneg' (log_monotone _)

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n_pos : n ≠ 0
s : Finset X
h : IsDynCoverOf T F U n ↑s
⊢ ↑(coverMincard T F U n) ≤ ↑(#s)
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: X : Type u_1
T : X → X
V : SetRel X X
inst✝ : UniformSpace X
h : Continuous T
F : Set X
U : SetRel X X
V_uni : V ∈ 𝓤 X
n : ℕ
⊢ coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n

Tactic:
rcases eq_top_or_lt_top (coverMincard T F U n) with h' | h'

Goal state after:
case inl
X : Type u_1
T : X → X
V : SetRel X X
inst✝ : UniformSpace X
h : Continuous T
F : Set X
U : SetRel X X
V_uni : V ∈ 𝓤 X
n : ℕ
h' : coverMincard T F U n = ⊤
⊢ coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n

case inr
X : Type u_1
T : X → X
V : SetRel X X
inst✝ : UniformSpace X
h : Continuous T
F : Set X
U : SetRel X X
V_uni : V ∈ 𝓤 X
n : ℕ
h' : coverMincard T F U n < ⊤
⊢ coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: G : Type u_3
inst✝⁸ : Group G
mG : MeasurableSpace G
inst✝⁷ : MeasurableMul₂ G
inst✝⁶ : MeasurableInv G
μ : Measure G
inst✝⁵ : μ.IsMulLeftInvariant
inst✝⁴ : SFinite μ
ν₁ ν₂ : Measure G
inst✝³ : IsFiniteMeasure ν₁
inst✝² : IsFiniteMeasure ν₂
inst✝¹ : ν₁.HaveLebesgueDecomposition μ
inst✝ : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
this : (ν₁ ∗ₘ ν₂).HaveLebesgueDecomposition μ
⊢ μ.withDensity ((ν₁ ∗ₘ ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ)

pp: G : Type u_3
inst✝⁸ : Group G
mG : MeasurableSpace G
inst✝⁷ : MeasurableMul₂ G
inst✝⁶ : MeasurableInv G
μ : Measure G
inst✝⁵ : μ.IsMulLeftInvariant
inst✝⁴ : SFinite μ
ν₁ ν₂ : Measure G
inst✝³ : IsFiniteMeasure ν₁
inst✝² : IsFiniteMeasure ν₂
inst✝¹ : ν₁.HaveLebesgueDecomposition μ
inst✝ : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
this : (ν₁ ∗ₘ ν₂).HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : G), (ν₁ ∗ₘ ν₂).rnDeriv μ x ∂μ ≠ ∞

Tactic:
withDensity_rnDeriv_eq _ _ (mconv_absolutelyContinuous hν₂),

Goal state after:
G : Type u_3
inst✝⁸ : Group G
mG : MeasurableSpace G
inst✝⁷ : MeasurableMul₂ G
inst✝⁶ : MeasurableInv G
μ : Measure G
inst✝⁵ : μ.IsMulLeftInvariant
inst✝⁴ : SFinite μ
ν₁ ν₂ : Measure G
inst✝³ : IsFiniteMeasure ν₁
inst✝² : IsFiniteMeasure ν₂
inst✝¹ : ν₁.HaveLebesgueDecomposition μ
inst✝ : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
this : (ν₁ ∗ₘ ν₂).HaveLebesgueDecomposition μ
⊢ ν₁ ∗ₘ ν₂ = μ.withDensity (ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ)

G : Type u_3
inst✝⁸ : Group G
mG : MeasurableSpace G
inst✝⁷ : MeasurableMul₂ G
inst✝⁶ : MeasurableInv G
μ : Measure G
inst✝⁵ : μ.IsMulLeftInvariant
inst✝⁴ : SFinite μ
ν₁ ν₂ : Measure G
inst✝³ : IsFiniteMeasure ν₁
inst✝² : IsFiniteMeasure ν₂
inst✝¹ : ν₁.HaveLebesgueDecomposition μ
inst✝ : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
this : (ν₁ ∗ₘ ν₂).HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : G), (ν₁ ∗ₘ ν₂).rnDeriv μ x ∂μ ≠ ∞
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f ↦ ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r ↦ ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
⊢ ϕ.IsExpansionOn M

Tactic:
by
  let := ϕ.defaultExpansion M
  refine ⟨fun {n} f xs => ?_, fun {n} r xs => ?_⟩
  · have hf : ϕ.onFunction f ∈ Set.range fun f : L.Functions n => ϕ.onFunction f := ⟨f, rfl⟩
    refine (dif_pos hf).trans ?_
    rw [h.onFunction hf.choose_spec]
  · have hr : ϕ.onRelation r ∈ Set.range fun r : L.Relations n => ϕ.onRelation r := ⟨r, rfl⟩
    refine (dif_pos hr).trans ?_
    rw [h.onRelation hr.choose_spec]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
n : ℕ
hn : n ≠ 0
hx : x ^ n ∈ solvableByRad F E
⊢ x ∈ solvableByRad F E

Tactic:
by
  grind [solvableByRad]

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

Goal state before:
pp: K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
ax : FieldAxiom
⊢ K ⊨ ax.toSentence ↔ toProp K ax

Tactic:
by
  cases ax <;>
  simp [Sentence.Realize, Formula.Realize, Fin.snoc]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : L.HomClass F M N
g : F
v : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (⇑g ∘ v) (_ts✝ a) = g (Term.realize v (_ts✝ a))
⊢ Term.realize (⇑g ∘ v) (func _f✝ _ts✝) = g (Term.realize v (func _f✝ _ts✝))

Tactic:
· rw [Term.realize, Term.realize, HomClass.map_fun]
    refine congr rfl ?_
    ext x
    simp [*]

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ φ (funMap f x) = funMap f (⇑φ ∘ x)

Tactic:
have h := φ.map_formula (Formula.graph f) (Fin.cons (funMap f x) x)

Goal state after:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
h : (Formula.graph f).Realize (⇑φ ∘ Fin.cons (funMap f x) x) ↔ (Formula.graph f).Realize (Fin.cons (funMap f x) x)
⊢ φ (funMap f x) = funMap f (⇑φ ∘ x)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
φ : L.Formula (Fin n)
v : Empty → M
x : Fin n → M
⊢ BoundedFormula.Realize φ (x ∘ Fin.cast ⋯) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default

Tactic:
cast_refl,

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
φ : L.Formula (Fin n)
v : Empty → M
x : Fin n → M
⊢ BoundedFormula.Realize φ (x ∘ id) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
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
inst✝ : Finite ι
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
⊢ A.Definable L (⋃ i, f i)

Tactic:
by
  have := Fintype.ofFinite ι
  convert! definable_finset_sup hf Finset.univ using 1
  simp

Goal state after:
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : L[[↑↑S]].Formula (Fin 1)
hφ : {x | x 0 ∈ D} = ofPred φ.Realize
hφx : φ.Realize ![x]
ψ : L[[↑↑S]].Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' : φ.Realize v'
⊢ (D ∩ ↑S).Nonempty

Tactic:
refine ⟨v' 0, ?_, by simp⟩

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : L[[↑↑S]].Formula (Fin 1)
hφ : {x | x 0 ∈ D} = ofPred φ.Realize
hφx : φ.Realize ![x]
ψ : L[[↑↑S]].Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' : φ.Realize v'
⊢ ↑(v' 0) ∈ D
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
⊢ x ∈ (fun g ↦ g ∘ Sum.inl) '' ofPred φ.Realize ↔ x ∈ ofPred (BoundedFormula.relabel id φ).exs.Realize

Tactic:
simp only [Set.mem_image, mem_ofPred_eq, BoundedFormula.realize_exs,
    BoundedFormula.realize_relabel, Function.comp_id, Fin.castAdd_zero, Fin.cast_refl]

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
⊢ (∃ x_1, φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x) ↔ ∃ xs, BoundedFormula.Realize φ (Sum.elim x xs) (xs ∘ Fin.natAdd m)
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
s : Set (α ⊕ Fin m → M)
h : A.Definable L s
⊢ A.Definable L ((fun g ↦ g ∘ Sum.inl) '' s)

Tactic:
obtain ⟨φ, rfl⟩ := h
  refine ⟨(BoundedFormula.relabel id φ).exs, ?_⟩
  ext x
  simp only [Set.mem_image, mem_ofPred_eq, BoundedFormula.realize_exs,
    BoundedFormula.realize_relabel, Function.comp_id, Fin.castAdd_zero, Fin.cast_refl]
  constructor
  · rintro ⟨y, hy, rfl⟩
    exact
      ⟨y ∘ Sum.inr, (congr (congr rfl (Sum.elim_comp_inl_inr y).symm) (funext finZeroElim)).mp hy⟩
  · rintro ⟨y, hy⟩
    exact ⟨Sum.elim x y, (congr rfl (funext finZeroElim)).mp hy, Sum.elim_comp_inl _ _⟩

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
h : TermDefinable₁ L f
⊢ A.Definable₂ L (Function.graph f)

Tactic:
by
  obtain ⟨t, h⟩ := h.termDefinable.definable_tupleGraph A L
  use t.relabel (Option.elim · 1 (fun _ ↦ 0))
  ext v
  convert! Set.ext_iff.1 h (v ∘ (Option.elim · 1 (fun _ ↦ 0)))
  simp

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case mp
L : Language
T : L.Theory
hcomp : T.IsComplete
M : T.ModelType
⊢ ∀ (N : T.ModelType), ↑M ≅[L] ↑N

Tactic:
N

Goal state after:
case mp
L : Language
T : L.Theory
hcomp : T.IsComplete
M N : T.ModelType
⊢ ↑M ≅[L] ↑N
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
a : σ → K
⊢ (eval a) (indicator a) = 1

Tactic:
by
  nontriviality
  have : 0 < Fintype.card K - 1 := tsub_pos_of_lt Fintype.one_lt_card
  simp only [indicator, map_prod, map_sub, map_one, map_pow, eval_X, eval_C, sub_self,
    zero_pow this.ne', sub_zero, Finset.prod_const_one]

Goal state after:
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: case refine_2
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 ⊤ = ⊥
⊢ (algebraMap F K) a =
    ∑ x, ↑(c x) / ↑(Fintype.card Gal(K/F)) * logDeriv (∏ x_1, x_1 (u x)) + ((∑ x, x v) / ↑(Fintype.card Gal(K/F)))′

Tactic:
Derivation.leibniz_div_const,

Goal state after:
case refine_2
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 ⊤ = ⊥
⊢ (algebraMap F K) a =
    ∑ x, ↑(c x) / ↑(Fintype.card Gal(K/F)) * logDeriv (∏ x_1, x_1 (u x)) + (↑(Fintype.card Gal(K/F)))⁻¹ • (∑ x, x v)′

case refine_2.h
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 ⊤ = ⊥
⊢ (↑(Fintype.card Gal(K/F)))′ = 0
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
⊢ #(Emb F E) = (fun c ↦ if ℵ₀ ≤ c then 2 ^ c else c) (Module.rank F E)

Tactic:
dsimp only

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
⊢ #(Emb F E) = if ℵ₀ ≤ Module.rank F E then 2 ^ Module.rank F E else Module.rank F E
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
hp : ¬1 < p
⊢ ⊥ ≤ nilradical R

Tactic:
bot_le

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y : ℕ × K
H : R K p x✝ y
n : ℕ
x : K
⊢ R K p ((n, x).1, (n, x).2⁻¹) ((n + 1, (frobenius K p) x).1, (n + 1, (frobenius K p) x).2⁻¹)

Tactic:
simp only [frobenius_def]
          rw [← inv_pow]
          apply R.intro

Goal state after:
Module: Mathlib.FieldTheory.MvRatFunc.Rank

Goal state before:
pp: case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : Module.rank F R ≤ Module.rank F K
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Tactic:
MvPolynomial.rank_eq_lift,

Goal state after:
case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : lift.{v, u} #(σ →₀ ℕ) ≤ Module.rank F K
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case neg
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 : ι
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
hcovers : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hcovers' : ¬⋃ i ∈ {x | K x = K k}, f i • ↑(K i) = Set.univ
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex

Tactic:
have hn' : (Finset.univ.image K).card < n := hn ▸ by
      refine ((Finset.card_le_card fun x => ?_).trans_lt <|
        Finset.card_erase_lt_of_mem (Finset.mem_image_of_mem H hj))
      rw [mem_image_univ_iff_mem_range, Set.mem_range]
      exact fun ⟨k, hk⟩ => hk ▸ hK' k

Goal state after:
case neg
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 : ι
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
hcovers : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hcovers' : ¬⋃ i ∈ {x | K x = K k}, f i • ↑(K i) = Set.univ
hn' : (Finset.image K Finset.univ).card < n
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : Gal(K[n√a]/K)
this : Fact (Irreducible (X ^ n - C a))
⊢ ↑((autAdjoinRootXPowSubCEquiv hζ H).symm σ) • root (X ^ n - C a) = σ (root (X ^ n - C a))

Tactic:
simp only [autAdjoinRootXPowSubCEquiv, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
    MulEquiv.symm_mk, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk, AdjoinRootXPowSubCEquivToRootsOfUnity,
    AdjoinRoot.algebraMap_eq, rootsOfUnity.mkOfPowEq, Units.smul_def, Algebra.smul_def,
    rootsOfUnityEquivOfPrimitiveRoots_symm_apply, Units.val_ofPowEqOne, ite_mul, one_mul]

Goal state after:
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : Gal(K[n√a]/K)
this : Fact (Irreducible (X ^ n - C a))
⊢ (if a = 0 then root (X ^ n - C a) else σ (root (X ^ n - C a)) / root (X ^ n - C a) * root (X ^ n - C a)) =
    σ (root (X ^ n - C a))
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
n : ℕ
a : K
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
inst✝ : NeZero n
this : eval (rootOfSplits ⋯ ⋯) (Polynomial.map (algebraMap K L) (X ^ n - C a)) = 0
⊢ rootOfSplitsXPowSubC ⋯ a L ^ n = (algebraMap K L) a

Tactic:
simpa only [eval_map, eval₂_sub, eval₂_X_pow, eval₂_C, sub_eq_zero] using this

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
c d : ConjRootClass K L
⊢ c.minpoly = d.minpoly ↔ c = d

Tactic:
by
  induction c
  induction d
  simp [isConjRoot_def]

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
inst✝ : Flat R ↥A
hc : ∀ (a b : ↥A), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
⊢ Module.rank R ↥A = 1

Tactic:
rw [← inf_of_le_left (le_refl A)] at hc ⊢

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
inst✝ : Flat R ↥A
hc : ∀ (a b : ↥(A ⊓ A)), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
⊢ Module.rank R ↥(A ⊓ A) = 1