mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: case refine_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
hprime : Prime p
hind : IsPrimitiveRoot μ n✝ → a.Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ a)
h : IsPrimitiveRoot μ n✝
hcop : (p * a).Coprime n✝
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ (p * a))

Tactic:
rw [hind h (Nat.Coprime.coprime_mul_left hcop)]

Goal state after:
case refine_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
hprime : Prime p
hind : IsPrimitiveRoot μ n✝ → a.Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ a)
h : IsPrimitiveRoot μ n✝
hcop : (p * a).Coprime n✝
⊢ minpoly ℤ (μ ^ a) = minpoly ℤ (μ ^ (p * a))
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
⊢ { val := (cyclotomic n R).roots, nodup := ⋯ } = primitiveRoots n R

Tactic:
ext a
  simp [cyclotomic_ne_zero n R, ← isRoot_cyclotomic_iff, mem_primitiveRoots,
    NeZero.pos_of_neZero_natCast R]

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

Goal state before:
pp: K : Type u_2
inst✝⁴ : Field K
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
μ : R
n : ℕ
inst✝¹ : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (cyclotomic n K)
inst✝ : NeZero ↑n
this : NeZero ↑n
⊢ eval₂ (algebraMap K R) μ (cyclotomic n K) = 0

Tactic:
eval₂_eq_eval_map,

Goal state after:
K : Type u_2
inst✝⁴ : Field K
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
μ : R
n : ℕ
inst✝¹ : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (cyclotomic n K)
inst✝ : NeZero ↑n
this : NeZero ↑n
⊢ eval μ (map (algebraMap K R) (cyclotomic n K)) = 0
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝⁶ : NeZero n
A : Type w
B : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : IsCyclotomicExtension {n} A B
inst✝¹ : IsDomain B
inst✝ : NeZero ↑n
⊢ eval (zeta n A B) (cyclotomic n B) = 0 ↔ eval₂ (algebraMap A B) (zeta n A B) (cyclotomic n A) = 0

Tactic:
eval₂_eq_eval_map,

Goal state after:
n : ℕ
inst✝⁶ : NeZero n
A : Type w
B : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : IsCyclotomicExtension {n} A B
inst✝¹ : IsDomain B
inst✝ : NeZero ↑n
⊢ eval (zeta n A B) (cyclotomic n B) = 0 ↔ eval (zeta n A B) (Polynomial.map (algebraMap A B) (cyclotomic n A)) = 0
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: p n : ℕ
inst✝⁹ : NeZero n
A : Type w
B : Type z
K : Type u
L : Type v
C : Type w
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsCyclotomicExtension {n} A B
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ PowerBasis K L

Tactic:
apply PowerBasis.ofAdjoinEqTop (((integral {n} K L).isIntegral ζ).sub isIntegral_one)
  exact PowerBasis.adjoin_eq_top_of_gen_mem_adjoin (hζ.powerBasis_gen_mem_adjoin_zeta_sub_one _)

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

Goal state before:
pp: case mk
p n : ℕ
inst✝¹² : NeZero n
A : Type w
B : Type z
K : Type u
L : Type v
C✝ : Type w
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsCyclotomicExtension {n} A B
inst✝⁷ : Field K
inst✝⁶ : CommRing L
inst✝⁵ : IsDomain L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
C : Type u_1
inst✝² : CommRing C
inst✝¹ : IsDomain C
inst✝ : Algebra K C
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
hn : NeZero ↑n
val✝ : C
property✝ : val✝ ∈ primitiveRoots n C
⊢ eval₂ (algebraMap K C) (↑⟨val✝, property✝⟩) (minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen) = 0

Tactic:
eval₂_eq_eval_map,

Goal state after:
case mk
p n : ℕ
inst✝¹² : NeZero n
A : Type w
B : Type z
K : Type u
L : Type v
C✝ : Type w
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsCyclotomicExtension {n} A B
inst✝⁷ : Field K
inst✝⁶ : CommRing L
inst✝⁵ : IsDomain L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
C : Type u_1
inst✝² : CommRing C
inst✝¹ : IsDomain C
inst✝ : Algebra K C
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
hn : NeZero ↑n
val✝ : C
property✝ : val✝ ∈ primitiveRoots n C
⊢ eval (↑⟨val✝, property✝⟩) (Polynomial.map (algebraMap K C) (minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen)) = 0
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
⊢ IsCyclotomicExtension S A B = IsCyclotomicExtension (S \ {0}) A B

Tactic:
by
  simp [isCyclotomicExtension_iff, and_assoc]

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

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl : l ≠ 0
⊢ l ∣ 2 * n

Tactic:
have hl : NeZero l := ⟨hl⟩

Goal state after:
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
⊢ l ∣ 2 * n
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝¹ : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝ : FiniteDimensional K L := finiteDimensional {n} K L
this : IsGalois K L := isGalois {n} K L
Hprod : ∏ σ, (1 - σ ζ) = eval 1 (cyclotomic' n E)
⊢ ∏ x, (1 - x ζ) = (algebraMap K E) ↑(eval 1 (cyclotomic n ℤ))

Tactic:
have : NeZero (n : E) := NeZero.of_faithfulSMul K _ n

Goal state after:
n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝² : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝¹ : FiniteDimensional K L := finiteDimensional {n} K L
this✝ : IsGalois K L := isGalois {n} K L
Hprod : ∏ σ, (1 - σ ζ) = eval 1 (cyclotomic' n E)
this : NeZero ↑n
⊢ ∏ x, (1 - x ζ) = (algebraMap K E) ↑(eval 1 (cyclotomic n ℤ))
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
this : Algebra.IsIntegral K L
h : (IntermediateField.adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}).toSubalgebra = ⊤.toSubalgebra
⊢ Algebra.IsSeparable K L

Tactic:
← AlgEquiv.Algebra.isSeparable_iff <|
    (IntermediateField.equivOfEq (IntermediateField.toSubalgebra_injective h)).trans
      IntermediateField.topEquiv,

Goal state after:
S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
this : Algebra.IsIntegral K L
h : (IntermediateField.adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}).toSubalgebra = ⊤.toSubalgebra
⊢ Algebra.IsSeparable K ↥(IntermediateField.adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : ψ b ≠ 1
h₁ : ψ b * ∑ i, ψ i = ∑ a, ψ a
h₂ : ∑ a, ψ a = Finset.univ.sum ⇑ψ
⊢ ∑ a, ψ a = 0

Tactic:
h₂

Goal state after:
R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : ψ b ≠ 1
h₁ : ψ b * Finset.univ.sum ⇑ψ = Finset.univ.sum ⇑ψ
h₂ : ∑ a, ψ a = Finset.univ.sum ⇑ψ
⊢ ∑ a, ψ a = 0
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
⊢ (X ^ n - 1).rootSet L = {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
refine Set.ext fun x => ?_

Goal state after:
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
x : L
⊢ x ∈ (X ^ n - 1).rootSet L ↔ x ∈ {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: 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
x : CyclotomicField 0 K
this : IsSplittingField K K (cyclotomic 0 K)
e : K ≃ₗ[K] CyclotomicField 0 K := ↑(IsSplittingField.algEquiv K (cyclotomic 0 K))
⊢ finrank K (CyclotomicField 0 K) = 1

Tactic:
simp [← LinearEquiv.finrank_eq e, finrank_self]

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✝) χ₀
⊢ x ∈ (toUnitHom χ).ker

Tactic:
MonoidHom.mem_ker,

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 χ) x = 1
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
⊢ 0 < n

Tactic:
refine Nat.pos_of_ne_zero fun hn ↦ ?_

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn : n = 0
⊢ False
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
⊢ (↑x).val ≡ 1 [MOD n.gcd m]

Tactic:
MonoidHom.mem_ker,

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 : (ZMod.unitsMap ⋯) x = 1
⊢ (↑x).val ≡ 1 [MOD n.gcd m]
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ Subsingleton (DirichletCharacter R 1)

Tactic:
by
  refine subsingleton_iff.mpr (fun χ χ' ↦ ?_)
  simp [level_one]

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

Goal state before:
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

Tactic:
rw [one_pow]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
h : χ.conductor = 0
⊢ χ.primitiveCharacter.IsPrimitive

Tactic:
isPrimitive_def

Goal state after:
case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
h : χ.conductor = 0
⊢ χ.primitiveCharacter.conductor = χ.conductor
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero m
hm : n ∣ m
this : NeZero n
⊢ ((changeLevel hm) χ).conductor ∣ χ.conductor

Tactic:
refine conductor_dvd_of_mem_conductorSet _
      ⟨χ.conductor_dvd_level.trans hm, χ.primitiveCharacter, ?_⟩

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero m
hm : n ∣ m
this : NeZero n
⊢ (changeLevel hm) χ = (changeLevel ⋯) χ.primitiveCharacter
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case inr
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'
b : R
hb : b ≠ 0
x : R
⊢ χ x * ψ (b * (x - 1)) = χ (b * x * b⁻¹) * ψ (b * x - b)

Tactic:
rw [mul_assoc, mul_comm x, ← mul_assoc, mul_inv_cancel₀ hb, one_mul, mul_sub, mul_one]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁ : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
n' : ℕ+
hp' : Nat.Prime (ringChar F')
hc' : Fintype.card F' = ringChar F' ^ ↑n'
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
hchar : ringChar F' = ringChar FF'
⊢ ((algebraMap F' FF') (χ (-1)) * ↑(Fintype.card F)) ^ (ringChar F' ^ ↑n' / 2) =
    (algebraMap F' FF') (χ ↑(ringChar F' ^ ↑n'))

Tactic:
hchar,

Goal state after:
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁ : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
n' : ℕ+
hp' : Nat.Prime (ringChar F')
hc' : Fintype.card F' = ringChar F' ^ ↑n'
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
hchar : ringChar F' = ringChar FF'
⊢ ((algebraMap F' FF') (χ (-1)) * ↑(Fintype.card F)) ^ (ringChar FF' ^ ↑n' / 2) =
    (algebraMap F' FF') (χ ↑(ringChar FF' ^ ↑n'))
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case hxy.e'_6.a
ι : 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
j : ι
hj : j ∈ s
⊢ Disjoint {j} {i}

Tactic:
rw [Finset.disjoint_singleton]
                  exact fun h ↦ hi (h ▸ hj)

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 ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : (↑#ι).HolderConjugate p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
⊢ 1 < #ι

Tactic:
by exact_mod_cast hp.lt

Goal state after:
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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp✝ : (↑(finrank ℝ E)).HolderConjugate p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : (↑#ι).HolderConjugate p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)
hc : 0 < c
h2c : μ = c • Measure.map (⇑e.symm) volume
h3c : ↑c ≠ 0
h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹
⊢ c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹ * c ^ p = c * ‖↑e.symm‖₊ ^ p

Tactic:
inv_mul_cancel_right₀ (NNReal.rpow_pos hc).ne'

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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp✝ : (↑(finrank ℝ E)).HolderConjugate p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : (↑#ι).HolderConjugate p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)
hc : 0 < c
h2c : μ = c • Measure.map (⇑e.symm) volume
h3c : ↑c ≠ 0
h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹
⊢ c * ‖↑e.symm‖₊ ^ p = c * ‖↑e.symm‖₊ ^ p
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 g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : f.graph.topologicalClosure = f'.graph
this : g.graph.topologicalClosure ≤ f'.graph
⊢ g.IsClosable

Tactic:
use g.graph.topologicalClosure.toLinearPMap

Goal state after:
case h
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 g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : f.graph.topologicalClosure = f'.graph
this : g.graph.topologicalClosure ≤ f'.graph
⊢ g.graph.topologicalClosure = g.graph.topologicalClosure.toLinearPMap.graph
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case e'_4.e'_5
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
⊢ eLpNormLESNormFDerivOneConst μ ↑(↑(finrank ℝ E)).conjExponent *
      (1 * (↑(finrank ℝ E) - 1) / (↑(finrank ℝ E) - 1)).toNNReal =
    eLpNormLESNormFDerivOneConst μ ↑(↑(finrank ℝ E)).conjExponent

Tactic:
simp only [n, NNReal.coe_one] at hnp

Goal state after:
case e'_4.e'_5
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 < ↑(finrank ℝ E) - 1
⊢ eLpNormLESNormFDerivOneConst μ ↑(↑(finrank ℝ E)).conjExponent *
      (1 * (↑(finrank ℝ E) - 1) / (↑(finrank ℝ E) - 1)).toNNReal =
    eLpNormLESNormFDerivOneConst μ ↑(↑(finrank ℝ E)).conjExponent
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case hfg
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'
x : E
⊢ ‖fderiv ℝ v x‖ₑ ≤ ↑γ * ‖u x‖ₑ ^ (↑γ - 1) * ‖fderiv ℝ u x‖ₑ

Tactic:
exact enorm_fderiv_norm_rpow_le (hu.differentiable one_ne_zero) h1γ

Goal state after:
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
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
F' : Type := ⋯
e : F ≃L[ℝ] F' := ⋯
C₁ : ℝ≥0 := ⋯
C : ℝ≥0 := ⋯
C₂ : ℝ≥0 := ⋯
v : E → F' := ⋯
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this : eLpNorm v (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ v) (↑p) μ
h4v : ∀ (x : E), ‖fderiv ℝ v x‖ ≤ ↑C₂ * ‖fderiv ℝ u x‖
⊢ ∀ᵐ (x : E) ∂μ, ‖(⇑e.symm ∘ v) x‖₊ ≤ C₁ * ‖v x‖₊

Tactic:
exact Eventually.of_forall (fun x ↦ (e.symm : F' →L[ℝ] F).le_opNNNorm _)

Goal state after:
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
inst✝⁵ : CompleteSpace E
inst✝⁴ : CompleteSpace G
inst✝³ : CompleteSpace (E ⊗[𝕜] G)
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace (F ⊗[𝕜] H)
f : E →L[𝕜] F
g : G →L[𝕜] H
⊢ ∀ (x : F) (y : H),
    ↑(ContinuousLinearMap.adjoint (mapL f g)) (x ⊗ₜ[𝕜] y) =
      ↑(mapL (ContinuousLinearMap.adjoint f) (ContinuousLinearMap.adjoint g)) (x ⊗ₜ[𝕜] y)

Tactic:
simp [TensorProduct.ext_iff_inner_right, ContinuousLinearMap.adjoint_inner_left]

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
⊢ μHE[finrank ℝ V] = map (⇑(IsometryEquiv.vaddConst p)) volume

Tactic:
by
  have h := (IsometryEquiv.vaddConst p)
    |>.measurePreserving_euclideanHausdorffMeasure (finrank ℝ V) |>.map_eq
  rw [InnerProductSpace.euclideanHausdorffMeasure_eq_volume] at h
  exact h.symm

Goal state after: