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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
hm : n ∣ m
a : ℤ
ha : IsCoprime a ↑m
⊢ ((changeLevel hm) χ) ↑a = χ ↑a

Tactic:
rw [← ZMod.coe_unitOfIsCoprime _ ha, changeLevel_eq_cast_of_dvd _ hm, ZMod.coe_unitOfIsCoprime,
    ZMod.cast_intCast hm]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
hd : d ∣ n
h : (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker
E : (ZMod d)ˣ →* Rˣ := ((ZMod.unitsMap hd).liftOfSurjective ⋯) ⟨toUnitHom χ, h⟩
hE : E.comp (ZMod.unitsMap hd) = toUnitHom χ
⊢ equivToUnitHom χ = (equivToUnitHom (ofUnitHom E)).comp (ZMod.unitsMap hd)

Tactic:
ofUnitHom_eq,

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
hd : d ∣ n
h : (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker
E : (ZMod d)ˣ →* Rˣ := ((ZMod.unitsMap hd).liftOfSurjective ⋯) ⟨toUnitHom χ, h⟩
hE : E.comp (ZMod.unitsMap hd) = toUnitHom χ
⊢ equivToUnitHom χ = (equivToUnitHom (equivToUnitHom.symm E)).comp (ZMod.unitsMap hd)
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
hd : d ∈ χ.conductorSet
⊢ χ = (changeLevel ⋯) ⋯.choose

Tactic:
rw [changeLevel_trans _ (conductor_dvd_level _) hd.dvd,
      ← (factorsThrough_conductor (Classical.choose hd.2)).2.choose_spec]

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
hd : d ∈ χ.conductorSet
⊢ χ = (changeLevel ⋯) (Classical.choose ⋯)
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case refine_1.inl
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
H : χ ↑x = 0
⊢ χ ↑x ^ 2 = 1

pp: case refine_1.inr.inl
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
H : χ ↑x = 1
⊢ χ ↑x ^ 2 = 1

pp: case refine_1.inr.inr
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
H : χ ↑x = -1
⊢ χ ↑x ^ 2 = 1

Tactic:
· exact (not_isUnit_zero <| H ▸ IsUnit.map χ <| x.isUnit).elim

Goal state after:
case refine_1.inr.inl
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
H : χ ↑x = 1
⊢ χ ↑x ^ 2 = 1

case refine_1.inr.inr
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
H : χ ↑x = -1
⊢ χ ↑x ^ 2 = 1
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case refine_1.inr.inr
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
H : χ ↑x = -1
⊢ χ ↑x ^ 2 = 1

Tactic:
simp only [H, even_two, Even.neg_pow, one_pow]

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

Goal state before:
pp: case pos
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ ^ 2 = 1
x : M
hx : IsUnit x
⊢ χ x ^ 2 = 1

Tactic:
← χ.pow_apply' two_ne_zero,

Goal state after:
case pos
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ ^ 2 = 1
x : M
hx : IsUnit x
⊢ (χ ^ 2) x = 1
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
⊢ (χ * ψ).conductor ∣ χ.conductor.lcm ψ.conductor

Tactic:
obtain rfl | hn := eq_zero_or_neZero n
  · simp [conductor_eq_zero_iff_level_eq_zero.mpr]
  have h := Nat.lcm_dvd χ.conductor_dvd_level ψ.conductor_dvd_level
  rw [← mem_conductorSet_iff_conductor_dvd _ h, mem_conductorSet_iff]
  refine ⟨h, χ.primitiveCharacter.mul ψ.primitiveCharacter, ?_⟩
  rw [mul, MonoidHom.map_mul, ← changeLevel_trans, ← changeLevel_trans,
    changeLevel_primitiveCharacter, changeLevel_primitiveCharacter]

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

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F : IntermediateField K L
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ IsCyclotomicExtension {n} K ↥F ↔ F = K⟮ζ⟯

Tactic:
rw [← toSubalgebra_inj, adjoin_simple_toSubalgebra_of_isAlgebraic
    (hζ.isIntegral (NeZero.pos _)).tower_top.isAlgebraic]
  exact _root_.isCyclotomicExtension_singleton_iff_eq_adjoin n F.toSubalgebra hζ

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case i_surj
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ b ∈ univ, ∃ a, ∃ (_ : a ∈ univ), a + x = b

pp: case h
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ a ∈ univ, χ x * φ a * ψ (x + a) = χ x * φ (a + x - x) * ψ (a + x)

Tactic:
· exact fun b _ ↦ ⟨b - x, mem_univ _, by rw [sub_add_cancel]⟩

Goal state after:
case h
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ a ∈ univ, χ x * φ a * ψ (x + a) = χ x * φ (a + x - x) * ψ (a + x)
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
this : ContinuousAt (fun x ↦ p * ‖x‖ ^ (p - 1)) 0
⊢ Filter.Tendsto (fun x ↦ p * ‖x‖ ^ (p - 1)) (𝓝 0) (𝓝 0)

Tactic:
by
      simpa [ContinuousAt, sub_ne_zero_of_ne hp.ne'] using this

Goal state after:
Module: Mathlib.Analysis.Hofer

Goal state before:
pp: X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'
this : Nonempty X
F : ℕ → X → X
hF : ∀ (k : ℕ) (x' : X), d x' x ≤ 2 * ε ∧ 2 ^ k * ϕ x ≤ ϕ x' → d x' (F k x') ≤ ε / 2 ^ k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun n ↦ Nat.recOn n x F
hu :
  ∀ (n : ℕ), d (u n) x ≤ 2 * ε ∧ 2 ^ n * ϕ x ≤ ϕ (u n) → d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / 2 ^ x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
y : X
limy : Tendsto u atTop (𝓝 y)
⊢ False

Tactic:
have lim_top : Tendsto (ϕ ∘ u) atTop atTop := by
    let v n := (ϕ ∘ u) (n + 1)
    suffices Tendsto v atTop atTop by rwa [tendsto_add_atTop_iff_nat] at this
    have hv₀ : 0 < v 0 := by
      calc
        0 ≤ 2 * ϕ (u 0) := by specialize nonneg x; positivity
        _ < ϕ (u (0 + 1)) := key₂ 0
    apply tendsto_atTop_of_geom_le hv₀ one_lt_two
    exact fun n => (key₂ (n + 1)).le

Goal state after:
X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'
this : Nonempty X
F : ℕ → X → X
hF : ∀ (k : ℕ) (x' : X), d x' x ≤ 2 * ε ∧ 2 ^ k * ϕ x ≤ ϕ x' → d x' (F k x') ≤ ε / 2 ^ k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun n ↦ Nat.recOn n x F
hu :
  ∀ (n : ℕ), d (u n) x ≤ 2 * ε ∧ 2 ^ n * ϕ x ≤ ϕ (u n) → d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / 2 ^ x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
y : X
limy : Tendsto u atTop (𝓝 y)
lim_top : Tendsto (ϕ ∘ u) atTop atTop
⊢ False
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)
⊢ ∫⁻ (t : A i), f (X t) ^ (1 - ↑(#s) * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p ∂μ i ≤
    (∫⋯∫⁻_{i}, f ∂μ) x ^ (1 - (↑(#s) - 1) * p) * ∏ x_1 ∈ s, (∫⋯∫⁻_{x_1}, ∫⋯∫⁻_{i}, f ∂μ ∂μ) x ^ p

Tactic:
have hF₀ : Measurable fun t ↦ f (X t) := hf.comp <| measurable_update _

Goal state after:
ι : 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)
⊢ ∫⁻ (t : A i), f (X t) ^ (1 - ↑(#s) * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p ∂μ i ≤
    (∫⋯∫⁻_{i}, f ∂μ) x ^ (1 - (↑(#s) - 1) * p) * ∏ x_1 ∈ s, (∫⋯∫⁻_{x_1}, ∫⋯∫⁻_{i}, f ∂μ ∂μ) x ^ p
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
⊢ ∀ (t : A i), (∫⋯∫⁻_{i}, f ∂μ) (X t) = (∫⋯∫⁻_{i}, f ∂μ) x

Tactic:
intro t

Goal state after:
ι : 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
t : A i
⊢ (∫⋯∫⁻_{i}, f ∂μ) (X t) = (∫⋯∫⁻_{i}, f ∂μ) x
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✝ : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
a : Fin (Module.finrank 𝕜 E) → E := fun i ↦ ↑√(⋯.eigenvalues ⋯ i) • (⋯.eigenvectorBasis ⋯) i
x✝ : E
⊢ T x✝ = ∑ i, ⟪a i, x✝⟫ • a i

Tactic:
a,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
a : Fin (Module.finrank 𝕜 E) → E := fun i ↦ ↑√(⋯.eigenvalues ⋯ i) • (⋯.eigenvectorBasis ⋯) i
x✝ : E
⊢ T x✝ = ∑ x, ⟪↑√(⋯.eigenvalues ⋯ x) • (⋯.eigenvectorBasis ⋯) x, x✝⟫ • ↑√(⋯.eigenvalues ⋯ x) • (⋯.eigenvectorBasis ⋯) x
Module: Mathlib.Analysis.InnerProductSpace.SingularValues

Goal state before:
pp: case mp
𝕜 : 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
T : E →ₗ[𝕜] F
this : (adjoint T ∘ₗ T).ker = ⊥ ↔ ¬End.HasEigenvalue (adjoint T ∘ₗ T) 0
h : End.HasEigenvalue (adjoint T ∘ₗ T) 0
⊢ ∃ i < finrank 𝕜 E, T.singularValues i ≤ 0

Tactic:
obtain ⟨i, hi⟩ := T.isSymmetric_adjoint_comp_self.exists_eigenvalues_eq rfl h

Goal state after:
case mp
𝕜 : 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
T : E →ₗ[𝕜] F
this : (adjoint T ∘ₗ T).ker = ⊥ ↔ ¬End.HasEigenvalue (adjoint T ∘ₗ T) 0
h : End.HasEigenvalue (adjoint T ∘ₗ T) 0
i : Fin (finrank 𝕜 E)
hi : ↑(⋯.eigenvalues ⋯ i) = 0
⊢ ∃ i < finrank 𝕜 E, T.singularValues i ≤ 0
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ‖f‖ ^ 2 • @Matrix.gram E (Fin n) 𝕜 inst✝⁶.toInner e - @Matrix.gram F (Fin n) 𝕜 inst✝⁴.toInner (⇑f ∘ e) =
    ∑ i, Matrix.vecMulVec (A i) (star (A i))
⊢ ‖(LinearMap.rTensor G ↑f) x‖ ≤ ‖f‖ * ‖x‖

Tactic:
apply (sq_le_sq₀ (norm_nonneg _) (by positivity)).mp

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ‖f‖ ^ 2 • @Matrix.gram E (Fin n) 𝕜 inst✝⁶.toInner e - @Matrix.gram F (Fin n) 𝕜 inst✝⁴.toInner (⇑f ∘ e) =
    ∑ i, Matrix.vecMulVec (A i) (star (A i))
⊢ ‖(LinearMap.rTensor G ↑f) x‖ ^ 2 ≤ (‖f‖ * ‖x‖) ^ 2
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ∀ (i j : Fin n),
    ‖f‖ ^ 2 • inner 𝕜 (e i) (e j) - (∑ i, Matrix.vecMulVec (A i) (star (A i))) i j = inner 𝕜 (f (e i)) (f (e j))
⊢ ‖∑ x, (LinearMap.rTensor G ↑f) (e x ⊗ₜ[𝕜] g x)‖ ^ 2 ≤ ‖f‖ ^ 2 * ‖∑ j, e j ⊗ₜ[𝕜] g j‖ ^ 2

Tactic:
LinearMap.rTensor_tmul,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ∀ (i j : Fin n),
    ‖f‖ ^ 2 • inner 𝕜 (e i) (e j) - (∑ i, Matrix.vecMulVec (A i) (star (A i))) i j = inner 𝕜 (f (e i)) (f (e j))
⊢ ‖∑ x, ↑f (e x) ⊗ₜ[𝕜] g x‖ ^ 2 ≤ ‖f‖ ^ 2 * ‖∑ j, e j ⊗ₜ[𝕜] g j‖ ^ 2
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : FiniteDimensional ℝ F
u : E → F
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < ↑(finrank ℝ E)
hpq : ↑p⁻¹ - (↑(finrank ℝ E))⁻¹ ≤ (↑q)⁻¹
hs : Bornology.IsBounded s
hq0 : ¬q = 0
p' : ℝ≥0 := (p⁻¹ - (↑(finrank ℝ E))⁻¹)⁻¹
hp' : ↑p'⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
H : (↑p')⁻¹ ≤ (↑q)⁻¹
⊢ ↑q ≤ ↑p'

Tactic:
norm_cast at H ⊢

Goal state after:
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : FiniteDimensional ℝ F
u : E → F
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < ↑(finrank ℝ E)
hpq : ↑p⁻¹ - (↑(finrank ℝ E))⁻¹ ≤ (↑q)⁻¹
hs : Bornology.IsBounded s
hq0 : ¬q = 0
p' : ℝ≥0 := (p⁻¹ - (↑(finrank ℝ E))⁻¹)⁻¹
hp' : ↑p'⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
H : p'⁻¹ ≤ q⁻¹
⊢ q ≤ p'
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq : {0} = parallelepiped ⇑basis
h✝ : volume = volume.addHaarScalarFactor μH[↑0] • μH[↑0]
h : (volume.addHaarScalarFactor μH[↑0] • μH[↑0]) {0} = volume {0}
⊢ μHE[0] = μH[0]

Tactic:
conv_rhs at h => rw [heq, OrthonormalBasis.volume_parallelepiped]

Goal state after:
X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq : {0} = parallelepiped ⇑basis
h✝ : volume = volume.addHaarScalarFactor μH[↑0] • μH[↑0]
h : (volume.addHaarScalarFactor μH[↑0] • μH[↑0]) {0} = 1
⊢ μHE[0] = μH[0]
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case refine_2
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
⊢ dimH s ≤ ⨆ x, limsup dimH (𝓝[s] x).smallSets

Tactic:
· rw [← bsupr_limsup_dimH]; exact iSup₂_le_iSup _ _

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

Goal state before:
pp: case neg
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
htr : ¬∀ (n : ℕ), ediam (t n) ≤ r
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)) =
    ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n))

Tactic:
· rw [iInf_eq_if, if_neg htr]
    push Not at htr; rcases htr with ⟨n, hn⟩
    refine ENNReal.tsum_eq_top_of_eq_top ⟨n, ?_⟩
    rw [iSup_eq_if, if_pos, iInf_eq_if, if_neg]
    · exact hn.not_ge
    rcases ediam_pos_iff.1 hn.pos with ⟨x, hx, -⟩
    exact ⟨x, hx⟩

Goal state after:
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
H : Type u_4
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : RKHS 𝕜 H X V
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace V
x y : X
⊢ kernel H x y = adjoint (kerFun H x) ∘SL kerFun H y

Tactic:
by
  simp [kerFun, kernel]

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

Goal state before:
pp: case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
⊢ ∀ (i : ℕ → Set X), {x} ⊆ ⋃ n, i n → (∀ (n : ℕ), ediam (i n) ≤ 1) → 1 ≤ ∑' (n : ℕ), ⨆ (_ : (i n).Nonempty), 1

Tactic:
intro t

Goal state after:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
t : ℕ → Set X
⊢ {x} ⊆ ⋃ n, t n → (∀ (n : ℕ), ediam (t n) ≤ 1) → 1 ≤ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), 1
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case neg
U : Type u_5
V : Type u_6
inst✝⁸ : NormedAddCommGroup U
inst✝⁷ : InnerProductSpace ℝ U
inst✝⁶ : FiniteDimensional ℝ U
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MeasurableSpace U
inst✝² : BorelSpace U
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : U →ₗ[ℝ] V
s : Set U
h : ¬f.ker = ⊥
⊢ μH[↑(finrank ℝ U)] (⇑f '' s) = ENNReal.ofReal f.normDet * μH[↑(finrank ℝ U)] s

Tactic:
suffices μH[finrank ℝ U] (f.range.subtypeₗᵢ '' (f.rangeRestrict '' s)) = 0 by
      simpa [(f.normDet_eq_zero_tfae.out 1 0).mp h, Set.image_image]
    rw [(LinearIsometry.isometry _).hausdorffMeasure_image (by simp)]
    have h : (finrank ℝ f.range : ℝ) < finrank ℝ U := by
      exact_mod_cast (f.normDet_eq_zero_tfae.out 1 3).mp h
    simp [Real.hausdorffMeasure_of_finrank_lt h]

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

Goal state before:
pp: H : Type u_1
inst✝¹ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S T : ClosedSubmodule ℝ H
⊢ (S ⊓ T).symplComp = S.symplComp ⊔ T.symplComp

Tactic:
by
  rw [symplComp, symplComp, symplComp, mulI_inf]
  exact Eq.symm (sup_orthogonal S.mulI T.mulI)

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

Goal state before:
pp: ι : Type u_4
inst✝ : Fintype ι
⊢ μH[↑(Fintype.card ι)] = volume

Tactic:
refine (pi_eq_generateFrom (fun _ => Real.borel_eq_generateFrom_Ioo_rat.symm)
    (fun _ => Real.isPiSystem_Ioo_rat) (fun _ => Real.finiteSpanningSetsInIooRat _) ?_).symm

Goal state after:
ι : Type u_4
inst✝ : Fintype ι
⊢ ∀ (s : ι → Set ℝ),
    (∀ (i : ι), s i ∈ ⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b}) → μH[↑(Fintype.card ι)] (univ.pi s) = ∏ i, volume (s i)
Module: Mathlib.Analysis.LocallyConvex.StrongTopology

Goal state before:
pp: R : Type u_1
𝕜₁ : Type u_2
𝕜₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : TopologicalSpace E
inst✝¹² : AddCommGroup F
inst✝¹¹ : TopologicalSpace F
inst✝¹⁰ : IsTopologicalAddGroup F
inst✝⁹ : Semiring R
inst✝⁸ : PartialOrder R
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
inst✝³ : Module R F
inst✝² : ContinuousConstSMul R F
inst✝¹ : LocallyConvexSpace R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) 𝔖
⊢ LocallyConvexSpace R (E →SLᵤ[σ, 𝔖] F)

Tactic:
apply LocallyConvexSpace.ofBasisZero _ _ _ _
    (UniformConvergenceCLM.hasBasis_nhds_zero_of_basis _ _ _ h𝔖₁ h𝔖₂
      (LocallyConvexSpace.convex_basis_zero R F)) _
  rintro ⟨S, V⟩ ⟨_, _, hVconvex⟩ f hf g hg a b ha hb hab x hx
  exact hVconvex (hf x hx) (hg x hx) ha hb hab

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

Goal state before:
pp: case e'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x y : E
⊢ (map (Fin 2) φ.toLinearEquiv) o = o

Tactic:
← o.map_eq_iff_det_pos φ.toLinearEquiv

Goal state after:
case e'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : (map (Fin 2) φ.toLinearEquiv) o = o
x y : E
⊢ (map (Fin 2) φ.toLinearEquiv) o = o

case e'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x y : E
⊢ Fintype.card (Fin 2) = finrank ℝ E