mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x✝ : n ≠ 0
this✝ : NeZero ↑n
this : NeZero ↑n
μ : CyclotomicField n K
hμ : IsPrimitiveRoot μ n
⊢ μ ∈ {b | b ^ n = 1}

pp: case refine_2
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x✝ : n ≠ 0
this✝ : NeZero ↑n
this : NeZero ↑n
μ : CyclotomicField n K
hμ : IsPrimitiveRoot μ n
⊢ IsPrimitiveRoot ⟨μ, ⋯⟩ n

Tactic:
· apply (isRoot_of_unity_iff (NeZero.pos n) (CyclotomicField n K)).mpr
      refine ⟨n, Nat.mem_divisors_self _ (NeZero.ne n), ?_⟩
      rwa [← isRoot_cyclotomic_iff] at hμ

Goal state after:
case refine_2
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x✝ : n ≠ 0
this✝ : NeZero ↑n
this : NeZero ↑n
μ : CyclotomicField n K
hμ : IsPrimitiveRoot μ n
⊢ IsPrimitiveRoot ⟨μ, ⋯⟩ n
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 4 → χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1
⊢ χ₄ ↑n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1

Tactic:
← Int.emod_emod_of_dvd n (by lia : (2 : ℤ) ∣ 4),

Goal state after:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 4 → χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1
⊢ χ₄ ↑n = if n % 4 % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R' : Type u_2
inst✝² : CommRing R'
R'' : Type u_3
inst✝¹ : CommRing R''
R : Type u_4
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
f : R' →+* R''
⊢ (χ.ringHomComp f)⁻¹ = χ⁻¹.ringHomComp f

Tactic:
by
  ext1
  simp only [inv_apply, Ring.inverse_unit, ringHomComp_apply]

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case inl
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = 0
⊢ 0 ^ p = 0

pp: case inr.inl
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = 1
⊢ 1 ^ p = 1

pp: case inr.inr
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = -1
⊢ (-1) ^ p = -1

Tactic:
· rw [zero_pow (@Fact.out p.Prime).ne_zero]

Goal state after:
case inr.inl
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = 1
⊢ 1 ^ p = 1

case inr.inr
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = -1
⊢ (-1) ^ p = -1
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
⊢ χ ^ (2 * n + 1) = χ

Tactic:
rw [pow_add, pow_one, hχ.pow_even (even_two_mul _), one_mul]

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ C = adjoin A {x | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ x ^ n_1 = 1} ↔ C = A[ζ]

Tactic:
simp only [Set.mem_singleton_iff, exists_eq_left]

Goal state after:
n : ℕ
inst✝⁴ : NeZero n
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ C = adjoin A {x | n ≠ 0 ∧ x ^ n = 1} ↔ C = A[ζ]
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : Fintype Mˣ
χ : MulChar M R
a✝ : Mˣ
⊢ χ (↑a✝ ^ Fintype.card Mˣ) = 1

Tactic:
← Units.val_pow_eq_pow_val,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : Fintype Mˣ
χ : MulChar M R
a✝ : Mˣ
⊢ χ ↑(a✝ ^ Fintype.card Mˣ) = 1
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case zero
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ ψ = χ 1 * gaussSum χ ψ

Tactic:
MulChar.map_one,

Goal state after:
case zero
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ ψ = 1 * gaussSum χ ψ
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: case e_6
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : FiniteDimensional 𝕜 E
A : Type u_3
inst✝³ : Ring A
inst✝² : Module 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
x✝² x✝¹ x✝ : E
⊢ ((AlgebraTensorModule.curry
          ((AlgebraTensorModule.curry
              (((↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) ∘ₗ LinearMap.rTensor E (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)) ∘ₗ
                ↑(assocIsometry 𝕜 E E E).symm.toLinearEquiv))
            x✝²))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry
          ((AlgebraTensorModule.curry
              ((↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) ∘ₗ LinearMap.lTensor E (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)))
            x✝²))
        x✝¹)
      x✝

Tactic:
simp [mul_assoc]

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

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
a b : E →ₗ[𝕜] E
hab : a ≤ b
c : E →ₗ[𝕜] E
⊢ a + c ≤ b + c

Tactic:
by simpa [le_def]

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

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : ↥(⋀[ℝ]^n E)
h : ∑ s, ((Module.Basis.exteriorPower n (stdOrthonormalBasis ℝ E).toBasis).repr x) s ^ 2 = 0
⊢ x = 0

Tactic:
Finset.sum_eq_zero_iff_of_nonneg (fun _ _ ↦ sq_nonneg _)

Goal state after:
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : ↥(⋀[ℝ]^n E)
h : ∀ i ∈ Finset.univ, ((Module.Basis.exteriorPower n (stdOrthonormalBasis ℝ E).toBasis).repr x) i ^ 2 = 0
⊢ x = 0
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
⊢ ∫⁻ (x : ι → ℝ), ∏ i, (∫⁻ (xᵢ : ℝ), ‖fderiv ℝ u (update x i xᵢ)‖ₑ) ^ (1 / (↑#ι - 1)) ≤
    (∫⁻ (x : ι → ℝ), ‖fderiv ℝ u x‖ₑ) ^ p

Tactic:
by
        -- apply the grid-lines lemma
        apply lintegral_prod_lintegral_pow_le _ hp
        fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric (T i)
hC : Pairwise (Commute on T)
⊢ (⨆ α, ⨅ j, (T j).eigenspace (α j))ᗮ = ⊥

Tactic:
rw [iSup_iInf_eq_top_of_commute hT hC, top_orthogonal_eq_bot]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫‖
h_anti : AntilipschitzWith c⁻¹ ⇑f
⊢ (↑f).range.topologicalClosure = ⊤

Tactic:
Submodule.topologicalClosure_eq_top_iff,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫‖
h_anti : AntilipschitzWith c⁻¹ ⇑f
⊢ (↑f).rangeᗮ = ⊥
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p' : ℝ≥0
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
n' : ℝ≥0 := (↑n).conjExponent
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hp : 1 ≤ 1
hp' : (↑p')⁻¹ = ↑1⁻¹ - (↑n)⁻¹
h2p : ↑1 < ↑n
hnp : 0 < ↑n - ↑1
this : ↑p' = ↑n'
⊢ ↑p' = ↑n'

Tactic:
simpa using this

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
ι : Type u_6
ι' : Type u_7
inst✝¹ : Fintype ι
inst✝ : Fintype ι'
x : E ⊗[𝕜] F
e : OrthonormalBasis ι 𝕜 E
f : OrthonormalBasis ι' 𝕜 F
⊢ ∑ i, ((e.toBasis.tensorProduct f.toBasis).repr x) i • (e.toBasis.tensorProduct f.toBasis) i =
    ∑ i, ∑ j, ((e.toBasis.tensorProduct f.toBasis).repr x) (i, j) • e i ⊗ₜ[𝕜] f j

Tactic:
simp [← Finset.sum_product', Basis.tensorProduct_apply']

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
⊢ singularValues 0 = 0

Tactic:
ext1 i

Goal state after:
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
i : ℕ
⊢ (singularValues 0) i = 0 i
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
a : E ⊗[𝕜] F
x✝³ : G
c : E ⊗[𝕜] F
x✝² : G
x✝¹ : E
x✝ : F
⊢ ∀ (x : E) (y : F),
    inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (x✝¹ ⊗ₜ[𝕜] x✝ ⊗ₜ[𝕜] x✝³))
        ((TensorProduct.assoc 𝕜 E F G) (x ⊗ₜ[𝕜] y ⊗ₜ[𝕜] x✝²)) =
      inner 𝕜 (x✝¹ ⊗ₜ[𝕜] x✝ ⊗ₜ[𝕜] x✝³) (x ⊗ₜ[𝕜] y ⊗ₜ[𝕜] x✝²)

Tactic:
simp [mul_assoc]

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

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s

Tactic:
have Ssep' : ∀ n, Metric.AreSeparated (S n) (s ∩ t) := fun n =>
    (Ssep n).mono Subset.rfl inter_subset_right

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:

Tactic:
eLpNorm u q μ
      = eLpNorm u q (μ.restrict s) := by rw [eLpNorm_restrict_eq_of_support_subset h2u]
    _ ≤ eLpNorm u p' (μ.restrict s) * t := by
        convert! eLpNorm_le_eLpNorm_mul_rpow_measure_univ this hu.continuous.aestronglyMeasurable
        rw [ENNReal.coe_rpow_of_nonneg]
        · simp [ENNReal.coe_toNNReal hs.measure_lt_top.ne]
        · rw [one_div, one_div]
          norm_cast
          rw [hp']
          simpa using hpq
    _ = eLpNorm u p' μ * t := by rw [eLpNorm_restrict_eq_of_support_subset h2u]
    _ ≤ (C * eLpNorm (fderiv ℝ u) p μ) * t := by
        have h2u' : HasCompactSupport u := by
          apply HasCompactSupport.of_support_subset_isCompact hs.isCompact_closure
          exact h2u.trans subset_closure
        rel [eLpNorm_le_eLpNorm_fderiv_of_eq μ hu h2u' hp (mod_cast h2p.pos) hp']
    _ = eLpNormLESNormFDerivOfLeConst F μ s p q * eLpNorm (fderiv ℝ u) p μ := by
      simp_rw [eLpNormLESNormFDerivOfLeConst, ENNReal.coe_mul]; ring

Goal state after:
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: case inr
X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℕ
h✝ : d₁ < d₂
s : Set X
h : μH[↑d₁] s = ⊤
⊢ (volume.addHaarScalarFactor μH[↑d₁] • μH[↑d₁]) s = ⊤

Tactic:
rw [smul_apply, h, ENNReal.smul_top]

Goal state after:
case inr
X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℕ
h✝ : d₁ < d₂
s : Set X
h : μH[↑d₁] s = ⊤
⊢ (if volume.addHaarScalarFactor μH[↑d₁] = 0 then 0 else ⊤) = ⊤
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case neg
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
hrank : finrank 𝕜 U ≠ finrank 𝕜 ↥f.range
⊢ f.normDet = ‖((toMatrix bu.toBasis bv.toBasis) f).det‖

Tactic:
· symm
    rw [normDet_eq_zero_iff_rank_range_ne.mpr hrank.symm]
    contrapose hrank with hdet
    have h : IsUnit ((f.toMatrix bu.toBasis bv.toBasis).det) := by
      simpa using hdet
    let f' := LinearEquiv.ofIsUnitDet h
    have hf : f.range = ⊤ := f'.range
    rw [hf]
    simpa using f'.finrank_eq

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

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
⊢ (mkMetric fun x ↦ ∞) = ⊤

Tactic:
simp_rw [mkMetric, mkMetric', mkMetric'.pre, extend_top, boundedBy_top, eq_top_iff]

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
⊢ ⊤ ≤ ⨆ r, ⨆ (_ : r > 0), ⊤
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup U
inst✝⁴ : InnerProductSpace 𝕜 U
inst✝³ : FiniteDimensional 𝕜 U
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : CompleteSpace V
f : U →L[𝕜] V
this✝ : CompleteSpace U
this : CompleteSpace ↥(↑f).range
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := ⋯
h : ¬(↑f).ker = ⊥
⊢ (ContinuousLinearMap.adjoint f ∘SL f).det = 0

Tactic:
det_eq_zero_iff_ker_ne_bot,

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup U
inst✝⁴ : InnerProductSpace 𝕜 U
inst✝³ : FiniteDimensional 𝕜 U
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : CompleteSpace V
f : U →L[𝕜] V
this✝ : CompleteSpace U
this : CompleteSpace ↥(↑f).range
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
h : ¬(↑f).ker = ⊥
⊢ (↑(ContinuousLinearMap.adjoint f ∘SL f)).ker ≠ ⊥
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case pos
𝕜 : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : InnerProductSpace 𝕜 W
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
hf : f.ker = ⊥
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
hgf : (g ∘ₗ f).ker = ⊥
bw : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥(g ∘ₗ f).range
bw' : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥(g.domRestrict f.range).range :=
  bw.map (LinearIsometryEquiv.ofEq (g ∘ₗ f).range (g.domRestrict f.range).range ⋯)
⊢ ‖((toMatrix bu.toBasis bw.toBasis) (g ∘ₗ f).rangeRestrict).det‖ =
    ‖((toMatrix bv.toBasis bw'.toBasis) (g.domRestrict f.range).rangeRestrict).det‖ *
      ‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖

Tactic:
rw [← norm_mul, ← Matrix.det_mul, ← LinearMap.toMatrix_comp]

Goal state after:
case pos
𝕜 : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : InnerProductSpace 𝕜 W
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
hf : f.ker = ⊥
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
hgf : (g ∘ₗ f).ker = ⊥
bw : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥(g ∘ₗ f).range
bw' : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥(g.domRestrict f.range).range :=
  bw.map (LinearIsometryEquiv.ofEq (g ∘ₗ f).range (g.domRestrict f.range).range ⋯)
⊢ ‖((toMatrix bu.toBasis bw.toBasis) (g ∘ₗ f).rangeRestrict).det‖ =
    ‖((toMatrix bu.toBasis bw'.toBasis) ((g.domRestrict f.range).rangeRestrict ∘ₗ f.rangeRestrict)).det‖
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝³ : EMetricSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst✝ : ∀ (n : β), Countable (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
⊢ (mkMetric m) s ≤ liminf (fun n ↦ ∑' (i : ι n), m (ediam (t n i))) l

Tactic:
have : ∀ n, Encodable (ι n) := fun n => Encodable.ofCountable _
  simp only [mkMetric_apply]
  refine iSup₂_le fun ε hε => ?_
  refine le_of_forall_gt_imp_ge_of_dense fun c hc => ?_
  rcases ((frequently_lt_of_liminf_lt (by isBoundedDefault) hc).and_eventually
        ((hr.eventually (gt_mem_nhds hε)).and (ht.and hst))).exists with
    ⟨n, hn, hrn, htn, hstn⟩
  set u : ℕ → Set X := fun j => ⋃ b ∈ decode₂ (ι n) j, t n b
  refine iInf₂_le_of_le u (by rwa [iUnion_decode₂]) ?_
  refine iInf_le_of_le (fun j => ?_) ?_
  · rw [ediam_iUnion_mem_option]
    exact iSup₂_le fun _ _ => (htn _).trans hrn.le
  · calc
      (∑' j : ℕ, ⨆ _ : (u j).Nonempty, m (ediam (u j))) = _ :=
        tsum_iUnion_decode₂ (fun t : Set X => ⨆ _ : t.Nonempty, m (ediam t)) (by simp) _
      _ ≤ ∑' i : ι n, m (ediam (t n i)) := ENNReal.tsum_le_tsum fun b => iSup_le fun _ => le_rfl
      _ ≤ c := hn.le

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

Goal state before:
pp: case mp
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
⊢ (∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0) → ∀ y ∈ S, ⟪y, x⟫.im = 0

Tactic:
intro h y hy

Goal state after:
case mp
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
h : ∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0
y : H
hy : y ∈ S
⊢ ⟪y, x⟫.im = 0
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n ↦ (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f ↦ univ.pi fun i ↦ Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n ↦ 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ 1 / ↑n
C : ∀ᶠ (n : ℕ) in atTop, (univ.pi fun i ↦ Ioo ↑(a i) ↑(b i)) ⊆ ⋃ i, t n i
⊢ liminf (fun n ↦ ∑ i, ediam (t n i) ^ ↑(Fintype.card ι)) atTop ≤ liminf (fun n ↦ ∑ i, (1 / ↑n) ^ Fintype.card ι) atTop

Tactic:
refine liminf_le_liminf ?_ ?_

Goal state after:
case refine_1
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n ↦ (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f ↦ univ.pi fun i ↦ Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n ↦ 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ 1 / ↑n
C : ∀ᶠ (n : ℕ) in atTop, (univ.pi fun i ↦ Ioo ↑(a i) ↑(b i)) ⊆ ⋃ i, t n i
⊢ ∀ᶠ (a_1 : ℕ) in atTop, ∑ i, ediam (t a_1 i) ^ ↑(Fintype.card ι) ≤ ∑ i, (1 / ↑a_1) ^ Fintype.card ι

case refine_2
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n ↦ (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f ↦ univ.pi fun i ↦ Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n ↦ 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ 1 / ↑n
C : ∀ᶠ (n : ℕ) in atTop, (univ.pi fun i ↦ Ioo ↑(a i) ↑(b i)) ⊆ ⋃ i, t n i
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) atTop fun n ↦ ∑ i, ediam (t n i) ^ ↑(Fintype.card ι)
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : FirstCountableTopology E
f : E →ₛₗ[σ] F
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i ↦ b i
bE' : (𝓝 0).HasBasis (fun x ↦ True) fun n ↦ c ^ n • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), f (u i) ∉ V
h_tendsto : Tendsto (fun n ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n ↦ (c ^ n)⁻¹ • u n)
hf : IsVonNBounded 𝕜' (Set.range fun x ↦ (σ c ^ x)⁻¹ • f (u x))
this✝ : Tendsto (fun n ↦ σ c ^ n) atTop (𝓝 0)
this : Tendsto ((fun n ↦ σ c ^ n) • fun n ↦ (σ c ^ n)⁻¹ • f (u n)) atTop (𝓝 0)
n : ℕ
⊢ ((fun n ↦ σ c ^ n) • fun n ↦ (σ c ^ n)⁻¹ • f (u n)) n = (⇑f ∘ u) n

Tactic:
simp [c_ne]

Goal state after:
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ rexp (-x) • cexp (-↑x) ^ (s - 1) • f = cexp (-s * ↑x) • f

Tactic:
change (rexp (-x) : ℂ) • _ = _ • f

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ ↑(rexp (-x)) • cexp (-↑x) ^ (s - 1) • f = cexp (-s * ↑x) • f