mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

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
v w : E
hwK : w ∈ K
hw : v - w ∈ Kᗮ
⊢ ∃ w ∈ Kᗮ, v - w ∈ Kᗮᗮ

Tactic:
refine ⟨_, hw, ?_⟩

Goal state after:
𝕜 : 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
v w : E
hwK : w ∈ K
hw : v - w ∈ Kᗮ
⊢ v - (v - w) ∈ Kᗮᗮ
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
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ⇑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y ↦ y - f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
n : ℕ
⊢ ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖

Tactic:
induction n with
    | zero => simp only [one_div, one_mul, iterate_zero_apply, pow_zero, le_rfl]
    | succ n IH =>
      rw [iterate_succ']
      apply le_trans (hle _) _
      rw [pow_succ', mul_assoc]
      gcongr

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) ↔ (span 𝕜 v)ᗮ = ⊥

Tactic:
rw [Submodule.eq_bot_iff]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) ↔ ∀ x ∈ (span 𝕜 v)ᗮ, x = 0
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
hp : p ≠ ∞
x y : WithLp p (α × β)
⊢ ↑(nndist x y) = ↑((nndist x.fst y.fst ^ p.toReal + nndist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal))

Tactic:
by
    push_cast
    exact prod_dist_eq_add (p.toReal_pos_iff_ne_top.mpr hp) _ _

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ x ∈ (span 𝕜 v)ᗮ, x = 0) → ∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v

Tactic:
simp only [Subset.antisymm_iff]
    rintro h u (huv : v ⊆ u) hu
    refine ⟨?_, huv⟩
    intro x hxu
    refine ((mt (h x)) (hu.ne_zero ⟨x, hxu⟩)).imp_symm ?_
    intro hxv y hy
    have hxv' : (⟨x, hxu⟩ : u) ∉ ((↑) ⁻¹' v : Set u) := by simp [hxv]
    obtain ⟨l, hl, rfl⟩ :
      ∃ l ∈ supported 𝕜 𝕜 ((↑) ⁻¹' v : Set u), (linearCombination 𝕜 ((↑) : u → E)) l = y := by
      rw [← Finsupp.mem_span_image_iff_linearCombination]
      simp [huv, inter_eq_self_of_subset_right, hy]
    exact hu.inner_finsupp_eq_zero hxv' hl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
p : ℝ≥0∞
x : WithLp p (α × β)
⊢ idemFst x + idemSnd x = 1 x

Tactic:
idemFst_apply,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
p : ℝ≥0∞
x : WithLp p (α × β)
⊢ toLp p (x.fst, 0) + idemSnd x = 1 x
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

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

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

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

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
α : ι → Type u_3
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → SeminormedAddCommGroup (α i)
R : Type u_5
inst✝² : SeminormedRing R
inst✝¹ : (i : ι) → Module R (α i)
inst✝ : ∀ (i : ι), NormSMulClass R (α i)
⊢ NormSMulClass R ((i : ι) → α i)

Tactic:
let := seminormedAddCommGroupToPi p α

Goal state after:
p : ℝ≥0∞
ι : Type u_2
α : ι → Type u_3
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → SeminormedAddCommGroup (α i)
R : Type u_5
inst✝² : SeminormedRing R
inst✝¹ : (i : ι) → Module R (α i)
inst✝ : ∀ (i : ι), NormSMulClass R (α i)
this : SeminormedAddCommGroup ((i : ι) → α i) := seminormedAddCommGroupToPi p α
⊢ NormSMulClass R ((i : ι) → α i)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
u : ℕ → E
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n ↦ {u n} + s)
h's : MeasurableSet s
H : ∀ (R : ℝ), μ (s ∩ closedBall 0 R) = 0
| μ s

Tactic:
rw [← iUnion_inter_closedBall_nat s 0]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
u : ℕ → E
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n ↦ {u n} + s)
h's : MeasurableSet s
H : ∀ (R : ℝ), μ (s ∩ closedBall 0 R) = 0
| μ (⋃ n, s ∩ closedBall 0 ↑n)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ

Tactic:
let ι := Fin (finrank ℝ E)

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: case refine_2.h
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 ι
a✝ b✝ : E
hxy : fract b a✝ = fract b b✝
⊢ (span ℤ (Set.range ⇑b)).quotientRel a✝ b✝

Tactic:
rwa [QuotientAddGroup.leftRel_apply, mem_toAddSubgroup, ← fract_eq_fract]

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

Goal state before:
pp: ι : Type u_1
l u : ι → ℝ
⊢ mk' l u = ⊥ ↔ ∃ i, u i ≤ l i

Tactic:
rw [mk']

Goal state after:
ι : Type u_1
l u : ι → ℝ
⊢ (if h : ∀ (i : ι), l i < u i then ↑{ lower := l, upper := u, lower_lt_upper := h } else ⊥) = ⊥ ↔ ∃ i, u i ≤ l i
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
l u lI uI : ι → ℝ
hI : ∀ (i : ι), lI i < uI i
⊢ mk' l u = ↑{ lower := lI, upper := uI, lower_lt_upper := hI } ↔
    l = { lower := lI, upper := uI, lower_lt_upper := hI }.lower ∧
      u = { lower := lI, upper := uI, lower_lt_upper := hI }.upper

Tactic:
rw [mk']

Goal state after:
ι : Type u_1
l u lI uI : ι → ℝ
hI : ∀ (i : ι), lI i < uI i
⊢ (if h : ∀ (i : ι), l i < u i then ↑{ lower := l, upper := u, lower_lt_upper := h } else ⊥) =
      ↑{ lower := lI, upper := uI, lower_lt_upper := hI } ↔
    l = { lower := lI, upper := uI, lower_lt_upper := hI }.lower ∧
      u = { lower := lI, upper := uI, lower_lt_upper := hI }.upper
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
l u : ι → ℝ
⊢ ↑(mk' l u) = univ.pi fun i ↦ Ioc (l i) (u i)

Tactic:
rw [mk']

Goal state after:
ι : Type u_1
l u : ι → ℝ
⊢ ↑(if h : ∀ (i : ι), l i < u i then ↑{ lower := l, upper := u, lower_lt_upper := h } else ⊥) =
    univ.pi fun i ↦ Ioc (l i) (u i)
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: case mp
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
H : π₁ ≤ π₂
J : Box ι
hJ : J ∈ π₁
J' : Box ι
hJ' : J' ∈ π₂
J'' : Box ι
hJ'' : J'' ∈ π₂
Hle : J ≤ J''
x : ι → ℝ
hx : x ∈ ↑J
hx' : x ∈ ↑J'
⊢ J ≤ J'

Tactic:
π₂.eq_of_mem_of_mem hJ' hJ'' hx' (Hle hx)

Goal state after:
case mp
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
H : π₁ ≤ π₂
J : Box ι
hJ : J ∈ π₁
J' : Box ι
hJ' : J' ∈ π₂
J'' : Box ι
hJ'' : J'' ∈ π₂
Hle : J ≤ J''
x : ι → ℝ
hx : x ∈ ↑J
hx' : x ∈ ↑J'
⊢ J ≤ J''
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case t_bound
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : μ u ≠ 0
R : ℝ
Rpos : 0 < R
t_bound : t ⊆ closedBall 0 R
t' : Set E := R⁻¹ • t
ht' : t' = R⁻¹ • t
u' : Set E := R⁻¹ • u
hu' : u' = R⁻¹ • u
⊢ closedBall (R⁻¹ • 0) (‖R⁻¹‖ * R) = closedBall 0 1

Tactic:
smul_zero,

Goal state after:
case t_bound
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : μ u ≠ 0
R : ℝ
Rpos : 0 < R
t_bound : t ⊆ closedBall 0 R
t' : Set E := R⁻¹ • t
ht' : t' = R⁻¹ • t
u' : Set E := R⁻¹ • u
hu' : u' = R⁻¹ • u
⊢ closedBall 0 (‖R⁻¹‖ * R) = closedBall 0 1
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: case mpr
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
⊢ (∃ J', (∃ J'_1 ∈ π, J' ∈ πi J'_1) ∧ J ∈ πi' (π.biUnionIndex πi J') J') → ∃ J' ∈ π, ∃ J'_1 ∈ πi J', J ∈ πi' J' J'_1

Tactic:
rintro ⟨J₁, ⟨J₂, hJ₂, hJ₁⟩, hJ⟩

Goal state after:
case mpr
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ : J ∈ πi' (π.biUnionIndex πi J₁) J₁
J₂ : Box ι
hJ₂ : J₂ ∈ π
hJ₁ : J₁ ∈ πi J₂
⊢ ∃ J' ∈ π, ∃ J'_1 ∈ πi J', J ∈ πi' J' J'_1
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : μ u ≠ 0
R : ℝ
Rpos : 0 < R
t_bound : t ⊆ closedBall 0 R
t' : Set E := R⁻¹ • t
ht' : t' = R⁻¹ • t
u' : Set E := R⁻¹ • u
hu' : u' = R⁻¹ • u
A : Tendsto (fun r ↦ μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) (𝓝[>] 0) (𝓝 0)
r : ℝ
rpos : r ∈ Ioi 0
⊢ R * r ∈ Ioi 0

Tactic:
exact mul_pos Rpos rpos

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝³ : Module.Finite ℤ ↥L
this✝² : Module ℚ E
this✝¹ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
h : finrank K E < Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range ⇑e
⊢ ¬LinearIndependent ℤ fun (x : ↑(insert v (Set.range ⇑e))) ↦ id ↑x

Tactic:
LinearIndependent.iff_fractionRing ℤ ℚ,

Goal state after:
case refine_1
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝³ : Module.Finite ℤ ↥L
this✝² : Module ℚ E
this✝¹ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
h : finrank K E < Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range ⇑e
⊢ ¬LinearIndependent ℚ fun (x : ↑(insert v (Set.range ⇑e))) ↦ id ↑x
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
⊢ Submodule.map L.subtype (span ℤ (Set.range ⇑b)) = L

Tactic:
simp [b.span_eq]

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.Filter

Goal state before:
pp: case refine_1.mpr
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → ↑(Set.Ioi 0)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = ↑I \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := ⋯
this : Disjoint π₁.iUnion π₂.iUnion
h : (π.filter p).iUnion ⊆ π.iUnion
x : ι → ℝ
⊢ x ∈ ↑I \ (π.filter p).iUnion → x ∈ ↑I \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion

Tactic:
· rintro ⟨hxI, hxp⟩
      by_cases hxπ : x ∈ π.iUnion
      exacts [Or.inr ⟨hxπ, hxp⟩, Or.inl ⟨hxI, hxπ⟩]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
a : OrthonormalBasis ι 𝕜 E
b : OrthonormalBasis ι' 𝕜 E
⊢ (a.toBasis.toMatrix ⇑b)ᴴ * a.toBasis.toMatrix ⇑b = 1

Tactic:
a.toMatrix_orthonormalBasis_conjTranspose_mul_self b

Goal state after:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
a : OrthonormalBasis ι 𝕜 E
b : OrthonormalBasis ι' 𝕜 E
⊢ 1 = 1
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case hfh
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] 0, μ (toMeasurable μ s ∩ closedBall x b) / μ (closedBall x b) ≤ 1

Tactic:
· filter_upwards [self_mem_nhdsWithin]
      rintro r -
      apply ENNReal.div_le_of_le_mul
      rw [one_mul]
      exact measure_mono inter_subset_right

Goal state after:
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
⊢ oscillationWithin f D x = 0

Tactic:
by
  rw [← nonpos_iff_eq_zero]
  refine _root_.le_of_forall_pos_le_add fun ε hε ↦ ?_
  rw [zero_add]
  have : eball (f x) (ε / 2) ∈ (𝓝[D] x).map f :=
    hf <| eball_mem_nhds _ (by simp [ne_of_gt hε])
  refine (biInf_le ediam this).trans (le_of_le_of_eq ediam_eball_le ?_)
  exact (ENNReal.mul_div_cancel (by simp) (by simp))

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.Additive

Goal state before:
pp: ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ : Box ι
i : ι
inst✝ : Finite ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf : ∀ (I : Box ι), ↑I ≤ I₀ → ∀ (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I
I : Box ι
hI : ↑I ≤ I₀
π : Prepartition I
hπ : π.IsPartition
Hle : ∀ J ∈ π, ↑J ≤ I₀
s : Finset (ι × ℝ)
hs : splitMany I s ≤ π
⊢ ∑ Ji ∈ π.boxes, f Ji = ∑ J ∈ (π ⊓ splitMany I s).boxes, f J

Tactic:
inf_splitMany,

Goal state after:
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I✝ : Box ι
i : ι
inst✝ : Finite ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf : ∀ (I : Box ι), ↑I ≤ I₀ → ∀ (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I
I : Box ι
hI : ↑I ≤ I₀
π : Prepartition I
hπ : π.IsPartition
Hle : ∀ J ∈ π, ↑J ≤ I₀
s : Finset (ι × ℝ)
hs : splitMany I s ≤ π
⊢ ∑ Ji ∈ π.boxes, f Ji = ∑ J ∈ (π.biUnion fun J ↦ splitMany J s).boxes, f J
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
i j : ι
hij : i ≤ j
⊢ f i ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)

Tactic:
rw [gramSchmidt_def' 𝕜 f i]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
i j : ι
hij : i ≤ j
⊢ gramSchmidt 𝕜 f i + ∑ i_1 < i, (𝕜 ∙ gramSchmidt 𝕜 f i_1).starProjection (f i) ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
b : OrthonormalBasis (Fin 0) ℝ E
hb : b.toBasis.orientation ≠ o
this : positiveOrientation ≠ o
⊢ o.volumeForm = -b.toBasis.det

Tactic:
simp_rw [volumeForm, Or.by_cases, dif_neg this.symm, Nat.rec_zero, Basis.det_isEmpty]

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

Goal state before:
pp: case e'_3
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
y : E ⧸ K
f : (E ⧸ K) ≃ₗ[𝕜] ↥Kᗮ := K.quotientEquivOfIsCompl Kᗮ ⋯
h : ‖Quotient.mk ↑(f y)‖ = sInf ((fun x ↦ ‖↑(f y) + x‖) '' ↑K.toAddSubgroup)
⊢ ⨅ x, ‖↑(f y) - ↑x‖ = sInf ((fun x ↦ ‖↑(f y) + x‖) '' ↑K.toAddSubgroup)

Tactic:
rw [sInf_image', ← Equiv.iInf_comp (Equiv.neg K)]
      simp

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

Goal state before:
pp: p : ℝ≥0∞
X✝ : Type u_1
inst✝⁵ : MeasurableSpace X✝
ι : Type u_2
X : ι → Type u_3
inst✝⁴ : Countable ι
inst✝³ : (i : ι) → MeasurableSpace (X i)
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), BorelSpace (X i)
inst✝ : ∀ (i : ι), SecondCountableTopology (X i)
⊢ MeasurableSpace.comap WithLp.ofLp inferInstance = MeasurableSpace.comap WithLp.ofLp (borel ((i : ι) → X i))

Tactic:
BorelSpace.measurable_eq (α := Π i, X i)

Goal state after:
p : ℝ≥0∞
X✝ : Type u_1
inst✝⁵ : MeasurableSpace X✝
ι : Type u_2
X : ι → Type u_3
inst✝⁴ : Countable ι
inst✝³ : (i : ι) → MeasurableSpace (X i)
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), BorelSpace (X i)
inst✝ : ∀ (i : ι), SecondCountableTopology (X i)
⊢ MeasurableSpace.comap WithLp.ofLp inferInstance = MeasurableSpace.comap WithLp.ofLp (borel ((i : ι) → X i))
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
p q : ℕ
hpq : p ≤ q
⊢ (fun x ↦ x ^ p) =O[cobounded R] fun x ↦ x ^ q

Tactic:
rcases hpq.eq_or_lt with rfl | h
  · exact isBigO_refl ..
  · exact (isLittleO_pow_pow_cobounded_of_lt h).isBigO

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
ι : Type u_2
inst✝⁴ : Finite ι
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T2Space E
b : Basis ι ℝ E
s : Set E
⊢ frontier (⇑b.equivFun '' s) = ⇑b.equivFun '' frontier s

Tactic:
rw [LinearEquiv.image_eq_preimage_symm, LinearEquiv.image_eq_preimage_symm]
  exact (Homeomorph.preimage_frontier b.equivFunL.toHomeomorph.symm s).symm

Goal state after:
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: case e'_3.e'_5
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 ↦ (x :: xs).getD x_1 0 ≠ 0
inst✝ : DecidablePred fun x ↦ xs.getD x 0 ≠ 0
⊢ Finsupp.single 0 x = [x].toFinsupp

Tactic:
exact (toFinsupp_singleton x).symm

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Comap

Goal state before:
pp: σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : τ → R
⊢ comap (↑f.symm) (comap (↑f) x) = x

Tactic:
← comap_comp_apply

Goal state after:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : τ → R
⊢ comap ((↑f).comp ↑f.symm) x = x
Module: Mathlib.Algebra.MvPolynomial.Comap

Goal state before:
pp: σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : σ → R
⊢ comap (↑f) (comap (↑f.symm) x) = x

Tactic:
← comap_comp_apply

Goal state after:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : σ → R
⊢ comap ((↑f.symm).comp ↑f) x = x
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p * q
this :
  p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) = (p * q).modMonomial (Finsupp.single i 1)
⊢ X i ∣ p ∨ X i ∣ q

Tactic:
by
      simp only [X_dvd_iff_modMonomial_eq_zero] at h ⊢
      rwa [h, mul_eq_zero] at this

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

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (Box.Icc I)
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ Integrable I l f μ.toBoxAdditive.toSMul

Tactic:
by
  apply integrable_of_bounded_and_ae_continuousWithinAt
  · obtain ⟨C, hC⟩ := (NormedSpace.isBounded_iff_subset_smul_closedBall ℝ).1
                        (I.isCompact_Icc.image_of_continuousOn hc).isBounded
    use ‖C‖, fun x hx ↦ by
      simpa only [smul_unitClosedBall, mem_closedBall_zero_iff] using hC (Set.mem_image_of_mem f hx)
  · refine eventually_of_mem ?_ (fun x hx ↦ hc.continuousWithinAt hx)
    rw [mem_ae_iff, μ.restrict_apply] <;> simp [MeasurableSet.compl_iff.2 I.measurableSet_Icc]

Goal state after: