mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: case _a
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → x ∈ s → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ ↑(K' x hx) * edist x y
t : Finset ↑s
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x) (ε ↑x ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : ↑s
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z) (ε ↑z ⋯ / 2)
hy' : y ∉ ball (↑z) (ε ↑z ⋯)
⊢ K ↑z ⋯ + 2 * K' ↑z ⋯ ≤ t.sup fun i ↦ K ↑i ⋯ + 2 * K' ↑i ⋯

Tactic:
exact .trans (by rfl) (t.le_sup hz)

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Tactic:
have h_int_finite : ∫⁻ a, F a ∂μ ≠ ∞ := by
    refine ((lintegral_mono_ae ?_).trans_lt h0.lt_top).ne
    filter_upwards [h_bound] with a ha using ha 0

Goal state after:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
inst✝ : Archimedean α
hδ : 0 < δ
m : ℕ
hm : b - a ≤ m • δ
n : ℕ
hn : n ≥ m
⊢ max a (min b (n • δ + a)) = b

Tactic:
min_eq_left_iff.mpr,

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
inst✝ : Archimedean α
hδ : 0 < δ
m : ℕ
hm : b - a ≤ m • δ
n : ℕ
hn : n ≥ m
⊢ max a b = b

α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
inst✝ : Archimedean α
hδ : 0 < δ
m : ℕ
hm : b - a ≤ m • δ
n : ℕ
hn : n ≥ m
⊢ b ≤ n • δ + a
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mp
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : ⟨i, x⟩ ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
⊢ ∀ (y : (i : ι) × E i), dist ⟨i, x⟩ y < min ε 1 → y ∈ s

Tactic:
rintro ⟨j, y⟩ hy

Goal state after:
case mp
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : ⟨i, x⟩ ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
j : ι
y : E j
hy : dist ⟨i, x⟩ ⟨j, y⟩ < min ε 1
⊢ ⟨j, y⟩ ∈ s
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mp
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
⊢ IsOpen[instTopologicalSpaceSigma] s → ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s

pp: case mpr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
⊢ (∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s) → IsOpen[instTopologicalSpaceSigma] s

Tactic:
· rintro hs ⟨i, x⟩ hx
    obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, ball x ε ⊆ Sigma.mk i ⁻¹' s :=
      Metric.isOpen_iff.1 (isOpen_sigma_iff.1 hs i) x hx
    refine ⟨min ε 1, lt_min εpos zero_lt_one, ?_⟩
    rintro ⟨j, y⟩ hy
    rcases eq_or_ne i j with (rfl | hij)
    · simp only [Sigma.dist_same, lt_min_iff] at hy
      exact hε (mem_ball'.2 hy.1)
    · apply (lt_irrefl (1 : ℝ) _).elim
      calc
        1 ≤ Sigma.dist ⟨i, x⟩ ⟨j, y⟩ := Sigma.one_le_dist_of_ne hij _ _
        _ < 1 := hy.trans_le (min_le_right _ _)

Goal state after:
case mpr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
⊢ (∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s) → IsOpen[instTopologicalSpaceSigma] s
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: case refine_1.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ↑(inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res (↑x) n), ∀ z ∈ A (res (↑x) n), dist y z < ε
y : ↑(inducedMap A).fst
hyx : res (↑y) n = res (↑x) n
⊢ (inducedMap A).snd y ∈ A (res (↑x) n)

Tactic:
rw [← hyx]

Goal state after:
case refine_1.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ↑(inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res (↑x) n), ∀ z ∈ A (res (↑x) n), dist y z < ε
y : ↑(inducedMap A).fst
hyx : res (↑y) n = res (↑x) n
⊢ (inducedMap A).snd y ∈ A (res (↑y) n)
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsν : ∀ (i : ι), ν (s i)ᶜ = 0
⊢ ∑' (i : ι), (μ i) (⋂ b, s b) = 0

Tactic:
ENNReal.tsum_eq_zero

Goal state after:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsν : ∀ (i : ι), ν (s i)ᶜ = 0
⊢ ∀ (i : ι), (μ i) (⋂ b, s b) = 0
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsProbabilityMeasure μ
hs : NullMeasurableSet s μ
⊢ 1 - μ s = 0 ↔ μ s = 1

Tactic:
tsub_eq_zero_iff_le,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsProbabilityMeasure μ
hs : NullMeasurableSet s μ
⊢ 1 ≤ μ s ↔ μ s = 1
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
a : α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
h✝ : a ∉ s
⊢ ∫⁻ (x : α), f x ∂0 = 0

Tactic:
· exact lintegral_zero_measure _

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: case neg
α : Type u_1
inst✝² : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
h✝ : a ∉ s
⊢ ∫⁻ (x : α), f x ∂0 = 0

Tactic:
· exact lintegral_zero_measure _

Goal state after:
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
⊢ Measurable dirac

Tactic:
by
  refine measurable_of_measurable_coe _ fun s hs => ?_
  simp_rw [dirac_apply' _ hs]
  exact measurable_one.indicator hs

Goal state after:
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → Measure β
hf : Measurable f
a : α
⊢ (dirac a).bind f = f a

Tactic:
simp [bind, map_dirac' hf]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Doubling

Goal state before:
pp: α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ihn : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ n * μ (closedBall x (2 * ε))
ε : ℝ
hεn : ∀ (x : α), μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ n * μ (closedBall x (2 * ε))
hε : ∀ (x : α), μ (closedBall x (2 * ε)) ≤ ↑(doublingConstant μ) * μ (closedBall x ε)
x : α
⊢ ↑C ^ n * (↑(doublingConstant μ) * μ (closedBall x ε)) ≤ ↑C ^ (n + 1) * μ (closedBall x ε)

Tactic:
← mul_assoc,

Goal state after:
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ihn : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ n * μ (closedBall x (2 * ε))
ε : ℝ
hεn : ∀ (x : α), μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ n * μ (closedBall x (2 * ε))
hε : ∀ (x : α), μ (closedBall x (2 * ε)) ≤ ↑(doublingConstant μ) * μ (closedBall x ε)
x : α
⊢ ↑C ^ n * ↑(doublingConstant μ) * μ (closedBall x ε) ≤ ↑C ^ (n + 1) * μ (closedBall x ε)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_3
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst✝ : IsFiniteMeasure μ
h : ∀ {s : Set α} {t : Set β}, MeasurableSet s → MeasurableSet t → μ (s ×ˢ t) = ν (s ×ˢ t)
s : Set (α × β)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
⊢ ∀ (f : ℕ → Set (α × β)),
    Pairwise (Disjoint on f) →
      (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), μ (f i) = ν (f i)) → μ (⋃ i, f i) = ν (⋃ i, f i)

Tactic:
· intro f h_disj hf h_eq
    simp_rw [measure_iUnion h_disj hf, h_eq]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : (hSK.equiv g₁).1 = (hSK.equiv g₂).1
⊢ (↑(hSK.equiv g₁).2)⁻¹ * (↑(hSK.equiv g₁).1)⁻¹ * (↑(hSK.equiv g₁).1 * ↑(hSK.equiv g₂).2) ∈ K

Tactic:
← mul_assoc,

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : (hSK.equiv g₁).1 = (hSK.equiv g₂).1
⊢ (↑(hSK.equiv g₁).2)⁻¹ * (↑(hSK.equiv g₁).1)⁻¹ * ↑(hSK.equiv g₁).1 * ↑(hSK.equiv g₂).2 ∈ K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
A : Set α
μ : Measure α
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ U ⊇ A, IsOpen[inst✝¹] U ∧ μ U ≤ μ A + ε

Tactic:
rcases eq_or_ne (μ A) ∞ with (H | H)
  · exact ⟨univ, subset_univ _, isOpen_univ, by simp only [H, _root_.top_add, le_top]⟩
  · rcases A.exists_isOpen_lt_add H hε with ⟨U, AU, U_open, hU⟩
    exact ⟨U, AU, U_open, hU.le⟩

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
⊢ g ∈ T → ↑(hST.equiv g).2 = g

Tactic:
intro h
    rw [hST.equiv_snd_eq_self_of_mem_of_one_mem h1 h]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_5
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst✝ : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {t | MeasurableSet t} {u | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} C₂
⊢ ∀ (f : ℕ → Set (α × β × γ)),
    Pairwise (Disjoint on f) →
      (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), μ (f i) = ν (f i)) → μ (⋃ i, f i) = ν (⋃ i, f i)

Tactic:
· intro f h_disj hf h_eq
    simp_rw [measure_iUnion h_disj hf, h_eq]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure ((α × β) × γ)
inst✝ : IsFiniteMeasure μ
h_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t → MeasurableSet u → (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
s : Set α
t : Set β
u : Set γ
h : μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ (map (⇑MeasurableEquiv.prodAssoc) μ) (s ×ˢ t ×ˢ u) = (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u)

Tactic:
rwa [h_eq μ hs ht hu, h_eq ν hs ht hu]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst✝¹]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst✝¹] U → p (s \ U)
⊢ μ.InnerRegularWRT p fun s ↦ MeasurableSet s ∧ μ s ≠ ∞

Tactic:
by
  rintro s ⟨hs, hμs⟩ r hr
  have h0 : p ∅ := by
    have : 0 < μ univ := (bot_le.trans_lt hr).trans_le (measure_mono (subset_univ _))
    obtain ⟨K, -, hK, -⟩ : ∃ K, K ⊆ univ ∧ p K ∧ 0 < μ K := H isOpen_univ _ this
    simpa using hd hK isOpen_univ
  obtain ⟨ε, hε, hεs, rfl⟩ : ∃ ε ≠ 0, ε + ε ≤ μ s ∧ r = μ s - (ε + ε) := by
    use (μ s - r) / 2
    simp [*, hr.le, ENNReal.add_halves, ENNReal.sub_sub_cancel, tsub_eq_zero_iff_le]
  rcases hs.exists_isOpen_sdiff_lt hμs hε with ⟨U, hsU, hUo, hUt, hμU⟩
  rcases (U \ s).exists_isOpen_lt_of_lt _ hμU with ⟨U', hsU', hU'o, hμU'⟩
  replace hsU' := sdiff_subset_comm.1 hsU'
  rcases H.exists_subset_lt_add h0 hUo hUt.ne hε with ⟨K, hKU, hKc, hKr⟩
  refine ⟨K \ U', fun x hx => hsU' ⟨hKU hx.1, hx.2⟩, hd hKc hU'o, ENNReal.sub_lt_of_lt_add hεs ?_⟩
  calc
    μ s ≤ μ U := μ.mono hsU
    _ < μ K + ε := hKr
    _ ≤ μ (K \ U') + μ U' + ε := by grw [tsub_le_iff_right.1 le_measure_sdiff]
    _ ≤ μ (K \ U') + ε + ε := by gcongr
    _ = μ (K \ U') + (ε + ε) := add_assoc _ _ _

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : μ.IsMulLeftInvariant
U : Set G
hU : IsOpen[inst✝⁴] U
h'U : (interior U).Nonempty
h : μ U ≠ ∞
K : Set G
hK : IsCompact K
t : Finset G
hKt : K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' U
⊢ ∀ i ∈ ↑t, μ ((fun h ↦ i * h) ⁻¹' U) < ∞

Tactic:
simp [h.lt_top]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case pos
α✝ : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β✝ : Type u_5
inst✝⁴ : MeasurableSpace β✝
β : Type u_6
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : StandardBorelSpace α
inst✝ : StandardBorelSpace β
e : α ≃ β
h : Countable α
this : Countable β := Countable.of_equiv α e
⊢ α ≃ᵐ β

Tactic:
refine ⟨e, ?_, ?_⟩ <;> apply measurable_of_countable

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ (μ.withDensity f).trim hm = (μ.trim hm).withDensity f

Tactic:
refine @Measure.ext _ m _ _ (fun s hs ↦ ?_)

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ((μ.withDensity f).trim hm) s = ((μ.trim hm).withDensity f) s
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
⊢ f a = f' a → f' a ≠ 0 → ↑(f a) * g a = ↑(f' a) * g' a

Tactic:
h'a

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a = f' a
⊢ f' a ≠ 0 → ↑(f a) * g a = ↑(f' a) * g' a
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun x ↦ ↑(f x) * g x) =ᵐ[μ] g'
a : α
hfga : ↑(f a) * g a = g' a
hff'a : f a = f' a
⊢ ↑(f a) ≠ 0 → g a = (↑(f' a))⁻¹ * g' a

Tactic:
h'a

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun x ↦ ↑(f x) * g x) =ᵐ[μ] g'
a : α
hfga : ↑(f a) * g a = g' a
hff'a : f a = f' a
h'a : ↑(f a) ≠ 0
⊢ g a = (↑(f' a))⁻¹ * g' a
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun x ↦ ↑(f x) * g x) =ᵐ[μ] g'
a : α
hfga : ↑(f' a) * g a = g' a
hff'a : f a = f' a
h'a : ↑(f' a) ≠ 0
⊢ g a = (↑(f' a))⁻¹ * (↑(f' a) * g a)

Tactic:
← mul_assoc,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun x ↦ ↑(f x) * g x) =ᵐ[μ] g'
a : α
hfga : ↑(f' a) * g a = g' a
hff'a : f a = f' a
h'a : ↑(f' a) ≠ 0
⊢ g a = (↑(f' a))⁻¹ * ↑(f' a) * g a
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : a < 0
this : Tendsto (fun x ↦ (a * x + b) * x + c) atTop atBot
x : K
hx : (a * x + b) * x + c < 0
⊢ a * (x * x) + b * x + c < 0

Tactic:
← mul_assoc,

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : a < 0
this : Tendsto (fun x ↦ (a * x + b) * x + c) atTop atBot
x : K
hx : (a * x + b) * x + c < 0
⊢ a * x * x + b * x + c < 0
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
⊢ discrim a b c ≤ 0

Tactic:
by
  rw [discrim, sq]
  obtain ha | rfl | ha : a < 0 ∨ a = 0 ∨ 0 < a := lt_trichotomy a 0
  -- if a < 0
  · have : Tendsto (fun x => (a * x + b) * x + c) atTop atBot :=
      tendsto_atBot_add_const_right _ c <|
        (tendsto_atBot_add_const_right _ b (tendsto_id.const_mul_atTop_of_neg ha)).atBot_mul_atTop₀
          tendsto_id
    rcases (this.eventually (eventually_lt_atBot 0)).exists with ⟨x, hx⟩
    exact False.elim ((h x).not_gt <| by rwa [← mul_assoc, ← add_mul])
  -- if a = 0
  · rcases eq_or_ne b 0 with (rfl | hb)
    · simp
    · have := h ((-c - 1) / b)
      rw [mul_div_cancel₀ _ hb] at this
      linarith
  -- if a > 0
  · have ha' : 0 ≤ 4 * a := mul_nonneg zero_le_four ha.le
    convert neg_nonpos.2 (mul_nonneg ha' (h (-b / (2 * a))))
    field

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x ≠ 0
⊢ i x = f x * ((f x)⁻¹ * i x)

Tactic:
← mul_assoc,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x ≠ 0
⊢ i x = f x * (f x)⁻¹ * i x
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_7
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
⊢ HasFiniteIntegral f μ → HasFiniteIntegral (↑c • f) μ

Tactic:
exact HasFiniteIntegral.smul _

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

Goal state before:
pp: z : ℂ
h : z ≠ 0
⊢ z * ((starRingEnd ℂ) z * ↑(normSq z)⁻¹) = 1

Tactic:
← mul_assoc,

Goal state after:
z : ℂ
h : z ≠ 0
⊢ z * (starRingEnd ℂ) z * ↑(normSq z)⁻¹ = 1
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case mpr
a₁ a₂ : ℝ
x : ℂ
x₁ : (equivRealProd x).1 ∈ [[a₁, a₂]]
⊢ x ∈ (fun x_1 ↦ ↑x_1 + ↑(equivRealProd x).2 * I) '' [[a₁, a₂]]

Tactic:
refine ⟨x.re, x₁, by simp⟩

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
a : α
s : Finset ι
f : ι → α
hs : s.Nonempty
h : a ≤ 𝔼 i ∈ s, f i
⊢ 𝔼 i ∈ s, a ≤ 𝔼 i ∈ s, f i

Tactic:
expect_const hs _

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
a : α
s : Finset ι
f : ι → α
hs : s.Nonempty
h : a ≤ 𝔼 i ∈ s, f i
⊢ a ≤ 𝔼 i ∈ s, f i
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
a : α
s : Finset ι
f : ι → α
hs : s.Nonempty
h : 𝔼 i ∈ s, f i ≤ a
⊢ 𝔼 i ∈ s, f i ≤ 𝔼 i ∈ s, a

Tactic:
expect_const hs _

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
a : α
s : Finset ι
f : ι → α
hs : s.Nonempty
h : 𝔼 i ∈ s, f i ≤ a
⊢ 𝔼 i ∈ s, f i ≤ a
Module: Mathlib.Algebra.Star.MonoidHom

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝⁷ : Mul A
inst✝⁶ : Mul B
inst✝⁵ : Mul C
inst✝⁴ : Mul D
inst✝³ : Star A
inst✝² : Star B
inst✝¹ : Star C
inst✝ : Star D
e₁ : A ≃⋆* B
e₂ : B ≃⋆* C
a : A
⊢ e₂.toFun (star (e₁.toFun a)) = star (e₂.toFun (e₁.toFun a))

Tactic:
e₂.map_star'

Goal state after:
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝⁷ : Mul A
inst✝⁶ : Mul B
inst✝⁵ : Mul C
inst✝⁴ : Mul D
inst✝³ : Star A
inst✝² : Star B
inst✝¹ : Star C
inst✝ : Star D
e₁ : A ≃⋆* B
e₂ : B ≃⋆* C
a : A
⊢ star (e₂.toFun (e₁.toFun a)) = star (e₂.toFun (e₁.toFun a))
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : StarMul G
a b : G
⊢ star a * (a * b⁻¹) = star b ↔ star a * a = star b * b

Tactic:
← mul_assoc,

Goal state after:
G : Type u_2
inst✝¹ : Group G
inst✝ : StarMul G
a b : G
⊢ star a * a * b⁻¹ = star b ↔ star a * a = star b * b
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : StarRing R
p : R
hp : IsStarProjection p
⊢ 2 * p - 1 ∈ unitary R

Tactic:
by
  simp only [two_mul, Unitary.mem_iff, star_sub, star_add,
    hp.isSelfAdjoint.star_eq, star_one, mul_sub, mul_add,
    sub_mul, add_mul, hp.isIdempotentElem.eq, one_mul, add_sub_cancel_right,
    mul_one, sub_sub_cancel, and_self]

Goal state after: