mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case nil
α : Type u_1
ι : Type u_2
β : Type u_3
inst✝ : NormedField β
l : Filter α
f g : ι → α → β
h : ∀ i ∈ [], f i ~[l] g i
⊢ (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) []).prod) ~[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) []).prod

Tactic:
simp [IsEquivalent.refl]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹⁴ : Ring S
inst✝¹³ : Ring R
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module R V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module R W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : Module S W
inst✝⁴ : SMulCommClass R S W
inst✝³ : ContinuousConstSMul S W
inst✝² : AddTorsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalAddTorsor Q
f : V →ᴬ[R] Q
x : V
⊢ f (x +ᵥ 0) = f x

Tactic:
vadd_eq_add,

Goal state after:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹⁴ : Ring S
inst✝¹³ : Ring R
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module R V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module R W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : Module S W
inst✝⁴ : SMulCommClass R S W
inst✝³ : ContinuousConstSMul S W
inst✝² : AddTorsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalAddTorsor Q
f : V →ᴬ[R] Q
x : V
⊢ f (x + 0) = f x
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: case refine_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
y : E
hy : y ∈ F
h₂ : ‖(↑‖x₀‖)⁻¹ • (x₀ - ↑‖x₀‖ • y)‖ = ‖x₀‖⁻¹ * ‖x₀ - ↑‖x₀‖ • y‖
h₁ : r * ‖x₀‖ ≤ ‖x₀ - ↑‖x₀‖ • y‖
⊢ r ≤ ‖(↑‖x₀‖)⁻¹ • x₀ - y‖

Tactic:
← le_inv_mul_iff₀' (by simpa),

Goal state after:
case refine_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
y : E
hy : y ∈ F
h₂ : ‖(↑‖x₀‖)⁻¹ • (x₀ - ↑‖x₀‖ • y)‖ = ‖x₀‖⁻¹ * ‖x₀ - ↑‖x₀‖ • y‖
h₁ : r ≤ ‖x₀‖⁻¹ * ‖x₀ - ↑‖x₀‖ • y‖
⊢ r ≤ ‖(↑‖x₀‖)⁻¹ • x₀ - y‖
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: s t : Set ℝ≥0
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
⊢ Bornology.IsBounded (s * t)

Tactic:
obtain ⟨Af, hAf⟩ := (isBounded_iff_subset_closedBall 0).mp hs
    obtain ⟨Ag, hAg⟩ := (isBounded_iff_subset_closedBall 0).mp ht
    have key : IsCompact (closedBall (0 : ℝ≥0) Af ×ˢ closedBall (0 : ℝ≥0) Ag) :=
      IsCompact.prod (isCompact_closedBall _ _) (isCompact_closedBall _ _)
    apply Bornology.IsBounded.subset (key.image continuous_mul).isBounded
    intro _ ⟨x, x_in_s, y, y_in_t, xy_eq⟩
    exact ⟨⟨x, y⟩, by simpa only [Set.mem_prod] using ⟨⟨hAf x_in_s, hAg y_in_t⟩, xy_eq⟩⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α → E
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f

Tactic:
by_cases hF : CompleteSpace F; swap
  · simp [setToFun, hF]
  by_cases hf : Integrable f μ
  · rw [setToFun_eq hT hf, setToFun_eq hT (hf.smul c), Integrable.toL1_smul' f hf,
      L1.setToL1_smul hT h_smul c]
  · by_cases hr : c = 0
    · rw [hr]; simp
    · have hf' : ¬Integrable (c • f) μ := by rwa [integrable_smul_iff hr f]
      rw [setToFun_undef hT hf, setToFun_undef hT hf', smul_zero]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ⋯
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ := ⋯
LA : LipschitzWith ‖↑A‖₊ ⇑A
L : LipschitzOnWith (‖↑A‖₊ * K) (⇑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (⇑A ∘ f) g s
LAsymm : LipschitzWith ‖↑A.symm‖₊ ⇑A.symm
⊢ ‖↑A.symm‖₊ * (‖↑A‖₊ * K) ≤ lipschitzExtensionConstant E' * K

Tactic:
rw [lipschitzExtensionConstant, ← mul_assoc]

Goal state after:
case refine_1
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv
LA : LipschitzWith ‖↑A‖₊ ⇑A
L : LipschitzOnWith (‖↑A‖₊ * K) (⇑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (⇑A ∘ f) g s
LAsymm : LipschitzWith ‖↑A.symm‖₊ ⇑A.symm
⊢ ‖↑A.symm‖₊ * ‖↑A‖₊ * K ≤
    (have A := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv;
      max (‖↑A.symm‖₊ * ‖↑A‖₊) 1) *
      K
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: F : Type u_1
α : Type u
β✝ : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β✝
inst✝¹ : PseudoMetricSpace γ
f g : α →ᵇ β✝
x : α
C : ℝ
β : Type ?u.21
inst✝ : MetricSpace β
x✝ y✝ : α →ᵇ β
hfg : dist x✝ y✝ = 0
⊢ x✝ = y✝

Tactic:
ext x
    exact eq_of_dist_eq_zero (le_antisymm (hfg ▸ dist_coe_le_dist _) dist_nonneg)

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f : α →ᵇ β
l : Filter (α →ᵇ β)
⊢ TendstoUniformly (fun i ↦ ⇑(id i)) (⇑f) l ↔
    TendstoUniformly (⇑UniformFun.toFun ∘ ⇑UniformFun.ofFun ∘ DFunLike.coe)
      (UniformFun.toFun ((⇑UniformFun.ofFun ∘ DFunLike.coe) f)) l

Tactic:
simp [comp_def]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x : α
C : ℝ
C_nonneg : 0 ≤ ↑(LipschitzAdd.C β)
⊢ ∀ (x y : (α →ᵇ β) × (α →ᵇ β)), dist (x.1 + x.2) (y.1 + y.2) ≤ ↑(LipschitzAdd.C β) * dist x y

Tactic:
rintro ⟨f₁, g₁⟩ ⟨f₂, g₂⟩

Goal state after:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x : α
C : ℝ
C_nonneg : 0 ≤ ↑(LipschitzAdd.C β)
f₁ g₁ f₂ g₂ : α →ᵇ β
⊢ dist ((f₁, g₁).1 + (f₁, g₁).2) ((f₂, g₂).1 + (f₂, g₂).2) ≤ ↑(LipschitzAdd.C β) * dist (f₁, g₁) (f₂, g₂)
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg : ∀ (x : α), f x = 0 ∨ g x = 0
hfg' : ∀ (x : α), ‖(f + g) x‖ = max ‖f x‖ ‖g x‖
key : ∀ (c : ℝ), 0 ≤ c → (‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c)
⊢ max ‖f‖ ‖g‖ ≤ ‖f + g‖

Tactic:
← key

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg : ∀ (x : α), f x = 0 ∨ g x = 0
hfg' : ∀ (x : α), ‖(f + g) x‖ = max ‖f x‖ ‖g x‖
key : ∀ (c : ℝ), 0 ≤ c → (‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c)
⊢ ‖f + g‖ ≤ ‖f + g‖

case hc
α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg : ∀ (x : α), f x = 0 ∨ g x = 0
hfg' : ∀ (x : α), ‖(f + g) x‖ = max ‖f x‖ ‖g x‖
key : ∀ (c : ℝ), 0 ≤ c → (‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c)
⊢ 0 ≤ ‖f + g‖
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
inst✝ : Unique α
f : α → E
⊢ ∫ (x : α), f default ∂μ = μ.real univ • f default

Tactic:
rw [integral_const]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
⊢ ‖setToFun μ T hT ↑↑f‖ ≤ max C 0 * ‖f‖

Tactic:
by
  by_cases hF : CompleteSpace F; swap
  · simp only [setToFun, hF, ↓reduceDIte, norm_zero]
    positivity
  rw [L1.setToFun_eq_setToL1]
  exact L1.norm_setToL1_le_mul_norm' hT f

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
lintegral_norm_tendsto_zero : Tendsto (fun n ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
x : α
hx : ↑↑(Integrable.toL1 (fs n - f) ⋯) x = (fs n - f) x
⊢ ‖(fs n - f) x‖ₑ = ENNReal.ofReal ‖fs n x - f x‖

Tactic:
ofReal_norm,

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
lintegral_norm_tendsto_zero : Tendsto (fun n ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
x : α
hx : ↑↑(Integrable.toL1 (fs n - f) ⋯) x = (fs n - f) x
⊢ ‖(fs n - f) x‖ₑ = ‖fs n x - f x‖ₑ
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos.convert_4
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝¹ : CompleteSpace E
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hF : CompleteSpace F
hf'' : ∀ (i : ι), AEMeasurable (fun x ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ ↑‖f n a‖₊
⊢ HasFiniteIntegral (fun a ↦ ∑' (n : ι), ↑‖f n a‖₊) μ

Tactic:
dsimp [HasFiniteIntegral]

Goal state after:
case pos.convert_4
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝¹ : CompleteSpace E
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hF : CompleteSpace F
hf'' : ∀ (i : ι), AEMeasurable (fun x ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ ↑‖f n a‖₊
⊢ ∫⁻ (a : α), ‖∑' (n : ι), ‖f n a‖‖ₑ ∂μ < ∞
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ ↑K₂
⊢ μ K₁ ≤ μ K₂

Tactic:
simpa using μ.mono' _ _ h

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
hU : ∫ (x : X) in t, f x ∂μ ≠ 0
⊢ ∃ x ∈ t, f x ≠ 0

Tactic:
contrapose! hU

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
hU : ∀ x ∈ t, f x = 0
⊢ ∫ (x : X) in t, f x ∂μ = 0
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
⊢ index (↑K) V ≤ s.card * index (↑K₀) V

Tactic:
← h2t,

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
⊢ index (↑K) V ≤ s.card * t.card
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: case h.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ g ∈ (fun h ↦ g₀ * h) ⁻¹' V

Tactic:
exact h2g₀

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: case ha
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K : Set G
h1K : IsCompact K
h2K : (interior K).Nonempty
⊢ 0 < index (↑{ carrier := K, isCompact' := h1K }) U

Tactic:
apply index_pos ⟨⟨K, h1K⟩, h2K⟩ hU

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case pos.h'f
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : X → ℝ := ⋯
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
⊢ ∀ a ∈ sᶜ, ENNReal.ofReal (g a) = 0

Tactic:
intro x hx
    simpa [g] using h's x hx

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ re ⟪x, x⟫ = ‖⟪x, x⟫‖

Tactic:
conv_rhs => rw [← inner_self_ofReal_re]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ re ⟪x, x⟫ = ‖↑(re ⟪x, x⟫)‖
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ⟪v, w⟫ = ↑‖v‖ ^ 2 ↔ ⟪v, v - w⟫ = 0

Tactic:
by
  rw [inner_sub_right, sub_eq_zero, inner_self_eq_norm_sq_to_K, eq_comm]

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

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = 0

Tactic:
by
  rw [@norm_sub_mul_self ℝ, add_right_cancel_iff, sub_eq_add_neg, add_eq_left, neg_eq_zero,
    mul_eq_zero]
  simp

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

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪x + y, x - y⟫_ℝ = 0 ↔ ‖x‖ = ‖y‖

Tactic:
by
  conv_rhs => rw [← mul_self_inj_of_nonneg (norm_nonneg _) (norm_nonneg _)]
  simp only [← @inner_self_eq_norm_mul_norm ℝ, inner_add_left, inner_sub_right, real_inner_comm y x,
    sub_eq_zero, re_to_real]
  grind

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Goal state before:
pp: case a
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
⊢ ⨅ w, ‖u - ↑w‖ ≤ ‖u - v‖

Tactic:
· change ⨅ w : K, ‖u - w‖ ≤ (fun w : K => ‖u - w‖) ⟨v, hv⟩
      apply ciInf_le
      use 0
      rintro y ⟨z, rfl⟩
      exact norm_nonneg _

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Subspace

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v w : α i
hvw : ⟨i, v⟩ ≠ ⟨i, w⟩
this : v ≠ w
⊢ ⟪(fun a ↦ (V a.fst) (v_family a.fst a.snd)) ⟨i, v⟩, (fun a ↦ (V a.fst) (v_family a.fst a.snd)) ⟨i, w⟩⟫ = 0

Tactic:
simpa only [LinearIsometry.inner_map_map] using (hv_family i).2 this

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.LinearMap

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_8
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : E
y : F
⊢ ((rankOne 𝕜) x) y = 0 ↔ x = 0 ∨ y = 0

Tactic:
by
  simp [ContinuousLinearMap.ext_iff, rankOne_apply, forall_or_right, or_comm,
    ext_iff_inner_right 𝕜 (E := F)]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i ∈ s, ∑ j ∈ s, ⟪v i, x⟫ * ⟪x, v j⟫ * ⟪v j, v i⟫ = ∑ k ∈ s, ⟪v k, x⟫ * ⟪x, v k⟫
h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2
hbf : ‖x - ∑ i ∈ s, ⟪v i, x⟫ • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2
⊢ ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2 ≤ ‖x‖ ^ 2

Tactic:
rw [← sub_nonneg, ← hbf]
    simp only [norm_nonneg, pow_nonneg]

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

Goal state before:
pp: ι : Sort u_1
R : Type u_2
N : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
inst✝² : Module R N
inst✝¹ : ContinuousAdd N
inst✝ : ContinuousConstSMul R N
f : ι → ClosedSubmodule R N
⊢ ↑(⨆ i, f i) = closure (⨆ i, ↑(f i)).carrier

Tactic:
simp only [← coe_toSubmodule, toSubmodule_iSup, Submodule.carrier_eq_coe]
  rfl

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
hK : ¬FiniteDimensional 𝕜 ↥Kᗮ
⊢ LinearMap.det ↑K.reflection.toLinearEquiv = (-1) ^ finrank 𝕜 ↥Kᗮ

Tactic:
rw [finrank_of_infinite_dimensional hK, pow_zero, LinearMap.det_eq_one_of_finrank_eq_zero]
    exact finrank_of_infinite_dimensional fun h ↦ hK (h.finiteDimensional_submodule _)

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
x : E
S : Submodule 𝕜 E
inst✝ : S.HasOrthogonalProjection
⊢ ‖x‖ ^ 2 = ‖S.starProjection x + Sᗮ.starProjection x‖ ^ 2

Tactic:
starProjection_add_starProjection_orthogonal

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
x : E
S : Submodule 𝕜 E
inst✝ : S.HasOrthogonalProjection
⊢ ‖x‖ ^ 2 = ‖x‖ ^ 2
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomIsometric σ
inst✝¹ : RingHomIsometric σ'
inst✝ : CompleteSpace F
surj : Surjective ⇑f
A : ⋃ n, closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y ≠ 0
hc' : 1 < ‖σ c‖
d : 𝕜'
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖σ c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ ⇑f '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ ⇑f '' ball 0 ↑n
x₂ : E
h₂ : dist a (f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : f x₂ = z₂
x : E := x₁ - x₂
I : ‖f x - d • y‖ ≤ 2 * δ
J : dist (f (σ' d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
K : ‖σ' d⁻¹ • x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
⊢ ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖

Tactic:
exact ⟨σ' d⁻¹ • x, J, K⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 1 (α × β)
⊢ ↑‖x‖₊ = ↑(‖x.fst‖₊ + ‖x.snd‖₊)

Tactic:
by
    push_cast
    exact prod_norm_eq_of_L1 x

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
U : Matrix n n α
⊢ Uᵀ * star Uᵀ = 1 ↔ star U * U = 1

Tactic:
show star Uᵀ = (star U)ᵀ by rfl,

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
U : Matrix n n α
⊢ Uᵀ * (star U)ᵀ = 1 ↔ star U * U = 1
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inl
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
hp : Fact (1 ≤ ∞)
x y : PiLp ∞ β
⊢ dist x y = ‖-x + y‖

Tactic:
simp only [dist_eq_iSup, norm_eq_ciSup, dist_eq_norm, add_apply, neg_apply, norm_neg_add]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (⇑g ∘ u) atTop (𝓝 y) → y = g x
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑g

Tactic:
by
  refine g.continuous_of_isClosed_graph (IsSeqClosed.isClosed ?_)
  rintro φ ⟨x, y⟩ hφg hφ
  refine hg (Prod.fst ∘ φ) x y ((continuous_fst.tendsto _).comp hφ) ?_
  have : g ∘ Prod.fst ∘ φ = Prod.snd ∘ φ := by
    ext n
    exact (hφg n).symm
  rw [this]
  exact (continuous_snd.tendsto _).comp hφ

Goal state after: