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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
⊢ (X ^ n - 1).coeff 0 = -(cyclotomic n R).coeff 0

Tactic:
← prod_cyclotomic_eq_X_pow_sub_one (zero_le_one.trans_lt hn),

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
⊢ (∏ i ∈ n.divisors, cyclotomic i R).coeff 0 = -(cyclotomic n R).coeff 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
⊢ (algebraMap R K) x ^ n - (algebraMap R K) y ^ n =
    ∏ x_1 ∈ nthRootsFinset n 1, ((algebraMap R K) x - (algebraMap R K) x_1 * (algebraMap R K) y)

Tactic:
h'.pow_sub_pow_eq_prod_sub_mul_field _ _ hpos

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
⊢ ∏ ζ ∈ nthRootsFinset n 1, ((algebraMap R K) x - ζ * (algebraMap R K) y) =
    ∏ x_1 ∈ nthRootsFinset n 1, ((algebraMap R K) x - (algebraMap R K) x_1 * (algebraMap R K) y)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x✝ y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
a : K
ha : a ∈ ↑(nthRootsFinset n 1)
this : ∀ b ∈ ↑(nthRootsFinset n 1), ∃ a, ∃ (_ : a ∈ ↑(nthRootsFinset n 1)), b = (algebraMap R K) a
x : R
hx : x ∈ ↑(nthRootsFinset n 1)
hx1 : a = (algebraMap R K) x
⊢ a ∈ ⇑(algebraMap R K) '' ↑(nthRootsFinset n 1)

Tactic:
exact ⟨x, hx, hx1.symm⟩

Goal state after:
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: K : Type u_1
S : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing S
inst✝⁴ : Algebra K S
R : Type u_3
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K S
B B' : PowerBasis K S
P : R[X]
h : (aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
⊢ ∀ (i : Fin B.dim) (j : Fin B'.dim), IsIntegral R (B.basis.toMatrix (⇑B'.basis) i j)

Tactic:
by
  intro i j
  rw [B.basis.toMatrix_apply, B'.coe_basis]
  refine repr_pow_isIntegral hB (fun i => ?_) hmin _ _
  rw [← h, aeval_eq_sum_range, map_sum, Finset.sum_apply']
  refine IsIntegral.sum _ fun n _ => ?_
  rw [Algebra.smul_def, IsScalarTower.algebraMap_apply R K S, ← Algebra.smul_def, map_smul,
    algebraMap_smul]
  exact (repr_gen_pow_isIntegral hB hmin _ _).smul _

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : ∑ i ∈ range n, x ^ i < 0
⊢ eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) ≤ 0

Tactic:
geom_sum_neg_iff hn'.ne'

Goal state after:
case hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
⊢ eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) ≤ 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) * cyclotomic n (ZMod p) =
    (expand (ZMod p) p) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))

Tactic:
rw [← map_expand, cyclotomic_expand_eq_cyclotomic_mul hp.out hn, Polynomial.map_mul,
    map_cyclotomic, map_cyclotomic]

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

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
⊢ IsCyclotomicExtension (S ∪ {n}) A B

Tactic:
by
  refine (iff_adjoin_eq_top _ A _).2 ⟨fun s hs hs' ↦ ?_, ?_⟩
  · rw [mem_union, mem_singleton_iff] at hs
    obtain hs | rfl := hs
    · exact H.exists_isPrimitiveRoot hs hs'
    · obtain ⟨m, hm, hm', ⟨x, rfl⟩⟩ := h
      obtain ⟨ζ, hζ⟩ := H.exists_isPrimitiveRoot hm hm'
      refine ⟨ζ ^ x, ?_⟩
      have h_xnz : x ≠ 0 := Nat.ne_zero_of_mul_ne_zero_right hm'
      have := hζ.pow_of_dvd h_xnz (dvd_mul_left x s)
      rwa [mul_div_cancel_right₀ _ h_xnz] at this
  · refine _root_.eq_top_iff.2 ?_
    rw [← ((iff_adjoin_eq_top S A B).1 H).2]
    refine adjoin_mono fun x hx ↦ ?_
    simp only [union_singleton, mem_insert_iff, mem_ofPred_eq] at hx ⊢
    obtain ⟨m, hm, hm'⟩ := hx
    exact ⟨m, ⟨Or.inr hm, hm'⟩⟩

Goal state after:
Module: Mathlib.FieldTheory.Finite.Trace

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Finite L
inst✝ : Algebra K L
x : L
this✝ : Finite K
this : Fintype K
⊢ ∏ σ, σ x = ∏ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i

Tactic:
Finset.prod_range

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Finite L
inst✝ : Algebra K L
x : L
this✝ : Finite K
this : Fintype K
⊢ ∏ σ, σ x = ∏ i, x ^ Nat.card K ^ ↑i
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n : ℕ
K : Type u_1
K' : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field K'
inst✝³ : Fintype K
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
⊢ CharP K p

Tactic:
← Algebra.charP_iff (ZMod p) K p

Goal state after:
p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n : ℕ
K : Type u_1
K' : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field K'
inst✝³ : Fintype K
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
⊢ CharP (ZMod p) p
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
inst✝ : IsCyclotomicExtension {n} K L
⊢ adjoin K ((cyclotomic n K).rootSet L) = ⊤

Tactic:
rw [← ((iff_adjoin_eq_top {n} K L).1 inferInstance).2]
      let := Classical.decEq L
      obtain ⟨ζ : L, hζ⟩ :=
        IsCyclotomicExtension.exists_isPrimitiveRoot K L (mem_singleton n) (NeZero.ne _)
      exact adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
hd : d ∣ n
x✝ : χ.FactorsThrough d
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap hd).ker
w✝ : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel w✝) χ₀
⊢ (toUnitHom χ) x = 1

Tactic:
hχ₀,

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
hd : d ∣ n
x✝ : χ.FactorsThrough d
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap hd).ker
w✝ : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel w✝) χ₀
⊢ (toUnitHom ((changeLevel w✝) χ₀)) x = 1
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: case inr
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
ζ : Rˣ
hζ₁ : ↑ζ ^ n = ↑1
hζ₂ : ↑ζ = χ a
k : ℕ
left✝ : k < n
hk : μ ^ k = ↑ζ
⊢ χ a ∈ ℤ[μ]

Tactic:
exact hζ₂ ▸ hk ▸ Subalgebra.pow_mem _ (Algebra.self_mem_adjoin_singleton ℤ μ) k

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

Goal state before:
pp: S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension S A ↥C₁
h₂ : IsCyclotomicExtension S A ↥C₂
⊢ C₁ = C₂

Tactic:
have hC (n) (hn₁ : n ∈ S) (hn₂ : n ≠ 0) : ∃ x : B, IsPrimitiveRoot x n := by
    obtain ⟨ζ, hζ⟩ := h₁.1 hn₁ hn₂
    exact ⟨ζ, IsPrimitiveRoot.coe_submonoidClass_iff.mpr hζ⟩
  rw [(isCyclotomicExtension_iff_eq_adjoin S C₁ hC).mp h₁,
    (isCyclotomicExtension_iff_eq_adjoin S C₂ hC).mp h₂]

Goal state after:
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
hx : x = 0
h2p : 0 < p - 1
⊢ Filter.Tendsto (fun x ↦ ‖x‖ ^ (p - 1)) (𝓝 0) (𝓝 0)

Tactic:
convert! continuousAt_id.norm.rpow_const (.inr h2p.le) |>.tendsto

Goal state after:
case e'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ 0 = ‖id 0‖ ^ (p - 1)
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s : Multiset α
a : α
⊢ s ⋖ a ::ₘ s

Tactic:
exact covBy_cons _ _

Goal state after:
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 c : P
t₁ t₂ : ℝ
h_inner : ⟪b -ᵥ a, c -ᵥ a⟫ = 0
hvec : (AffineMap.lineMap a b) t₁ -ᵥ (AffineMap.lineMap a c) t₂ = t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a)
⊢ dist ((AffineMap.lineMap a b) t₁) ((AffineMap.lineMap a c) t₂) ^ 2 = t₁ ^ 2 * dist a b ^ 2 + t₂ ^ 2 * dist a c ^ 2

Tactic:
rw [dist_eq_norm_vsub V, hvec, norm_sub_sq_real, norm_smul, norm_smul,
      Real.norm_eq_abs, Real.norm_eq_abs, inner_smul_left, inner_smul_right, h_inner]

Goal state after:
V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
t₁ t₂ : ℝ
h_inner : ⟪b -ᵥ a, c -ᵥ a⟫ = 0
hvec : (AffineMap.lineMap a b) t₁ -ᵥ (AffineMap.lineMap a c) t₂ = t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a)
⊢ (|t₁| * ‖b -ᵥ a‖) ^ 2 - 2 * ((starRingEnd ℝ) t₁ * (t₂ * 0)) + (|t₂| * ‖c -ᵥ a‖) ^ 2 =
    t₁ ^ 2 * dist a b ^ 2 + t₂ ^ 2 * dist a c ^ 2
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
⊢ (∫⋯∫⁻_{i}, f ∂μ) x ^ p * ((∫⋯∫⁻_{i}, f ∂μ) x ^ (1 - k * p) * ∏ j ∈ s, (∫⋯∫⁻_{i, j}, f ∂μ) x ^ p) =
    (∫⋯∫⁻_{i}, f ∂μ) x ^ (p + (1 - k * p)) * ∏ j ∈ s, (∫⋯∫⁻_{i, j}, f ∂μ) x ^ p

Tactic:
ENNReal.rpow_add_of_nonneg

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
⊢ (∫⋯∫⁻_{i}, f ∂μ) x ^ p * ((∫⋯∫⁻_{i}, f ∂μ) x ^ (1 - k * p) * ∏ j ∈ s, (∫⋯∫⁻_{i, j}, f ∂μ) x ^ p) =
    (∫⋯∫⁻_{i}, f ∂μ) x ^ p * (∫⋯∫⁻_{i}, f ∂μ) x ^ (1 - k * p) * ∏ j ∈ s, (∫⋯∫⁻_{i, j}, f ∂μ) x ^ p

case hy
ι : 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
⊢ 0 ≤ p

case hz
ι : 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
⊢ 0 ≤ 1 - k * p
Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram

Goal state before:
pp: V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖
⊢ ∀ (x : V), ‖x‖ ≤ ↑C⁻¹.toNNReal * ‖(continuousLinearMapOfBilin B) x‖

Tactic:
Real.coe_toNNReal',

Goal state after:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖
⊢ ∀ (x : V), ‖x‖ ≤ max C⁻¹ 0 * ‖(continuousLinearMapOfBilin B) x‖
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: case pos
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ f.graph ≤ f.closure.graph

Tactic:
← hf.graph_closure_eq_closure_graph

Goal state after:
case pos
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ f.graph ≤ f.graph.topologicalClosure
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ IsClosed[instTopologicalSpaceProd] ↑f.closure.graph

Tactic:
← hf.graph_closure_eq_closure_graph

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ IsClosed[instTopologicalSpaceProd] ↑f.graph.topologicalClosure
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
hcf : f.closure.toFun.ker = ⊥
⊢ f.inverse.closure = f.closure.inverse

Tactic:
by
  apply eq_of_eq_graph
  rw [closure_inverse_graph hf hf' hcf,
    ((inverse_isClosable_iff hf hf').mpr hcf).graph_closure_eq_closure_graph]

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

Goal state before:
pp: case h'
𝕜 : 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
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
x : F
y : x ∈ ((↑A).toPMap p)†.domain
hxy : x ∈ ((↑(adjoint A)).toPMap ⊤).domain
⊢ ↑((↑A).toPMap p)† ⟨x, y⟩ = ↑((↑(adjoint A)).toPMap ⊤) ⟨x, hxy⟩

Tactic:
refine LinearPMap.adjoint_apply_eq hp _ fun v => ?_

Goal state after:
case h'
𝕜 : 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
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
x : F
y : x ∈ ((↑A).toPMap p)†.domain
hxy : x ∈ ((↑(adjoint A)).toPMap ⊤).domain
v : ↥((↑A).toPMap p).domain
⊢ ⟪↑((↑(adjoint A)).toPMap ⊤) ⟨x, hxy⟩, ↑v⟫ = ⟪↑⟨x, y⟩, ↑((↑A).toPMap p) v⟫
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: case h'
𝕜 : 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
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
x : F
y : x ∈ ((↑A).toPMap p)†.domain
hxy : x ∈ ((↑(adjoint A)).toPMap ⊤).domain
v : ↥((↑A).toPMap p).domain
⊢ ⟪↑((↑(adjoint A)).toPMap ⊤) ⟨x, hxy⟩, ↑v⟫ = ⟪↑⟨x, y⟩, ↑((↑A).toPMap p) v⟫

Tactic:
simp only [adjoint_inner_left, LinearMap.toPMap_apply, coe_coe]

Goal state after:
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 p' : ℝ≥0
hp✝ : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
q : ℝ := (↑p).conjExponent
hq : (↑p).HolderConjugate q
h0p : p ≠ 0
h1p : ↑p ≠ 1
h3p : ↑p - 1 ≠ 0
h2q : 1 / ↑n' - 1 / q = 1 / ↑p'
γ : ℝ≥0 := NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯
h0γ : ↑γ = ↑p * (↑n - 1) / (↑n - ↑p)
h1γ : 1 < ↑γ
h2γ : γ * n' = p'
h3γ : (↑γ - 1) * q = ↑p'
h4γ : ↑γ ≠ 0
h3u : ¬∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ = 0
h4u : ∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ ≠ ∞
h5u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ 0
h6u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ ∞
h7u : Continuous u
v : E → ℝ := fun x ↦ ‖u x‖ ^ ↑γ
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
C : ℝ≥0 := eLpNormLESNormFDerivOneConst μ ↑n'
this :
  (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / ↑n') ≤
    ↑C * ↑γ * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p) * (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q)
⊢ ↑C * (↑p * (↑n - 1) / (↑n - ↑p)) = ↑C * ↑(↑p * (↑n - 1) / (↑n - ↑p)).toNNReal

Tactic:
Real.coe_toNNReal',

Goal state after:
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 p' : ℝ≥0
hp✝ : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
q : ℝ := (↑p).conjExponent
hq : (↑p).HolderConjugate q
h0p : p ≠ 0
h1p : ↑p ≠ 1
h3p : ↑p - 1 ≠ 0
h2q : 1 / ↑n' - 1 / q = 1 / ↑p'
γ : ℝ≥0 := NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯
h0γ : ↑γ = ↑p * (↑n - 1) / (↑n - ↑p)
h1γ : 1 < ↑γ
h2γ : γ * n' = p'
h3γ : (↑γ - 1) * q = ↑p'
h4γ : ↑γ ≠ 0
h3u : ¬∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ = 0
h4u : ∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ ≠ ∞
h5u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ 0
h6u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ ∞
h7u : Continuous u
v : E → ℝ := fun x ↦ ‖u x‖ ^ ↑γ
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
C : ℝ≥0 := eLpNormLESNormFDerivOneConst μ ↑n'
this :
  (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / ↑n') ≤
    ↑C * ↑γ * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p) * (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q)
⊢ ↑C * (↑p * (↑n - 1) / (↑n - ↑p)) = ↑C * max (↑p * (↑n - 1) / (↑n - ↑p)) 0
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case neg
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_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ∞
⊢ ∀ (a : ℕ), ∑' (k : ℕ), μ (S (2 * k + 1 + a) \ S (2 * k + a)) ≠ ∞

Tactic:
refine fun r => ne_top_of_le_ne_top htop ?_

Goal state after:
case neg
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_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ∞
r : ℕ
⊢ ∑' (k : ℕ), μ (S (2 * k + 1 + r) \ S (2 * k + r)) ≤ μ (s \ t)
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: 𝕜 : Type u_3
V : Type u_4
P : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedSpace 𝕜 V
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : BorelSpace P
d : ℕ
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ ‖c‖₊ ^ ↑d • volume.addHaarScalarFactor μH[↑d] • μH[↑d] s = ‖c‖₊ ^ d • volume.addHaarScalarFactor μH[↑d] • μH[↑d] s

Tactic:
NNReal.rpow_natCast

Goal state after:
𝕜 : Type u_3
V : Type u_4
P : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedSpace 𝕜 V
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : BorelSpace P
d : ℕ
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ ‖c‖₊ ^ d • volume.addHaarScalarFactor μH[↑d] • μH[↑d] s = ‖c‖₊ ^ d • volume.addHaarScalarFactor μH[↑d] • μH[↑d] s
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: 𝕜 : Type u_3
V : Type u_4
P : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedSpace 𝕜 V
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : BorelSpace P
d : ℕ
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ ‖c‖₊⁻¹ ^ ↑d • volume.addHaarScalarFactor μH[↑d] • μH[↑d] s = ‖c‖₊⁻¹ ^ d • volume.addHaarScalarFactor μH[↑d] • μH[↑d] s

Tactic:
NNReal.rpow_natCast

Goal state after:
𝕜 : Type u_3
V : Type u_4
P : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedSpace 𝕜 V
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : BorelSpace P
d : ℕ
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ ‖c‖₊⁻¹ ^ d • volume.addHaarScalarFactor μH[↑d] • μH[↑d] s = ‖c‖₊⁻¹ ^ d • volume.addHaarScalarFactor μH[↑d] • μH[↑d] s