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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
n k : ℕ
x✝ : 0 ≤ k
ih : (T ^ k).IsSymmetric
⊢ ((T ^ k) ∘ₗ T).IsSymmetric

Tactic:
← Module.End.mul_eq_comp

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
n k : ℕ
x✝ : 0 ≤ k
ih : (T ^ k).IsSymmetric
⊢ IsSymmetric (T ^ k * T)
Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection

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
x : E
⊢ 2 ≠ 0

Tactic:
exact two_ne_zero

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ᗮ

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:
· 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:
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ᗮ
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
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
x : ⨁ (i : ι), ↥(V i)
i : ι
inst✝ : CompleteSpace ↥(V i)
⊢ (V i).orthogonalProjectionOnto ((DirectSum.coeAddMonoidHom V) x) = x i

Tactic:
induction x using DirectSum.induction_on with

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

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x₁ x₂ : α
⊢ ‖toLp p (x₁ - x₂, 0)‖₊ = ‖x₁ - x₂‖₊

Tactic:
nnnorm_toLp_inl

Goal state after:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x₁ x₂ : α
⊢ ‖x₁ - x₂‖₊ = ‖x₁ - x₂‖₊
Module: Mathlib.Data.Matrix.Reflection

Goal state before:
pp: case refine_2
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i✝ : Fin (n + 1)
j : Fin m
i : Fin n
⊢ of (vecCons (FinVec.map (fun v ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) i.succ j = Aᵀ i.succ j

Tactic:
simp only [of_apply, Matrix.cons_val_succ]

Goal state after:
case refine_2
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i✝ : Fin (n + 1)
j : Fin m
i : Fin n
⊢ (A.submatrix id Fin.succ)ᵀ i j = Aᵀ i.succ j
Module: Mathlib.Data.Matrix.Reflection

Goal state before:
pp: α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin n) α
⊢ A.etaExpand = A

Tactic:
etaExpand,

Goal state after:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin n) α
⊢ of (FinVec.etaExpand fun i ↦ FinVec.etaExpand fun j ↦ A i j) = A
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
inst✝ : RingHomInvPair σ' σ
e : E ≃ₛₗ[σ] F
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑e
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑e.symm ⁻¹' s)

Tactic:
← e.image_eq_preimage_symm

Goal state after:
𝕜 : 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
inst✝ : RingHomInvPair σ' σ
e : E ≃ₛₗ[σ] F
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑e
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑e '' s)
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖ = √(∑ i, ‖x.ofLp i‖ ^ 2)

Tactic:
by
  rw [norm_eq_of_nat 2 (by norm_cast) _]
  rw [Real.sqrt_eq_rpow]
  norm_cast

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 2 β
⊢ dist x y ^ 2 = ∑ i, dist (x.ofLp i) (y.ofLp i) ^ 2

Tactic:
by
  simp_rw [dist_eq_norm, norm_sq_eq_of_L2, sub_apply]

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

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
x : E
⊢ x ∈ parallelepiped v ↔ ∃ t ∈ Icc 0 1, x = ∑ i, t i • v i

Tactic:
simp [parallelepiped, eq_comm]

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
⊢ (∃ t, (∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1) ∧ x = ∑ x, Pi.single x (t x • a x)) ↔
    ∀ (x_1 : ι), min 0 (a x_1) ≤ x x_1 ∧ x x_1 ≤ max 0 (a x_1)

Tactic:
← Pi.smul_apply',

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
⊢ (∃ t, (∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1) ∧ x = ∑ x, Pi.single x ((t • a) x)) ↔
    ∀ (x_1 : ι), min 0 (a x_1) ≤ x x_1 ∧ x x_1 ≤ max 0 (a x_1)
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 : ι), IsBoundedSMul R (α i)
⊢ IsBoundedSMul R ((i : ι) → α i)

Tactic:
by
  let := pseudoMetricSpaceToPi p α
  refine ⟨fun x y z ↦ ?_, fun x y z ↦ ?_⟩
  · simpa [dist_pseudoMetricSpaceToPi] using dist_smul_pair x (toLp p y) (toLp p z)
  · simpa [dist_pseudoMetricSpaceToPi] using dist_pair_smul x y (toLp p z)

Goal state after:
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 ≤ ∑' (n : ℕ), μ (s ∩ closedBall 0 ↑n)

Tactic:
by
        conv_lhs => rw [← iUnion_inter_closedBall_nat s 0]
        exact measure_iUnion_le _

Goal state after:
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
r : ℝ
hr : r ≠ 0
⊢ map (fun x ↦ r • x) μ = ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ

Tactic:
let f : E →ₗ[ℝ] E := r • (1 : E →ₗ[ℝ] 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
r : ℝ
hr : r ≠ 0
f : E →ₗ[ℝ] E := r • 1
⊢ map (fun x ↦ r • x) μ = ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
I J : Box ι
⊢ [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE

Tactic:
tfae_have 1 ↔ 2 := Iff.rfl
  tfae_have 2 → 3
  | h => by simpa [coe_eq_pi, closure_pi_set, lower_ne_upper] using closure_mono h
  tfae_have 3 ↔ 4 := Icc_subset_Icc_iff I.lower_le_upper
  tfae_have 4 → 2
  | h, x, hx, i => Ioc_subset_Ioc (h.1 i) (h.2 i) (hx i)
  tfae_finish

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

Goal state before:
pp: ι : Type u_2
G : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A : parallelepiped v = ⇑((b.constr ℕ) v) '' parallelepiped ⇑b
⊢ ENNReal.ofReal |((LinearMap.toMatrix b b) ((b.constr ℕ) v)).det| = ENNReal.ofReal |b.det v|

Tactic:
← Basis.toMatrix_eq_toMatrix_constr,

Goal state after:
ι : Type u_2
G : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A : parallelepiped v = ⇑((b.constr ℕ) v) '' parallelepiped ⇑b
⊢ ENNReal.ofReal |(b.toMatrix v).det| = ENNReal.ofReal |b.det v|
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
ι : Type u_2
G : Type u_3
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : G [⋀^Fin n]→ₗ[ℝ] ℝ
⊢ ω.measure.IsAddLeftInvariant

Tactic:
rw [AlternatingMap.measure]; infer_instance

Goal state after:
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
ι : Type u_2
G : Type u_3
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : G [⋀^Fin n]→ₗ[ℝ] ℝ
⊢ IsLocallyFiniteMeasure ω.measure

Tactic:
rw [AlternatingMap.measure]; infer_instance

Goal state after:
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
t_bound : t ⊆ closedBall 0 1
A : Tendsto (fun r ↦ μ (s ∩ ({x} + r • t)) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
r : ℝ
rpos : 0 < r
this : closedBall x r = {x} + r • closedBall 0 1
⊢ μ (closedBall x 1) / μ ({x} + u) = μ (closedBall x r) / μ ({x} + r • u)

Tactic:
simp only [this, addHaar_singleton_add_smul_div_singleton_add_smul μ rpos.ne']

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
t_bound : t ⊆ closedBall 0 1
A : Tendsto (fun r ↦ μ (s ∩ ({x} + r • t)) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
r : ℝ
rpos : 0 < r
this : closedBall x r = {x} + r • closedBall 0 1
⊢ μ (closedBall x 1) / μ ({x} + u) = μ (closedBall 0 1) / μ u
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₀
⊢ span ℝ ↑L₀ = ⊤

Tactic:
by
    rw [← (Submodule.map_injective_of_injective (injective_subtype _)).eq_iff, Submodule.map_span,
      Submodule.map_top, range_subtype, h_img]

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

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
s : Finset (ι × ℝ)
⊢ π ⊓ splitMany I s = π.biUnion fun J ↦ splitMany J s

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert p s _ ihp => simp_rw [splitMany_insert, ← inf_assoc, ihp, inf_split, biUnion_assoc]

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✝ : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
⊢ (b.reindex e) i' = b (e.symm i')

Tactic:
classical
    dsimp [reindex]
    rw [coe_ofRepr]
    dsimp
    rw [← b.repr_symm_single, LinearIsometryEquiv.piLpCongrLeft_symm,
      EuclideanSpace.piLpCongrLeft_single]

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

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

Tactic:
rw [star_def, RCLike.mul_conj] at this

Goal state after:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
this : ↑‖(a.toBasis.toMatrix ⇑b).det‖ ^ 2 = 1
⊢ ‖a.toBasis.det ⇑b‖ = 1
Module: Mathlib.Analysis.BoxIntegral.Partition.Measure

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
I : Box (Fin (n + 1))
⊢ (∏ j, ((I.face i).upper j - (I.face i).lower j)) * (I.upper i - I.lower i) = ∏ j, (I.upper j - I.lower j)

Tactic:
simp only [face_lower, face_upper, Fin.prod_univ_succAbove _ i, mul_comm]

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
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hf : f =ᵐ[μ.restrict ↑I] 0
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : ↑ε > 0
⊢ ∃ r,
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ ↑ε

Tactic:
rw [gt_iff_lt, NNReal.coe_pos] at ε0

Goal state after:
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hf : f =ᵐ[μ.restrict ↑I] 0
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
⊢ ∃ r,
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ ↑ε
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y : F
a : ℝ
h :
  ∀ (ε : ℝ),
    0 < ε →
      ∃ r,
        (∀ (c : ℝ≥0), l.RCond (r c)) ∧
          ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
            l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ a * ε
ε : ℝ
hε : ε > 0
ε' : ℝ
hε' : 0 < ε'
ha : a * ε' < ε
⊢ ∃ r,
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ ε

Tactic:
rcases h ε' hε' with ⟨r, hr, H⟩

Goal state after:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y : F
a : ℝ
h :
  ∀ (ε : ℝ),
    0 < ε →
      ∃ r,
        (∀ (c : ℝ≥0), l.RCond (r c)) ∧
          ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
            l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ a * ε
ε : ℝ
hε : ε > 0
ε' : ℝ
hε' : 0 < ε'
ha : a * ε' < ε
r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0)
hr : ∀ (c : ℝ≥0), l.RCond (r c)
H :
  ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
    l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ a * ε'
⊢ ∃ r,
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ ε
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c₁ c₂ : ℝ≥0
ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
hpos₁ : 0 < ε₁
hpos₂ : 0 < ε₂
h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁
h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂
HU : π₁.iUnion = π₂.iUnion
⊢ dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂

Tactic:
by
  rcases h₁.exists_common_compl h₂ HU with ⟨π, hπU, hπc₁, hπc₂⟩
  set r : ℝⁿ → Ioi (0 : ℝ) := fun x => min (h.convergenceR ε₁ c₁ x) (h.convergenceR ε₂ c₂ x)
  set πr := π.toSubordinate r
  have H₁ :
    dist (integralSum f vol (π₁.unionComplToSubordinate π hπU r)) (integral I l f vol) ≤ ε₁ :=
    h.dist_integralSum_integral_le_of_memBaseSet hpos₁
      (h₁.unionComplToSubordinate (fun _ _ => min_le_left _ _) hπU hπc₁)
      (isPartition_unionComplToSubordinate _ _ _ _)
  rw [HU] at hπU
  have H₂ :
    dist (integralSum f vol (π₂.unionComplToSubordinate π hπU r)) (integral I l f vol) ≤ ε₂ :=
    h.dist_integralSum_integral_le_of_memBaseSet hpos₂
      (h₂.unionComplToSubordinate (fun _ _ => min_le_right _ _) hπU hπc₂)
      (isPartition_unionComplToSubordinate _ _ _ _)
  simpa [unionComplToSubordinate] using (dist_triangle_right _ _ _).trans (add_le_add H₁ H₂)

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)
⊢ WithLp.measurableSpace p ((i : ι) → X i) = borel (PiLp p X)

Tactic:
rw [topologicalSpace, borel_comap, WithLp.measurableSpace,
      BorelSpace.measurable_eq (α := Π i, X i)]

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
⊢ (Summable fun k ↦ (↑(u (k + 1)) - ↑(u k)) * f (u k)) ↔ Summable f

Tactic:
simp only [← tsum_coe_ne_top_iff_summable, Ne, not_iff_not, ENNReal.coe_mul]
  constructor <;> intro h
  · replace hf : ∀ m n, 1 < m → m ≤ n → (f n : ℝ≥0∞) ≤ f m := fun m n hm hmn =>
      ENNReal.coe_le_coe.2 (hf (zero_lt_one.trans hm) hmn)
    have h_nonneg : ∀ n, 0 ≤ (f n : ℝ≥0∞) := fun n =>
      ENNReal.coe_le_coe.2 (f n).2
    obtain hC := tsum_schlomilch_le hf h_pos h_nonneg hu_strict.monotone h_succ_diff
    simpa [add_eq_top, mul_ne_top, mul_eq_top, hC_nonzero] using eq_top_mono hC h
  · replace hf : ∀ m n, 0 < m → m ≤ n → (f n : ℝ≥0∞) ≤ f m := fun m n hm hmn =>
      ENNReal.coe_le_coe.2 (hf hm hmn)
    have : ∑ k ∈ range (u 0), (f k : ℝ≥0∞) ≠ ∞ := sum_ne_top.2 fun a _ => coe_ne_top
    simpa [h, add_eq_top, this] using le_tsum_schlomilch hf h_pos hu_strict

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: a s : ℝ
⊢ (Summable fun n ↦ 1 / |↑n + a| ^ s) ↔ 1 < s

Tactic:
have hnorm : Tendsto (fun n : ℕ ↦ ‖(n : ℝ)‖) atTop atTop :=
    tendsto_natCast_atTop_atTop.congr' (by simp)
  have h_abs : (fun n : ℕ ↦ |n + a|) ~[atTop] (·) := by
    apply (IsEquivalent.refl.add_const_of_norm_tendsto_atTop hnorm).congr_left
    · filter_upwards [eventually_gt_atTop (Nat.ceil |a|)] with _ hn
      rw [abs_of_pos]
      linarith [lt_of_abs_lt ((abs_neg a).symm ▸ Nat.lt_of_ceil_lt hn)]
  rw [← summable_one_div_nat_rpow, Asymptotics.IsEquivalent.summable_iff_nat]
  simpa [one_div] using! (IsEquivalent.rpow (fun n ↦ by positivity) h_abs).inv

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
n : ℕ
r : ℝ
s : ℕ → Finset (ι → ℤ) := fun n ↦ Fintype.piFinset fun i ↦ Icc (-↑n) ↑n
d : ℕ := Fintype.card ι
hr : r < -↑d
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ}, a ≤ b → s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
⊢ 2 * ↑d * 3 ^ (d - 1) * ε ^ r * ∑ k ∈ range n, ↑(k + 1) ^ (↑d - 1 + r) ≤
    2 * ↑d * 3 ^ (d - 1) * ε ^ r * (∑ k ∈ range n, ↑(k + 1) ^ (↑d - 1 + r) + ↑0 ^ (↑d - 1 + r))

Tactic:
Nat.cast_zero,

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
n : ℕ
r : ℝ
s : ℕ → Finset (ι → ℤ) := fun n ↦ Fintype.piFinset fun i ↦ Icc (-↑n) ↑n
d : ℕ := Fintype.card ι
hr : r < -↑d
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ}, a ≤ b → s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
⊢ 2 * ↑d * 3 ^ (d - 1) * ε ^ r * ∑ k ∈ range n, ↑(k + 1) ^ (↑d - 1 + r) ≤
    2 * ↑d * 3 ^ (d - 1) * ε ^ r * (∑ k ∈ range n, ↑(k + 1) ^ (↑d - 1 + r) + 0 ^ (↑d - 1 + r))
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
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
⊢ comap (g.comp f) x = comap f (comap g x)

Tactic:
by
  funext i
  trans aeval x (aeval (fun i => g (X i)) (f (X i)))
  · apply eval₂Hom_congr rfl rfl
    rw [AlgHom.comp_apply]
    suffices g = aeval fun i => g (X i) by rw [← this]
    exact aeval_unique g
  · simp only [comap, aeval_eq_eval₂Hom, map_eval₂Hom]
    refine eval₂Hom_congr ?_ rfl rfl
    ext r
    apply aeval_C

Goal state after: