mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case e'_4
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this✝ : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
p : ℕ
hp : Nat.Prime p
x : 𝕊 := u ⟨p, hp⟩
f : 𝕊 → 𝕊 := fun y ↦ p • y + x
n : ℕ
hn : 0 < n
h_ndiv : ¬p * p ∣ n
h_cop : (addOrderOf x).Coprime (n / p)
h_div : n / p * p = n
hf : f = (fun y ↦ x + y) ∘ fun y ↦ p • y
this :
  (fun y ↦ x + y) '' (fun y ↦ p • y) '' approxAddOrderOf 𝕊 n (δ n) ⊆
    (fun y ↦ x + y) '' approxAddOrderOf 𝕊 (n / p) (↑p * δ n)
⊢ n = n / p * p

Tactic:
h_div

Goal state after:
case e'_4
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this✝ : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
p : ℕ
hp : Nat.Prime p
x : 𝕊 := u ⟨p, hp⟩
f : 𝕊 → 𝕊 := fun y ↦ p • y + x
n : ℕ
hn : 0 < n
h_ndiv : ¬p * p ∣ n
h_cop : (addOrderOf x).Coprime (n / p)
h_div : n / p * p = n
hf : f = (fun y ↦ x + y) ∘ fun y ↦ p • y
this :
  (fun y ↦ x + y) '' (fun y ↦ p • y) '' approxAddOrderOf 𝕊 n (δ n) ⊆
    (fun y ↦ x + y) '' approxAddOrderOf 𝕊 (n / p) (↑p * δ n)
⊢ n = n
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: ι α β : Type u
c : Cardinal.{u}
l✝ l : Filter α
inst✝ : CountableInterFilter l
S : Set (Set α)
hS : #↑S < ℵ_ 1
a : ∀ s ∈ S, s ∈ l
⊢ S.Countable

Tactic:
rwa [← le_aleph0_iff_set_countable, ← lt_aleph_one_iff]

Goal state after:
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: α : Type u
c : Cardinal.{u}
g : Set (Set α)
hc : 2 < c
⊢ CardinalInterFilter (cardinalGenerate g hc) c

Tactic:
delta cardinalGenerate

Goal state after:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
hc : 2 < c
⊢ CardinalInterFilter (ofCardinalInter {s | CardinalGenerateSets g s} hc ⋯ ⋯) c
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
ht : t ⊆ s
he : s.chainHeight r < t.encard
hh : IsChain r t
⊢ False

Tactic:
encard_le_chainHeight_of_isChain _ _ ht hh

Goal state after:
α : Type u_1
r : α → α → Prop
s t : Set α
ht : t ⊆ s
he : s.chainHeight r < s.chainHeight r
hh : IsChain r t
⊢ False
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
⊢ IF.I.IsProper

Tactic:
by
  obtain ⟨w, h⟩ := IF.F.nonempty
  apply isProper_of_notMem (_ : w ∉ IF.I)
  rwa [← IF.compl_I_eq_F] at h

Goal state after:
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin✝ : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
this : IsStronglyAtomic αs
a₀ : αs
ha₀ : a₀.fst = 0
ha₀inf : (Ici a₀).Infinite
hfin : ∀ (a : αs), {x | a ⋖ x}.Finite
f : ℕ ↪o αs
hf0 : f 0 = a₀
hf : ∀ (i : ℕ), f i ⋖ f (i + 1)
hr : ∀ (i : ℕ), (f i).fst = i
i : ℕ
⊢ α i

Tactic:
by rw [← hr i]; exact (f i).2

Goal state after:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case refine_2
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ ⨆ y ∈ Y, f a y = f a b

Tactic:
apply le_antisymm
    · exact le_trans h (iInf₂_le a ha)
    · apply le_iSup₂ b hb

Goal state after:
Module: Mathlib.Order.ScottContinuity.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α × β → γ
D : Set (Set (α × β))
h₁ : ∀ (a : α), ScottContinuousOn ((fun d ↦ Prod.snd '' d) '' D) fun b ↦ f (a, b)
h₂ : ∀ (b : β), ScottContinuousOn ((fun d ↦ Prod.fst '' d) '' D) fun a ↦ f (a, b)
h₁' : ∀ (a : α), Monotone fun b ↦ f (a, b)
h₂' : ∀ (b : β), Monotone fun a ↦ f (a, b)
d : Set (α × β)
hX : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : α × β
p1 : α
p2 : β
hdp : IsLUB d (p1, p2)
⊢ IsLUB (f '' d) (f (p1, p2))

Tactic:
isLUB_congr ((monotone_prod_iff.mpr ⟨h₁', h₂'⟩).upperBounds_image_of_directedOn_prod hd₂),

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α × β → γ
D : Set (Set (α × β))
h₁ : ∀ (a : α), ScottContinuousOn ((fun d ↦ Prod.snd '' d) '' D) fun b ↦ f (a, b)
h₂ : ∀ (b : β), ScottContinuousOn ((fun d ↦ Prod.fst '' d) '' D) fun a ↦ f (a, b)
h₁' : ∀ (a : α), Monotone fun b ↦ f (a, b)
h₂' : ∀ (b : β), Monotone fun a ↦ f (a, b)
d : Set (α × β)
hX : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : α × β
p1 : α
p2 : β
hdp : IsLUB d (p1, p2)
⊢ IsLUB (f '' (Prod.fst '' d) ×ˢ (Prod.snd '' d)) (f (p1, p2))
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case refine_2
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
h : a ≠ b → P.Rel a b
⊢ f a = f b

Tactic:
obtain rfl | hne := eq_or_ne a b

Goal state after:
case refine_2.inl
α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun f
h : a ≠ a → P.Rel a a
⊢ f a = f a

case refine_2.inr
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
h : a ≠ b → P.Rel a b
hne : a ≠ b
⊢ f a = f b
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: o : OrderType.{u}
α : Type u
x✝ : LinearOrder α
⊢ 1 * type α = type α

Tactic:
simp only [show 1 = type PUnit by rfl, ← type_lex_prod]
      exact (Prod.Lex.prodUnique α PUnit).type_congr

Goal state after:
Module: Mathlib.Order.UpperLower.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s₁ s₂ : LowerSet α
t₁ t₂ : LowerSet β
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂

Tactic:
simp_rw [disjoint_iff, prod_inf_prod, prod_eq_bot]

Goal state after:
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝⁶ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : PartialOrder F
inst✝³ : IsOrderedAddMonoid F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : IsOrderedModule ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Submartingale f ℱ μ
⊢ Submartingale (c • f) ℱ μ

Tactic:
← neg_neg (c • f),

Goal state after:
Ω : Type u_1
ι : Type u_3
inst✝⁶ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : PartialOrder F
inst✝³ : IsOrderedAddMonoid F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : IsOrderedModule ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Submartingale f ℱ μ
⊢ Submartingale (- -(c • f)) ℱ μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ¬IsMin i
ω : Ω
⊢ τ ω < ↑i ↔ τ ω ≤ ↑(Order.pred i)

Tactic:
cases τ ω with
    | top => simp
    | coe t =>
      simp only [coe_lt_coe, coe_le_coe]
      rw [le_pred_iff_of_not_isMin hi_min]

Goal state after:
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
ω : Ω
hω : martingalePart (f + g) ℱ μ n ω = f n ω
| (f + g) n ω

Tactic:
← martingalePart_add_predictablePart ℱ μ (f + g)

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
ω : Ω
hω : martingalePart (f + g) ℱ μ n ω = f n ω
| (martingalePart (f + g) ℱ μ + predictablePart (f + g) ℱ μ) n ω
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
h_exists : ∃ j, n ≤ j ∧ u j ω ∈ s
⊢ u (hittingAfter u s n ω).untopA ω ∈ s

Tactic:
by
  rw [hittingAfter, if_pos h_exists]
  have h_nonempty : {i : ι | n ≤ i ∧ u i ω ∈ s}.Nonempty := by
    obtain ⟨k, hk₁, hk₂⟩ := h_exists
    exact ⟨k, Set.mem_inter hk₁ hk₂⟩
  exact (csInf_mem h_nonempty).2

Goal state after:
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n : ι
⊢ Monotone fun x ↦ hittingBtwn u s n x ω

Tactic:
by
  intro m₁ m₂ hm
  by_cases h : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s
  · exact (hittingBtwn_eq_hittingBtwn_of_exists hm h).le
  · simp_rw [hittingBtwn, if_neg h]
    split_ifs with h'
    · obtain ⟨j, hj₁, hj₂⟩ := h'
      refine le_csInf ⟨j, hj₁, hj₂⟩ ?_
      by_contra! ⟨i, hi₁, hi₂⟩
      exact h ⟨i, ⟨hi₁.1.1, hi₂.le⟩, hi₁.2⟩
    · exact hm

Goal state after:
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
h_notMem_s : ∀ (x : ι), ¬(x ∈ Set.univ ∧ u x ω ∈ s)
⊢ sInf {i | u i ω ∈ s} = ⊤

Tactic:
sInf_eq_top

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
h_notMem_s : ∀ (x : ι), ¬(x ∈ Set.univ ∧ u x ω ∈ s)
⊢ ∀ a ∈ {i | u i ω ∈ s}, a = ⊤
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (fun x ↦ X x - integral μ X) μ
h_add : X = (fun x ↦ X x - integral μ X) + fun x ↦ integral μ X
⊢ Integrable X μ

Tactic:
rw [h_add]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (fun x ↦ X x - integral μ X) μ
h_add : X = (fun x ↦ X x - integral μ X) + fun x ↦ integral μ X
⊢ Integrable ((fun x ↦ X x - integral μ X) + fun x ↦ integral μ X) μ
Module: Mathlib.Probability.BorelCantelli

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ∞
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = (fun x ↦ μ.real (s (n + 1))) ω
ω : Ω
hω : ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = μ.real (s (n + 1))
htends : Tendsto (fun n ↦ ∑ k ∈ Finset.range n, μ (s (k + 1))) atTop (𝓝 ∞)
⊢ Tendsto (fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) atTop atTop

Tactic:
rw [ENNReal.tendsto_nhds_top_iff_nnreal] at htends

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ∞
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = (fun x ↦ μ.real (s (n + 1))) ω
ω : Ω
hω : ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
⊢ Tendsto (fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) atTop atTop
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
h_int_Y : Integrable (fun ω ↦ rexp (t * Y ω)) μ
⊢ Integrable (fun ω ↦ rexp (t * (X + Y) ω)) μ

Tactic:
simp_rw [Pi.add_apply, mul_add, exp_add]
  exact (h_indep.exp_mul t t).integrable_mul h_int_X h_int_Y

Goal state after:
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : RCLike 𝕜
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : CompleteSpace E
inst✝⁵ : CompleteSpace F
inst✝⁴ : MeasurableSpace E
μ : Measure E
inst✝³ : OpensMeasurableSpace E
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
h : Integrable id μ
L : E →L[𝕜] F
⊢ ∫ (x : E), L x ∂μ = L (∫ (x : E), x ∂μ)

Tactic:
simp [L.integral_comp_id_comm h]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case refine_2
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ rexp (-(c⁻¹ * x - μ) ^ 2 / (2 * ↑v)) = rexp (-(x - c * μ) ^ 2 / (2 * (c ^ 2 * ↑v)))

Tactic:
· congr 1
    field

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case refine_2
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ∀ᵐ (x : ℝ), gaussianPDF μ v x ≠ 0

Tactic:
· exact ae_of_all _ (fun _ ↦ (gaussianPDF_pos _ hv _).ne')

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case neg.e_f
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
⊢ ¬|c| = 0

Tactic:
abs_eq_zero

Goal state after:
case neg.e_f
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
⊢ ¬c = 0
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
c : ℝ
⊢ Measure.map (fun x ↦ x * c) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)

Tactic:
simp_rw [mul_comm _ c]
  exact gaussianReal_map_const_mul c

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
⊢ gaussianReal m₁ v₁ ∗ gaussianReal m₂ v₂ = gaussianReal (m₁ + m₂) (v₁ + v₂)

Tactic:
refine Measure.ext_of_charFun ?_

Goal state after:
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
⊢ charFun (gaussianReal m₁ v₁ ∗ gaussianReal m₂ v₂) = charFun (gaussianReal (m₁ + m₂) (v₁ + v₂))
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
⊢ IsGaussian μ ↔ ∀ (t : E), charFun μ t = cexp ((∫ (x : E), ↑⟪t, x⟫ ∂μ) * I - ↑Var[fun x ↦ ⟪t, x⟫; μ] / 2)

Tactic:
isGaussian_iff_charFunDual_eq,

Goal state after:
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
⊢ (∀ (L : StrongDual ℝ E), charFunDual μ L = cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)) ↔
    ∀ (t : E), charFun μ t = cexp ((∫ (x : E), ↑⟪t, x⟫ ∂μ) * I - ↑Var[fun x ↦ ⟪t, x⟫; μ] / 2)
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
⊢ (∀ (x : E),
      charFunDual μ ((toDual ℝ E) x) =
        cexp ((∫ (x_1 : E), ↑(((toDual ℝ E) x) x_1) ∂μ) * I - ↑Var[⇑((toDual ℝ E) x); μ] / 2)) ↔
    ∀ (t : E), charFunDual μ ((toDualMap ℝ E) t) = cexp ((∫ (x : E), ↑⟪t, x⟫ ∂μ) * I - ↑Var[fun x ↦ ⟪t, x⟫; μ] / 2)

Tactic:
simp [toDualMap, toDual]

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: β : Type u_1
inst✝ : LinearOrder β
t : ℕ → β
ht_mono : StrictMono t
ht_tendsto : Tendsto t atTop atTop
x : β
hx : t 0 < x
⊢ ∃ n, t n < x ∧ x ≤ t (n + 1)

Tactic:
by
  have h : ∃ n, x ≤ t n := by
    simp only [tendsto_atTop_atTop_iff_of_monotone ht_mono.monotone] at ht_tendsto
    exact ht_tendsto x
  have h' m := Nat.find_min h (m := m)
  simp only [not_le] at h'
  exact ⟨Nat.find h - 1, h' _ (by simp [hx]), by simp [Nat.find_spec h, hx]⟩

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case refine_3
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
x : E
⊢ ‖L₁ x‖ * ‖L₂ x‖ ≤ ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖

Tactic:
rw [mul_assoc]

Goal state after:
case refine_3
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
x : E
⊢ ‖L₁ x‖ * ‖L₂ x‖ ≤ ‖L₁‖ * ‖x‖ * (‖L₂‖ * ‖x‖)
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case e_a
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}) ^ 2 ^ n =
    ENNReal.ofReal ((1 - μ {x | ‖x‖ ≤ a}).toReal / (μ {x | ‖x‖ ≤ a}).toReal) ^ 2 ^ n

Tactic:
← ENNReal.toReal_div,

Goal state after:
case e_a
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}) ^ 2 ^ n =
    ENNReal.ofReal ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}).toReal ^ 2 ^ n
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : E ≃ₗᵢ[ℝ] F
⊢ Measure.map (⇑f) (stdGaussian E) = stdGaussian F

Tactic:
by
  have := f.finiteDimensional
  apply Measure.ext_of_charFunDual
  ext L
  simp_rw [show ⇑f = f.toContinuousLinearEquiv.toContinuousLinearMap from rfl, charFunDual_map,
    charFunDual_stdGaussian, L.opNorm_comp_linearIsometryEquiv]

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c * a⁻¹ ^ 2
| ENNReal.ofReal (rexp (C * t (n + 1) ^ 2)) * c * ENNReal.ofReal (rexp (-Real.log (c / (1 - c)).toReal * 2 ^ n))

Tactic:
rw [mul_assoc]

Goal state after:
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c * a⁻¹ ^ 2
| ENNReal.ofReal (rexp (C * t (n + 1) ^ 2)) * (c * ENNReal.ofReal (rexp (-Real.log (c / (1 - c)).toReal * 2 ^ n)))
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
⊢ ∫⁻ (x : E), ENNReal.ofReal (rexp (logRatio c' * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤
    μ {x | ‖x‖ ≤ a} *
      (ENNReal.ofReal (rexp (logRatio c')) +
        ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * 2 ^ n)))

Tactic:
change ∫⁻ x, .ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ
      ≤ c * (.ofReal (rexp (logRatio c'))
            + ∑' n, .ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * 2 ^ n)))

Goal state after:
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
⊢ ∫⁻ (x : E), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    c *
      (ENNReal.ofReal (rexp (logRatio c')) +
        ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * 2 ^ n)))