mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
h' : ∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 → α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 '' univ
⊢ u ∈ f '' univ

Tactic:
apply h' _ _ rfl

Goal state after:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
⊢ LiftpPreservation ↔ IsUniform

Tactic:
rw [← suppPreservation_iff_liftpPreservation, suppPreservation_iff_uniform]

Goal state after:
Module: Mathlib.Data.Set.Enumerate

Goal state before:
pp: case some.zero
α : Type u_1
sel : Set α → Option α
s : Set α
n : ℕ
h : enumerate sel s (n + 1) = none
val✝ : α
hs : sel s = some val✝
hm : n + 1 ≤ 0
⊢ enumerate sel s 0 = none

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case cons.inr.inl
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : s.think ∈ l
a' : α
e' :
  (match Sum.inl a' with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match c.destruct with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inl a'
⊢ s ∈ l'

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case none
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
ht' : none ∈ s.destruct
ht2 : Option.rec nil Prod.snd none = t
td : some a ∈ Computation.pure none
this : some a = none
⊢ ∃ a', some a' ∈ s.destruct

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case none.inl
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
h✝ : some a = none
⊢ C s'

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Set.FiniteExhaustion

Goal state before:
pp: case neg
α : Type u_1
s✝ : Set α
K : s✝.FiniteExhaustion
s : Set α
hs : s.Countable
h : ¬Nonempty ↑s
⊢ Nonempty s.FiniteExhaustion

Tactic:
· refine ⟨fun _ ↦ ∅, by simp [Finite.to_subtype], fun n ↦ by simp, ?_⟩
    simp [Set.not_nonempty_iff_eq_empty'.mp h]

Goal state after:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
this : s ∈ l'
⊢ (corec parallel.aux1
      (match Seq.destruct S with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S'))).Terminates

Tactic:
rcases Seq.destruct S with (_ | ⟨_ | c, S'⟩) <;> apply IH <;> simp [this]

Goal state after:
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ a ≤ b → ∃ h, h ▸ a.snd ≤ b.snd

Tactic:
rintro ⟨i, a, b, h⟩
    exact ⟨rfl, h⟩

Goal state after:
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
a b : (i : ι) × α i
⊢ a < b → ∃ h, h ▸ a.snd < b.snd

Tactic:
rintro ⟨i, a, b, h⟩
    exact ⟨rfl, h⟩

Goal state after:
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case neg.cons
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
cs₂ : List Char
h : ¬c₁ = c₁
h' : List.Lex (fun x1 x2 ↦ x1 < x2) cs₁ cs₂
⊢ c₁ < c₁

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.WSeq.Productive

Goal state before:
pp: case some
α : Type u
s : WSeq α
inst✝ : s.Productive
n : ℕ
h : (s.drop n).head.get = none
val✝ : α
e : (s.get? (n + 1)).get = some val✝
this✝ : some val✝ ∈ (s.drop (n + 1)).head
a' : α
h' : some a' ∈ (s.drop n).head
this : some a' = none
⊢ (fun n ↦ (s.get? n).get) (n + 1) = none

Tactic:
contradiction

Goal state after:
Module: Mathlib.Order.SemiconjSup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g ⇑fa ⇑fb
g' : β → α
hg' : IsOrderRightAdjoint g g'
⊢ Semiconj g' ⇑fb ⇑fa

Tactic:
refine fun y => (hg' _).unique ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g ⇑fa ⇑fb
g' : β → α
hg' : IsOrderRightAdjoint g g'
y : β
⊢ IsLUB {x | g x ≤ fb y} (fa (g' y))
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
hf : Continuous ⇑f
H : ∀ (x : ℝ), x + τ f < f x
⊢ False

Tactic:
exact lt_irrefl _ (f.lt_translationNumber_of_forall_add_lt hf H)

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
x : ℝ
g : G
this : τ (f₂ g⁻¹) = -τ (f₂ g)
⊢ x + τ (f₂ g) + τ (f₂ g⁻¹) + 1 + 1 = x + 2

Tactic:
by simp [this, add_assoc, one_add_one_eq_two]

Goal state after:
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: case inl
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s = 0
⊢ μ s = 0 ∨ μ s = ENNReal.ofReal T

Tactic:
exact Or.inl h

Goal state after:
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun δ ↦ volume (closedBall x δ)) (𝓝[<] ε) (𝓝 (volume (closedBall x ε)))

Tactic:
volume_closedBall

Goal state after:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun δ ↦ ENNReal.ofReal (min T (2 * δ))) (𝓝[<] ε) (𝓝 (ENNReal.ofReal (min T (2 * ε))))
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: case refine_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᵐ[volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
hG_card : #Finset.univ = n
⊢ volume univ ≤ ∑' (g : ↥G), volume I

Tactic:
rw [AddCircle.measure_univ, tsum_fintype, Finset.sum_const, measure_congr hI,
      volume_closedBall, ← ENNReal.ofReal_nsmul, mul_div, mul_div_mul_comm,
      div_self, one_mul, min_eq_right (div_le_self hT.out.le hn), hG_card,
      nsmul_eq_mul, mul_div_cancel₀ T (lt_of_lt_of_le zero_lt_one hn).ne.symm]

Goal state after:
case refine_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᵐ[volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
hG_card : #Finset.univ = n
⊢ 2 ≠ 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
⊢ (μ.singularPart ν) (f ⁻¹' s)ᶜ = 0

Tactic:
← mem_ae_iff,

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 ∈ ae (μ.singularPart ν)
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: case map_eq
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
hs : MeasurableSet s
⊢ (ν.withDensity (μ.rnDeriv ν)) (f ⁻¹' s) + (μ.singularPart ν) s = μ s

Tactic:
← (hfμ.singularPart hfν).measure_preimage hs.nullMeasurableSet,

Goal state after:
case map_eq
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
hs : MeasurableSet s
⊢ (ν.withDensity (μ.rnDeriv ν)) (f ⁻¹' s) + (μ.singularPart ν) (f ⁻¹' s) = μ s
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
⊢ {x | (fun x ↦ 0 < ν.rnDeriv μ x) x} ∈ ae (μ.withDensity (ν.rnDeriv μ))

Tactic:
filter_upwards [Measure.rnDeriv_pos (withDensity_absolutelyContinuous μ (ν.rnDeriv μ)),
    (withDensity_absolutelyContinuous μ (ν.rnDeriv μ)).ae_le
    (Measure.rnDeriv_withDensity μ (Measure.measurable_rnDeriv ν μ))] with x hx hx2

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
x : α
hx : 0 < (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x
hx2 : (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x = ν.rnDeriv μ x
⊢ 0 < ν.rnDeriv μ x
Module: Mathlib.Dynamics.Flow

Goal state before:
pp: τ : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace τ
inst✝² : TopologicalSpace α
inst✝¹ : SubtractionCommMonoid τ
inst✝ : ContinuousNeg τ
ϕ : Flow τ α
x✝² x✝¹ : τ
x✝ : α
⊢ ϕ.toFun (-(x✝² + x✝¹)) x✝ = ϕ.toFun (-x✝²) (ϕ.toFun (-x✝¹) x✝)

Tactic:
neg_add,

Goal state after:
τ : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace τ
inst✝² : TopologicalSpace α
inst✝¹ : SubtractionCommMonoid τ
inst✝ : ContinuousNeg τ
ϕ : Flow τ α
x✝² x✝¹ : τ
x✝ : α
⊢ ϕ.toFun (-x✝² + -x✝¹) x✝ = ϕ.toFun (-x✝²) (ϕ.toFun (-x✝¹) x✝)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
⊢ μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν

Tactic:
have h_ac : ν ≪ ν + ν' := Measure.AbsolutelyContinuous.rfl.add_right _

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
⊢ μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
⊢ μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν

Tactic:
have h_ac : ν ≪ ν + ν' := Measure.AbsolutelyContinuous.rfl.add_right _

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
⊢ μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case htn
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)).Nonempty

Tactic:
intro u
    have hn : (image2 ϕ (u ∩ v) s).Nonempty :=
      Nonempty.image2 (Filter.nonempty_of_mem (inter_mem u.prop hv₁)) hs
    exact hn.mono subset_closure

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

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
this : netMaxcard T F U n = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_bdda : BddAbove (Finset.card '' {s | IsDynNetIn T F U n ↑s})
⊢ 0 ∈ Finset.card '' {s | IsDynNetIn T F U n ↑s}

Tactic:
simp only [mem_image, mem_ofPred_eq, Finset.card_eq_zero, exists_eq_right, Finset.coe_empty]

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
this : netMaxcard T F U n = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_bdda : BddAbove (Finset.card '' {s | IsDynNetIn T F U n ↑s})
⊢ IsDynNetIn T F U n ∅
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 ↦ ?_, fun h ↦ h ▸ ν.rnDeriv_self⟩

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
h : μ.rnDeriv ν =ᵐ[ν] 1
⊢ μ = ν
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : SetRel X X
U_uni : U ∈ 𝓤 X
i : ι
h_i : p i
si_U : s i ⊆ U
⊢ netEntropyInfEntourage T F U ≤ ⨆ i, ⨆ (_ : p i), netEntropyInfEntourage T F (s i)

Tactic:
apply (netEntropyInfEntourage_antitone T F si_U).trans

Goal state after:
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : SetRel X X
U_uni : U ∈ 𝓤 X
i : ι
h_i : p i
si_U : s i ⊆ U
⊢ (fun U ↦ netEntropyInfEntourage T F U) (s i) ≤ ⨆ i, ⨆ (_ : p i), netEntropyInfEntourage T F (s i)
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : (map (algebraMap F q.SplittingField) p).Splits
hp : Group.IsSolvable p.Gal
hq : Group.IsSolvable (map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
this : Fact (map (algebraMap F L) p).Splits
ϕ : Gal(L/K) ≃* (map (algebraMap F K) q).Gal := (IsSplittingField.algEquiv L (map (algebraMap F K) q)).autCongr
⊢ Group.IsSolvable q.Gal

Tactic:
have ϕ_inj : Function.Injective ϕ.toMonoidHom := ϕ.injective

Goal state after:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : (map (algebraMap F q.SplittingField) p).Splits
hp : Group.IsSolvable p.Gal
hq : Group.IsSolvable (map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
this : Fact (map (algebraMap F L) p).Splits
ϕ : Gal(L/K) ≃* (map (algebraMap F K) q).Gal := (IsSplittingField.algEquiv L (map (algebraMap F K) q)).autCongr
ϕ_inj : Function.Injective ⇑ϕ.toMonoidHom
⊢ Group.IsSolvable q.Gal
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
⊢ (σ * τ) a = (τ * σ) a

Tactic:
obtain ⟨c, hc⟩ := key σ

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
⊢ (σ * τ) a = (τ * σ) a
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
⊢ (fun x ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x) =ᵐ[μ + ν] fun x ↦ μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x

Tactic:
by
  have h1 : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ :=
    Measure.rnDeriv_mul_rnDeriv (rfl.absolutelyContinuous.add_right _)
  have h2 : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] ν.rnDeriv ξ :=
    Measure.rnDeriv_mul_rnDeriv (rfl.absolutelyContinuous.add_right' _)
  have h_ac : μ + ν ≪ ξ := hμ.add_left hν
  filter_upwards [h_ac h1, h_ac h2, h_ac <| (μ + ν).rnDeriv_lt_top ξ, ν.rnDeriv_lt_top (μ + ν),
    Measure.rnDeriv_pos h_ac] with a h1 h2 h_lt_top1 h_lt_top2 h_pos
  rw [← h1, ← h2, Pi.mul_apply, Pi.mul_apply, div_eq_mul_inv,
    ENNReal.mul_inv (Or.inr h_lt_top1.ne) (Or.inl h_lt_top2.ne), div_eq_mul_inv, mul_assoc,
    mul_comm ((μ + ν).rnDeriv ξ a), mul_assoc, ENNReal.inv_mul_cancel h_pos.ne' h_lt_top1.ne,
    mul_one]

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

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ (x : α) in s, f x ∂μ

Tactic:
rw [← setIntegral_withDensity_eq_setIntegral_toReal_smul, withDensity_rnDeriv_eq _ _ hμν]
  exacts [measurable_rnDeriv _ _, ae_restrict_of_ae (rnDeriv_lt_top _ _), hs]

Goal state after:
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 ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
key : ∀ (σ : (X ^ n - C a).Gal), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
⊢ (σ * τ) b = (τ * σ) b

Tactic:
obtain ⟨c, hc⟩ := key σ

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 : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
key : ∀ (σ : (X ^ n - C a).Gal), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
c : F
hc : σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c
⊢ (σ * τ) b = (τ * σ) b
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝ : L.Structure M
e : M ≃ N
this : L.Structure N := e.inducedStructure
⊢ M ≃[L] N

Tactic:
exact
  { e with
    map_fun' := @fun n f x => by simp [← Function.comp_assoc e.symm e x]
    map_rel' := @fun n r x => by simp [← Function.comp_assoc e.symm e x] }

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
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
hp : p.comp (X ^ n) ≠ 0
⊢ (aeval x) (p.comp (X ^ n)) = 0

Tactic:
rw [aeval_comp, aeval_X_pow, minpoly.aeval]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case mul
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : Group.IsSolvable (minpoly F z).Gal
⊢ Group.IsSolvable (minpoly F (y * z)).Gal

Tactic:
apply induction_step hy hz (mul_mem hy hz) hy' hz' (mul_mem ..) <;> apply subset_adjoin <;> 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
h : funMap f (⇑φ ∘ x) = φ (funMap f x) ↔ funMap f x = funMap f x
⊢ φ (funMap f x) = funMap f (⇑φ ∘ x)

Tactic:
rw [eq_comm, h]

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
h :
  ∀ (φ : (n : ℕ) × L.BoundedFormula α n) (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (φ.snd.listEncode ++ l') = φ :: listDecode l'
⊢ listDecode (flatMap (fun φ ↦ φ.snd.listEncode) l) = l

Tactic:
induction l with
    | nil =>
      simp [listDecode]
    | cons φ l ih => rw [flatMap_cons, h φ _, ih]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
n : ℕ
ψ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ (φ.onBoundedFormula ψ).Realize v xs ↔ ψ.Realize v xs

Tactic:
by
  induction ψ with
  | falsum => rfl
  | equal => simp only [onBoundedFormula, realize_bdEqual, realize_onTerm]; rfl
  | rel =>
    simp only [onBoundedFormula, realize_rel, LHom.map_onRelation,
      Function.comp_apply, realize_onTerm]
    rfl
  | imp _ _ ih1 ih2 => simp only [onBoundedFormula, ih1, ih2, realize_imp]
  | all _ ih3 => simp only [onBoundedFormula, ih3, realize_all]

Goal state after:
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
a : M
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
i : Fin (n + 1)
j : Fin n
⊢ ↑(x j) ∈ A

Tactic:
← hA.closure_eq_self

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
a : M
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
i : Fin (n + 1)
j : Fin n
⊢ ↑(x j) ∈ ↑((closure L).toFun A)
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
a : M
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
hD : A.Definable₁ L D
b : M
hbD : b ∈ D
hbA : b ∈ A
⊢ b ∈ (closure L).toFun A

Tactic:
← hA.closure_eq_self

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
a : M
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
hD : A.Definable₁ L D
b : M
hbD : b ∈ D
hbA : b ∈ ↑((closure L).toFun A)
⊢ b ∈ (closure L).toFun A