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

Goal state before:
pp: α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
⊢ ∃ f, Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ Surjective f

Tactic:
have s_closed : IsClosed s := by
    refine isClosed_iff_clusterPt.mpr fun x hx ↦ ?_
    have L : Tendsto (fun n : ℕ => diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0) := by
      have : Tendsto (fun n : ℕ => (2 : ℝ) * (1 / 2) ^ n) atTop (𝓝 (2 * 0)) :=
        (tendsto_pow_atTop_nhds_zero_of_lt_one I0.le I1).const_mul _
      rw [mul_zero] at this
      exact
        squeeze_zero (fun n => diam_nonneg) (fun n => diam_closedBall (pow_nonneg I0.le _)) this
    refine nonempty_iInter_of_nonempty_biInter (fun n => isClosed_closedBall)
      (fun n => isBounded_closedBall) (fun N ↦ ?_) L
    obtain ⟨y, hxy, ys⟩ : ∃ y, y ∈ ball x ((1 / 2) ^ N) ∩ s :=
      clusterPt_principal_iff.1 hx _ (ball_mem_nhds x (pow_pos I0 N))
    have E :
      ⋂ (n : ℕ) (H : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n) =
        ⋂ (n : ℕ) (H : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n) := by
      refine iInter_congr fun n ↦ iInter_congr fun hn ↦ ?_
      have : x n = y n := apply_eq_of_dist_lt (mem_ball'.1 hxy) hn
      rw [this]
    rw [E]
    apply Nonempty.mono _ ys
    apply iInter_subset_iInter₂

Goal state after:
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
s_closed : IsClosed s
⊢ ∃ f, Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ Surjective f
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ μ' : Measure α
ν ν' : Measure β
inst✝ : SFinite ν'
h1 : μ ≤ μ'
h2 : ν ≤ ν'
⊢ μ.prod ν ≤ μ'.prod ν'

Tactic:
apply Measure.le_iff.2 (fun s hs ↦ ?_)
  calc μ.prod ν s
  _ ≤ ∫⁻ x, ν (Prod.mk x ⁻¹' s) ∂μ := prod_apply_le hs
  _ ≤ ∫⁻ x, ν' (Prod.mk x ⁻¹' s) ∂μ' := by gcongr
  _ = (μ'.prod ν') s := (prod_apply hs).symm

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.IsComplement' K
ϕ : ↥H × ↥K ≃ ↥K × ↥H :=
  { toFun := fun x ↦ (x.2⁻¹, x.1⁻¹), invFun := fun x ↦ (x.2⁻¹, x.1⁻¹), left_inv := ⋯, right_inv := ⋯ }
ψ : G ≃ G := { toFun := fun g ↦ g⁻¹, invFun := fun g ↦ g⁻¹, left_inv := ⋯, right_inv := ⋯ }
hf : (⇑ψ ∘ fun x ↦ ↑x.1 * ↑x.2) = (fun x ↦ ↑x.1 * ↑x.2) ∘ ⇑ϕ
⊢ K.IsComplement' H

Tactic:
isComplement'_def,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.IsComplement' K
ϕ : ↥H × ↥K ≃ ↥K × ↥H :=
  { toFun := fun x ↦ (x.2⁻¹, x.1⁻¹), invFun := fun x ↦ (x.2⁻¹, x.1⁻¹), left_inv := ⋯, right_inv := ⋯ }
ψ : G ≃ G := { toFun := fun g ↦ g⁻¹, invFun := fun g ↦ g⁻¹, left_inv := ⋯, right_inv := ⋯ }
hf : (⇑ψ ∘ fun x ↦ ↑x.1 * ↑x.2) = (fun x ↦ ↑x.1 * ↑x.2) ∘ ⇑ϕ
⊢ IsComplement ↑K ↑H
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
h : IsComplement (↑H) T
⊢ T.ncard = H.index

Tactic:
rw [← Nat.card_coe_set_eq, h.card_right]

Goal state after:
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.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₁
γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝ : UpgradedIsCompletelyMetrizableSpace γ := ⋯
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable ↑b
A : Type (max 0 u_3) := ⋯
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := ⋯
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := ⋯
⊢ range f ⊆ ⋂ n, F n

Tactic:
rintro x ⟨y, rfl⟩
    refine mem_iInter.2 fun n => ?_
    obtain ⟨s, sb, ys, hs⟩ : ∃ (s : Set γ), s ∈ b ∧ y ∈ s ∧ s ⊆ ball y (u n / 2) := by
      apply hb.mem_nhds_iff.1
      exact ball_mem_nhds _ (half_pos (u_pos n))
    have diam_s : diam s ≤ u n := by
      apply (diam_mono hs isBounded_ball).trans
      convert! diam_ball (x := y) (half_pos (u_pos n)).le
      ring
    refine mem_iUnion.2 ⟨⟨s, sb⟩, ?_⟩
    refine mem_iUnion.2 ⟨⟨isBounded_ball.subset hs, diam_s⟩, ?_⟩
    apply mem_inter (subset_closure (mem_image_of_mem _ ys))
    refine mem_iInter.2 fun t => mem_iInter.2 fun ht => ⟨?_, ?_⟩
    · apply hq1
      exact mem_image_of_mem _ ys
    · apply disjoint_left.1 (hq2 ⟨(t, ⟨s, sb⟩), ht.symm⟩)
      exact mem_image_of_mem _ ys

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case snd
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
this : (hSK.equiv (g * ↑k)).1 = (hSK.equiv g).1
⊢ ↑(hSK.equiv (g * ↑k)).2 = ↑((hSK.equiv g).1, (hSK.equiv g).2 * k).2

Tactic:
· rw [coe_mul, equiv_snd_eq_inv_mul, this, equiv_snd_eq_inv_mul, mul_assoc]

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: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set (β × α)
hs : MeasurableSet s
⊢ (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) s =
    (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))) s

Tactic:
rw [sum_apply _ hs, sum_apply _ hs]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set (β × α)
hs : MeasurableSet s
⊢ ∑' (i : ℕ × ℕ), (map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) s =
    ∑' (i : ℕ × ℕ), (map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))) s
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case inl
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
inst✝ : ⊥.IsCountablyGenerated
⊢ MeasurableSet {x | ∃ c, Tendsto (fun n ↦ f n x) ⊥ (𝓝 c)}

pp: case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
⊢ MeasurableSet {x | ∃ c, Tendsto (fun n ↦ f n x) l (𝓝 c)}

Tactic:
· simp

Goal state after:
case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
⊢ MeasurableSet {x | ∃ c, Tendsto (fun n ↦ f n x) l (𝓝 c)}
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : ¬AEMeasurable Y μ
⊢ (map (fun a ↦ (X a, Y a)) μ).snd = map Y μ

Tactic:
· have : ¬AEMeasurable (fun x ↦ (X x, Y x)) μ := by
      contrapose hY
      exact measurable_snd.comp_aemeasurable hY
    simp [map_of_not_aemeasurable, hY, this]

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

Goal state before:
pp: case inl
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
s : Set G
hs : IsOpen[inst✝⁵] s
inst✝¹ : IsMulLeftInvariant 0
inst✝ : Regular 0
⊢ 0 s = 0 ↔ s = ∅ ∨ 0 = 0

pp: case inr
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
μ : Measure G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : μ.Regular
s : Set G
hs : IsOpen[inst✝⁵] s
hμ : NeZero μ
⊢ μ s = 0 ↔ s = ∅ ∨ μ = 0

Tactic:
· simp

Goal state after:
case inr
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
μ : Measure G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : μ.Regular
s : Set G
hs : IsOpen[inst✝⁵] s
hμ : NeZero μ
⊢ μ s = 0 ↔ s = ∅ ∨ μ = 0
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α✝ : 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 β
h : ¬Countable α
⊢ α ≃ᵐ (ℕ → Bool)

Tactic:
apply Nonempty.some

Goal state after:
α✝ : 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 β
h : ¬Countable α
⊢ Nonempty (α ≃ᵐ (ℕ → Bool))
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.InnerRegular
⊢ (∃ K, IsCompact K ∧ ¬μ K = 0) ↔ ∃ x ⊆ univ, IsCompact x ∧ ¬μ x = 0

Tactic:
subset_univ,

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.InnerRegular
⊢ (∃ K, IsCompact K ∧ ¬μ K = 0) ↔ ∃ x, True ∧ IsCompact x ∧ ¬μ x = 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = (r • μ.withDensity f) s

Tactic:
Measure.coe_smul,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = (r • ⇑(μ.withDensity f)) s
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = (r • μ.withDensity f) s

Tactic:
Measure.coe_smul,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = (r • ⇑(μ.withDensity f)) s
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ.withDensity 0 = 0

Tactic:
by
  ext1 s hs
  simp [withDensity_apply _ hs]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ.withDensity 1 = μ

Tactic:
by
  ext1 s hs
  simp [withDensity_apply _ hs]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
⊢ (μ.withDensity fun x ↦ c) = c • μ

Tactic:
by
  ext1 s hs
  simp [withDensity_apply _ hs]

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.Regular
⊢ (∃ K, IsCompact K ∧ ¬μ K = 0) ↔ ∃ x ⊆ univ, IsCompact x ∧ ¬μ x = 0

Tactic:
subset_univ,

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.Regular
⊢ (∃ K, IsCompact K ∧ ¬μ K = 0) ↔ ∃ x, True ∧ IsCompact x ∧ ¬μ x = 0
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' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : f a = f' a
⊢ a ∈ {x | f' x ≠ 0}ᶜ → ↑(f a) * g a = ↑(f' a) * g' a

Tactic:
ha_null

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' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : f a = f' a
ha_null : a ∈ {x | f' x ≠ 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' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : f a = f' a
ha_null✝ : a ∈ {x | f' x ≠ 0}ᶜ
ha_null : f' a = 0
⊢ ↑(f a) * g a = ↑(f' a) * g' a

Tactic:
ha_null

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' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : f a = 0
ha_null✝ : a ∈ {x | f' x ≠ 0}ᶜ
ha_null : f' a = 0
⊢ ↑(f a) * g a = ↑0 * g' a
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case mp.htc
α : 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' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}ᶜ, (fun x ↦ ↑(f x) * g x) x = (fun x ↦ ↑(f' x) * g' x) x

Tactic:
· rw [ae_restrict_iff' A.compl]
      filter_upwards [hf'_ae] with a ha ha_null
      have ha_null : f' a = 0 := Function.notMem_support.mp ha_null
      rw [ha_null] at ha ⊢
      rw [ha]
      simp only [ENNReal.coe_zero, zero_mul]

Goal state after:
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: case inl
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
⊢ b * b - 4 * a * c ≤ 0

Tactic:
exact False.elim ((h x).not_gt <| by rwa [← mul_assoc, ← add_mul])

Goal state after:
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: case inr.inl.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + 0 * x + c
⊢ 0 * 0 - 4 * 0 * c ≤ 0

pp: case inr.inl.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
hb : b ≠ 0
⊢ b * b - 4 * 0 * c ≤ 0

Tactic:
· simp

Goal state after:
case inr.inl.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
hb : b ≠ 0
⊢ b * b - 4 * 0 * c ≤ 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, g x ∂μ.withDensity f = ∫⁻ (x : α) in s, (f * g) x ∂μ

Tactic:
by
  rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul _ hf hg]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
h : x ^ 2 ≤ y
⊢ |x| ≤ √y

Tactic:
rw [← sqrt_sq_eq_abs]

Goal state after:
x y : ℝ
h : x ^ 2 ≤ y
⊢ √(x ^ 2) ≤ √y
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
⊢ √7 ≠ 0

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g : α → ℝ≥0∞
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f ≤ ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
rw [← iSup_lintegral_measurable_le_eq_lintegral, ← iSup_lintegral_measurable_le_eq_lintegral]
  refine iSup₂_le fun i i_meas => iSup_le fun hi => ?_
  rw [lintegral_withDensity_eq_lintegral_mul _ f_meas i_meas]
  exact le_iSup₂_of_le (f * i) (f_meas.mul i_meas) <| le_iSup_of_le (by grw [hi]) le_rfl

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
⊢ SFinite (μ.withDensity f)

Tactic:
set s := {x | f x = ∞}

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x | f x = ∞}
⊢ SFinite (μ.withDensity f)
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NontrivialTopology V
⊢ 1 ≤ ‖id V‖

Tactic:
by
    let ⟨x, hx⟩ := exists_norm_ne_zero V
    have := (id V).ratio_le_opNorm x
    rwa [id_apply, div_self hx] at this

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
⊢ unitary Rˣ = Submonoid.comap (Units.coeHom R) (unitary R)

Tactic:
by
  ext
  simp [mem_iff, Units.ext_iff]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: case succ
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x ^ 2 ^ (k + 1)‖₊ = ‖x‖₊ ^ 2 ^ (k + 1)

Tactic:
rw [pow_succ', pow_mul', sq, (hx.pow (2 ^ k)).nnnorm_mul_self, hk, pow_mul']

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst✝³ : DivisionSemiring γ
inst✝² : Module γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
⊢ ∑'[L] (i : β), 0 • f i = 0 • ∑'[L] (i : β), f i

pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst✝³ : DivisionSemiring γ
inst✝² : Module γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hg : g ≠ 0
⊢ ∑'[L] (i : β), g • f i = g • ∑'[L] (i : β), f i

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst✝³ : DivisionSemiring γ
inst✝² : Module γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hg : g ≠ 0
⊢ ∑'[L] (i : β), g • f i = g • ∑'[L] (i : β), f i
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomInvPair σ' σ
L : SummationFilter ι
f : ι → M
e : M ≃SL[σ] M₂
x : M
⊢ HasSum (fun b ↦ e (f b)) (e x) L ↔ HasSum f x L

Tactic:
e.hasSum,

Goal state after:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomInvPair σ' σ
L : SummationFilter ι
f : ι → M
e : M ≃SL[σ] M₂
x : M
⊢ HasSum f (e.symm (e x)) L ↔ HasSum f x L
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Star E
inst✝¹ : Module ℂ E
inst✝ : StarModule ℂ E
r : ℝ
a : E
⊢ star ((r • 1) • a) = star r • star a

Tactic:
star_smul,

Goal state after:
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Star E
inst✝¹ : Module ℂ E
inst✝ : StarModule ℂ E
r : ℝ
a : E
⊢ star (r • 1) • star a = star r • star a
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Star E
inst✝¹ : Module ℂ E
inst✝ : StarModule ℂ E
r : ℝ
a : E
⊢ star (r • 1) • star a = star r • star a

Tactic:
star_smul,

Goal state after:
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Star E
inst✝¹ : Module ℂ E
inst✝ : StarModule ℂ E
r : ℝ
a : E
⊢ (star r • star 1) • star a = star r • star a
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < normSq z ↔ z ≠ 0

Tactic:
by
  rw [lt_iff_le_and_ne, Ne, eq_comm]; simp [normSq_nonneg]

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x y : A
⊢ x = y → ℜ x = ℜ y ∧ ℑ x = ℑ y

Tactic:
by grind

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝ : RCLike K
⊢ 0⁻¹ = (starRingEnd K) 0 * ↑(‖0‖ ^ 2)⁻¹

pp: case inr
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ z⁻¹ = (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹

Tactic:
· simp

Goal state after:
case inr
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ z⁻¹ = (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
q : ℚ≥0
⊢ re ↑q = ↑q

Tactic:
rw [← ofReal_nnratCast, ofReal_re]

Goal state after: