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

Goal state before:
pp: case cons.cons
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
⊢ (if c₁ = c₂ then ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ } { s := ofList (c₂ :: cs₂), i := 0 + c₂ } = true
    else c₁ < c₂) ↔
    c₁ :: cs₁ < c₂ :: cs₂

Tactic:
split_ifs with h

Goal state after:
case pos
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : c₁ = c₂
⊢ ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ } { s := ofList (c₂ :: cs₂), i := 0 + c₂ } = true ↔ c₁ :: cs₁ < c₂ :: cs₂

case neg
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
⊢ c₁ < c₂ ↔ c₁ :: cs₁ < c₂ :: cs₂
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
β : Type v
f : α → β
S : WSeq (Computation α)
c1 c2 : Computation β
h : ∃ l S, c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
⊢ BisimO
    (fun c1 c2 ↦
      ∃ l S,
        c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S))
    c1.destruct c2.destruct

Tactic:
exact
    match c1, c2, h with
    | _, _, ⟨l, S, rfl, rfl⟩ => by
      have : parallel.aux2 (l.map (map f))
          = lmap f (rmap (List.map (map f)) (parallel.aux2 l)) := by
        simp only [parallel.aux2, rmap, lmap]
        induction l with
        | nil => grind
        | cons => grind [destruct_map, lmap, rmap]
      simp only [BisimO, destruct_map, lmap, rmap, corec_eq, parallel.aux1.eq_1]
      rw [this]
      rcases parallel.aux2 l with a | l'
      · simp
      simp only [lmap, rmap]
      induction S using WSeq.recOn <;> simpa using ⟨_, _, rfl, rfl⟩

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

Goal state before:
pp: α : Type u
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
s : WSeq α
S T : WSeq (WSeq α)
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (fun c1 c2 ↦ ∃ s S T, c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
    (s.append (S.append T).join).destruct.destruct (s.append (S.join.append T.join)).destruct.destruct

Tactic:
induction s using WSeq.recOn with
  | nil =>
    induction S using WSeq.recOn with
    | nil =>
      simp only [nil_append, join_nil]
      induction T using WSeq.recOn with
      | nil => simp
      | cons s T =>
        simp only [join_cons, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]
        refine ⟨s, nil, T, ?_, ?_⟩ <;> simp
      | think T =>
        simp only [join_think, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]
        refine ⟨nil, nil, T, ?_, ?_⟩ <;> simp
    | cons s S => simpa using ⟨s, S, T, rfl, rfl⟩
    | think S => refine ⟨nil, S, T, ?_, ?_⟩ <;> simp
  | cons a s => simpa using ⟨s, S, T, rfl, rfl⟩
  | think s => simpa using ⟨s, S, T, rfl, rfl⟩

Goal state after:
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
⊢ ¬∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ inl c₁ = inr c₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
rintro ⟨_, _, c₂, _, _, h, _⟩

Goal state after:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
w✝¹ : α₂
w✝ : β₂
c₂ : γ₂
left✝¹ : a = inr w✝¹
left✝ : b = inr w✝
h : inl c₁ = inr c₂
right✝ : c₂ ∈ g w✝¹ w✝
⊢ False
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₂ : γ₂
⊢ ¬∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ inr c₂ = inl c₁ ∧ c₁ ∈ f a₁ b₁

Tactic:
rintro ⟨_, _, c₂, _, _, h, _⟩

Goal state after:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₂✝ : γ₂
w✝¹ : α₁
w✝ : β₁
c₂ : γ₁
left✝¹ : a = inl w✝¹
left✝ : b = inl w✝
h : inr c₂✝ = inl c₂
right✝ : c₂ ∈ f w✝¹ w✝
⊢ False
Module: Mathlib.Data.Vector.Snoc

Goal state before:
pp: α : Type u_1
n : ℕ
val : α
⊢ replicate (n + 1) val = (replicate n val).snoc val

Tactic:
by
  induction n with
  | zero => rfl
  | succ n ih =>
    rw [replicate_succ]
    conv => rhs; rw [replicate_succ]
    rw [snoc_cons, ih]

Goal state after:
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case mpr.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₁
c : γ₁
hc : c ∈ f₁ a b
⊢ inl c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inl b)

pp: case mpr.inr.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₂
c : γ₁
hc : c ∈ g₁ a b
⊢ inl c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)

pp: case mpr.inr.inr.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₂
c : γ₂
hc : c ∈ g₂ a b
⊢ inr c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)

pp: case mpr.inr.inr.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₂
b : β₂
c : γ₂
hc : c ∈ f₂ a b
⊢ inr c ∈ sumLexLift f₁ f₂ g₁ g₂ (inr a) (inr b)

Tactic:
· exact mem_map_of_mem _ hc

Goal state after:
case mpr.inr.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₂
c : γ₁
hc : c ∈ g₁ a b
⊢ inl c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)

case mpr.inr.inr.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₂
c : γ₂
hc : c ∈ g₂ a b
⊢ inr c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)

case mpr.inr.inr.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₂
b : β₂
c : γ₂
hc : c ∈ f₂ a b
⊢ inr c ∈ sumLexLift f₁ f₂ g₁ g₂ (inr a) (inr b)
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case mpr.inr.inr.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₂
b : β₂
c : γ₂
hc : c ∈ f₂ a b
⊢ inr c ∈ sumLexLift f₁ f₂ g₁ g₂ (inr a) (inr b)

Tactic:
· exact mem_map_of_mem _ hc

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

Goal state before:
pp: f : CircleDeg1Lift
τ' : ℝ
h : Tendsto (fun n ↦ (⇑f)^[n] 0 / ↑n) atTop (𝓝 τ')
⊢ Tendsto f.transnumAuxSeq atTop (𝓝 τ')

Tactic:
by
    simpa [Function.comp_def, transnumAuxSeq_def, coe_pow] using
      h.comp (tendsto_pow_atTop_atTop_of_one_lt one_lt_two)

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: G : Type u_1
inst✝¹¹ : Group G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : ContinuousInv G
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : MulAction G X
inst✝³ : ContinuousSMul G X
g : G
hg : DenseRange fun x ↦ g ^ x
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul G X μ
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
s : Set X
hsm : MeasurableSet s
hs : (fun x ↦ g • x) ⁻¹' s = s
⊢ g⁻¹ ∈ MulAction.aestabilizer G μ s

Tactic:
MulAction.mem_aestabilizer,

Goal state after:
G : Type u_1
inst✝¹¹ : Group G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : ContinuousInv G
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : MulAction G X
inst✝³ : ContinuousSMul G X
g : G
hg : DenseRange fun x ↦ g ^ x
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul G X μ
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
s : Set X
hsm : MeasurableSet s
hs : (fun x ↦ g • x) ⁻¹' s = s
⊢ g⁻¹ • s =ᵐ[μ] s
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:
by rw [neg_add, map_add]

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty
n✝ : Set β
hn : n✝ ∈ 𝓝 y
U✝ : Set τ
hu : U✝ ∈ f
w✝¹ : τ
ht : w✝¹ ∈ U✝
w✝ : α
hx : w✝ ∈ s
left✝ : ϕ w✝¹ w✝ ∈ n✝
⊢ w✝ ∈ ϕ w✝¹ ⁻¹' n✝

Tactic:
mem_preimage

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty
n✝ : Set β
hn : n✝ ∈ 𝓝 y
U✝ : Set τ
hu : U✝ ∈ f
w✝¹ : τ
ht : w✝¹ ∈ U✝
w✝ : α
hx : w✝ ∈ s
left✝ : ϕ w✝¹ w✝ ∈ n✝
⊢ ϕ w✝¹ w✝ ∈ n✝
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
x : α
y : β
⊢ (∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, x ∈ ϕ t ⁻¹' n) ↔ ∀ s ∈ 𝓝 y, ∃ᶠ (a : τ) in f, ϕ a x ∈ s

Tactic:
mem_preimage

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case mp
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ (s₁ ∪ s₂) → y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂

Tactic:
simp only [mem_union, mem_omegaLimit_iff_frequently, union_inter_distrib_right, union_nonempty,
      frequently_or_distrib]
    contrapose!
    simp only [← subset_empty_iff]
    rintro ⟨⟨n₁, hn₁, h₁⟩, ⟨n₂, hn₂, h₂⟩⟩
    refine ⟨n₁ ∩ n₂, inter_mem hn₁ hn₂, h₁.mono fun t ↦ ?_, h₂.mono fun t ↦ ?_⟩
    exacts [Subset.trans <| inter_subset_inter_right _ <| preimage_mono inter_subset_left,
      Subset.trans <| inter_subset_inter_right _ <| preimage_mono inter_subset_right]

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case htc
τ : 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), IsCompact (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s))

Tactic:
intro
    apply hc₁.of_isClosed_subset isClosed_closure
    grw [inter_subset_right, hv₂]

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
inst✝ : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
n : ℕ
V : SetRel X X
V_uni : V ∈ 𝓤 X
V_symm : V.IsSymm
V_U : V ○ V ⊆ U
s : Finset X
left✝ : ∀ x ∈ s, x ∈ F
s_cover : F ⊆ ⋃ x ∈ s, ball x V
this : IsDynCoverOf T F V 1 ↑s
t : Finset X
t_dyncover : IsDynCoverOf T F (V ○ V) (1 * n) ↑t
t_card : #t ≤ #s ^ n
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Tactic:
rw [one_mul n] at t_dyncover

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst✝ : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
n : ℕ
V : SetRel X X
V_uni : V ∈ 𝓤 X
V_symm : V.IsSymm
V_U : V ○ V ⊆ U
s : Finset X
left✝ : ∀ x ∈ s, x ∈ F
s_cover : F ⊆ ⋃ x ∈ s, ball x V
this : IsDynCoverOf T F V 1 ↑s
t : Finset X
t_dyncover : IsDynCoverOf T F (V ○ V) n ↑t
t_card : #t ≤ #s ^ n
⊢ ∃ s, IsDynCoverOf T F U n ↑s
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
⊢ ∀ᵐ (a : α) ∂ν, μ.rnDeriv ν a ≠ 0 → p a

Tactic:
by
  rw [ν.haveLebesgueDecomposition_add μ, ae_add_measure_iff]
  constructor
  · rw [← ν.haveLebesgueDecomposition_add μ]
    have : ∀ᵐ x ∂(ν.singularPart μ), μ.rnDeriv ν x = 0 := μ.rnDeriv_eq_zero_ae_singularPart ν
    filter_upwards [this] with x hx h_absurd using absurd hx h_absurd
  · have h_ac : μ.withDensity (ν.rnDeriv μ) ≪ μ := withDensity_absolutelyContinuous _ _
    rw [← ν.haveLebesgueDecomposition_add μ]
    suffices ∀ᵐx ∂μ, μ.rnDeriv ν x ≠ 0 → p x from h_ac this
    filter_upwards [h] with _ h _ using h

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ ∫⁻ (x : α) in Set.univ, μ.rnDeriv ν x ∂ν = μ Set.univ

Tactic:
setLIntegral_rnDeriv' hμν MeasurableSet.univ

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ μ Set.univ = μ Set.univ
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

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

Tactic:
withDensity_apply',

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
h : μ.rnDeriv ν ≤ᵐ[ν] 1
s : Set α
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν ≤ ν s
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
⊢ σ * τ = τ * σ

Tactic:
ext a ha

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 ∈ (X ^ n - 1).rootSet (X ^ n - 1).SplittingField
⊢ (σ * τ) a = (τ * σ) a
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✝¹ : ν₁.HaveLebesgueDecomposition μ
inst✝ : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ ν₁ ∗ₘ ν₂ = (0, ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ).1 + μ.withDensity (0, ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ).2

Tactic:
simpa using mconv_eq_withDensity_mlconvolution_rnDeriv hν₁ hν₂

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case h
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := ⋯
hs : map i (X ^ n - C a) = (Multiset.map (fun x ↦ X - C x) s).prod
hs' : s.card = n
⊢ map i (X ^ n - 1) =
    C (i (X ^ n - 1).leadingCoeff) * (Multiset.map (fun x ↦ X - C x) (Multiset.map (fun c ↦ c / b) s)).prod

Tactic:
rw [leadingCoeff_X_pow_sub_one hn', map_one, C_1, one_mul, Multiset.map_map]

Goal state after:
case h
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (map i (X ^ n - C a)).roots
hs : map i (X ^ n - C a) = (Multiset.map (fun x ↦ X - C x) s).prod
hs' : s.card = n
⊢ map i (X ^ n - 1) = (Multiset.map ((fun x ↦ X - C x) ∘ fun c ↦ c / b) s).prod
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
α : Type w'
⊢ lift.{w', max u v} L.card + lift.{max u v, w'} (constantsOn α).card =
    lift.{w', max u v} L.card + lift.{max u v, w'} #α

Tactic:
card_constantsOn

Goal state after:
L : Language
α : Type w'
⊢ lift.{w', max u v} L.card + lift.{max u v, w'} #α = lift.{w', max u v} L.card + lift.{max u v, w'} #α
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case all
L : Language
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : (LHom.id L).onBoundedFormula f✝ = id f✝
⊢ (LHom.id L).onBoundedFormula f✝.all = id f✝.all

Tactic:
rw [onBoundedFormula, ih3, id, id]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case falsum
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
n✝ : ℕ
xs : Fin (n✝ + n') → M
hmn : m ≤ n✝
⊢ (mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) falsum).Realize v xs ↔
    falsum.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n')

Tactic:
simp [mapTermRel, Realize]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.refine_1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f✝ : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M},
    m ≤ k + 1 →
      ((mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m ≤ k
h : k + 1 + n' = k + n' + 1
x : M
⊢ snoc xs x (Fin.cast h (if k < m then castAdd n' (last k) else (last k).addNat n')) = x

Tactic:
refine (congr rfl (Fin.ext ?_)).trans (snoc_last _ _)

Goal state after:
case all.refine_1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f✝ : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M},
    m ≤ k + 1 →
      ((mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m ≤ k
h : k + 1 + n' = k + n' + 1
x : M
⊢ ↑(Fin.cast h (if k < m then castAdd n' (last k) else (last k).addNat n')) = ↑(last (k + n'))
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case inr
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
p : ℕ
hp : p ∈ {q | Nat.Prime q}
⊢ Nonempty { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ∼(eqZero p) }

Tactic:
refine ⟨⟨{⟨p, hp⟩}, ?_⟩⟩
      rintro ⟨q, _⟩ hq ⟨K⟩ _ _
      have hqp : q ≠ p := by simpa [← Nat.Primes.coe_nat_inj] using hq
      let _ := fieldOfModelACF q K
      have := modelField_of_modelACF q K
      let _ := compatibleRingOfModelField K
      have := charP_of_model_fieldOfChar q K
      simp only [eqZero, Term.equal, BoundedFormula.realize_not, BoundedFormula.realize_bdEqual,
        Term.realize_relabel, Sum.elim_comp_inl, realize_termOfFreeCommRing, map_natCast,
        realize_zero, ← CharP.charP_iff_prime_eq_zero hp]
      intro _
      exact hqp <| CharP.eq K this inferInstance

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case refine_2.inr.inr
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
⊢ a ∣ b ∨ a ∣ c

pp: a✝ a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
⊢ a ∣ b ∨ a ∣ c

Tactic:
· cases le_total c b <;> [solve_by_elim; rw [or_comm]]
    apply_assumption
    assumption'
    all_goals rwa [mul_comm]

Goal state after:
a✝ a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
⊢ a ∣ b ∨ a ∣ c
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: k : Type u_1
inst✝⁶ : Field k
inst✝⁵ : Finite k
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP k p
l : Type u_2
inst✝² : Field l
inst✝¹ : Algebra k l
inst✝ : Finite l
g : Gal(l/k)
⊢ ∃ i, ∀ (x : l), g x = x ^ Nat.card k ^ i

Tactic:
by
  let n := Module.finrank k l
  have : NeZero n := NeZero.of_pos Module.finrank_pos
  obtain ⟨i, _, hi⟩ := Extension.exists_frob_pow_eq k p n <|
    (algEquivExtension k p n l rfl).symm.trans (g.trans (algEquivExtension k p n l rfl))
  refine ⟨i, fun x ↦ ?_⟩
  simpa using (AlgEquiv.congr_arg (f := (algEquivExtension k p n l rfl).symm) <|
    AlgEquiv.congr_fun hi (algEquivExtension k p n l rfl x)).symm

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
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
c₀ : ι → F := fun i ↦ c i / ↑(Fintype.card Gal(K/F))
u₁ : ι → K := fun i ↦ ∏ x, x (u i)
ffb : fixedField ⊤ = ⊥
u₀ : ι → F
hu₀ : ∀ (i : ι), (algebraMap F K) (u₀ i) = u₁ i
v₁ : K := (∑ x, x v) / ↑(Fintype.card Gal(K/F))
⊢ ∃ ι₀ x c₀, ∃ (_ : ∀ (x : ι₀), (c₀ x)′ = 0), ∃ u₀ v₀, a = ∑ x, c₀ x * logDeriv (u₀ x) + v₀′

Tactic:
have : v₁ ∈ fixedField (⊤ : Subgroup (K ≃ₐ[F] K)) := by
      rintro ⟨e, _⟩
      change e v₁ = v₁
      simp only [v₁, map_div₀, map_sum, map_natCast]
      congr 1
      apply Fintype.sum_equiv (Equiv.mulLeft e)
      simp

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
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
c₀ : ι → F := fun i ↦ c i / ↑(Fintype.card Gal(K/F))
u₁ : ι → K := fun i ↦ ∏ x, x (u i)
ffb : fixedField ⊤ = ⊥
u₀ : ι → F
hu₀ : ∀ (i : ι), (algebraMap F K) (u₀ i) = u₁ i
v₁ : K := (∑ x, x v) / ↑(Fintype.card Gal(K/F))
this : v₁ ∈ fixedField ⊤
⊢ ∃ ι₀ x c₀, ∃ (_ : ∀ (x : ι₀), (c₀ x)′ = 0), ∃ u₀ v₀, a = ∑ x, c₀ x * logDeriv (u₀ x) + v₀′
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))

pp: 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

Tactic:
case h => simp

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)) + (∑ x, x v)′ / ↑(Fintype.card Gal(K/F))