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

Goal state before:
pp: case refine_3
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 : CyclotomicField n K
hx : x ∈ adjoin A {b | b ^ n = 1}
y z : CyclotomicField n K
x✝¹ : y ∈ adjoin A {b | b ^ n = 1}
x✝ : z ∈ adjoin A {b | b ^ n = 1}
hy : ⟨y, x✝¹⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
hz : ⟨z, x✝⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
⊢ ⟨y + z, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
exact Subalgebra.add_mem _ hy hz

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n / 2)

Tactic:
nth_rewrite 3 [← Nat.div_add_mod n 4]

Goal state after:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ ((4 * (n / 4) + n % 4) / 2)
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero n
ψ : DirichletCharacter R m
h : (changeLevel ⋯) χ = (changeLevel ⋯) ψ
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap ⋯).ker
z : ℕ
hz₁ : ↑z = ↑x
hz₂ : ↑z = 1
hz₀ : z.gcd (n * m) = 1
this : ((changeLevel ⋯) χ) ↑(ZMod.unitOfCoprime z hz₀) = χ (↑(ZMod.unitOfCoprime z hz₀)).cast
⊢ χ ↑x = 1

Tactic:
simp only [ZMod.coe_unitOfCoprime, dvd_mul_right, ZMod.cast_natCast] at this

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero n
ψ : DirichletCharacter R m
h : (changeLevel ⋯) χ = (changeLevel ⋯) ψ
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap ⋯).ker
z : ℕ
hz₁ : ↑z = ↑x
hz₂ : ↑z = 1
hz₀ : z.gcd (n * m) = 1
this : ((changeLevel ⋯) χ) ↑z = χ ↑z
⊢ χ ↑x = 1
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
hn : n = 1
⊢ χ = 1

Tactic:
by
  subst hn
  exact level_one _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
hd : d ∈ χ.conductorSet
⊢ χ.conductor ∣ d

Tactic:
have : NeZero d := ⟨by
    contrapose hd
    exact hd ▸ zero_ne_mem_conductorSet χ⟩

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
hd : d ∈ χ.conductorSet
this : NeZero d
⊢ χ.conductor ∣ d
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
⊢ ∑ a, 1 a = ↑(Fintype.card Rˣ)

Tactic:
calc
    (∑ a, (1 : MulChar R R') a) = ∑ a : R, if IsUnit a then 1 else 0 :=
      Finset.sum_congr rfl fun a _ => ?_
    _ = ((Finset.univ : Finset R).filter IsUnit).card := Finset.sum_boole _ _
    _ = (Finset.univ.map ⟨((↑) : Rˣ → R), Units.val_injective⟩).card := ?_
    _ = Fintype.card Rˣ := congr_arg _ (Finset.card_map _)
  · split_ifs with h
    · exact one_apply_coe h.unit
    · exact map_nonunit _ h
  · congr
    ext a
    simp [IsUnit]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝ : NeZero n
d : ℕ
a✝ b✝ : DirichletCharacter R n
hχ : a✝ ∈ {χ | d.Coprime χ.conductor}
hψ : b✝ ∈ {χ | d.Coprime χ.conductor}
⊢ a✝ * b✝ ∈ {χ | d.Coprime χ.conductor}

Tactic:
apply Nat.Coprime.of_dvd_right (conductor_mul_dvd_lcm_conductor _ _)

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝ : NeZero n
d : ℕ
a✝ b✝ : DirichletCharacter R n
hχ : a✝ ∈ {χ | d.Coprime χ.conductor}
hψ : b✝ ∈ {χ | d.Coprime χ.conductor}
⊢ d.Coprime (a✝.conductor.lcm b✝.conductor)
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝¹ : NeZero n
inst✝ : Nontrivial R
p : ℕ
hp : Fact (Nat.Prime p)
this : NeZero (n / p ^ n.factorization p)
hcop : p.Coprime (n / p ^ n.factorization p)
h : χ.primitiveCharacter ↑p = 1
hdvd : χ.conductor ∣ n / p ^ n.factorization p
⊢ ((changeLevel hdvd) χ.primitiveCharacter) ↑p = 1

Tactic:
rw [show (p : ZMod (n / p ^ n.factorization p))
          = ((p : ℤ) : ZMod (n / p ^ n.factorization p)) from (Int.cast_natCast p).symm,
        changeLevel_eq_cast_of_dvd' χ.primitiveCharacter hdvd (Nat.isCoprime_iff_coprime.mpr hcop),
        Int.cast_natCast]
      exact h

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = ↑(Fintype.card R)

Tactic:
simp only [gaussSum, AddChar.inv_apply, Finset.sum_mul, Finset.mul_sum, MulChar.inv_apply']

Goal state after:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ x, ∑ i, χ i * ψ i * (χ x⁻¹ * ψ (-x)) = ↑(Fintype.card R)
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : ψ.IsPrimitive
⊢ χ * χ ^ (orderOf χ - 1) = 1

Tactic:
rw [← pow_succ', Nat.sub_one_add_one_eq_of_pos χ.orderOf_pos, pow_orderOf_eq_one]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: 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
χ : MulChar R R'
ψ : AddChar R R'
⊢ ∑ x, (frobenius R' p) (χ x * ψ x) = ∑ a, (χ ^ p) a * (ψ ^ p) a

Tactic:
pow_apply' χ fp.1.ne_zero,

Goal state after:
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
χ : MulChar R R'
ψ : AddChar R R'
⊢ ∑ x, (frobenius R' p) (χ x * ψ x) = ∑ x, χ x ^ p * (ψ ^ p) x
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ ‖p‖ * ‖‖f x‖‖ ^ (p - 2) * ‖(innerSL ℝ) (f x) ∘SL fderiv ℝ f x‖ ≤ p * ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖

Tactic:
norm_norm,

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ ‖p‖ * ‖f x‖ ^ (p - 2) * ‖(innerSL ℝ) (f x) ∘SL fderiv ℝ f x‖ ≤ p * ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ ‖p‖ * ‖‖x‖‖ ^ (p - 2) * ‖(innerSL ℝ) x‖ = p * ‖x‖ ^ (p - 1)

Tactic:
norm_norm,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ ‖p‖ * ‖x‖ ^ (p - 2) * ‖(innerSL ℝ) x‖ = p * ‖x‖ ^ (p - 1)
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ t ⊆ s ∧ #(s \ t) = 1 → ∃ a ∉ t, insert a t = s

Tactic:
card_eq_one

Goal state after:
case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (t ⊆ s ∧ ∃ a, s \ t = {a}) → ∃ a ∉ t, insert a t = s
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: case pos.mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
hst : s ⊆ t
⊢ (∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u) → s ⊆ u ∧ u ⊆ t

pp: case pos.mpr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
hst : s ⊆ t
⊢ s ⊆ u ∧ u ⊆ t → ∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u

Tactic:
· rintro ⟨u, hut, -, rfl⟩
          exact ⟨subset_union_right, union_subset hut hst⟩

Goal state after:
case pos.mpr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
hst : s ⊆ t
⊢ s ⊆ u ∧ u ⊆ t → ∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u
Module: Mathlib.Analysis.InnerProductSpace.Affine

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p : P
t : ℝ
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
⊢ dist p ((AffineMap.lineMap a b) t) ^ 2 = dist p a ^ 2 + t ^ 2 * dist a b ^ 2

Tactic:
by
  have h := dist_sq_lineMap_lineMap_of_inner_eq_zero (t₁ := 1) (t₂ := t) h_inner
  simp only [AffineMap.lineMap_apply_one, one_pow, one_mul] at h
  rwa [dist_comm a p] at h

Goal state after:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : A i → (a : ι) → A a := update x i
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
this : ∀ (t : A i), (∫⋯∫⁻_{i}, f ∂μ) (X t) = (∫⋯∫⁻_{i}, f ∂μ) x
⊢ ∫⁻ (t : A i), (∫⋯∫⁻_{i}, f ∂μ) x ^ p * (f (X t) ^ (1 - k * p) * ∏ j ∈ s, (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p) ∂μ i =
    (∫⋯∫⁻_{i}, f ∂μ) x ^ p * ∫⁻ (t : A i), f (X t) ^ (1 - k * p) * ∏ j ∈ s, (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p ∂μ i

Tactic:
rw [lintegral_const_mul]

Goal state after:
case hf
ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : A i → (a : ι) → A a := update x i
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
this : ∀ (t : A i), (∫⋯∫⁻_{i}, f ∂μ) (X t) = (∫⋯∫⁻_{i}, f ∂μ) x
⊢ Measurable fun t ↦ f (X t) ^ (1 - k * p) * ∏ j ∈ s, (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x : E
⊢ 1 * x = x

Tactic:
dsimp [OfNat.ofNat]
    rw [← rTensor_tmul, ← comp_apply, ← adjoint_rTensor, ← adjoint_comp, rTensor_counit_comp_comul,
      ← toLinearMap_symm_lid, ← toLinearEquiv_lidIsometry, ← toLinearEquiv_symm,
      adjoint_toLinearMap_eq_symm]
    exact one_smul _ _

Goal state after:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case e'_4
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
p : ℝ
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ Disjoint {i} (insert i s)ᶜ

Tactic:
Finset.disjoint_singleton_left,

Goal state after:
case e'_4
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
p : ℝ
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ i ∉ (insert i s)ᶜ
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case e'_4
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
p : ℝ
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ ∫⋯∫⁻_sᶜ, f ∂μ = ∫⋯∫⁻_{i}, ∫⋯∫⁻_(insert i s)ᶜ, f ∂μ ∂μ

Tactic:
rw [← lmarginal_union μ f hf]
    · rw [← insert_compl_insert hi]
      rfl
    rw [Finset.disjoint_singleton_left, notMem_compl]
    exact mem_insert_self i s

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

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : LinearOrder ι
b : OrthonormalBasis ι ℝ E
x y : ↥(⋀[ℝ]^n E)
| (innerProductForm x) y

Tactic:
← (b.toBasis.exteriorPower n).sum_repr x,

Goal state after:
n : ℕ
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : LinearOrder ι
b : OrthonormalBasis ι ℝ E
x y : ↥(⋀[ℝ]^n E)
| (innerProductForm
      (∑ i, ((Module.Basis.exteriorPower n b.toBasis).repr x) i • (Module.Basis.exteriorPower n b.toBasis) i))
    y
Module: Mathlib.Analysis.InnerProductSpace.MeanErgodic

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
hf : ‖f‖ ≤ 1
x : E
⊢ Tendsto (fun x_1 ↦ birkhoffAverage 𝕜 (⇑f) id x_1 x) atTop (𝓝 ↑(((↑f).eqLocus ↑1).orthogonalProjectionOnto x))

Tactic:
apply (f : E →ₗ[𝕜] E).tendsto_birkhoffAverage_of_ker_subset_closure (f.lipschitz.weaken hf)

Goal state after:
case hg_proj
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
⊢ ∀ (x : ↥((↑f).eqLocus 1)), ((↑f).eqLocus ↑1).orthogonalProjectionOnto ↑x = x

case hg_ker
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
⊢ ↑(↑((↑f).eqLocus ↑1).orthogonalProjectionOnto).ker ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(↑f - 1).range
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
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 ↥f.range
⊢ Nat.card ι = finrank 𝕜 ↥f.range

Tactic:
finrank_eq_nat_card_basis bv.toBasis

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
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 ↥f.range
⊢ Nat.card ι = Nat.card ι
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
h : r < dimH s
⊢ ∃ x ∈ s, ∀ t ∈ 𝓝[s] x, r < dimH t

Tactic:
by
  contrapose! h; choose! t htx htr using h
  rcases countable_cover_nhdsWithin htx with ⟨S, hSs, hSc, hSU⟩
  calc
    dimH s ≤ dimH (⋃ x ∈ S, t x) := dimH_mono hSU
    _ = ⨆ x ∈ S, dimH (t x) := dimH_bUnion hSc _
    _ ≤ r := iSup₂_le fun x hx => htr x <| hSs hx

Goal state after:
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
f : U →ₗ[𝕜] V
h : f.ker = ⊥
⊢ Function.Injective ⇑f.rangeRestrict

Tactic:
by simpa using ker_eq_bot.mp h

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

Goal state before:
pp: V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
⊢ finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction = 1

Tactic:
rw [AffineSubspace.direction_mk']

Goal state after:
V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
⊢ finrank ℝ ↥(ℝ ∙ v) = 1
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
⊢ dimH (Metric.ball x r) = ↑(Fintype.card ι)

Tactic:
← ENNReal.coe_natCast

Goal state after:
case inr
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
⊢ dimH (Metric.ball x r) = ↑↑(Fintype.card ι)
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
hdet : ¬‖((toMatrix bu.toBasis bv.toBasis) f).det‖ = 0
⊢ finrank 𝕜 U = finrank 𝕜 ↥f.range

Tactic:
have h : IsUnit ((f.toMatrix bu.toBasis bv.toBasis).det) := by
      simpa using hdet

Goal state after:
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
hdet : ¬‖((toMatrix bu.toBasis bv.toBasis) f).det‖ = 0
h : IsUnit ((toMatrix bu.toBasis bv.toBasis) f).det
⊢ finrank 𝕜 U = finrank 𝕜 ↥f.range
Module: Mathlib.Analysis.InnerProductSpace.Reproducing

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
this : ∀ {h p1 p2 p3 : Prop}, (h → [p1, p2, p3].TFAE) → [h ∧ p1, h ∧ p2, h ∧ p3].TFAE
hHerm : K.IsHermitian
x✝ : Nontrivial V
v : V
hv : v ≠ 0
h : ∀ (x : X →₀ V →L[𝕜] V) (x_1 : V), 0 ≤ RCLike.re (x.sum fun i a ↦ x.sum fun i_1 a_1 ↦ ⟪(K i i_1) (a_1 x_1), a x_1⟫_𝕜)
ff : X × V →₀ 𝕜
⊢ 0 ≤ RCLike.re (ff.sum fun xv z ↦ ff.sum fun xv' w ↦ (starRingEnd 𝕜) z * w * ⟪(K xv'.1 xv.1) xv.2, xv'.2⟫_𝕜)

Tactic:
rw [Finsupp.sum_comm]
    convert! h (ff.sum fun xv z ↦ .single xv.1 ((z / ‖v‖ ^ 2) • (innerSL 𝕜 v).smulRight xv.2)) v
    simp [Finsupp.sum_sum_index, inner_add_right, inner_add_left, ← smul_assoc, hv]
    simp [inner_smul_left, inner_smul_right, ← mul_assoc, mul_comm]

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

Goal state before:
pp: case inr.refine_2
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
hCd0 : ↑C ^ d ≠ 0
hCd : ↑C ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (fun d ↦ ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → ↑C * x ^ ↑r < R
t : ℕ → Set X
hst : s ⊆ ⋃ n, t n
htδ : ∀ (n : ℕ), ediam (t n) ≤ δ
n : ℕ
⊢ ⨆ (_ : ((fun n ↦ f '' (t n ∩ s)) n).Nonempty), ediam ((fun n ↦ f '' (t n ∩ s)) n) ^ d ≤
    ⨆ (_ : (t n).Nonempty), ↑C ^ d * ediam (t n) ^ (↑r * d)

Tactic:
simp only [iSup_le_iff, image_nonempty]

Goal state after:
case inr.refine_2
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
hCd0 : ↑C ^ d ≠ 0
hCd : ↑C ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (fun d ↦ ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → ↑C * x ^ ↑r < R
t : ℕ → Set X
hst : s ⊆ ⋃ n, t n
htδ : ∀ (n : ℕ), ediam (t n) ≤ δ
n : ℕ
⊢ (t n ∩ s).Nonempty → ediam (f '' (t n ∩ s)) ^ d ≤ ⨆ (_ : (t n).Nonempty), ↑C ^ d * ediam (t n) ^ (↑r * d)
Module: Mathlib.Analysis.InnerProductSpace.Reproducing

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
x y : X
v w : V
⊢ ⟪(kernel (OfKernel K) x y) v, w⟫_𝕜 = ⟪(K x y) v, w⟫_𝕜

Tactic:
simp [kernel, adjoint_inner_left, -inner_kerFun, -kerFun_inner,
    coeCLM, OfKernel.kerFun, inner_H₀_def, RKHS.kerFun]

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

Goal state before:
pp: E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
x : ℝ
⊢ ‖LinearMap.id x‖ * (‖‖v‖‖⁻¹ * ‖v‖) = ‖x‖

Tactic:
norm_norm,

Goal state after:
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
x : ℝ
⊢ ‖LinearMap.id x‖ * (‖v‖⁻¹ * ‖v‖) = ‖x‖
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ ⟪o.rightAngleRotation (φ.symm x), φ.symm y⟫ = ⟪φ (o.rightAngleRotation (φ.symm x)), φ (φ.symm y)⟫

pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ ⟪φ (o.rightAngleRotation (φ.symm x)), φ (φ.symm y)⟫ = ⟪φ (o.rightAngleRotation (φ.symm x)), y⟫

Tactic:
· rw [φ.inner_map_map]

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ ⟪φ (o.rightAngleRotation (φ.symm x)), φ (φ.symm y)⟫ = ⟪φ (o.rightAngleRotation (φ.symm x)), y⟫
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝²⁵ : RCLike 𝕜
inst✝²⁴ : AddCommGroup E
inst✝²³ : Module 𝕜 E
inst✝²² : AddCommGroup F
inst✝²¹ : Module 𝕜 F
inst✝²⁰ : Module ℝ E
inst✝¹⁹ : IsScalarTower ℝ 𝕜 E
inst✝¹⁸ : Module ℝ F
inst✝¹⁷ : IsScalarTower ℝ 𝕜 F
inst✝¹⁶ : TopologicalSpace E
inst✝¹⁵ : IsTopologicalAddGroup E
inst✝¹⁴ : ContinuousSMul 𝕜 E
inst✝¹³ : LocallyConvexSpace ℝ E
inst✝¹² : TopologicalSpace F
inst✝¹¹ : IsTopologicalAddGroup F
inst✝¹⁰ : ContinuousSMul 𝕜 F
inst✝⁹ : LocallyConvexSpace ℝ F
R : Type u_4
V : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : T2Space R
inst✝⁵ : ContinuousAdd R
inst✝⁴ : ContinuousConstSMul R R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : TopologicalSpace V
inst✝ : SeparatingDual R V
x✝¹ x✝ : V
h : (topDualPairing R V).flip x✝¹ = (topDualPairing R V).flip x✝
⊢ x✝¹ = x✝

Tactic:
by
    by_contra hne
    obtain ⟨f, hf⟩ := SeparatingDual.exists_separating_of_ne (R := R) hne
    exact hf (DFunLike.congr_fun h f)

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
⊢ (-↑x).im ≤ π

Tactic:
simpa using pi_nonneg

Goal state after: