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
j : ℕ
⊢ j ∈ n.properDivisors.erase 1 → 2 ≤ j

Tactic:
hj

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
j : ℕ
hj : j ∈ n.properDivisors.erase 1
⊢ 2 ≤ j
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
hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j
j : ℕ
⊢ j ∈ n.properDivisors.erase 1 → (cyclotomic j R).coeff 0 = 1

Tactic:
hj

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
hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j
j : ℕ
hj : j ∈ n.properDivisors.erase 1
⊢ (cyclotomic j R).coeff 0 = 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case h
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 : ∏ i ∈ n.divisors.erase 1, cyclotomic i R = ∑ i ∈ range n, X ^ i
⊢ 0 < eval x (cyclotomic n R)

Tactic:
apply_fun eval x at this

Goal state after:
case h
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 (∏ i ∈ n.divisors.erase 1, cyclotomic i R) = eval x (∑ i ∈ range n, X ^ i)
⊢ 0 < eval x (cyclotomic n R)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case neg.refine_1
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
m : ℕ
hm₁ : m ∈ S ∪ {n}
hm₂ : m ≠ 0
⊢ ∃ r, IsPrimitiveRoot r m

Tactic:
obtain hm₁ | rfl := hm₁

Goal state after:
case neg.refine_1.inl
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
m : ℕ
hm₂ : m ≠ 0
hm₁ : m ∈ S
⊢ ∃ r, IsPrimitiveRoot r m

case neg.refine_1.inr
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
m : ℕ
hm₂ : m ≠ 0
inst✝ : NeZero m
hr : IsPrimitiveRoot r m
hn : ¬m = 0
⊢ ∃ r, IsPrimitiveRoot r m
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
⊢ ∏ x, -1 * (1 - x ζ) = (algebraMap K E) ↑(eval 1 (cyclotomic n ℤ))

Tactic:
prod_mul_distrib,

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
⊢ (∏ x, -1) * ∏ x, (1 - x ζ) = (algebraMap K E) ↑(eval 1 (cyclotomic n ℤ))
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2
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
x : B
m : ℕ
hm : m ∈ S
hm' : m ≠ 0 ∧ x ^ m = 1
⊢ ∃ n_1, (n_1 = n ∨ n_1 ∈ S) ∧ n_1 ≠ 0 ∧ x ^ n_1 = 1

Tactic:
exact ⟨m, ⟨Or.inr hm, hm'⟩⟩

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

Goal state before:
pp: case a
S : Set ℕ
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension S K L
M : Type u_1
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤
⊢ {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} ⊆ ↑(IntermediateField.adjoin K (⇑i '' {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))

Tactic:
· rintro x ⟨n, hn, h1, h2⟩
    have : NeZero n := ⟨h1⟩
    obtain ⟨y, hy⟩ := exists_isPrimitiveRoot K L hn h1
    obtain ⟨m, -, rfl⟩ := (hy.map_of_injective i.injective).eq_pow_of_pow_eq_one h2
    exact pow_mem (IntermediateField.subset_adjoin K (i '' {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
      ⟨y, ⟨n, hn, h1, hy.pow_eq_one⟩, rfl⟩) m

Goal state after:
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
M : Type u_1
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsSepClosed M
⊢ Nonempty (L ≃ₐ[K] ↥(IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))

Tactic:
by
  have := isSeparable S K L
  let i : L →ₐ[K] M := IsSepClosed.lift
  refine ⟨(show L ≃ₐ[K] i.fieldRange from AlgEquiv.ofInjectiveField i).trans
    (IntermediateField.equivOfEq ?_)⟩
  have htop : IntermediateField.adjoin K {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤ :=
    IntermediateField.adjoin_eq_top_of_algebra K _ ((iff_adjoin_eq_top S K L).1 ‹_›).2
  rw [AlgHom.fieldRange_eq_map, ← htop, IntermediateField.adjoin_map]
  apply le_antisymm <;> rw [IntermediateField.adjoin_le_iff]
  · rintro _ ⟨y, ⟨n, hn, h1, h2⟩, rfl⟩
    exact IntermediateField.subset_adjoin K _ ⟨n, hn, h1, by simpa using congrArg i h2⟩
  · rintro x ⟨n, hn, h1, h2⟩
    have : NeZero n := ⟨h1⟩
    obtain ⟨y, hy⟩ := exists_isPrimitiveRoot K L hn h1
    obtain ⟨m, -, rfl⟩ := (hy.map_of_injective i.injective).eq_pow_of_pow_eq_one h2
    exact pow_mem (IntermediateField.subset_adjoin K (i '' {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
      ⟨y, ⟨n, hn, h1, hy.pow_eq_one⟩, rfl⟩) m

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

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
he : ¬e.IsPrimitive
⊢ ∃ d, d ∣ N ∧ d < N ∧ e.mulShift ↑d = 1

Tactic:
simp_rw [IsPrimitive, not_forall, not_ne_iff] at he
  rcases he with ⟨b, hb_ne, hb⟩
  -- We have `AddChar.mulShift e b = 1`, but `b ≠ 0`.
  obtain ⟨d, hd, u, hu, rfl⟩ := b.eq_unit_mul_divisor
  refine ⟨d, hd, lt_of_le_of_ne (Nat.le_of_dvd (NeZero.pos _) hd) ?_, ?_⟩
  · exact fun h ↦ by simp only [h, ZMod.natCast_self, mul_zero, ne_eq, not_true_eq_false] at hb_ne
  · rw [← mulShift_unit_eq_one_iff _ hu, ← hb, mul_comm]
    ext1 y
    rw [mulShift_apply, mulShift_apply, mulShift_apply, mul_assoc]

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed

Goal state before:
pp: F : Type u_1
inst✝² : Field F
n k : ℕ
inst✝¹ : NeZero ↑n
inst✝ : IsSepClosed F
⊢ ∃ m, IsPrimitiveRoot m n

Tactic:
have : NeZero n := .of_neZero_natCast F

Goal state after:
F : Type u_1
inst✝² : Field F
n k : ℕ
inst✝¹ : NeZero ↑n
inst✝ : IsSepClosed F
this : NeZero n
⊢ ∃ m, IsPrimitiveRoot m n
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 (equivToUnitHom.symm E)).comp (ZMod.unitsMap hd)

Tactic:
Equiv.apply_symm_apply,

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 χ = E.comp (ZMod.unitsMap hd)
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_4
inst✝¹ : CommGroupWithZero R
R' : Type u_5
inst✝ : CommRing R'
χ : MulChar R R'
n : ℤ
a : Rˣ
⊢ (χ ^ n) ↑a = χ ↑(a ^ n)

Tactic:
obtain ⟨m, rfl | rfl⟩ := Int.eq_nat_or_neg n
  · simp [pow_apply_coe]
  · simp [pow_apply_coe, inv_apply', ← inv_pow]

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
this✝ : NeZero d
hd : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel hd) χ₀
this : (changeLevel ⋯) χ₀ = (changeLevel ⋯) χ.primitiveCharacter
w✝ : d.gcd χ.conductor ∣ d
χ₁ : DirichletCharacter R (d.gcd χ.conductor)
hχ₁ : χ₀ = (changeLevel w✝) χ₁
⊢ d.gcd χ.conductor ∈ χ.conductorSet

Tactic:
refine ⟨Nat.dvd_trans (d.gcd_dvd_left χ.conductor) hd, χ₁, ?_⟩

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
this✝ : NeZero d
hd : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel hd) χ₀
this : (changeLevel ⋯) χ₀ = (changeLevel ⋯) χ.primitiveCharacter
w✝ : d.gcd χ.conductor ∣ d
χ₁ : DirichletCharacter R (d.gcd χ.conductor)
hχ₁ : χ₀ = (changeLevel w✝) χ₁
⊢ χ = (changeLevel ⋯) χ₁
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
inst✝¹ : Nontrivial R
m : ℕ
inst✝ : NeZero m
hm : n ∣ m
χ : DirichletCharacter R n
a : ℤ
ha : IsCoprime a ↑χ.conductor
⊢ ((changeLevel hm) χ).primitiveCharacter ↑a = χ.primitiveCharacter ↑a

Tactic:
suffices changeLevel (dvd_of_eq <| conductor_changeLevel ..)
        (changeLevel hm χ).primitiveCharacter = χ.primitiveCharacter by
      have := DFunLike.congr_fun this (a : ZMod _)
      rwa [changeLevel_eq_cast_of_dvd' _ _ ha] at this

Goal state after:
case pos
R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
inst✝¹ : Nontrivial R
m : ℕ
inst✝ : NeZero m
hm : n ∣ m
χ : DirichletCharacter R n
a : ℤ
ha : IsCoprime a ↑χ.conductor
⊢ (changeLevel ⋯) ((changeLevel hm) χ).primitiveCharacter = χ.primitiveCharacter
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

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

Tactic:
Set.mem_ofPred,

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝ : NeZero n
d : ℕ
x✝ : DirichletCharacter R n
hχ : x✝ ∈ {χ | d.Coprime χ.conductor}
⊢ d.Coprime x✝⁻¹.conductor
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)
⊢ gaussSum χ ψ ≠ 0

Tactic:
intro hf

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)
hf : gaussSum χ ψ = 0
⊢ False
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
⊢ 2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))

Tactic:
have hp2 (n : ℕ) : (2 ^ n : F) ≠ 0 := pow_ne_zero n (Ring.two_ne_zero hF)

Goal state after:
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
⊢ 2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
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
⊢ ∫⋯∫⁻_insert i s, f ^ (1 - ↑(#s) * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) ^ p ∂μ =
    ∫⋯∫⁻_s, fun x ↦
      ∫⁻ (t : A i), f (update x i t) ^ (1 - ↑(#s) * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) (update x i t) ^ p ∂μ i ∂μ

Tactic:
rw [lmarginal_insert' _ _ hi]

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
⊢ ∫⋯∫⁻_s, fun x ↦
      ∫⁻ (xᵢ : A i), (f ^ (1 - ↑(#s) * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) ^ p) (update x i xᵢ) ∂μ i ∂μ =
    ∫⋯∫⁻_s, fun x ↦
      ∫⁻ (t : A i), f (update x i t) ^ (1 - ↑(#s) * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) (update x i t) ^ p ∂μ i ∂μ

ι : 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
⊢ Measurable (f ^ (1 - ↑(#s) * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) ^ p)
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

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

Tactic:
have : (1 : ℝ) ≤ ↑#ι - 1 := by
    have hι : (2 : ℝ) ≤ #ι := by exact_mod_cast hp.lt
    linarith
  calc ∫⁻ x, ‖u x‖ₑ ^ p
      = ∫⁻ x, (‖u x‖ₑ ^ (1 / (#ι - 1 : ℝ))) ^ (#ι : ℝ) := by
        -- a little algebraic manipulation of the exponent
        congr! 2 with x
        rw [← ENNReal.rpow_mul, hp.conjugate_eq]
        field_simp
    _ = ∫⁻ x, ∏ _i : ι, ‖u x‖ₑ ^ (1 / (#ι - 1 : ℝ)) := by
        -- express the left-hand integrand as a product of identical factors
        congr! 2 with x
        simp_rw [prod_const]
        norm_cast
    _ ≤ ∫⁻ x, ∏ i, (∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖ₑ) ^ ((1 : ℝ) / (#ι - 1 : ℝ)) := ?_
    _ ≤ (∫⁻ x, ‖fderiv ℝ u x‖ₑ) ^ p := by
        -- apply the grid-lines lemma
        apply lintegral_prod_lintegral_pow_le _ hp
        fun_prop
  -- we estimate |u x| using the fundamental theorem of calculus.
  gcongr with x i
  calc ‖u x‖ₑ
    _ ≤ ∫⁻ xᵢ in Iic (x i), ‖deriv (u ∘ update x i) xᵢ‖ₑ := by
        apply le_trans (by simp) (HasCompactSupport.enorm_le_lintegral_Ici_deriv _ _ _)
        · exact hu.comp (by convert! contDiff_update 1 x i)
        · exact h2u.comp_isClosedEmbedding (isClosedEmbedding_update x i)
    _ ≤ ∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖ₑ := ?_
  gcongr with y
  · exact Measure.restrict_le_self
  -- bound the derivative which appears
  calc ‖deriv (u ∘ update x i) y‖ₑ = ‖fderiv ℝ u (update x i y) (deriv (update x i) y)‖ₑ := by
        rw [fderiv_comp_deriv _ (hu.differentiable one_ne_zero).differentiableAt
          (hasDerivAt_update x i y).differentiableAt]
    _ ≤ ‖fderiv ℝ u (update x i y)‖ₑ * ‖deriv (update x i) y‖ₑ := ContinuousLinearMap.le_opENorm _ _
    _ ≤ ‖fderiv ℝ u (update x i y)‖ₑ := by simp [deriv_update, Pi.enorm_single]

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)
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤ ↑C * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂μ) ^ p

Tactic:
have hιcard : #ι = finrank ℝ E := Fintype.card_fin (finrank ℝ E)

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
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤ ↑C * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂μ) ^ p
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst✝¹ : U.HasOrthogonalProjection
inst✝ : V.HasOrthogonalProjection
⊢ (↑U.starProjection).range ≤ (↑V.starProjection).range ↔ U ≤ V

Tactic:
toLinearMap_starProjection_eq_isComplProjection,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst✝¹ : U.HasOrthogonalProjection
inst✝ : V.HasOrthogonalProjection
⊢ (U.projection Uᗮ ⋯).range ≤ (V.projection Vᗮ ⋯).range ↔ U ≤ V
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
A : E →ₗ.[𝕜] E
hA : A† = A
h : ¬Dense ↑A.domain
⊢ A.domain = ⊤

Tactic:
← hA,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
A : E →ₗ.[𝕜] E
hA : A† = A
h : ¬Dense ↑A.domain
⊢ A†.domain = ⊤
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
A : E →ₗ.[𝕜] E
hA : IsSelfAdjoint A
⊢ Dense ↑A.domain

Tactic:
by
  by_contra h
  rw [isSelfAdjoint_def] at hA
  have h' : A.domain = ⊤ := by
    rw [← hA, Submodule.eq_top_iff']
    intro x
    rw [mem_adjoint_domain_iff, ← hA]
    refine (innerSL 𝕜 x).cont.comp ?_
    simp only [adjoint, h]
    exact continuous_const
  simp [h'] at h

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
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))
⊢ RCLike.re (∑ x, ∑ i, inner 𝕜 (f (e i)) (f (e x)) * inner 𝕜 (g i) (g x)) ≤
    ‖f‖ ^ 2 * RCLike.re (∑ x, ∑ i, inner 𝕜 (e i) (e x) * inner 𝕜 (g i) (g x))

Tactic:
← hA,

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))
⊢ RCLike.re
      (∑ x,
        ∑ x_1,
          (‖f‖ ^ 2 • inner 𝕜 (e x_1) (e x) - (∑ i, Matrix.vecMulVec (A i) (star (A i))) x_1 x) *
            inner 𝕜 (g x_1) (g x)) ≤
    ‖f‖ ^ 2 * RCLike.re (∑ x, ∑ i, inner 𝕜 (e i) (e x) * inner 𝕜 (g i) (g x))
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
i : ℝ≥0
hi : μH[↑i] s = 0
j : ℝ≥0
⊢ μH[↑j] s = ∞ → j ≤ i

Tactic:
hj

Goal state after:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
i : ℝ≥0
hi : μH[↑i] s = 0
j : ℝ≥0
hj : μH[↑j] s = ∞
⊢ j ≤ i
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
⊢ dimH s ≤ ⨅ d, ⨅ (_ : μH[↑d] s = 0), ↑d

Tactic:
rw [dimH_def]
    simp only [le_iInf_iff, iSup_le_iff, ENNReal.coe_le_coe]
    intro i hi j hj
    by_contra! hij
    simpa [hi, hj] using hausdorffMeasure_mono hij.le s

Goal state after:
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) = ∞
r n i j : ℕ
⊢ i < j → AreSeparated (S (2 * i + 1 + r)) (s \ S (2 * j + r))

Tactic:
hj

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 n i j : ℕ
hj : i < j
⊢ AreSeparated (S (2 * i + 1 + r)) (s \ S (2 * j + r))