mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Complement

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

Tactic:
by
  rw [← h.finite_right.cast_ncard_eq, h.ncard_right]

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

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
ν : Measure α
inst✝¹ : μ.OuterRegular
inst✝ : ν.OuterRegular
hμν : ∀ (U : Set α), IsOpen[inst✝²] U → μ U = ν U
⊢ μ = ν

Tactic:
ext s ms
  rw [Set.measure_eq_iInf_isOpen, Set.measure_eq_iInf_isOpen]
  congr! 4 with t _ ht2
  exact hμν t ht2

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

Goal state before:
pp: G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h ↦ h * g) ⁻¹' A) = μ A) ↔
    ∀ (g : G), Measure.map (fun x ↦ x * g) μ = μ

pp: G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G), Measure.map (fun x ↦ x * g) μ = μ) ↔ μ.IsMulRightInvariant

Tactic:
· simp_rw [Measure.ext_iff]
    refine forall_congr' fun g => forall_congr' fun A => forall_congr' fun hA => ?_
    rw [map_apply (measurable_mul_const g) hA]

Goal state after:
G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G), Measure.map (fun x ↦ x * g) μ = μ) ↔ μ.IsMulRightInvariant
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul G
H : Subgroup G
inst✝¹ : H.FiniteIndex
hH : MeasurableSet ↑H
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s ↑H
hs' : Finite ↑s
⊢ Pairwise (Disjoint on fun x ↦ ↑x • ↑H)

Tactic:
exact fun a b hab ↦ hs.pairwiseDisjoint_smul a.2 b.2 (Subtype.val_injective.ne hab)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
⊢ map Prod.fst (map Prod.swap ρ) = ρ.snd

Tactic:
Measure.map_map measurable_fst measurable_swap

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
⊢ map (Prod.fst ∘ Prod.swap) ρ = ρ.snd
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 α
this : UpgradedStandardBorel α := upgradeStandardBorel α
⊢ ¬univ.Countable

Tactic:
← countable_coe_iff,

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 α
this : UpgradedStandardBorel α := upgradeStandardBorel α
⊢ ¬Countable ↑univ
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous[inst✝⁴, inst✝¹] f
s : Set β
hs : MeasurableSet s
h's : (map f μ) s ≠ ∞
⊢ μ (f ⁻¹' s) ≠ ∞

Tactic:
map_apply hf.measurable hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous[inst✝⁴, inst✝¹] f
s : Set β
hs : MeasurableSet s
h's : μ (f ⁻¹' s) ≠ ∞
⊢ μ (f ⁻¹' s) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.WithDensity

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

Tactic:
ae_restrict_iff' A

Goal state after:
case mp.ht
α : 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}
⊢ ∀ᵐ (x : α) ∂μ, x ∈ {x | f' x ≠ 0} → (fun x ↦ ↑(f x) * g x) x = (fun x ↦ ↑(f' x) * g' x) x
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
x : K
hx : ∀ (y : K), (fun x_1 ↦ (2 * a * x + b) ^ 2 = (2 * a * x_1 + b) ^ 2) y → y = x
⊢ (2 * a * x + b) ^ 2 = 0

Tactic:
specialize hx (-(x + b / a))

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
x : K
hx : (fun x_1 ↦ (2 * a * x + b) ^ 2 = (2 * a * x_1 + b) ^ 2) (-(x + b / a)) → -(x + b / a) = x
⊢ (2 * a * x + b) ^ 2 = 0
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
⊢ √x = y ↔ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0

Tactic:
by
  constructor
  · rintro rfl
    rcases le_or_gt 0 x with hle | hlt
    · exact Or.inl ⟨mul_self_sqrt hle, sqrt_nonneg x⟩
    · exact Or.inr ⟨hlt, sqrt_eq_zero_of_nonpos hlt.le⟩
  · rintro (⟨rfl, hy⟩ | ⟨hx, rfl⟩)
    exacts [sqrt_mul_self hy, sqrt_eq_zero_of_nonpos hx.le]

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

Goal state before:
pp: x y : ℝ
⊢ √x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2

Tactic:
← and_iff_right_of_imp fun h => (sqrt_nonneg x).trans h,

Goal state after:
x y : ℝ
⊢ 0 ≤ y ∧ √x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ √(x * y) = √x * √y

Tactic:
rw [mul_comm, sqrt_mul hy, mul_comm]

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

Goal state before:
pp: ι : Type u_2
s : Finset ι
f g : ι → ℝ≥0
⊢ ∑ i ∈ s, sqrt (f i) * sqrt (g i) ≤ sqrt (∑ i ∈ s, f i) * sqrt (∑ i ∈ s, g i)

Tactic:
by
  simpa [*] using sum_mul_le_sqrt_mul_sqrt _ (fun x ↦ sqrt (f x)) (fun x ↦ sqrt (g x))

Goal state after:
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
⊢ ‖z + w‖ * ‖z + w‖ ≤ (‖z‖ + ‖w‖) * (‖z‖ + ‖w‖)

Tactic:
norm_mul_self_eq_normSq,

Goal state after:
z w : ℂ
⊢ normSq (z + w) ≤ (‖z‖ + ‖w‖) * (‖z‖ + ‖w‖)
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
⊢ normSq (z + w) ≤ ‖z‖ * ‖z‖ + 2 * ‖z‖ * ‖w‖ + ‖w‖ * ‖w‖

Tactic:
norm_mul_self_eq_normSq,

Goal state after:
z w : ℂ
⊢ normSq (z + w) ≤ normSq z + 2 * ‖z‖ * ‖w‖ + ‖w‖ * ‖w‖
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
⊢ normSq (z + w) ≤ normSq z + 2 * ‖z‖ * ‖w‖ + ‖w‖ * ‖w‖

Tactic:
norm_mul_self_eq_normSq,

Goal state after:
z w : ℂ
⊢ normSq (z + w) ≤ normSq z + 2 * ‖z‖ * ‖w‖ + normSq w
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f' = ∫⁻ (a : α), (f' * g) a ∂μ

Tactic:
apply lintegral_withDensity_eq_lintegral_mul_non_measurable _ hf.measurable_mk
      filter_upwards [h'f, hf.ae_eq_mk]
      intro x hx h'x
      rwa [← h'x]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
s : Set α
hs : MeasurableSet s
hμs : s.indicator f =ᵐ[μ] 0
⊢ μ s = 0

Tactic:
Filter.EventuallyEq,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
s : Set α
hs : MeasurableSet s
hμs : ∀ᵐ (x : α) ∂μ, s.indicator f x = 0 x
⊢ μ s = 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: z : ℂ
⊢ (z + (starRingEnd ℂ) z).re = (↑(2 * z.re)).re ∧ (z + (starRingEnd ℂ) z).im = (↑(2 * z.re)).im

Tactic:
by simp [two_mul, ofReal]

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

Goal state before:
pp: case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ m0 ≤ m0

Tactic:
intro _ hs

Goal state after:
case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
s✝ : Set α
hs : MeasurableSet s✝
⊢ MeasurableSet s✝
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ MeasurableEmbedding fun z0 ↦ f z0

Tactic:
intro _ hs

Goal state after:
case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ MeasurableEmbedding fun z0 ↦ f z0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ Measure.map (fun z ↦ z.1) (μ.prod ν) ≪ μ

Tactic:
intro _ hs

Goal state after:
case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
s✝ : Set α
hs : μ s✝ = 0
⊢ (Measure.map (fun z ↦ z.1) (μ.prod ν)) s✝ = 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ mβ ≤ mβ

Tactic:
intro _ hs

Goal state after:
case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
s✝ : Set β
hs : MeasurableSet s✝
⊢ MeasurableSet s✝
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ MeasurableEmbedding fun z0 ↦ g z0

Tactic:
intro _ hs

Goal state after:
case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ MeasurableEmbedding fun z0 ↦ g z0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ Measure.map (fun z ↦ z.2) (μ.prod ν) ≪ ν

Tactic:
intro _ hs

Goal state after:
case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
s✝ : Set β
hs : ν s✝ = 0
⊢ (Measure.map (fun z ↦ z.2) (μ.prod ν)) s✝ = 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ mβ ≤ mβ

Tactic:
intro _ hs

Goal state after:
case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
s✝ : Set β
hs : MeasurableSet s✝
⊢ MeasurableSet s✝
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ MeasurableEmbedding fun z0 ↦ g z0

Tactic:
intro _ hs

Goal state after:
case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ MeasurableEmbedding fun z0 ↦ g z0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ Measure.map (fun z ↦ z.2) (μ.prod ν) ≪ ν

Tactic:
intro _ hs

Goal state after:
case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
s✝ : Set β
hs : ν s✝ = 0
⊢ (Measure.map (fun z ↦ z.2) (μ.prod ν)) s✝ = 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ m0 ≤ m0

Tactic:
intro _ hs

Goal state after:
case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
s✝ : Set α
hs : MeasurableSet s✝
⊢ MeasurableSet s✝
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ MeasurableEmbedding fun z0 ↦ f z0

Tactic:
intro _ hs

Goal state after:
case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ MeasurableEmbedding fun z0 ↦ f z0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ Measure.map (fun z ↦ z.1) (μ.prod ν) ≪ μ

Tactic:
intro _ hs

Goal state after:
case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
s✝ : Set α
hs : μ s✝ = 0
⊢ (Measure.map (fun z ↦ z.1) (μ.prod ν)) s✝ = 0
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * B * star (U * B) = U * B * (star B * star U)

Tactic:
rw [star_mul]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_3
inst✝ : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
x : V₁
x✝ : x ∈ (incl s).range
y : ↥s
hy : (incl s).toAddMonoidHom y = x
⊢ x ∈ s

Tactic:
rw [← hy]; simp

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f g : NormedAddGroupHom V W
x : ↥(f.equalizer g)
⊢ f ((ι f g) x) = g ((ι f g) x)

Tactic:
← sub_eq_zero,

Goal state after:
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f g : NormedAddGroupHom V W
x : ↥(f.equalizer g)
⊢ f ((ι f g) x) - g ((ι f g) x) = 0
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: case negSucc
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarMul R
U : ↥(unitary R)
a✝ : ℕ
⊢ ↑(U ^ Int.negSucc a✝) = ↑U ^ Int.negSucc a✝

Tactic:
· simp [coe_inv]

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

Goal state before:
pp: case neg
ι : 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 ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f L
hL : ¬L.NeBot
⊢ ∑ᶠ (z : ι), e (f z) = y ↔ e (∑ᶠ (z : ι), f z) = y

Tactic:
constructor <;> rintro rfl

Goal state after:
case neg.mp
ι : 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 ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
hf : Summable f L
hL : ¬L.NeBot
⊢ e (∑ᶠ (z : ι), f z) = ∑ᶠ (z : ι), e (f z)

case neg.mpr
ι : 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 ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
hf : Summable f L
hL : ¬L.NeBot
⊢ ∑ᶠ (z : ι), e (f z) = e (∑ᶠ (z : ι), f z)
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
a : A
⊢ IsSelfAdjoint (I • a) ↔ a ∈ skewAdjoint A

Tactic:
simp [← I_smul_mem_skewAdjoint_iff_isSelfAdjoint, smul_smul]

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

Goal state before:
pp: r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
⊢ (∀ x ∈ s, ¬x ≤ 0) ↔ -↑r ∉ s

Tactic:
contrapose!

Goal state after:
r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
⊢ (∃ x ∈ s, x ≤ 0) ↔ -↑r ∈ s
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 : A
⊢ ℑ x = 0 ↔ IsSelfAdjoint x

Tactic:
simpa [-ker_imaginaryPart] using! SetLike.ext_iff.mp ker_imaginaryPart x

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ star x * x = x * star x ↔ Commute ↑(ℜ x) ↑(ℑ x)

Tactic:
← sub_eq_zero,

Goal state after:
A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ star x * x - x * star x = 0 ↔ Commute ↑(ℜ x) ↑(ℑ x)
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ IsStarNormal x ↔ Commute ↑(ℜ x) ↑(ℑ x)

Tactic:
by
  rw [isStarNormal_iff, commute_iff_eq, ← sub_eq_zero, star_mul_self_sub_self_mul_star,
    two_smul ℕ, ← two_smul ℂ, smul_eq_zero_iff_right two_ne_zero, smul_eq_zero_iff_right I_ne_zero,
    sub_eq_zero, commute_iff_eq]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ ‖(starRingEnd K) x + x‖ ^ 2 = re ((starRingEnd K) x + x) ^ 2

Tactic:
by
  rw [add_comm, norm_sq_re_add_conj]

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : PartialHomeomorph X Y
f : PartialEquiv X Y
h : IsHomeomorph ⇑f.toEquiv
⊢ ContinuousOn (↑f) f.source

Tactic:
rw [continuousOn_iff_continuous_domRestrict,
      ← continuous_codRestrict_iff (s := f.target) (by simp)]
    exact h.continuous

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ IsOpen[inst✝] (range (e.source.domRestrict ↑e))

Tactic:
by
    rw [range_domRestrict, image_source_eq_target]
    exact e.open_target

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z w : K
hz : 0 < z
hw : 0 < w
⊢ 0 < z * w

Tactic:
rw [lt_iff_re_im, map_zero] at hz hw ⊢

Goal state after:
K : Type u_1
inst✝ : RCLike K
z w : K
hz : 0 < re z ∧ im 0 = im z
hw : 0 < re w ∧ im 0 = im w
⊢ 0 < re (z * w) ∧ im 0 = im (z * w)
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Y → Z
s : Set Y
h : s ⊆ e.target
x : Y
hx : x ∈ s
⊢ e.source ∈ 𝓝 (↑e.symm x)

Tactic:
exact IsOpen.mem_nhds e.open_source (e.map_target (h hx))

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (fun x ↦ -f' x) =O[l] g ↔ f' =O[l] g

Tactic:
simp only [IsBigO_def]
  exact exists_congr fun _ => isBigOWith_neg_left

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
⊢ (fun x ↦ c • f' x) =O[l] g ↔ f' =O[l] g

Tactic:
have cne0 : ‖c‖ ≠ 0 := norm_ne_zero_iff.mpr hc
  rw [← isBigO_norm_left]
  simp only [norm_smul]
  rw [isBigO_const_mul_left_iff cne0, isBigO_norm_left]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: 𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
c : ℝ
hc : ∀ᶠ (a : α) in l, ‖f a‖ / ‖g a‖ ≤ c
⊢ f =O[l] g

Tactic:
refine IsBigO.of_bound c (hc.mp <| hgf.mono fun x hx₁ hx₂ => ?_)

Goal state after:
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
c : ℝ
hc : ∀ᶠ (a : α) in l, ‖f a‖ / ‖g a‖ ≤ c
x : α
hx₁ : g x = 0 → f x = 0
hx₂ : ‖f x‖ / ‖g x‖ ≤ c
⊢ ‖f x‖ ≤ c * ‖g x‖