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

Goal state before:
pp: case some
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
a' : α
s' : WSeq α
om : some (a', s') ∈ (s.drop n).destruct
i : a' = a
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct

Tactic:
rw [i] at om

Goal state after:
case some
α : Type u
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ s.get? n
a' : α
s' : WSeq α
om : some (a, s') ∈ (s.drop n).destruct
i : a' = a
⊢ ∃ s', some (a, s') ∈ (s.drop n).destruct
Module: Mathlib.Data.String.Lemmas

Goal state before:
pp: n : ℕ
c : Char
x✝ : String
s : String := x✝
⊢ (replicate (n - x✝.length) c).IsPrefix (leftpad n c x✝)

Tactic:
by simp [leftpad, IsPrefix, replicate, length_toList]

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
xs : Vector α n
f : α → β
⊢ map f xs = (mapAccumr (fun x x_1 ↦ ((), f x)) xs ()).2

Tactic:
by
  induction xs using Vector.revInductionOn <;> simp_all

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

Goal state before:
pp: f : CircleDeg1Lift
n : ℕ
⊢ Function.Commute ⇑f fun x ↦ x + ↑-[n+1]

Tactic:
by simpa [sub_eq_add_neg] using f.commute_sub_nat (n + 1)

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

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ x + ↑n * ↑m ≤ (⇑f)^[n] x ↔ x + ↑m ≤ f x

Tactic:
simpa only [not_lt] using not_congr (f.iterate_pos_lt_iff hn)

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

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun n ↦ ((f ^ n) x - x) / ↑n) atTop
    (𝓝 (τ (↑(translate (Multiplicative.ofAdd x))⁻¹ * f * ↑(translate (Multiplicative.ofAdd x)))))

Tactic:
refine (tendsto_translation_number₀ _).congr fun n ↦ ?_

Goal state after:
f : CircleDeg1Lift
x : ℝ
n : ℕ
⊢ ((↑(translate (Multiplicative.ofAdd x))⁻¹ * f * ↑(translate (Multiplicative.ofAdd x))) ^ n) 0 / ↑n =
    ((f ^ n) x - x) / ↑n
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}ᶜ
⊢ {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}ᶜ ∈ 𝓝 z

Tactic:
replace hz : ∀ᶠ ε : ℝ≥0∞ in 𝓝 0, ε < μ ((f z ⁻¹' t) ∆ s) := by
    apply gt_mem_nhds
    rwa [pos_iff_ne_zero, ne_eq, measure_symmDiff_eq_zero_iff]

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)
⊢ {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}ᶜ ∈ 𝓝 z
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: 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))
hI : I =ᵐ[volume] B
⊢ IsAddFundamentalDomain (↥G) I volume

Tactic:
have hn : 1 ≤ (n : ℝ) := by norm_cast; linarith [hu.addOrderOf_pos]

Goal state after:
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))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
⊢ IsAddFundamentalDomain (↥G) I volume
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
h : μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ IsProbabilityMeasure ν}
⊢ μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = 1}

Tactic:
simpa only [isProbabilityMeasure_iff] using h

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
hμ'ν : μ' ≪ ν
⊢ (μ.withDensity f).rnDeriv ν =ᵐ[ν] fun x ↦ f x * μ.rnDeriv ν x

Tactic:
have h := rnDeriv_withDensity_left_of_absolutelyContinuous hμ'ν hfν

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
hμ'ν : μ' ≪ ν
h : (μ'.withDensity f).rnDeriv ν =ᵐ[ν] fun x ↦ f x * μ'.rnDeriv ν x
⊢ (μ.withDensity f).rnDeriv ν =ᵐ[ν] fun x ↦ f x * μ.rnDeriv ν x
Module: Mathlib.Dynamics.Flow

Goal state before:
pp: τ : Type u_1
α : Type u_2
ϕ : τ → α → α
s : Set α
⊢ IsInvariant ϕ s ↔ ∀ (t : τ), ϕ t '' s ⊆ s

Tactic:
by
  simp_rw [IsInvariant, mapsTo_iff_image_subset]

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

Goal state before:
pp: A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
hmem : v * w ∈ Finset.image (fun x ↦ v * x) p.support
ex : ∃ w' ∈ p.support, v * w' = v * w
⊢ p.mulShift v (v * w) = p.config w

Tactic:
have h1 : p.mulShift v (v * w) = p.config (Classical.choose ex) := by
    simp [Pattern.mulShift, hmem]

Goal state after:
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
hmem : v * w ∈ Finset.image (fun x ↦ v * x) p.support
ex : ∃ w' ∈ p.support, v * w' = v * w
h1 : p.mulShift v (v * w) = p.config (Classical.choose ex)
⊢ p.mulShift v (v * w) = p.config w
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
⊢ μ = 0 + (ν.withDensity f).withDensity fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x

Tactic:
ext1 s hs
    conv_lhs => rw [← Measure.withDensity_rnDeriv_eq _ _ hμν]
    rw [zero_add, withDensity_apply _ hs, withDensity_apply _ hs]
    rw [setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]
    · simp only [Pi.mul_apply]
      have : (fun a ↦ f a * ((f a)⁻¹ * μ.rnDeriv ν a)) =ᵐ[ν] μ.rnDeriv ν := by
        filter_upwards [hf_ne_zero, hf_ne_top] with x hx1 hx2
        simp [← mul_assoc, ENNReal.mul_inv_cancel, hx1, hx2]
      rw [lintegral_congr_ae (ae_restrict_of_ae this)]
    · refine ae_restrict_of_ae ?_
      filter_upwards [hf_ne_top] with x hx using hx.lt_top
    · exact hf.restrict

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h✝ : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h✝.nullSet
ht : MeasurableSet t
h : (μ.restrict t).rnDeriv ν' =ᵐ[ν] t.indicator (μ.rnDeriv ν')
x : α
hx : (μ.restrict t).rnDeriv ν' x = t.indicator (μ.rnDeriv ν') x
hxt : x ∈ t
⊢ μ.rnDeriv ν' x = (μ.restrict t).rnDeriv ν' x

Tactic:
rw [hx, Set.indicator_of_mem hxt]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x = 0

Tactic:
by
  refine rnDeriv_eq_zero_of_mutuallySingular (mutuallySingular_singularPart ν μ).symm ?_
  exact (Measure.singularPart_le _ _).absolutelyContinuous

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 α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
v : Set τ
hn₂ : ⋂ u, closure[inst✝] (image2 ϕ (↑u ∩ v) s) ⊆ n
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ ⋂ i, k ∩ closure[inst✝] (image2 ϕ (↑i ∩ v) s) ⊆ n

Tactic:
← inter_iInter

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
v : Set τ
hn₂ : ⋂ u, closure[inst✝] (image2 ϕ (↑u ∩ v) s) ⊆ n
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ k ∩ ⋂ i, closure[inst✝] (image2 ϕ (↑i ∩ v) s) ⊆ n
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inr.inl
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
h : IsDynCoverOf T F U 0 ↑s
⊢ ∃ t, IsDynCoverOf T F (U ○ U) (0 * n) ↑t ∧ #t ≤ #s ^ n

Tactic:
use {x}
    simp only [zero_mul, Finset.coe_singleton, Finset.card_singleton]
    exact ⟨isDynCoverOf_zero T F (U ○ U) (singleton_nonempty x),
      one_le_pow_of_one_le' (Nat.one_le_of_lt (Finset.Nonempty.card_pos s_nemp)) n⟩

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 α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
hj₂ : k \ n ⊆ ⋃ u ∈ f, j u
g : Set (Set τ)
hg₁ : ∀ u ∈ g, u ∈ f
hg₂ : g.Finite
hg₃ : k \ n ⊆ ⋃ i ∈ g, j i
w : Set τ := (⋂ u ∈ g, u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ (closure[inst✝] (image2 ϕ w s))ᶜ
⊢ closure[inst✝] (image2 ϕ w s) ⊆ k

Tactic:
exact closure_mono (image2_subset inter_subset_right Subset.rfl)

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
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
V : SetRel X X
hV : V ∈ 𝓤 X
hVsymm : V.IsSymm
hVU : V ⊆ U
uni_ite : dynEntourage T V n ∈ 𝓤 X
openCover : X → Set X := fun x ↦ ball x (dynEntourage T V n)
s : Finset X
left✝ : ∀ x ∈ s, x ∈ F
s_cover : F ⊆ ⋃ x ∈ s, openCover x
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Tactic:
exact ⟨s, .of_entourage_subset hVU <| .of_subset_iUnion_ball s_cover⟩

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

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
inst✝ : V.IsSymm
n : ℕ
h' : coverMincard T (φ '' F) V n < ⊤
t : Finset Y
t_cover : IsDynCoverOf T (φ '' F) V n ↑t
t_card : ↑t.card = coverMincard T (φ '' F) V n
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n

Tactic:
obtain ⟨s, s_cover, s_card⟩ := t_cover.preimage h

Goal state after:
case inr
X : Type u_1
Y : Type u_2
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
inst✝ : V.IsSymm
n : ℕ
h' : coverMincard T (φ '' F) V n < ⊤
t : Finset Y
t_cover : IsDynCoverOf T (φ '' F) V n ↑t
t_card : ↑t.card = coverMincard T (φ '' F) V n
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s
s_card : s.card ≤ t.card
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
n : ℕ
x : X
h✝ : x ∈ F
⊢ coverMincard T F univ n ≤ 1

Tactic:
have := isDynCoverOf_univ T F n (singleton_nonempty x)

Goal state after:
X : Type u_1
F : Set X
T : X → X
n : ℕ
x : X
h✝ : x ∈ F
this : IsDynCoverOf T F univ n {x}
⊢ coverMincard T F univ n ≤ 1
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
h✝ : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : ↑s.card = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ ↑s, ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
larger_net : IsDynNetIn T F U n ↑(insert x s)
x_s : x ∈ s
⊢ False

Tactic:
exact x_uncov x x_s (ball_mono (dynEntourage_monotone T n SetRel.left_subset_comp) x <|
    SetRel.rfl (dynEntourage T U n))

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 : ℕ
inst✝ : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n ↑s
h' : ↑(#s) = coverMincard T F U n
⊢ ∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty

Tactic:
classical
  by_contra! ⟨x, x_s, ball_empt⟩
  have smaller_cover : IsDynCoverOf T F U n (s.erase x) := by
    intro y y_F
    specialize h y_F
    simp only [s.mem_coe] at h
    simp only [s.coe_erase, mem_sdiff, s.mem_coe, mem_singleton_iff]
    obtain ⟨z, z_s, hz⟩ := h
    refine ⟨z, ⟨z_s, fun z_x ↦ notMem_empty y ?_⟩, hz⟩
    rw [← ball_empt]
    rw [z_x] at hz
    exact mem_inter y_F <| (dynEntourage T U n).symm hz
  apply smaller_cover.coverMincard_le_card.not_gt
  rw [← h']
  exact_mod_cast s.card_erase_lt_of_mem x_s

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
⊢ coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F

Tactic:
by
  rw [← coverEntropyInf_restrict_subset hF hG]
  have hφ : Semiconj (G.domRestrict φ) (hG.restrict S G G) T := by
    intro a
    rw [G.domRestrict_apply, G.domRestrict_apply, hG.val_restrict_apply, h.eq a]
  apply (coverEntropyInf_image_le_of_uniformContinuous hφ
    (uniformContinuousOn_iff_restrict.1 h') (val ⁻¹' F)).trans_eq'
  rw [← image_image_val_eq_domRestrict_image, 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✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ μ.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ μ.rnDeriv ν x / (μ.rnDeriv ν x + 1)

Tactic:
by
  have h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν) :=
    (ae_add_measure_iff.mp (μ.rnDeriv_add' ν (μ + ν))).2
  have h_one_add := (ae_add_measure_iff.mp (μ + ν).rnDeriv_self).2
  have : (μ.rnDeriv (μ + ν)) =ᵐ[ν] fun x ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹ := by
    filter_upwards [h_add, h_one_add, rnDeriv_add_self ν μ] with a h4 h5 h6
    rw [h5, Pi.add_apply] at h4
    nth_rw 1 [h4, h6]
    simp
  filter_upwards [this, μ.rnDeriv_lt_top ν] with a ha ha_lt_top
  rw [ha, div_eq_mul_inv]
  refine ENNReal.sub_eq_of_eq_add (by simp) ?_
  nth_rewrite 2 [← one_mul (μ.rnDeriv ν a + 1)⁻¹]
  have h := add_mul (μ.rnDeriv ν a) 1 (μ.rnDeriv ν a + 1)⁻¹
  rwa [ENNReal.mul_inv_cancel (by simp) (by simp [ha_lt_top.ne])] at h

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ f.comp f.symm = refl L N

Tactic:
by
  ext; rw [comp_apply, apply_symm_apply, refl_apply]

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✝ S : L.Substructure M
A : Set M
h : A ⊆ ↑S
n : ℕ
f : L[[↑A]].Functions n
⊢ ClosedUnder f ↑S

Tactic:
obtain f | f := f
    · exact S.fun_mem f
    · cases n
      · exact fun _ _ => h f.2
      · exact isEmptyElim f

Goal state after:
Module: Mathlib.ModelTheory.Encoding

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

Tactic:
induction φ with
  | falsum => intro l; rw [listEncode, singleton_append, listDecode]
  | equal =>
    intro l
    rw [listEncode, cons_append, cons_append, listDecode, dif_pos]
    · simp only [eq_mp_eq_cast, cast_eq, nil_append]
    · simp only
  | @rel φ_n φ_l φ_R ts =>
    intro l
    rw [listEncode, cons_append, cons_append, singleton_append, cons_append, listDecode]
    have h : ∀ i : Fin φ_l, ((List.map Sum.getLeft? (List.map (fun i : Fin φ_l =>
      Sum.inl (⟨(⟨φ_n, rel φ_R ts⟩ : Σ n, L.BoundedFormula α n).fst, ts i⟩ :
        Σ n, L.Term (α ⊕ (Fin n)))) (finRange φ_l) ++ l))[↑i]?).join = some ⟨_, ts i⟩ := by
      intro i
      simp only [Option.join, map_append, map_map, getElem?_fin, id, Option.bind_eq_some_iff,
        getElem?_eq_some_iff, length_append, length_map, length_finRange, exists_eq_right]
      refine ⟨lt_of_lt_of_le i.2 le_self_add, ?_⟩
      rw [getElem_append_left, getElem_map]
      · simp only [getElem_finRange, cast_mk, Fin.eta, Function.comp_apply, Sum.getLeft?_inl]
      · simp only [length_map, length_finRange, is_lt]
    rw [dif_pos]
    swap
    · exact fun i => Option.isSome_iff_exists.2 ⟨⟨_, ts i⟩, h i⟩
    rw [dif_pos]
    swap
    · intro i
      obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i)
      rw [h2]
    simp only [Option.join, eq_mp_eq_cast, cons.injEq, Sigma.mk.inj_iff, heq_eq_eq, rel.injEq,
      true_and]
    refine ⟨funext fun i => ?_, ?_⟩
    · obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i)
      rw [cast_eq_iff_heq]
      exact (Sigma.ext_iff.1 ((Sigma.eta (Option.get _ h1)).trans h2)).2
    rw [List.drop_append, length_map, length_finRange, Nat.sub_self, drop, drop_eq_nil_of_le,
      nil_append]
    rw [length_map, length_finRange]
  | imp _ _ ih1 ih2 =>
    intro l
    simp only at *
    rw [listEncode, List.append_assoc, cons_append, listDecode]
    simp only [ih1, ih2, length_cons, le_add_iff_nonneg_left, _root_.zero_le, ↓reduceDIte,
      getElem_cons_zero, getElem_cons_succ, sigmaImp_apply, drop_succ_cons, drop_zero]
  | all _ ih =>
    intro l
    simp only at *
    rw [listEncode, cons_append, listDecode]
    simp only [ih, length_cons, le_add_iff_nonneg_left, _root_.zero_le, ↓reduceDIte,
      getElem_cons_zero, sigmaAll_apply, drop_succ_cons, drop_zero]

Goal state after:
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
n : ℕ
inst✝ : NeZero n
⊢ Module.finrank k (Extension k p n) = n

Tactic:
by
  refine Nat.pow_right_injective (Finite.one_lt_card : 2 ≤ Nat.card k) ?_
  simp only [← Module.natCard_eq_pow_finrank, natCard_extension]

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

Goal state before:
pp: case a
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
B : IntermediateField F K
inst✝¹ : FiniteDimensional F ↥B
inst : IsLiouville F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → ↥B
v : ↥B
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
| ∑ x, ↑(c x) * logDeriv ↑(u x)

Tactic:
rhs
        intro x
        rhs
        apply logDeriv_algebraMap (u x)

Goal state after:
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
e : Gal(L/K)
⊢ (normalBasis K L) e = e ((normalBasis K L) 1)

Tactic:
normalBasis,

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
e : Gal(L/K)
⊢ (basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯) e = e ((basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯) 1)
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L₁ L₂ L₃ : (FiniteGaloisIntermediateField k K)ᵒᵖ
f : L₁ ⟶ L₂
g : L₂ ⟶ L₃
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
iterate 2
    induction L₁ with | _ L₁ => ?_
    induction L₂ with | _ L₂ => ?_
    induction L₃ with | _ L₃ => ?_
  algebraize [Subsemiring.inclusion g.unop.le, Subsemiring.inclusion f.unop.le,
    Subsemiring.inclusion (g.unop.le.trans f.unop.le)]
  have : IsScalarTower k L₂ L₁ := IsScalarTower.of_algebraMap_eq' rfl
  have : IsScalarTower k L₃ L₁ := IsScalarTower.of_algebraMap_eq' rfl
  have : IsScalarTower k L₃ L₂ := IsScalarTower.of_algebraMap_eq' rfl
  have : IsScalarTower L₃ L₂ L₁ := IsScalarTower.of_algebraMap_eq' rfl
  ext : 1
  apply IsScalarTower.AlgEquiv.restrictNormalHom_comp k L₃ L₂ L₁

Goal state after:
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥{ toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }.toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h :
  { toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ } ≤
    { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }
this✝ : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
this : IsScalarTower k ↥L ↥L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)
⊢ ↑(((proj { toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }) g) x) =
    ↑(((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g) ⟨↑x, ⋯⟩)

Tactic:
← finGaloisGroupFunctor_map_proj_eq_proj g h.hom

Goal state after:
case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥{ toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }.toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h :
  { toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ } ≤
    { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }
this✝ : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
this : IsScalarTower k ↥L ↥L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)
⊢ ↑(((ConcreteCategory.hom ((finGaloisGroupFunctor k K).map h.hom.op))
          ((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g))
        x) =
    ↑(((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g) ⟨↑x, ⋯⟩)