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

Goal state before:
pp: case inr.inr
α : 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
h : μ s ≠ 0
h' : ν s ≠ 0
u : ℝ≥0∞
hu : u < μ s
v : ℝ≥0∞
hv : v < ν s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < μ K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < ν K'
⊢ μ K + ν K' ≤ μ (K ∪ K') + ν (K ∪ K')

Tactic:
gcongr

Goal state after:
case h
α : 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
h : μ s ≠ 0
h' : ν s ≠ 0
u : ℝ≥0∞
hu : u < μ s
v : ℝ≥0∞
hv : v < ν s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < μ K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < ν K'
⊢ K ⊆ K ∪ K'

case h
α : 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
h : μ s ≠ 0
h' : ν s ≠ 0
u : ℝ≥0∞
hu : u < μ s
v : ℝ≥0∞
hv : v < ν s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < μ K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < ν K'
⊢ K' ⊆ K ∪ K'
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⁻¹) μ
⊢ μ ≪ map (fun x ↦ g * x) (map Inv.inv μ)

Tactic:
conv_lhs => 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) μ ≪ map (fun x ↦ g * x) (map Inv.inv μ)
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
⊢ (μ.withDensity f) univ < ∞

Tactic:
by
      rwa [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ, lt_top_iff_ne_top]

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
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := ⋯
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed[inst✝⁷] (L n)
M : ∀ (n : ℕ), μ (L n) = ↑(n + 1) * μ K
⊢ Tendsto (fun x ↦ ↑(x + 1)) atTop (𝓝 ∞)

Tactic:
exact ENNReal.tendsto_nat_nhds_top.comp (tendsto_add_atTop_nat _)

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁴] K
hμK : μ (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst✝⁴] U
hμU : μ U < μ K + ε / 2
⊢ μ (U \ s) + μ (s \ U) < ε / 2 + ε / 2

Tactic:
gcongr

Goal state after:
case ac
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁴] K
hμK : μ (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst✝⁴] U
hμU : μ U < μ K + ε / 2
⊢ μ (U \ s) < ε / 2

case bd
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁴] K
hμK : μ (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst✝⁴] U
hμU : μ U < μ K + ε / 2
⊢ μ (s \ U) < ε / 2
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁴] K
hμK : μ (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst✝⁴] U
hμU : μ U < μ K + ε / 2
⊢ μ (U \ s) ≤ μ (U \ K)

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁴] K
hμK : μ (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst✝⁴] U
hμU : μ U < μ K + ε / 2
⊢ μ K ≤ μ s

Tactic:
gcongr

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
hμs : μ' s ≠ ∞
this : ∀ {s : Set G}, μ' s ≠ ∞ → MeasurableSet s → ∀ᵐ (x : G) ∂μ', ν' ((fun x_1 ↦ x_1 * x) ⁻¹' s) < ∞
sm : ¬MeasurableSet s
x : G
hx : ν' ((fun x_1 ↦ x_1 * x) ⁻¹' toMeasurable μ' s) < ∞
⊢ ν' ((fun x_1 ↦ x_1 * x) ⁻¹' s) ≤ ν' ((fun x_1 ↦ x_1 * x) ⁻¹' toMeasurable μ' s)

Tactic:
gcongr

Goal state after:
case h
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
hμs : μ' s ≠ ∞
this : ∀ {s : Set G}, μ' s ≠ ∞ → MeasurableSet s → ∀ᵐ (x : G) ∂μ', ν' ((fun x_1 ↦ x_1 * x) ⁻¹' s) < ∞
sm : ¬MeasurableSet s
x : G
hx : ν' ((fun x_1 ↦ x_1 * x) ⁻¹' toMeasurable μ' s) < ∞
⊢ s ⊆ toMeasurable μ' s
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁴] K
hμK : μ (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst✝⁴] U
hμU : μ U < μ K + ε / 2
⊢ μ (s \ U) ≤ μ (s \ K)

Tactic:
gcongr

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

Goal state before:
pp: case inr
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s t : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
this : ∀ (s : Set G), ν' s ≠ 0 → ν' s ≠ ∞ → MeasurableSet s → μ' s * ν' t = ν' s * μ' t
hs : ¬MeasurableSet s
s' : Set G
hm : MeasurableSet s'
hμ : μ' s' = μ' s
hν : ν' s' = ν' s
⊢ μ' s' * ν' t = ν' s' * μ' t

Tactic:
this s' _ _ hm

Goal state after:
case inr
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s t : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
this : ∀ (s : Set G), ν' s ≠ 0 → ν' s ≠ ∞ → MeasurableSet s → μ' s * ν' t = ν' s * μ' t
hs : ¬MeasurableSet s
s' : Set G
hm : MeasurableSet s'
hμ : μ' s' = μ' s
hν : ν' s' = ν' s
⊢ ν' s' * μ' t = ν' s' * μ' t

G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s t : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
this : ∀ (s : Set G), ν' s ≠ 0 → ν' s ≠ ∞ → MeasurableSet s → μ' s * ν' t = ν' s * μ' t
hs : ¬MeasurableSet s
s' : Set G
hm : MeasurableSet s'
hμ : μ' s' = μ' s
hν : ν' s' = ν' s
⊢ ν' s' ≠ 0

G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s t : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
this : ∀ (s : Set G), ν' s ≠ 0 → ν' s ≠ ∞ → MeasurableSet s → μ' s * ν' t = ν' s * μ' t
hs : ¬MeasurableSet s
s' : Set G
hm : MeasurableSet s'
hμ : μ' s' = μ' s
hν : ν' s' = ν' s
⊢ ν' s' ≠ ∞
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ≥0
⊢ x * y ≤ max x y * max x y

Tactic:
gcongr

Goal state after:
case h₁
x y : ℝ≥0
⊢ x ≤ max x y

case h₂
x y : ℝ≥0
⊢ y ≤ max x y
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ⊢ √1 < √2

Tactic:
gcongr

Goal state after:
case h
⊢ 1 < 2
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
⊢ normSq z + normSq ((starRingEnd ℂ) w) + 2 * (z * (starRingEnd ℂ) w).re ≤
    normSq z + normSq ((starRingEnd ℂ) w) + 2 * √(normSq (z * (starRingEnd ℂ) w))

Tactic:
gcongr

Goal state after:
case hbc
z w : ℂ
⊢ (z * (starRingEnd ℂ) w).re ≤ √(normSq (z * (starRingEnd ℂ) w))
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: r s : ℝ
⊢ (↑(r + s)).re = (↑r + ↑s).re ∧ (↑(r + s)).im = (↑r + ↑s).im

Tactic:
simp [ofReal]

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

Goal state before:
pp: r : ℝ
⊢ (↑(-r)).re = (-↑r).re ∧ (↑(-r)).im = (-↑r).im

Tactic:
simp [ofReal]

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
⊢ (cauSeqRe f).lim = (↑(cauSeqRe f).lim + ↑(cauSeqIm f).lim * I).re

Tactic:
simp [ofReal]

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

Goal state before:
pp: r s : ℝ
⊢ (↑(r * s)).re = (↑r * ↑s).re ∧ (↑(r * s)).im = (↑r * ↑s).im

Tactic:
simp [ofReal]

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

Goal state before:
pp: r : ℝ
z : ℂ
⊢ (↑r * z).re = r * z.re

Tactic:
simp [ofReal]

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

Goal state before:
pp: r : ℝ
z : ℂ
⊢ (↑r * z).im = r * z.im

Tactic:
simp [ofReal]

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

Goal state before:
pp: z : ℂ
r : ℝ
⊢ (z * ↑r).re = z.re * r

Tactic:
simp [ofReal]

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

Goal state before:
pp: z : ℂ
r : ℝ
⊢ (z * ↑r).im = z.im * r

Tactic:
simp [ofReal]

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
⊢ (cauSeqIm f).lim = (↑(cauSeqRe f).lim + ↑(cauSeqIm f).lim * I).im

Tactic:
simp [ofReal]

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

Goal state before:
pp: a b : ℝ
⊢ { re := a, im := b }.re = (↑a + ↑b * I).re ∧ { re := a, im := b }.im = (↑a + ↑b * I).im

Tactic:
simp [ofReal]

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

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

Tactic:
simp [ofReal]

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

Goal state before:
pp: case refine_1.hs
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
n : ℕ
⊢ μ (spanningSets μ n ∩ f ⁻¹' Iic ↑n) ≠ ∞

pp: case refine_1.hbdd
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
n : ℕ
⊢ BddAbove (f '' (spanningSets μ n ∩ f ⁻¹' Iic ↑n))

Tactic:
· exact ((measure_mono inter_subset_left).trans_lt (measure_spanningSets_lt_top μ n)).ne

Goal state after:
case refine_1.hbdd
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
n : ℕ
⊢ BddAbove (f '' (spanningSets μ n ∩ f ⁻¹' Iic ↑n))
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: r : ℝ
⊢ ↑(↑r).re = ↑r

Tactic:
simp [ofReal]

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

Goal state before:
pp: r s : ℝ
⊢ (↑(r - s)).re = (↑r - ↑s).re ∧ (↑(r - s)).im = (↑r - ↑s).im

Tactic:
simp [ofReal]

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

Goal state before:
pp: r : ℝ
⊢ (↑r⁻¹).re = (↑r)⁻¹.re ∧ (↑r⁻¹).im = (↑r)⁻¹.im

Tactic:
simp [ofReal]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : AddCommMonoid α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Module ℚ≥0 α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
⊢ 𝔼 i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0

Tactic:
by
  simp +contextual [expect, sum_eq_zero_iff_of_nonneg hf]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : ExistsAddOfLE R
inst✝¹ : Module ℚ≥0 R
inst✝ : PosSMulMono ℚ≥0 R
s : Finset ι
f g : ι → R
⊢ (↑(#s) ^ 2)⁻¹ • (∑ x ∈ s, f x * g x) ^ 2 ≤ (↑(#s) ^ 2)⁻¹ • ((∑ x ∈ s, f x ^ 2) * ∑ x ∈ s, g x ^ 2)

Tactic:
gcongr

Goal state after:
case hb
ι : Type u_1
R : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : ExistsAddOfLE R
inst✝¹ : Module ℚ≥0 R
inst✝ : PosSMulMono ℚ≥0 R
s : Finset ι
f g : ι → R
⊢ (∑ x ∈ s, f x * g x) ^ 2 ≤ (∑ x ∈ s, f x ^ 2) * ∑ x ∈ s, g x ^ 2
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 : V → W
M : ℝ
h : ∀ (x : V), ‖f x‖ ≤ M * ‖x‖
x : V
⊢ M * ‖x‖ ≤ max M 1 * ‖x‖

Tactic:
gcongr

Goal state after:
case hbc
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f : V → W
M : ℝ
h : ∀ (x : V), ‖f x‖ ≤ M * ‖x‖
x : V
⊢ M ≤ max M 1
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : f.SurjectiveOnWith K C
H : C ≤ C'
g : V₁
k_in : f g ∈ K
hg : ‖g‖ ≤ C * ‖f g‖
Hg : ¬‖f g‖ = 0
⊢ C * ‖f g‖ ≤ C' * ‖f g‖

Tactic:
gcongr

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

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
c : ℝ
x : V₁
h : ‖x‖ ≤ c
⊢ ‖f‖ * ‖x‖ ≤ ‖f‖ * c

Tactic:
gcongr

Goal state after:
case ha
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
c : ℝ
x : V₁
h : ‖x‖ ≤ c
⊢ 0 ≤ ‖f‖
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
c : ℝ
h : ‖f‖ ≤ c
x : V₁
⊢ ‖f‖ * ‖x‖ ≤ c * ‖x‖

Tactic:
gcongr

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

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : V₁ →+ V₂
C : ℝ
h : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖
x : V₁
⊢ C * ‖x‖ ≤ max C 0 * ‖x‖

Tactic:
gcongr

Goal state after:
case hbc
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : V₁ →+ V₂
C : ℝ
h : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖
x : V₁
⊢ C ≤ max C 0
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f g : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖f v‖ + ‖g v‖ ≤ ‖f‖ * ‖v‖ + ‖g‖ * ‖v‖

Tactic:
gcongr

Goal state after:
case h₁
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f g : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖f v‖ ≤ ‖f‖ * ‖v‖

case h₂
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f g : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖g v‖ ≤ ‖g‖ * ‖v‖
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝¹¹ : SeminormedAddCommGroup V
inst✝¹⁰ : SeminormedAddCommGroup V₁
inst✝⁹ : SeminormedAddCommGroup V₂
inst✝⁸ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst✝⁷ : MonoidWithZero R
inst✝⁶ : DistribMulAction R V₂
inst✝⁵ : PseudoMetricSpace R
inst✝⁴ : IsBoundedSMul R V₂
inst✝³ : MonoidWithZero R'
inst✝² : DistribMulAction R' V₂
inst✝¹ : PseudoMetricSpace R'
inst✝ : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this : ‖r • f x‖ ≤ dist r 0 * ‖f x‖
⊢ dist r 0 * ‖f x‖ ≤ dist r 0 * (b * ‖x‖)

Tactic:
gcongr

Goal state after:
case hbc
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝¹¹ : SeminormedAddCommGroup V
inst✝¹⁰ : SeminormedAddCommGroup V₁
inst✝⁹ : SeminormedAddCommGroup V₂
inst✝⁸ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst✝⁷ : MonoidWithZero R
inst✝⁶ : DistribMulAction R V₂
inst✝⁵ : PseudoMetricSpace R
inst✝⁴ : IsBoundedSMul R V₂
inst✝³ : MonoidWithZero R'
inst✝² : DistribMulAction R' V₂
inst✝¹ : PseudoMetricSpace R'
inst✝ : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this : ‖r • f x‖ ≤ dist r 0 * ‖f x‖
⊢ ‖f x‖ ≤ b * ‖x‖
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
n : ℕ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ↑n * ‖f v‖ ≤ ↑n * (b * ‖v‖)

Tactic:
gcongr

Goal state after:
case hbc
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
n : ℕ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖f v‖ ≤ b * ‖v‖
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
z : ℤ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖z‖ * ‖f v‖ ≤ ‖z‖ * (b * ‖v‖)

Tactic:
gcongr

Goal state after:
case hbc
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
z : ℤ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖f v‖ ≤ b * ‖v‖
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖g‖ * ‖f v‖ ≤ ‖g‖ * (‖f‖ * ‖v‖)

Tactic:
gcongr

Goal state after:
case hbc
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖f v‖ ≤ ‖f‖ * ‖v‖
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
C₁ C₂ : ℝ
hg : ‖g‖ ≤ C₂
hf : ‖f‖ ≤ C₁
⊢ ‖g‖ * ‖f‖ ≤ C₂ * C₁

Tactic:
gcongr

Goal state after:
case b0
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
C₁ C₂ : ℝ
hg : ‖g‖ ≤ C₂
hf : ‖f‖ ≤ C₁
⊢ 0 ≤ C₂
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : NonUnitalNormedRing E
inst✝ : StarRing E
h : ∀ (x : E), ‖x‖ * ‖x‖ ≤ ‖x * x⋆‖
x : E
hx : 0 < ‖x⋆‖
⊢ ‖x⋆‖ ≤ ‖x‖

Tactic:
· refine le_of_mul_le_mul_right ?_ hx
          simpa [sq, mul_comm ‖x⋆‖] using h x⋆ |>.trans <| norm_mul_le _ _

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

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

Tactic:
by
  simp only [I_re, zero_sub, I_im', zero_mul, mul_re]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
⊢ ∀ (x y : ℂ),
    (Algebra.linearMap ℝ A ∘ₗ reLm + LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) (x * y) =
      (Algebra.linearMap ℝ A ∘ₗ reLm + LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) x *
        (Algebra.linearMap ℝ A ∘ₗ reLm + LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) y

Tactic:
finally
  rintro ⟨x₁, y₁⟩ ⟨x₂, y₂⟩
  rw [mk_mul_mk]
  change
    algebraMap ℝ A (x₁ * x₂ - y₁ * y₂) + (x₁ * y₂ + y₁ * x₂) • I' =
      (algebraMap ℝ A x₁ + y₁ • I') * (algebraMap ℝ A x₂ + y₂ • I')
  rw [add_mul, mul_add, mul_add, add_comm _ (y₁ • I' * y₂ • I'), add_add_add_comm]
  congr 1
  -- equate "real" and "imaginary" parts
  · rw [smul_mul_smul_comm, hf, smul_neg, ← algebraMap_eq_smul_one, ← sub_eq_add_neg,
      ← map_mul, ← map_sub]
  · rw [smul_def, smul_def, smul_def, ← right_comm _ x₂,
      ← mul_assoc, ← add_mul, ← map_mul, ← map_mul, ← map_add]

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

Goal state before:
pp: A : Type u_1
inst✝⁴ : SeminormedAddCommGroup A
inst✝³ : StarAddMonoid A
inst✝² : NormedSpace ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : NormedStarGroup A
x : A
⊢ 2⁻¹ * ‖x + star x‖ ≤ 2⁻¹ * (2 * ‖x‖)

Tactic:
gcongr

Goal state after:
case hbc
A : Type u_1
inst✝⁴ : SeminormedAddCommGroup A
inst✝³ : StarAddMonoid A
inst✝² : NormedSpace ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : NormedStarGroup A
x : A
⊢ ‖x + star x‖ ≤ 2 * ‖x‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ c * ‖g x‖ ≤ max c 1 * ‖g x‖

Tactic:
gcongr

Goal state after:
case hbc
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ c ≤ max c 1
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'
c c' : ℝ
f : α → E
g' : α → F'
l : Filter α
h : IsBigOWith c l f g'
hc : c ≤ c'
x : α
hx : x ∈ {x | (fun x ↦ ‖f x‖ ≤ c * ‖g' x‖) x}
⊢ c * ‖g' x‖ ≤ c' * ‖g' x‖

Tactic:
gcongr

Goal state after: