mathlib-initiative/mathlib-tactics huggingface dataset:
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
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 * δ
⊢ ‖d⁻¹ • f x - (d⁻¹ * d) • y‖ = ‖d⁻¹ • (f x - d • y)‖

Tactic:
by rw [mul_smul, smul_sub]

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
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
y : E
⊢ ∀ w ∈ U, ⟪y - ↑(U.orthogonalProjectionOnto y), w⟫ = 0

Tactic:
exact starProjection_inner_eq_zero _

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

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : v = 0
⊢ (𝕜 ∙ v).starProjection w = (⟪v, w⟫ / ↑(‖v‖ ^ 2)) • v

Tactic:
hv

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : v = 0
⊢ (𝕜 ∙ 0).starProjection w = (⟪0, w⟫ / ↑(‖0‖ ^ 2)) • 0
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: case succ
𝕜 : 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 : ℕ
IH : ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
⊢ ‖h^[n + 1] y‖ ≤ (1 / 2) ^ (n + 1) * ‖y‖

Tactic:
rw [iterate_succ']
      apply le_trans (hle _) _
      rw [pow_succ', mul_assoc]
      gcongr

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 α
A✝ : Matrix n n α
A : ↥(specialUnitaryGroup n α)
⊢ star ↑A ∈ ↑(MonoidHom.mker detMonoidHom)

Tactic:
by have := A.prop.2; simp_all [star_eq_conjTranspose]

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 + idemSnd) x = 1 x

Tactic:
AddMonoidHom.add_apply,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
p : ℝ≥0∞
x : WithLp p (α × β)
⊢ idemFst x + idemSnd x = 1 x
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: ι : Type u_2
inst✝² : Fintype ι
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_5
hp : p ≠ ∞
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp p β
⊢ ‖f‖₊ = (∑ i, ‖f.ofLp i‖₊ ^ p.toReal) ^ (1 / p.toReal)

Tactic:
ext
  simp [NNReal.coe_sum, norm_eq_sum (p.toReal_pos_iff_ne_top.mpr hp)]

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

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 1 β
⊢ dist x y = ∑ i, dist (x.ofLp i) (y.ofLp i)

Tactic:
by
  simp_rw [dist_eq_norm, norm_eq_of_L1, sub_apply]

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

Goal state before:
pp: case inr
a : ℝ
r : ℝ≥0
⊢ ofReal (↑r + ↑r) = 2 * ↑r

Tactic:
← NNReal.coe_add,

Goal state after:
case inr
a : ℝ
r : ℝ≥0
⊢ ofReal ↑(r + r) = 2 * ↑r
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i ↦ t
⊢ parallelepiped ⇑(b.reindex e) = Icc 0 1 ∨ parallelepiped ⇑(b.reindex e) = Icc (-1) 0

Tactic:
have A : Icc (0 : Fin 1 → ℝ) 1 = F '' Icc (0 : ℝ) 1 := by
    apply Subset.antisymm
    · intro x hx
      refine ⟨x 0, ⟨hx.1 0, hx.2 0⟩, ?_⟩
      ext j
      simp only [F, Subsingleton.elim j 0]
    · rintro x ⟨y, hy, rfl⟩
      exact ⟨fun _j => hy.1, fun _j => hy.2⟩

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i ↦ t
A : Icc 0 1 = F '' Icc 0 1
⊢ parallelepiped ⇑(b.reindex e) = Icc 0 1 ∨ parallelepiped ⇑(b.reindex e) = Icc (-1) 0
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x ↦ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x ↦ ofReal (g x - f x)
⊢ ∫⁻ (x : α), volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Tactic:
rw [h, lintegral_indicator]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x ↦ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x ↦ ofReal (g x - f x)
⊢ ∫⁻ (a : α) in s, ofReal (g a - f a) ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

case hs
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x ↦ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x ↦ ofReal (g x - f x)
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : ⊥ ≠ ⊤
⊢ μ ∅ = 0

Tactic:
measure_empty

Goal state after:
case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : ⊥ ≠ ⊤
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: G : Type u_3
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : G [⋀^Fin n]→ₗ[ℝ] ℝ
v : Fin n → G
| ENNReal.ofReal |ω v|

Tactic:
rw [ω.eq_smul_basis_det (finBasisOfFinrankEq ℝ G _i.out)]

Goal state after:
G : Type u_3
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : G [⋀^Fin n]→ₗ[ℝ] ℝ
v : Fin n → G
| ENNReal.ofReal |(ω ⇑(finBasisOfFinrankEq ℝ G ⋯) • (finBasisOfFinrankEq ℝ G ⋯).det) v|
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
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind ⋯
this✝ : Fintype ↑s
this : (fundamentalDomain b ∩ ↑L).Finite
x : E
h_mem : x ∈ ↑L
⊢ ↑((quotientEquiv b) (Submodule.Quotient.mk x)) ∈ fundamentalDomain b ∩ ↑L

Tactic:
quotientEquiv_apply_mk,

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
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind ⋯
this✝ : Fintype ↑s
this : (fundamentalDomain b ∩ ↑L).Finite
x : E
h_mem : x ∈ ↑L
⊢ ↑(fractRestrict b x) ∈ fundamentalDomain b ∩ ↑L
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✝
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
f : ↥(span ℝ ↑L) →ₗ[ℝ] E := (span ℝ ↑L).subtype
L₀ : Submodule ℤ ↥(span ℝ ↑L) := comap (↑ℤ f) L
h_img : ⇑f '' ↑L₀ = ↑L
this : DiscreteTopology ↥L₀
⊢ Module.Finite ℤ ↥L₀

Tactic:
have : IsZLattice ℝ L₀ := ⟨by
    rw [← (Submodule.map_injective_of_injective (injective_subtype _)).eq_iff, Submodule.map_span,
      Submodule.map_top, range_subtype, h_img]⟩

Goal state after:
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✝
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
f : ↥(span ℝ ↑L) →ₗ[ℝ] E := (span ℝ ↑L).subtype
L₀ : Submodule ℤ ↥(span ℝ ↑L) := comap (↑ℤ f) L
h_img : ⇑f '' ↑L₀ = ↑L
this✝ : DiscreteTopology ↥L₀
this : IsZLattice ℝ L₀
⊢ Module.Finite ℤ ↥L₀
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)
⊢ Tendsto (fun r ↦ μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 0)

Tactic:
have B : Tendsto (fun r : ℝ => R * r) (𝓝[>] 0) (𝓝[>] (R * 0)) := by
    apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
    · exact (tendsto_const_nhds.mul tendsto_id).mono_left nhdsWithin_le_nhds
    · filter_upwards [self_mem_nhdsWithin]
      intro r rpos
      rw [mul_zero]
      exact mul_pos Rpos rpos

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
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)
B : Tendsto (fun r ↦ R * r) (𝓝[>] 0) (𝓝[>] (R * 0))
⊢ Tendsto (fun r ↦ μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 0)
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
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type u_6
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := ⋯
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := ⋯
v w : PiLp 2 fun i ↦ ↥(V i)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [sum_inner, hV'.inner_right_fintype, PiLp.inner_apply]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case inl
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 : Set E
ht : MeasurableSet t
h''t : μ t ≠ ∞
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t = 0
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] 0, μ (s ∩ ({x} + b • t)) / μ ({x} + b • t) < ε

Tactic:
filter_upwards with r
    suffices H : μ (s ∩ ({x} + r • t)) = 0 by
      rw [H]; simpa only [ENNReal.zero_div] using εpos
    rw [← nonpos_iff_eq_zero]
    calc
      μ (s ∩ ({x} + r • t)) ≤ μ ({x} + r • t) := measure_mono inter_subset_right
      _ = 0 := by
        simp only [h't, addHaar_smul, image_add_left, measure_preimage_add, singleton_add,
          mul_zero]

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

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
⊢ (∀ x ∈ I, ∃ J ∈ π, x ∈ J) ↔ π.iUnion = ↑I

Tactic:
Set.Subset.antisymm_iff,

Goal state after:
ι : Type u_1
I : Box ι
π : Prepartition I
⊢ (∀ x ∈ I, ∃ J ∈ π, x ∈ J) ↔ π.iUnion ⊆ ↑I ∧ ↑I ⊆ π.iUnion
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: case insert
ι : Type u_1
I : Box ι
π : Prepartition I
p : ι × ℝ
s : Finset (ι × ℝ)
a✝ : p ∉ s
ihp : π ⊓ splitMany I s = π.biUnion fun J ↦ splitMany J s
⊢ ((π.biUnion fun J ↦ splitMany J s).biUnion fun J ↦ split J p.1 p.2) =
    π.biUnion fun J ↦ (splitMany J s).biUnion fun J ↦ split J p.1 p.2

Tactic:
biUnion_assoc

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

Goal state before:
pp: case refine_1
ι : 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 := π.filter fun J ↦ ¬p J
this : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂.toPrepartition this).iUnion = ↑I \ (π.filter p).iUnion

Tactic:
suffices ↑I \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion = ↑I \ (π.filter p).iUnion by
      simp [π₂, *]
    have h : (π.filter p).iUnion ⊆ π.iUnion :=
      biUnion_subset_biUnion_left (Finset.filter_subset _ _)
    ext x
    fconstructor
    · rintro (⟨hxI, hxπ⟩ | ⟨hxπ, hxp⟩)
      exacts [⟨hxI, mt (@h x) hxπ⟩, ⟨π.iUnion_subset hxπ, hxp⟩]
    · rintro ⟨hxI, hxp⟩
      by_cases hxπ : x ∈ π.iUnion
      exacts [Or.inr ⟨hxπ, hxp⟩, Or.inl ⟨hxI, hxπ⟩]

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

Goal state before:
pp: case neg
𝕜 : 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
b✝ b : ι
ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
h : ¬gramSchmidt 𝕜 f a = 0
⊢ ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
      ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 / ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 * ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 =
    0

Tactic:
div_mul_cancel₀,

Goal state after:
case neg
𝕜 : 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
b✝ b : ι
ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
h : ¬gramSchmidt 𝕜 f a = 0
⊢ ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 - ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 = 0

case neg.h
𝕜 : 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
b✝ b : ι
ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
h : ¬gramSchmidt 𝕜 f a = 0
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 ≠ 0
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case h
R : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
⊢ (map ι f) (rayOfNeZero R g hg) = rayOfNeZero R g hg

Tactic:
| h g hg =>

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case intro.h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Finite ι
e : Basis ι R M
f : M ≃ₗ[R] M
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
⊢ (Orientation.map ι f) (rayOfNeZero R g hg) = (LinearEquiv.det f)⁻¹ • rayOfNeZero R g hg

Tactic:
| h g hg =>

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
f : M ≃ₗ[R] M
⊢ (e.map f).orientation = e.orientation ↔ 0 < LinearMap.det ↑f

Tactic:
by
  rw [orientation_map, e.map_orientation_eq_det_inv_smul, units_inv_smul, units_smul_eq_self_iff,
    LinearEquiv.coe_det]

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

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
x : ι → ℝ
⊢ ∀ {m n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖

Tactic:
m

Goal state after:
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
x : ι → ℝ
m : ℕ
⊢ ∀ {n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖
Module: Mathlib.Analysis.InnerProductSpace.ProdL2

Goal state before:
pp: 𝕜 : 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
⊢ ‖(K.quotientEquivOfIsCompl Kᗮ ⋯) y‖ = ‖y‖

Tactic:
by
    set f := K.quotientEquivOfIsCompl Kᗮ K.isCompl_orthogonal
    rw [coe_norm, ← norm_orthogonalProjectionOnto_apply Kᗮ (f y).2,
      orthogonalProjectionOnto_orthogonal, coe_norm, starProjection_minimal, eq_comm]
    have h : ‖Quotient.mk (f y).val‖ = sInf ((fun (x : E) ↦ ‖(f y).val + x‖) '' K.toAddSubgroup) :=
      quotient_norm_mk_eq K.toAddSubgroup (f y).1
    convert! h using 2
    · simp [f]
    · rw [sInf_image', ← Equiv.iInf_comp (Equiv.neg K)]
      simp

Goal state after:
Module: Mathlib.Data.Set.SMulAntidiagonal

Goal state before:
pp: G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst✝¹ : SMul G P
x y : ↑(s.smulAntidiagonal t a)
inst✝ : IsCancelSMul G P
h : (↑x).1 = (↑y).1
⊢ a = (↑y).1 • (↑x).2

Tactic:
by
          rw [← h]
          exact x.2.2.2.symm

Goal state after:
Module: Mathlib.Data.Set.SMulAntidiagonal

Goal state before:
pp: G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst✝¹ : SMul G P
x y : ↑(s.smulAntidiagonal t a)
inst✝ : IsCancelSMul G P
h : (↑x).2 = (↑y).2
⊢ a = (↑x).1 • (↑y).2

Tactic:
by
          rw [← h]
          exact x.2.2.2.symm

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

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
x : σ → R
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x = x

Tactic:
by
  funext i
  simp only [comap, AlgHom.id_apply, aeval_X]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case pos
α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
ha : a ∈ s
⊢ n ! = ∏ x ∈ s, (Pi.single a n x)!

Tactic:
rw [Finset.prod_eq_single a (by simp_all) (by simp_all), Pi.single_eq_same]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
⊢ coeff d ((X 0 + X 1) ^ n) = ↑(if (d 0, d 1) ∈ Finset.antidiagonal n then n.choose (d 0) else 0)

Tactic:
rw [← Fin.sum_univ_two, coeff_sum_X_pow_of_fintype]
  congr 1
  have : d.sum (fun x m ↦ m) = d 0 + d 1 := by
    simp [Finsupp.sum_of_support_subset d (Finset.subset_univ d.support)]
  simp only [Finset.mem_antidiagonal, this]
  split_ifs with hd
  · rw [multinomial_eq_of_support_subset (Finset.subset_univ d.support), Finset.univ_fin2,
      Nat.binomial_eq_choose Fin.zero_ne_one, hd]
  · rfl

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
a : α
f : α →₀ ℕ
⊢ Nat.multinomial f.support ⇑f =
    (f.sum fun x ↦ id).choose (f a) * Nat.multinomial (f.update a 0).support ⇑(f.update a 0)

Tactic:
classical
    by_cases h : a ∈ f.support
    · rw [← Finset.insert_erase h, Nat.multinomial_insert (Finset.notMem_erase a _),
        Finset.add_sum_erase _ f h, support_update_zero]
      congr 1
      exact Nat.multinomial_congr fun _ h ↦ (Function.update_of_ne (mem_erase.1 h).1 0 f).symm
    rw [notMem_support_iff] at h
    rw [h, Nat.choose_zero_right, one_mul, ← h, update_self]

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

Goal state before:
pp: case hc
ι : 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 μ
⊢ ∀ᵐ (x : ι → ℝ) ∂μ.restrict (Box.Icc I), ContinuousWithinAt f (Box.Icc I) x

Tactic:
refine eventually_of_mem ?_ (fun x hx ↦ hc.continuousWithinAt hx)

Goal state after:
case hc
ι : 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 μ
⊢ Box.Icc I ∈ ae (μ.restrict (Box.Icc I))