mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : MeasurableSpace β
inst✝⁸ : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁷ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝⁶ : PseudoMetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : PseudoMetricSpace Y
inst✝³ : MeasurableSpace Y
μ : Measure X
ν : Measure Y
inst✝² : SFinite ν
inst✝¹ : IsUnifLocDoublingMeasure μ
inst✝ : IsUnifLocDoublingMeasure ν
r : ℝ
hμr : ∀ (x : X), μ (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant μ) * μ (Metric.closedBall x r)
hνr : ∀ (x : Y), ν (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant ν) * ν (Metric.closedBall x r)
x : X × Y
⊢ ↑(doublingConstant μ) * μ (Metric.closedBall x.1 r) * (↑(doublingConstant ν) * ν (Metric.closedBall x.2 r)) ≤
    ↑(doublingConstant μ * doublingConstant ν) * (μ (Metric.closedBall x.1 r) * ν (Metric.closedBall x.2 r))

Tactic:
ENNReal.coe_mul,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : MeasurableSpace β
inst✝⁸ : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁷ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝⁶ : PseudoMetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : PseudoMetricSpace Y
inst✝³ : MeasurableSpace Y
μ : Measure X
ν : Measure Y
inst✝² : SFinite ν
inst✝¹ : IsUnifLocDoublingMeasure μ
inst✝ : IsUnifLocDoublingMeasure ν
r : ℝ
hμr : ∀ (x : X), μ (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant μ) * μ (Metric.closedBall x r)
hνr : ∀ (x : Y), ν (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant ν) * ν (Metric.closedBall x r)
x : X × Y
⊢ ↑(doublingConstant μ) * μ (Metric.closedBall x.1 r) * (↑(doublingConstant ν) * ν (Metric.closedBall x.2 r)) ≤
    ↑(doublingConstant μ) * ↑(doublingConstant ν) * (μ (Metric.closedBall x.1 r) * ν (Metric.closedBall x.2 r))
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ = 0 ↔ (fun x ↦ ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0

Tactic:
lintegral_eq_zero_iff (measurable_measure_prodMk_left hs)

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ (fun x ↦ ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0 ↔ (fun x ↦ ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
⊢ QuasiMeasurePreserving Prod.fst (μ.prod ν) μ

Tactic:
by
  refine ⟨measurable_fst, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩
  rw [map_apply measurable_fst hs, ← prod_univ, ← nonpos_iff_eq_zero]
  refine (prod_prod_le _ _).trans_eq ?_
  rw [h2s, zero_mul]

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

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure β
pa qa : Set α → Prop
pb qb : Set β → Prop
H : μ.InnerRegularWRT pb qb
f : α → β
hf : MeasurableEmbedding f
hAB : ∀ (U : Set α), qa U → qb (f '' U)
hAB' : ∀ K ⊆ range f, pb K → pa (f ⁻¹' K)
U : Set α
hU : qa U
r : ℝ≥0∞
hr : r < μ (f '' U)
K : Set β
hKU : K ⊆ f '' U
hK : pb K
hμU : r < μ K
hKrange : K ⊆ range f
⊢ f ⁻¹' K ⊆ U

Tactic:
← hf.injective.preimage_image U

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure β
pa qa : Set α → Prop
pb qb : Set β → Prop
H : μ.InnerRegularWRT pb qb
f : α → β
hf : MeasurableEmbedding f
hAB : ∀ (U : Set α), qa U → qb (f '' U)
hAB' : ∀ K ⊆ range f, pb K → pa (f ⁻¹' K)
U : Set α
hU : qa U
r : ℝ≥0∞
hr : r < μ (f '' U)
K : Set β
hKU : K ⊆ f '' U
hK : pb K
hμU : r < μ K
hKrange : K ⊆ range f
⊢ f ⁻¹' K ⊆ f ⁻¹' f '' U
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
⊢ Nat.card ↑(⇑H.subtype '' S) * Nat.card ↥(map H.subtype H'') = Nat.card ↑S * Nat.card ↑↑H''

Tactic:
refine congr_arg₂ (· * ·) ?_ ?_

Goal state after:
case refine_2.refine_1
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
⊢ Nat.card ↑(⇑H.subtype '' S) = Nat.card ↑S

case refine_2.refine_2
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
⊢ Nat.card ↥(map H.subtype H'') = Nat.card ↑↑H''
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this✝ : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'') S
this : Nat.card ↥H'' * Nat.card ↑S = Nat.card ↥H
⊢ Nat.card ↥(map H.subtype H'') * Nat.card ↑(⇑H.subtype '' S) = Nat.card ↥H'' * Nat.card ↑S

Tactic:
refine congr_arg₂ (· * ·) ?_ ?_

Goal state after:
case refine_2.refine_1
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this✝ : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'') S
this : Nat.card ↥H'' * Nat.card ↑S = Nat.card ↥H
⊢ Nat.card ↥(map H.subtype H'') = Nat.card ↥H''

case refine_2.refine_2
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this✝ : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'') S
this : Nat.card ↥H'' * Nat.card ↑S = Nat.card ↥H
⊢ Nat.card ↑(⇑H.subtype '' S) = Nat.card ↑S
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'') S
⊢ Nat.card ↥(map H.subtype H'') * Nat.card ↑(⇑H.subtype '' S) = Nat.card ↥H

Tactic:
have : Nat.card H'' * Nat.card S = Nat.card H := cmem.card_mul_card
    rw [← this]
    refine congr_arg₂ (· * ·) ?_ ?_ <;>
      exact Nat.card_congr (Equiv.Set.image _ _ <| subtype_injective H).symm

Goal state after:
Module: Mathlib.GroupTheory.Complement

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

Tactic:
equiv_snd_eq_self_iff_mem _ h1

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
⊢ g ∈ T ↔ g ∈ T
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.IsComplement' K
⊢ IsCompl H K

Tactic:
refine
    ⟨disjoint_iff_inf_le.mpr fun g ⟨p, q⟩ =>
        let x : H × K := ⟨⟨g, p⟩, 1⟩
        let y : H × K := ⟨1, g, q⟩
        Subtype.ext_iff.mp
          (Prod.ext_iff.mp (show x = y from h.1 ((mul_one g).trans (one_mul g).symm))).1,
      codisjoint_iff_le_sup.mpr fun g _ => ?_⟩
  obtain ⟨⟨h, k⟩, rfl⟩ := h.2 g
  exact Subgroup.mul_mem_sup h.2 k.2

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

Goal state before:
pp: G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_3
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable ⇑f
h_surj : Surjective ⇑f
g : G
| Measure.map (⇑f) μ

Tactic:
rw [← map_mul_left_eq_self μ g]

Goal state after:
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_3
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable ⇑f
h_surj : Surjective ⇑f
g : G
| Measure.map (⇑f) (Measure.map (fun x ↦ g * x) μ)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (μ + ν) s
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν) K

Tactic:
simp only [Measure.coe_add, Pi.add_apply] at hr

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s + ν s
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν) K
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (withDensity 0 f) s = 0 s

Tactic:
rw [withDensity_apply _ hs]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂0 = 0 s
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
this : map (fun x ↦ g * x) (map Inv.inv μ) = map (fun x ↦ g * x⁻¹) μ
| μ

Tactic:
rw [← map_mul_left_eq_self μ g]

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
this : map (fun x ↦ g * x) (map Inv.inv μ) = map (fun x ↦ g * x⁻¹) μ
| map (fun x ↦ g * x) μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : 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 = ∫⁻ (a : α) in s, f a ∂μ.trim hm

Tactic:
restrict_trim _ _ 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 = ∫⁻ (a : α), f a ∂(μ.restrict s).trim hm
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
A : ∀ᵐ (x : α) ∂μ, x ∈ toMeasurable (μ.withDensity f) s → f x = 0 x
⊢ μ ({x | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) = 0

pp: case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
A : ∀ᵐ (x : α) ∂μ.restrict (toMeasurable (μ.withDensity f) s), f x = 0 x
⊢ NullMeasurableSet (toMeasurable (μ.withDensity f) s) μ

Tactic:
ae_iff

Goal state after:
case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
A : μ {a | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0 a)} = 0
⊢ μ ({x | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) = 0

case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
A : ∀ᵐ (x : α) ∂μ.restrict (toMeasurable (μ.withDensity f) s), f x = 0 x
⊢ NullMeasurableSet (toMeasurable (μ.withDensity f) s) μ
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : Group G
inst✝⁸ : TopologicalSpace G
μ : Measure G
inst✝⁷ : μ.IsHaarMeasure
inst✝⁶ : BorelSpace G
inst✝⁵ : ContinuousMul G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : MeasurableSpace H
inst✝¹ : BorelSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst✝⁸, inst✝³] ⇑f
h_surj : Surjective ⇑f
h_prop : Tendsto (⇑f) (cocompact G) (cocompact H)
K : Set H
hK : IsCompact K
⊢ (map (⇑f) μ) K < ∞

Tactic:
rw [← hK.measure_closure, map_apply hf.measurable isClosed_closure.measurableSet]

Goal state after:
G : Type u_1
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : Group G
inst✝⁸ : TopologicalSpace G
μ : Measure G
inst✝⁷ : μ.IsHaarMeasure
inst✝⁶ : BorelSpace G
inst✝⁵ : ContinuousMul G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : MeasurableSpace H
inst✝¹ : BorelSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst✝⁸, inst✝³] ⇑f
h_surj : Surjective ⇑f
h_prop : Tendsto (⇑f) (cocompact G) (cocompact H)
K : Set H
hK : IsCompact K
⊢ μ (⇑f ⁻¹' closure[inst✝³] K) < ∞
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (f n x) (g x) < ε
⊢ μ (s ∩ ⋂ j, notConvergentSeq f g n j) = 0

Tactic:
ae_iff

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (f n a) (g a) < ε)} = 0
⊢ μ (s ∩ ⋂ j, notConvergentSeq f g n j) = 0
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ QuasiMeasurePreserving (fun h ↦ g * h) μ μ

Tactic:
by
  have :=
    (quasiMeasurePreserving_mul_right μ.inv g⁻¹).mono (inv_absolutelyContinuous μ.inv)
      (absolutelyContinuous_inv μ.inv)
  rw [μ.inv_inv] at this
  have :=
    (quasiMeasurePreserving_inv_of_right_invariant μ).comp
      (this.comp (quasiMeasurePreserving_inv_of_right_invariant μ))
  simp_rw [Function.comp_def, mul_inv_rev, inv_inv] at this
  exact this

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

Goal state before:
pp: x : ℝ
⊢ x.toNNReal = 0 ↔ x ≤ 0

Tactic:
Real.toNNReal_eq_zero

Goal state after:
x : ℝ
⊢ x ≤ 0 ↔ x ≤ 0
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 : ∀ᵐ (x : α) ∂μ, s.indicator f x = 0 x
⊢ μ s = 0

Tactic:
ae_iff

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 : μ {a | ¬s.indicator f a = 0 a} = 0
⊢ μ s = 0
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
ε : Type u_4
m : MeasurableSpace α
inst✝¹ : ENorm ε
inst✝ : MeasurableSingletonClass α
f : α → ε
⊢ HasFiniteIntegral f Measure.count ↔ ∑' (x : α), ‖f x‖ₑ < ∞

Tactic:
by
  simp only [hasFiniteIntegral_iff_enorm, lintegral_count]

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

Goal state before:
pp: r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ ↑z.re = z

Tactic:
← conj_eq_iff_re,

Goal state after:
r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ (starRingEnd ℂ) z = z
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
⊢ star (U * B) * (U * B) = star B * star U * U * B

Tactic:
by simp only [mul_assoc, star_mul]

Goal state after:
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 ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
⊢ ∑'[L] (z : ι), f z = e.symm (e (∑'[L] (z : ι), f z))

Tactic:
e.symm_apply_apply _

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 ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
⊢ ∑'[L] (z : ι), f z = ∑'[L] (z : ι), f z
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z + (starRingEnd K) z = ↑(re z) + ↑(im z) * I + (↑(re z) - ↑(im z) * I)

Tactic:
rw [re_add_im, conj_eq_re_sub_im]

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
⊢ IsStarNormal x ↔ Commute ↑(ℜ x) ↑(ℑ x)

Tactic:
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
⊢ I⁻¹ = -I

Tactic:
by_cases h : (I : K) = 0

Goal state after:
case pos
K : Type u_1
inst✝ : RCLike K
h : I = 0
⊢ I⁻¹ = -I

case neg
K : Type u_1
inst✝ : RCLike K
h : ¬I = 0
⊢ I⁻¹ = -I
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
a : K
h : ‖a‖ ≤ re a
⊢ ↑(re a) = a

Tactic:
← conj_eq_iff_re,

Goal state after:
K : Type u_1
inst✝ : RCLike K
a : K
h : ‖a‖ ≤ re a
⊢ (starRingEnd K) a = a
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝³ : RCLike K
inst✝² : NormedField E
inst✝¹ : CharZero E
inst✝ : NormedSpace K E
ι : Type u_3
s : Finset ι
f : ι → E
x✝¹ : ℕ
x✝ : E
⊢ ‖(↑x✝¹)⁻¹ • x✝‖ = (↑x✝¹)⁻¹ • ‖x✝‖

Tactic:
norm_nnqsmul K

Goal state after:
K : Type u_1
E : Type u_2
inst✝³ : RCLike K
inst✝² : NormedField E
inst✝¹ : CharZero E
inst✝ : NormedSpace K E
ι : Type u_3
s : Finset ι
f : ι → E
x✝¹ : ℕ
x✝ : E
⊢ (↑x✝¹)⁻¹ • ‖x✝‖ = (↑x✝¹)⁻¹ • ‖x✝‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (f =o[l] fun x ↦ ‖g' x‖) ↔ f =o[l] g'

Tactic:
by
  simp only [IsLittleO_def]
  exact forall₂_congr fun _ _ => isBigOWith_norm_right

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
⊢ ∀ j ≥ max n i, abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) (max n i)) < ε

Tactic:
intro j ji

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
j : ℕ
ji : j ≥ max n i
⊢ abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) (max n i)) < ε
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ insert n' (Finset.range n') = Finset.cons n' (Finset.range n') ⋯

Tactic:
Finset.insert_eq_cons

Goal state after:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ Finset.cons n' (Finset.range n') ?h = Finset.cons n' (Finset.range n') ⋯

case h
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ n' ∉ Finset.range n'
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
R : Type u_13
inst✝³ : SeminormedRing R
S : Type u_17
inst✝² : NormedRing S
inst✝¹ : NormMulClass S
c : ℝ
l : Filter α
inst✝ : NormOneClass S
f : α → R
g : α → S
h : IsBigOWith c l f g
n : ℕ
⊢ IsBigOWith (Nat.casesOn (n + 2) ‖1‖ fun n ↦ c ^ (n + 1)) l (fun x ↦ f x ^ (n + 2)) fun x ↦ g x ^ (n + 2)

Tactic:
simpa [pow_succ] using (IsBigOWith.pow' h (n + 1)).mul h

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
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
h : ∀ i ∈ s, A i =O[l] g
⊢ (∑ i ∈ s, A i) =O[l] g

Tactic:
simp only [IsBigO_def] at *

Goal state after:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
h : ∀ i ∈ s, ∃ c, IsBigOWith c l (A i) g
⊢ ∃ c, IsBigOWith c l (∑ i ∈ s, A i) g
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
B : ι → α → ℝ
hAB : ∀ i ∈ s, A i =O[l] B i
⊢ (fun H ↦ ∑ i ∈ s, A i H) =O[l] fun H ↦ ∑ i ∈ s, ‖B i H‖

Tactic:
simp only [IsBigO_def] at *

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
B : ι → α → ℝ
hAB : ∀ i ∈ s, ∃ c, IsBigOWith c l (A i) (B i)
⊢ ∃ c, IsBigOWith c l (fun H ↦ ∑ i ∈ s, A i H) fun H ↦ ∑ i ∈ s, ‖B i H‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
C : ℝ
i : α → Finset ι
hAB : ∀ᶠ (x : ι × α) in ⊤ ×ˢ l, ‖Function.uncurry A x‖ ≤ C * ‖Function.uncurry B x‖
s₁ : ι → Prop
hs₁ : ∀ᶠ (x : ι) in ⊤, s₁ x
s₂ : α → Prop
hs₂ : ∀ᶠ (y : α) in l, s₂ y
hbound : ∀ {x : ι}, s₁ x → ∀ {y : α}, s₂ y → ‖Function.uncurry A (x, y)‖ ≤ C * ‖Function.uncurry B (x, y)‖
H : α
⊢ s₂ H → ‖∑ j ∈ i H, A j H‖ ≤ C * ‖∑ j ∈ i H, ‖B j H‖‖

Tactic:
hH

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
C : ℝ
i : α → Finset ι
hAB : ∀ᶠ (x : ι × α) in ⊤ ×ˢ l, ‖Function.uncurry A x‖ ≤ C * ‖Function.uncurry B x‖
s₁ : ι → Prop
hs₁ : ∀ᶠ (x : ι) in ⊤, s₁ x
s₂ : α → Prop
hs₂ : ∀ᶠ (y : α) in l, s₂ y
hbound : ∀ {x : ι}, s₁ x → ∀ {y : α}, s₂ y → ‖Function.uncurry A (x, y)‖ ≤ C * ‖Function.uncurry B (x, y)‖
H : α
hH : s₂ H
⊢ ‖∑ j ∈ i H, A j H‖ ≤ C * ‖∑ j ∈ i H, ‖B j H‖‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x y : ℂ
j m : ℕ
x✝ : m ∈ range j
⊢ (x + y) ^ m / ↑m.factorial = ∑ k ∈ range (m + 1), x ^ k / ↑k.factorial * (y ^ (m - k) / ↑(m - k).factorial)

Tactic:
add_pow,

Goal state after:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
⊢ (∑ m_1 ∈ range (m + 1), x ^ m_1 * y ^ (m - m_1) * ↑(m.choose m_1)) / ↑m.factorial =
    ∑ k ∈ range (m + 1), x ^ k / ↑k.factorial * (y ^ (m - k) / ↑(m - k).factorial)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
⊢ (starRingEnd ℂ) (cexp ↑x) = cexp ↑x

Tactic:
rw [← exp_conj, conj_ofReal]

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

Goal state before:
pp: x : ℂ
⊢ sinh (2 * x) = 2 * sinh x * cosh x

Tactic:
rw [two_mul, sinh_add]
  ring

Goal state after: