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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Refl R
a : Option (α × WSeq α)
⊢ LiftRelO R (fun x1 x2 ↦ x1 = x2) a a

Tactic:
by
    rcases a with - | a
    · simp
    · cases a
      simp only [LiftRelO, and_true]
      apply refl_of R

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

Goal state before:
pp: α : Type u
s : WSeq α
a : α
h : some a ∈ s.tail.head
⊢ ∃ a', some a' ∈ s.head

Tactic:
unfold head at h
  rcases Computation.exists_of_mem_map h with ⟨o, md, e⟩; clear h
  rcases o with - | o <;> [injection e; injection e with h']; clear h'
  obtain ⟨a, am⟩ := destruct_some_of_destruct_tail_some md
  exact ⟨_, Computation.mem_map (@Prod.fst α (WSeq α) <$> ·) am⟩

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

Goal state before:
pp: case left
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨j, b⟩

pp: case right
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩

Tactic:
· obtain ⟨k, hi, hj⟩ := exists_between h
      obtain ⟨c⟩ : Nonempty (α k) := inferInstance
      exact ⟨⟨k, c⟩, left _ _ hi, left _ _ hj⟩

Goal state after:
case right
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMinOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ ∀ (a : Σₗ (i : ι), α i), ∃ b, b < a

Tactic:
rintro ⟨i, a⟩
    obtain ⟨j, h⟩ := exists_lt i
    obtain ⟨b⟩ : Nonempty (α j) := inferInstance
    exact ⟨⟨j, b⟩, left _ _ h⟩

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

Goal state before:
pp: case refine_2.inl.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
val✝¹ : α₁
val✝ : β₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inl val✝¹ = inl a₁ → inl val✝ = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inl val✝¹ = inr a₂ → inl val✝ = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inl val✝¹) (inl val✝) = ∅

pp: case refine_2.inl.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
val✝¹ : α₁
val✝ : β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inl val✝¹ = inl a₁ → inr val✝ = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inl val✝¹ = inr a₂ → inr val✝ = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inl val✝¹) (inr val✝) = ∅

pp: case refine_2.inr.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
val✝¹ : α₂
val✝ : β₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val✝¹ = inl a₁ → inl val✝ = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inr val✝¹ = inr a₂ → inl val✝ = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inr val✝¹) (inl val✝) = ∅

pp: case refine_2.inr.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
val✝¹ : α₂
val✝ : β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val✝¹ = inl a₁ → inr val✝ = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inr val✝¹ = inr a₂ → inr val✝ = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inr val✝¹) (inr val✝) = ∅

Tactic:
· exact map_eq_empty.2 (h.1 _ _ rfl rfl)

Goal state after:
case refine_2.inl.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
val✝¹ : α₁
val✝ : β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inl val✝¹ = inl a₁ → inr val✝ = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inl val✝¹ = inr a₂ → inr val✝ = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inl val✝¹) (inr val✝) = ∅

case refine_2.inr.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
val✝¹ : α₂
val✝ : β₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val✝¹ = inl a₁ → inl val✝ = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inr val✝¹ = inr a₂ → inl val✝ = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inr val✝¹) (inl val✝) = ∅

case refine_2.inr.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
val✝¹ : α₂
val✝ : β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val✝¹ = inl a₁ → inr val✝ = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inr val✝¹ = inr a₂ → inr val✝ = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inr val✝¹) (inr val✝) = ∅
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 : ∀ᶠ (ε : ℝ≥0∞) in 𝓝 0, ε < μ ((⇑(f z) ⁻¹' t) ∆ s)
w : Z
hw : μ ((⇑(f w) ⁻¹' t) ∆ (⇑(f z) ⁻¹' t)) < μ ((⇑(f z) ⁻¹' t) ∆ s)
⊢ w ∈ {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}ᶜ

Tactic:
intro (hw' : f w ⁻¹' t =ᵐ[μ] s)

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 : ∀ᶠ (ε : ℝ≥0∞) in 𝓝 0, ε < μ ((⇑(f z) ⁻¹' t) ∆ s)
w : Z
hw : μ ((⇑(f w) ⁻¹' t) ∆ (⇑(f z) ⁻¹' t)) < μ ((⇑(f z) ⁻¹' t) ∆ s)
hw' : ⇑(f w) ⁻¹' t =ᵐ[μ] s
⊢ False
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: case inl
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ closedBall x ε =ᵐ[volume] ball x ε

Tactic:
rw [ball_eq_empty.mpr hε, ae_eq_empty, volume_closedBall,
      min_eq_right (by linarith [hT.out] : 2 * ε ≤ T), ENNReal.ofReal_eq_zero]

Goal state after:
case inl
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ 2 * ε ≤ 0
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
⊢ ∀ᵐ (x : α) ∂μ, ∀ (k : ℕ), f^[k] x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
by
  refine ae_all_iff.2 fun k => ?_
  refine (hf.ae_mem_imp_frequently_image_mem
    (hs.preimage <| hf.toQuasiMeasurePreserving.iterate k)).mono fun x hx hk => ?_
  rw [← map_add_atTop_eq_nat k, frequently_map]
  refine (hx hk).mono fun n hn => ?_
  rwa [add_comm, iterate_add_apply]

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

Goal state before:
pp: case a
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
| x

pp: case a
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
| DivisibleBy.div x (n - 1)

Tactic:
rw [← DivisibleBy.div_cancel x h]

Goal state after:
case a
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
| (n - 1) • DivisibleBy.div x (n - 1)

case a
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
| DivisibleBy.div x (n - 1)
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: case inr
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
this : (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν ∘ f =ᵐ[ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
hμν : ¬μ ≪ ν
⊢ μ.rnDeriv ν =ᵐ[ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν

Tactic:
exact (rnDeriv_withDensity ν (measurable_rnDeriv μ ν)).symm

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂μ, 0 < μ.rnDeriv ν x

Tactic:
by
  rw [← Measure.withDensity_rnDeriv_eq _ _ hμν,
    ae_withDensity_iff (Measure.measurable_rnDeriv _ _), Measure.withDensity_rnDeriv_eq _ _ hμν]
  exact ae_of_all _ (fun x hx ↦ hx.pos)

Goal state after:
Module: Mathlib.Dynamics.FixedPoints.Support

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
f : X → X
inst✝ : R1Space X
⊢ HasCompactFixedSupport f ↔ ∃ K, IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K

Tactic:
rw [HasCompactFixedSupport_iff']
  refine ⟨fun ⟨K, hK₁, hK₂, hf⟩ ↦ ⟨K, hK₂, hf⟩, fun ⟨K, hK, hf⟩ ↦ ?_⟩
  exact ⟨closure K, isClosed_closure, hK.closure, hf.trans subset_closure⟩

Goal state after:
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : T1Space A
p : Pattern A G
g : G
⊢ IsClosed[Pi.topologicalSpace] {x | p.mulOccursInAt x g}

Tactic:
simpa [mulOccursInAt_eq_cylinder] using isClosed_cylinder _ _

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case h.left
τ : 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
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x1 x2 ↦ x1 ⊇ x2) ((fun i ↦ closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)) ⟨u₁, hu₁⟩)
    ((fun i ↦ closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)) ⟨u₁ ∩ u₂, ⋯⟩)

Tactic:
exact closure_mono (image2_subset (inter_subset_inter_left _ (by simp)) Subset.rfl)

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case h.right
τ : 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
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x1 x2 ↦ x1 ⊇ x2) ((fun i ↦ closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)) ⟨u₂, hu₂⟩)
    ((fun i ↦ closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)) ⟨u₁ ∩ u₂, ⋯⟩)

Tactic:
exact closure_mono (image2_subset (inter_subset_inter_left _ (by simp)) Subset.rfl)

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

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

Tactic:
suffices ∀ᵐx ∂μ, μ.rnDeriv ν x ≠ 0 → p x from h_ac this

Goal state after:
case right
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
h_ac : μ.withDensity (ν.rnDeriv μ) ≪ μ
⊢ ∀ᵐ (x : α) ∂μ, μ.rnDeriv ν x ≠ 0 → p x
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
⊢ netEntropyInfEntourage T F univ = 0

Tactic:
← expGrowthInf_const one_ne_zero one_ne_top,

Goal state after:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
⊢ netEntropyInfEntourage T F univ = expGrowthInf fun x ↦ 1
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = ∫ (x : α) in Set.univ, (μ.rnDeriv ν x).toReal ∂ν

Tactic:
setIntegral_univ

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
⊢ coverEntropyInfEntourage T F univ = 0

Tactic:
← expGrowthInf_const one_ne_zero one_ne_top,

Goal state after:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
⊢ coverEntropyInfEntourage T F univ = expGrowthInf fun x ↦ 1
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
a : α
h4 : 1 = (μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)) a
h5 : (μ + ν).rnDeriv (μ + ν) a = 1
h6 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹

Tactic:
Pi.add_apply

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
a : α
h4 : 1 = μ.rnDeriv (μ + ν) a + ν.rnDeriv (μ + ν) a
h5 : (μ + ν).rnDeriv (μ + ν) a = 1
h6 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case pos
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
⊢ Group.IsSolvable (X ^ n - C a).Gal

Tactic:
rw [hn, pow_zero, ← C_1, ← C_sub]

Goal state after:
case pos
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
⊢ Group.IsSolvable (C (1 - a)).Gal
Module: Mathlib.RingTheory.Algebraic.Cardinality

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : IsTorsionFree R L
inst✝ : Algebra.IsAlgebraic R L
x y : L
h :
  ↑(Classical.indefiniteDescription (fun x_1 ↦ ¬x_1 = 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯) =
      ↑(Classical.indefiniteDescription (fun x ↦ ¬x = 0 ∧ (Polynomial.aeval y) x = 0) ⋯) ∧
    ⟨x, ⋯⟩ ≍ ⟨y, ⋯⟩
⊢ ∀ (x_1 : L),
    x_1 ∈ (↑(Classical.indefiniteDescription (fun x_2 ↦ ¬x_2 = 0 ∧ (Polynomial.aeval x) x_2 = 0) ⋯)).aroots L ↔
      x_1 ∈ (↑(Classical.indefiniteDescription (fun x ↦ ¬x = 0 ∧ (Polynomial.aeval y) x = 0) ⋯)).aroots L

Tactic:
simp only [h.1, forall_true_iff]

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
K' : Type u
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsAlgClosed K'
ι' : Type u
v' : ι' → K'
hv : IsTranscendenceBasis R v'
⊢ #K' ≤ max (max #R #ι') ℵ₀

Tactic:
simpa using cardinal_le_max_transcendence_basis v' hv

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case all
L : Language
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (h : n✝ + 1 ≤ n✝ + 1), castLE h f✝ = f✝
h : n✝ ≤ n✝
⊢ castLE h f✝.all = f✝.all

Tactic:
| all _ ih3 =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case all
L : Language
α : Type u'
k n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {m n : ℕ} (km : n✝ + 1 ≤ m) (mn : m ≤ n), castLE mn (castLE km f✝) = castLE ⋯ f✝
⊢ ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km f✝.all) = castLE ⋯ f✝.all

Tactic:
| all _ ih3 =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case all
L : Language
L' : Language
α : Type u'
β : Type v'
γ : Type u_1
L'' : Language
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
ft' : (n : ℕ) → L'.Term (β ⊕ Fin n) → L''.Term (γ ⊕ Fin n)
fr' : (n : ℕ) → L'.Relations n → L''.Relations n
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 :
  mapTermRel ft' fr' (fun x ↦ id) (mapTermRel ft fr (fun x ↦ id) f✝) =
    mapTermRel (fun x ↦ ft' x ∘ ft x) (fun x ↦ fr' x ∘ fr x) (fun x ↦ id) f✝
⊢ mapTermRel ft' fr' (fun x ↦ id) (mapTermRel ft fr (fun x ↦ id) f✝.all) =
    mapTermRel (fun x ↦ ft' x ∘ ft x) (fun x ↦ fr' x ∘ fr x) (fun x ↦ id) f✝.all

Tactic:
| all _ ih3 =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

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

Tactic:
| all _ ih3 =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case all
L : Language
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : mapTermRel (fun x t ↦ Term.relabel (Sum.map id (natAdd 0)) t) (fun x ↦ id) (fun x ↦ castLE ⋯) f✝ = castLE ⋯ f✝
⊢ mapTermRel (fun x t ↦ Term.relabel (Sum.map id (natAdd 0)) t) (fun x ↦ id) (fun x ↦ castLE ⋯) f✝.all = castLE ⋯ f✝.all

Tactic:
| all _ ih3 =>

Goal state after:
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:
| all _ ih3 =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case all
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : (φ.comp ψ).onBoundedFormula f✝ = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f✝
⊢ (φ.comp ψ).onBoundedFormula f✝.all = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f✝.all

Tactic:
| all _ ih3 =>

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case all.h₁
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin k → (a : α) → M a
⊢ (∀ (x_1 : Quotient ((↑u).productSetoid M)),
      φ.Realize (fun i ↦ Quotient.mk' (x i)) (Fin.snoc (fun i ↦ Quotient.mk' (v i)) x_1)) ↔
    ∀ (m : (a : α) → M a), φ.Realize (fun i ↦ Quotient.mk' (x i)) (Fin.snoc (Quotient.mk' ∘ v) (Quotient.mk' m))

Tactic:
exact Quotient.forall

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.refine_2
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
i : Fin k
⊢ snoc xs x (Fin.cast h (if ↑i.castSucc < m then castAdd n' i.castSucc else i.castSucc.addNat n')) =
    xs (if ↑i < m then castAdd n' i else i.addNat n')

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

Goal state after:
case all.refine_2
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
i : Fin k
⊢ ↑(Fin.cast h (if ↑i.castSucc < m then castAdd n' i.castSucc else i.castSucc.addNat n')) =
    ↑(if ↑i < m then castAdd n' i else i.addNat n').castSucc
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 :
  ∀ {f : ↥f✝.freeVarFinset → β} {xs : Fin (n✝ + 1) → M},
    (∀ (a : ↥f✝.freeVarFinset), v (f a) = v' ↑a) → ((f✝.restrictFreeVar f).Realize v xs ↔ f✝.Realize v' xs)
f : ↥(∀' f✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(∀' f✝).freeVarFinset), v (f a) = v' ↑a
⊢ ((∀' f✝).restrictFreeVar f).Realize v xs ↔ (∀' f✝).Realize v' xs

Tactic:
| all _ ih3 =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
n : ℕ
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, (φ.onBoundedFormula f✝).Realize v xs ↔ f✝.Realize v xs
xs : Fin n✝ → M
⊢ (φ.onBoundedFormula (∀' f✝)).Realize v xs ↔ (∀' f✝).Realize v xs

Tactic:
| all _ ih3 =>

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝⁴ : L.Structure M
inst✝³ : L.Structure N
inst✝² : L.Structure P
S✝ : L.Substructure M
L' : Language
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
S : L'.Substructure M
n : ℕ
f : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ ↑S
h : funMap (φ.onFunction f) x ∈ ↑S
⊢ funMap f x ∈ ↑S

Tactic:
simp only [LHom.map_onFunction, Substructure.mem_carrier] at h

Goal state after:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝⁴ : L.Structure M
inst✝³ : L.Structure N
inst✝² : L.Structure P
S✝ : L.Substructure M
L' : Language
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
S : L'.Substructure M
n : ℕ
f : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ ↑S
h : funMap f x ∈ S
⊢ funMap f x ∈ ↑S
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 (⋂ i ∈ s, f i)

Tactic:
rw [← Finset.inf_set_eq_iInter]

Goal state after:
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)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
⊢ (∀' f✝).toFormula.Realize v ↔ (∀' f✝).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
| all _ ih3 =>

Goal state after:
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
⊢ ℵ₀ ≤ sum fun i ↦ #(L.BoundedFormula Empty (i + 1))

Tactic:
· rw [← mk_sigma]
    exact infinite_iff.1 (Infinite.of_injective (fun n => ⟨n, ⊥⟩) fun x y xy =>
      (Sigma.mk.inj_iff.1 xy).1)

Goal state after: