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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
hle : 1 ≤ infEDist x E / ENNReal.ofReal δ
⊢ 1 - infEDist y E / ENNReal.ofReal δ ≤ 1 - infEDist x E / ENNReal.ofReal δ

Tactic:
rw [tsub_eq_zero_of_le hle, tsub_eq_zero_of_le]

Goal state after:
case inr
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
hle : 1 ≤ infEDist x E / ENNReal.ofReal δ
⊢ 1 ≤ infEDist y E / ENNReal.ofReal δ
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case pos.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : ∫ (x : α), -f x ∂μ = 0
this : -f =ᵐ[μ] 0
⊢ f =ᵐ[μ] 0

Tactic:
filter_upwards [this] with ω hω

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : ∫ (x : α), -f x ∂μ = 0
this : -f =ᵐ[μ] 0
ω : α
hω : (-f) ω = 0 ω
⊢ f ω = 0 ω
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: case h
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ thickenedIndicatorAux δ E y ≤ thickenedIndicatorAux δ E x

Tactic:
exact thickenedIndicatorAux_mono_infEDist δ h

Goal state after:
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: case inr
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
this :
  ∀ (x y : α),
    infEDist x E ≤ infEDist y E →
      edist ((thickenedIndicator δ_pos E) x) ((thickenedIndicator δ_pos E) y) ≤ ↑δ.toNNReal⁻¹ * edist x y
h : ¬infEDist x E ≤ infEDist y E
⊢ edist ((thickenedIndicator δ_pos E) x) ((thickenedIndicator δ_pos E) y) ≤ ↑δ.toNNReal⁻¹ * edist x y

Tactic:
specialize this y x (le_of_not_ge h)

Goal state after:
case inr
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
this : edist ((thickenedIndicator δ_pos E) y) ((thickenedIndicator δ_pos E) x) ≤ ↑δ.toNNReal⁻¹ * edist y x
h : ¬infEDist x E ≤ infEDist y E
⊢ edist ((thickenedIndicator δ_pos E) x) ((thickenedIndicator δ_pos E) y) ≤ ↑δ.toNNReal⁻¹ * edist x y
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: case inr
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
this :
  ∀ (x y : α),
    infEDist x E ≤ infEDist y E →
      edist ((thickenedIndicator δ_pos E) x) ((thickenedIndicator δ_pos E) y) ≤ ↑δ.toNNReal⁻¹ * edist x y
h : ¬infEDist x E ≤ infEDist y E
⊢ edist ((thickenedIndicator δ_pos E) x) ((thickenedIndicator δ_pos E) y) ≤ ↑δ.toNNReal⁻¹ * edist x y

Tactic:
specialize this y x (le_of_not_ge h)
    rwa [edist_comm, edist_comm x]

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x = ⊥
⊢ leftLim f x ≤ f y

Tactic:
simpa [leftLim, h'] using hf h

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : TopologicalSpace R
f✝ : StieltjesFunction R
inst✝ : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
hx : ∀ (y : R), y ≤ x
⊢ ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s

Tactic:
filter_upwards [self_mem_nhdsWithin] with y (hy : x ≤ y)
      rw [show y = x by exact le_antisymm (hx y) hy]
      exact lus hlu

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
A : ContinuousWithinAt (fun r ↦ ↑f r - ↑f a) (Ioi a) a
⊢ ∃ a', ↑f a' - ↑f a < ↑δ ∧ a < a'

Tactic:
have B : f a - f a < δ := by rwa [sub_self, NNReal.coe_pos, ← ENNReal.coe_pos]

Goal state after:
R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
A : ContinuousWithinAt (fun r ↦ ↑f r - ↑f a) (Ioi a) a
B : ↑f a - ↑f a < ↑δ
⊢ ∃ a', ↑f a' - ↑f a < ↑δ ∧ a < a'
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
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t μ
f' : X → E := AEStronglyMeasurable.mk f ⋯
⊢ ∫ (x : X) in t, f' x ∂μ = ∫ (x : X) in s, f' x ∂μ

Tactic:
by
      apply
        setIntegral_eq_of_subset_of_ae_sdiff_eq_zero_aux hts _ h.1.stronglyMeasurable_mk
          (h.congr h.1.ae_eq_mk)
      filter_upwards [h't, ae_imp_of_ae_restrict h.1.ae_eq_mk] with x hx h'x h''x
      rw [← h'x h''x.1, hx h''x]

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

Goal state before:
pp: G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : R1Space G
S : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : WeaklyLocallyCompactSpace G
⊢ μ.measure.Regular

Tactic:
have : IsFiniteMeasureOnCompacts μ.measure := by
    refine ⟨fun K hK => ?_⟩
    apply (measure_mono subset_closure).trans_lt _
    rw [measure_apply _ isClosed_closure.measurableSet]
    exact μ.outerMeasure_lt_top_of_isCompact hK.closure
  refine ⟨fun U hU r hr => ?_⟩
  rw [measure_apply _ hU.measurableSet, μ.outerMeasure_of_isOpen U hU] at hr
  simp only [innerContent, lt_iSup_iff] at hr
  rcases hr with ⟨K, hKU, hr⟩
  refine ⟨K, hKU, K.2, hr.trans_le ?_⟩
  exact (μ.le_outerMeasure_compacts K).trans (le_toMeasure_apply _ _ _)

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

Goal state before:
pp: G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝³ : MeasurableConstSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in t, f x ∂μ

Tactic:
by
  by_cases hfs : IntegrableOn f s μ
  · have hft : IntegrableOn f t μ := by rwa [ht.integrableOn_iff hs hf]
    calc
      ∫ x in s, f x ∂μ = ∑' g : G, ∫ x in s ∩ g • t, f x ∂μ := ht.setIntegral_eq_tsum hfs
      _ = ∑' g : G, ∫ x in g • t ∩ s, f (g⁻¹ • x) ∂μ := by simp only [hf, inter_comm]
      _ = ∫ x in t, f x ∂μ := (hs.setIntegral_eq_tsum' hft).symm
  · rw [integral_undef hfs, integral_undef]
    rwa [hs.integrableOn_iff ht hf] at hfs

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

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
s : Set X
f : X → ℝ
c : ℝ
hs : MeasurableSet s
hμs : μ s ≠ ∞
hf : ∀ x ∈ s, c ≤ f x
hfint : IntegrableOn (fun x ↦ f x) s μ
⊢ c * μ.real s ≤ ∫ (x : X) in s, f x ∂μ

Tactic:
by
  simpa [mul_comm] using setIntegral_ge_of_const_le hs hμs hf hfint

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

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝⁵ : Countable ι
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace X
inst✝² : BorelSpace X
inst✝¹ : T2Space X
inst✝ : IsLocallyFiniteMeasure μ
f : C(X, E)
s : ι → Compacts X
hf : Summable fun i ↦ ‖ContinuousMap.restrict (↑(s i)) f‖ * μ.real ↑(s i)
⊢ IntegrableOn (⇑f) (⋃ i, ↑(s i)) μ

Tactic:
by
  refine
    integrableOn_iUnion_of_summable_integral_norm
      (fun i => (map_continuous f).continuousOn.integrableOn_compact (s i).isCompact)
      (.of_nonneg_of_le (fun ι => integral_nonneg fun x => norm_nonneg _) (fun i => ?_) hf)
  rw [← (Real.norm_of_nonneg (integral_nonneg fun x => norm_nonneg _) : ‖_‖ = ∫ x in s i, ‖f x‖ ∂μ)]
  exact
    norm_setIntegral_le_of_norm_le_const (s i).isCompact.measure_lt_top
      fun x hx => (norm_norm (f x)).symm ▸ (f.restrict (s i : Set X)).norm_coe_le_norm ⟨x, hx⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h₃ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rwa [← inner_conj_symm, conj_re]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
cd : Core 𝕜 F
x y : F
h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h₃ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rwa [← inner_conj_symm, conj_re]

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 y : E
⊢ re ⟪x, y⟫ = (‖x + y‖ * ‖x + y‖ - ‖x - y‖ * ‖x - y‖) / 4

Tactic:
by
  rw [@norm_add_mul_self 𝕜, @norm_sub_mul_self 𝕜]
  ring

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

Goal state before:
pp: E : Type u_4
𝕜 : Type u_7
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪v, x⟫ = 0
v : E
hv : v ∈ S
⊢ (starRingEnd 𝕜) ⟪v, x⟫ = 0

Tactic:
simp [-inner_conj_symm, h, hv]

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

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
⊢ √((R ^ 2 / (‖x‖ * ‖y‖)) ^ 2 * ‖x - y‖ ^ 2) = R ^ 2 / (‖x‖ * ‖y‖) * dist x y

Tactic:
rw [sqrt_mul, sqrt_sq, sqrt_sq, dist_eq_norm]

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
⊢ 0 ≤ ‖x - y‖

F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
⊢ 0 ≤ R ^ 2 / (‖x‖ * ‖y‖)

case hx
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
⊢ 0 ≤ (R ^ 2 / (‖x‖ * ‖y‖)) ^ 2
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ‖⟪x, y⟫ / (↑‖x‖ * ↑‖y‖)‖ = 1
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x

Tactic:
refine ⟨hx₀, (norm_inner_eq_norm_iff hx₀ hy₀).1 <| eq_of_div_eq_one ?_⟩

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ‖⟪x, y⟫ / (↑‖x‖ * ↑‖y‖)‖ = 1
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ ‖⟪x, y⟫‖ / (‖x‖ * ‖y‖) = 1
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : re ⟪x, y⟫ = ‖y‖ ^ 2
H₁ : ‖x‖ ^ 2 ≤ ‖y‖ ^ 2
⊢ re ⟪y, x⟫ = ‖y‖ ^ 2

Tactic:
rwa [← inner_conj_symm, conj_re]

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
v w : ι → E
hv : Orthonormal 𝕜 v
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
⊢ Orthonormal 𝕜 w

Tactic:
classical
  rw [orthonormal_iff_ite] at *
  intro i j
  rcases hw i with hi | hi <;> rcases hw j with hj | hj <;>
    replace hv := hv i j <;> split_ifs at hv ⊢ with h <;>
    simpa only [hi, hj, h, inner_neg_right, inner_neg_left, neg_neg, eq_self_iff_true,
      neg_eq_zero] using hv

Goal state after:
Module: Mathlib.Topology.Baire.CompleteMetrizable

Goal state before:
pp: case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : IsCompletelyPseudoMetrizableSpace X
x✝ : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n ↦ 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → X → ℝ≥0∞ → X
radius : ℕ → X → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ := fun n ↦ Nat.recOn n (x, min ε (B 0)) fun n p ↦ (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun n ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun n ↦ (F n).2
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
n : ℕ
⊢ r (n + 1) ≤ B (n + 1)

Tactic:
exact HB n (c n) (r n) (r0 n)

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Module R M
x : M
s : ClosedSubmodule R M
⊢ x ∈ ↑s ↔ x ∈ s

Tactic:
by
  rfl

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
v : Π₀ (i : ι), ↥(V i)
hv : ((DFinsupp.lsum ℕ) fun i ↦ (V i).subtype) v = 0
i : ι
⊢ ⟪↑(v i), ((DFinsupp.lsum ℕ) fun i ↦ (V i).subtype) v⟫ = 0

Tactic:
simp only [hv, inner_zero_right]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ Module.rank ℝ K = Module.rank ℝ ↥(Submodule.span ℝ {1, I})

Tactic:
by rw [span_one_I]; simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ⊥ᗮ = ⊤

Tactic:
exact bot_orthogonal_eq_top

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

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ⊥ᗮ = ⊤

Tactic:
exact bot_orthogonal_eq_top

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
⊢ ∀ (x : E), ‖K.reflectionLinearEquiv x‖ = ‖x‖

Tactic:
intro x
      let w : K := K.orthogonalProjectionOnto x
      let v := x - w
      have : ⟪v, w⟫ = 0 := starProjection_inner_eq_zero x w w.2
      convert norm_sub_eq_norm_add this
      · dsimp [reflectionLinearEquiv, v, w]
        abel
      · simp only [v, add_sub_cancel]

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
⊢ v ∈ K → v ∈ Kᗮᗮ

Tactic:
intro hv w hw
    rw [inner_eq_zero_symm]
    exact hw v hv

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

Goal state before:
pp: case pos
𝕜 : 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:
let e := K.prodEquivOfIsCompl _ K.isCompl_orthogonal

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
hK : FiniteDimensional 𝕜 ↥Kᗮ
e : (↥K × ↥Kᗮ) ≃ₗ[𝕜] E := K.prodEquivOfIsCompl Kᗮ ⋯
⊢ LinearMap.det ↑K.reflection.toLinearEquiv = (-1) ^ finrank 𝕜 ↥Kᗮ
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
K : Submodule 𝕜 E
inst✝ : Kᗮ.HasOrthogonalProjection
v : E
hv : v ∈ K
⊢ Kᗮ.starProjection v = 0

Tactic:
rw [starProjection_apply, coe_eq_zero]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : Kᗮ.HasOrthogonalProjection
v : E
hv : v ∈ K
⊢ Kᗮ.orthogonalProjectionOnto v = 0
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
v : E
⊢ (𝕜 ∙ v)ᗮ.starProjection v = 0

Tactic:
rw [starProjection_apply, coe_eq_zero]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : E
⊢ (𝕜 ∙ v)ᗮ.orthogonalProjectionOnto v = 0
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case h₁
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ edist f.fst h.fst ≤ edist f.fst g.fst + edist g.fst h.fst

Tactic:
apply edist_triangle

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

Goal state before:
pp: case h₁
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ edist f.snd h.snd ≤ edist f.snd g.snd + edist g.snd h.snd

Tactic:
apply edist_triangle

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

Goal state before:
pp: 𝕜 : 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
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →SL[σ] F
hsurj : (↑f).range = ⊤
⊢ 0 < (f.nonlinearRightInverseOfSurjective hsurj).nnnorm

Tactic:
by
  rw [nonlinearRightInverseOfSurjective]
  exact Classical.choose_spec (exists_nonlinearRightInverse_of_surjective f hsurj)

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

Goal state before:
pp: case h₁
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g h : PiLp p β
hp : 1 ≤ p.toReal
i : ι
a✝ : i ∈ Finset.univ
⊢ edist (f.ofLp i) (h.ofLp i) ≤ edist (f.ofLp i) (g.ofLp i) + edist (g.ofLp i) (h.ofLp i)

Tactic:
apply edist_triangle

Goal state after:
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✝⁷ : Semiring 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (α i)
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → Module 𝕜 (α i)
inst✝³ : (i : ι) → Module 𝕜 (β i)
c : 𝕜
ι' : Type u_5
inst✝² : Fintype ι'
E : Type u_6
inst✝¹ : SeminormedAddCommGroup E
inst✝ : Module 𝕜 E
e : ι ≃ ι'
hp : Fact (1 ≤ ∞)
__LinearEquiv✝ : (PiLp ∞ fun x ↦ E) ≃ₗ[𝕜] PiLp ∞ fun x ↦ E :=
  WithLp.linearEquiv ∞ 𝕜 (ι → E) ≪≫ₗ
    (LinearEquiv.piCongrLeft' 𝕜 (fun x ↦ E) e ≪≫ₗ (WithLp.linearEquiv ∞ 𝕜 (ι' → E)).symm)
x' : PiLp ∞ fun x ↦ E
⊢ ‖(WithLp.linearEquiv ∞ 𝕜 (ι → E) ≪≫ₗ
          (LinearEquiv.piCongrLeft' 𝕜 (fun x ↦ E) e ≪≫ₗ (WithLp.linearEquiv ∞ 𝕜 (ι' → E)).symm))
        x'‖ =
    ‖x'‖

pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝⁸ : Fintype ι
inst✝⁷ : Semiring 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (α i)
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → Module 𝕜 (α i)
inst✝³ : (i : ι) → Module 𝕜 (β i)
c : 𝕜
ι' : Type u_5
inst✝² : Fintype ι'
E : Type u_6
inst✝¹ : SeminormedAddCommGroup E
inst✝ : Module 𝕜 E
e : ι ≃ ι'
x' : PiLp p fun x ↦ E
h : 1 ≤ p.toReal
⊢ ‖(WithLp.linearEquiv p 𝕜 (ι → E) ≪≫ₗ
          (LinearEquiv.piCongrLeft' 𝕜 (fun x ↦ E) e ≪≫ₗ (WithLp.linearEquiv p 𝕜 (ι' → E)).symm))
        x'‖ =
    ‖x'‖

Tactic:
· simp_rw [norm_eq_ciSup]
      exact e.symm.iSup_congr fun _ => rfl

Goal state after:
case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝⁸ : Fintype ι
inst✝⁷ : Semiring 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (α i)
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → Module 𝕜 (α i)
inst✝³ : (i : ι) → Module 𝕜 (β i)
c : 𝕜
ι' : Type u_5
inst✝² : Fintype ι'
E : Type u_6
inst✝¹ : SeminormedAddCommGroup E
inst✝ : Module 𝕜 E
e : ι ≃ ι'
x' : PiLp p fun x ↦ E
h : 1 ≤ p.toReal
⊢ ‖(WithLp.linearEquiv p 𝕜 (ι → E) ≪≫ₗ
          (LinearEquiv.piCongrLeft' 𝕜 (fun x ↦ E) e ≪≫ₗ (WithLp.linearEquiv p 𝕜 (ι' → E)).symm))
        x'‖ =
    ‖x'‖
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
h : a ≤ b
⊢ (volume (univ.pi fun i ↦ Ico (a i) (b i))).toReal = ∏ i, (b i - a i)

Tactic:
simp only [volume_pi_Ico, ENNReal.toReal_prod, ENNReal.toReal_ofReal (sub_nonneg.2 (h _))]

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m n : E
⊢ fract b m = fract b n ↔ -m + n ∈ span ℤ (Set.range ⇑b)

Tactic:
rw [eq_comm, Basis.ext_elem_iff b]
  simp_rw [repr_fract_apply, Int.fract_eq_fract, eq_comm, Basis.mem_span_iff_repr_mem,
    sub_eq_neg_add, map_add, map_neg, Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply,
    Pi.neg_apply, ← eq_intCast (algebraMap ℤ K) _, Set.mem_range]

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I : Box ι
i : ι
c : ℝ≥0
h : I.distortion ≤ c
this : 0 ≤ ↑c * (I.upper i - I.lower i)
x : ι → ℝ
hx : x ∈ Box.Icc I
y : ι → ℝ
hy : y ∈ Box.Icc I
⊢ ↑I.distortion * (I.upper i - I.lower i) ≤ ↑c * (I.upper i - I.lower i)

Tactic:
by gcongr; exact sub_nonneg.2 (I.lower_le_upper i)

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

Goal state before:
pp: ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
⊢ Disjoint ↑(I.splitCenterBox s) ↑(I.splitCenterBox t)

Tactic:
disjoint_iff_inf_le

Goal state after:
ι : Type u_1
I : Box ι
s t : Set ι
h : s ≠ t
⊢ ↑(I.splitCenterBox s) ⊓ ↑(I.splitCenterBox t) ⊆ ⊥