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

Goal state before:
pp: case inr.refine_1
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : eval μ (cyclotomic m R ^ (p ^ k - p ^ (k - 1))) = 0
⊢ IsPrimitiveRoot μ m

Tactic:
eval_pow

Goal state after:
case inr.refine_1
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : eval μ (cyclotomic m R) ^ (p ^ k - p ^ (k - 1)) = 0
⊢ IsPrimitiveRoot μ m
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: K : Type u_1
inst✝¹ : CommRing K
p q : ℕ
inst✝ : CharP K p
h : p ∣ q
⊢ (X ^ q - X).Separable

Tactic:
use 1, X ^ q - X - 1

Goal state after:
case h
K : Type u_1
inst✝¹ : CommRing K
p q : ℕ
inst✝ : CharP K p
h : p ∣ q
⊢ 1 * (X ^ q - X) + (X ^ q - X - 1) * derivative (X ^ q - X) = 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case convert_5
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∀ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 (q - 1).toNNReal ⋯ ≤ Units.mk0 ‖↑q - ↑i‖₊ ⋯

pp: case convert_6
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∃ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 (q - 1).toNNReal ⋯ < Units.mk0 ‖↑q - ↑i‖₊ ⋯

Tactic:
· simp only [Finset.mem_attach, forall_true_left, Subtype.forall, ←
      Units.val_le_val, ← NNReal.coe_le_coe, norm_nonneg, Units.val_mk0,
      Real.coe_toNNReal', coe_nnnorm, max_le_iff, tsub_le_iff_right]
    intro x hx
    simpa only [and_true, tsub_le_iff_right] using hfor x hx

Goal state after:
case convert_6
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∃ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 (q - 1).toNNReal ⋯ < Units.mk0 ‖↑q - ↑i‖₊ ⋯
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
A : Type w
K : Type u
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsDomain A
ζ : A
inst✝ : IsCyclotomicExtension {n} K A
hζ : IsPrimitiveRoot ζ n
h : Irreducible (cyclotomic n K)
this : NeZero ↑n
⊢ minpoly K (ζ + (algebraMap K A) (-1)) = (cyclotomic n K).comp (X + 1)

Tactic:
minpoly.add_algebraMap ζ,

Goal state after:
n : ℕ
inst✝⁵ : NeZero n
A : Type w
K : Type u
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsDomain A
ζ : A
inst✝ : IsCyclotomicExtension {n} K A
hζ : IsPrimitiveRoot ζ n
h : Irreducible (cyclotomic n K)
this : NeZero ↑n
⊢ (minpoly K ζ).comp (X - C (-1)) = (cyclotomic n K).comp (X + 1)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case inl
n : ℕ
hn' : 1 < n
hq : 0 ≠ 1
⊢ 0 < (eval (↑0) (cyclotomic n ℤ)).natAbs

Tactic:
pos_iff_ne_zero,

Goal state after:
case inl
n : ℕ
hn' : 1 < n
hq : 0 ≠ 1
⊢ (eval (↑0) (cyclotomic n ℤ)).natAbs ≠ 0
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case pos
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
⊢ False

pp: case neg
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : ¬p ∣ x
⊢ False

Tactic:
· have h := Nat.dvd_sub hp hpx
    rw [add_comm, Nat.add_sub_cancel] at h
    rcases pp.dvd_mul.mp h with h | h
    · have ⟨q, hq, hq'⟩ := (pp.prime.dvd_finsetProd_iff id).mp h
      rw [Finset.mem_filter, Nat.mem_primeFactors,
        ← (Nat.prime_dvd_prime_iff_eq pp hq.1.1).mp hq'] at hq
      exact hq.2 hpx
    · exact Nat.Prime.not_coprime_iff_dvd.mpr ⟨p, pp, hpx, h⟩ hx

Goal state after:
case neg
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : ¬p ∣ x
⊢ False
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
⊢ (∃ x, ψ x ≠ 1) ↔ ψ 1 ≠ 1

Tactic:
refine ⟨?_, fun h => ⟨_, h⟩⟩

Goal state after:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
⊢ (∃ x, ψ x ≠ 1) → ψ 1 ≠ 1
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1
n : ℕ
inst✝⁷ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑n
this✝¹ : NeZero ↑n
this✝ : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : (cyclotomic n K).degree ≠ 0
ζ : (cyclotomic n K).SplittingField
hζ : IsPrimitiveRoot ζ n
⊢ ∀ {n_1 : ℕ}, n_1 ∈ {n} → n_1 ≠ 0 → ∃ r, IsPrimitiveRoot r n_1

Tactic:
simp only [mem_singleton_iff, forall_eq]
    exact fun _ ↦ ⟨ζ, hζ⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ toUnits (toCircle x) ∈ rootsOfUnity n Circle

Tactic:
ext; simp [← AddChar.map_nsmul_eq_pow]

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

Goal state before:
pp: case pos
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (χ a)
⊢ (fun x ↦ χ a * x) (χ a)⁻¹ʳ = (fun x ↦ χ a * x) (χ a⁻¹ʳ)

Tactic:
dsimp only

Goal state after:
case pos
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (χ a)
⊢ χ a * (χ a)⁻¹ʳ = χ a * χ a⁻¹ʳ
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : n ≠ 0
a : R
ha : ¬IsUnit a
⊢ (χ ^ n) a = χ a ^ n

Tactic:
map_nonunit (χ ^ n) ha,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : n ≠ 0
a : R
ha : ¬IsUnit a
⊢ 0 = χ a ^ n
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 : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
h : IsCyclotomicExtension S A ↥C
this : Subalgebra.map C.val (adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = Subalgebra.map C.val ⊤
⊢ Subalgebra.map C.val (adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = adjoin A {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

Tactic:
AlgHom.map_adjoin

Goal state after:
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
h : IsCyclotomicExtension S A ↥C
this : Subalgebra.map C.val (adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = Subalgebra.map C.val ⊤
⊢ adjoin A (⇑C.val '' {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = adjoin A {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
H : Set (ZMod n)ˣ
χ : DirichletCharacter R n
hχ : ∀ (x : (↥(Submonoid.map (Units.coeHom (ZMod n)) (Submonoid.closure H)))ˣ), χ ↑↑x = 1
x : (ZMod n)ˣ
hx : x ∈ Submonoid.closure H
⊢ χ ↑x = 1

Tactic:
exact hχ <| (Submonoid.unitsEquivUnitsType _) <|
      ⟨x, Submonoid.mem_units_of_val_mem_inv_val_mem _ ⟨x, hx, rfl⟩
        ⟨x⁻¹, by simpa [← Subgroup.closure_toSubmonoid_of_finite] using hx, rfl⟩⟩

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

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
h_ne : gaussSum χ e ≠ 0
⊢ (ZMod.unitsMap hd).ker ≤ (MulChar.toUnitHom χ).ker

Tactic:
intro _ hu

Goal state after:
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
h_ne : gaussSum χ e ≠ 0
x✝ : (ZMod N)ˣ
hu : x✝ ∈ (ZMod.unitsMap hd).ker
⊢ x✝ ∈ (MulChar.toUnitHom χ).ker
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
| fun i ↦ ∑ j, χ i * ψ i * (φ j * ψ j)

Tactic:
x,

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
| ∑ j, χ x * ψ x * (φ j * ψ j)
Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum

Goal state before:
pp: case neg
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
a : ZMod N
ha : ¬IsUnit a
⊢ gaussSum χ (e.mulShift a) = χ⁻¹ a * gaussSum χ e

Tactic:
· rw [MulChar.map_nonunit _ ha, zero_mul]
    exact gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitive _ hχ (not_isPrimitive_mulShift e ha)

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
| fun x ↦ ∑ i, χ i * ψ i * (χ x⁻¹ * ψ (-x))

Tactic:
x,

Goal state after:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
x : R
| ∑ i, χ i * ψ i * (χ x⁻¹ * ψ (-x))
Module: Mathlib.Analysis.InnerProductSpace.NormPow

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

Tactic:
gcongr _ * ?_

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

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

Tactic:
rintro ⟨u, hut, -, rfl⟩

Goal state after:
case pos.mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
u : Finset α
hut : u ⊆ t
⊢ s ⊆ u ∪ s ∧ u ∪ s ⊆ t
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
hst : ¬s ⊆ t
⊢ (u ∈ if s ⊆ t then map { toFun := fun u ↦ (↑u).disjUnion s ⋯, inj' := ⋯ } (t \ s).powerset.attach else ∅) ↔
    s ⊆ u ∧ u ⊆ t

Tactic:
suffices s ⊆ u → ¬u ⊆ t by simpa [hst]

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
hst : ¬s ⊆ t
⊢ s ⊆ u → ¬u ⊆ t
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case h₂.hp
ι : 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 := ⋯
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ⋯
hk' : 0 ≤ 1 - k * p
⊢ ∀ i ∈ s, 0 ≤ p

Tactic:
· exact fun _ _ ↦ hp₀

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
this : q ⊔ qᗮ = ⊤
⊢ q ⊔ qᗮ ⊓ p = p

Tactic:
by rw [← sup_inf_assoc_of_le _ hq₂, this, top_inf_eq p]

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

Goal state before:
pp: case h2
ι : 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
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
i : ι
a✝ : i ∈ Finset.univ
⊢ volume.restrict (Set.Iic (x i)) ≤ volume

pp: case hfg
ι : 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
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
i : ι
a✝ : i ∈ Finset.univ
y : ℝ
⊢ ‖deriv (u ∘ update x i) y‖ₑ ≤ ‖fderiv ℝ u (update x i y)‖ₑ

Tactic:
· exact Measure.restrict_le_self

Goal state after:
case hfg
ι : 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
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
i : ι
a✝ : i ∈ Finset.univ
y : ℝ
⊢ ‖deriv (u ∘ update x i) y‖ₑ ≤ ‖fderiv ℝ u (update x i y)‖ₑ
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E ≃ₗ[𝕜] E
hT : (↑T).IsPositive
x : E
this : 0 ≤ re ⟪x, T.symm x⟫
⊢ 0 ≤ re ⟪↑T.symm x, x⟫

Tactic:
← T.symm.coe_toLinearMap,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E ≃ₗ[𝕜] E
hT : (↑T).IsPositive
x : E
this : 0 ≤ re ⟪x, ↑T.symm x⟫
⊢ 0 ≤ re ⟪↑T.symm x, x⟫
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
this : CompleteSpace ↑↑(↑(continuousLinearMapOfBilin B)).range
⊢ (↑(continuousLinearMapOfBilin B)).rangeᗮᗮ = ⊤

Tactic:
Submodule.eq_top_iff'

Goal state after:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(↑(continuousLinearMapOfBilin B)).range
⊢ ∀ (x : V), x ∈ (↑(continuousLinearMapOfBilin B)).rangeᗮᗮ
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case e'_3
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
⊢ (↑p')⁻¹ = (↑n')⁻¹

Tactic:
hp'

Goal state after:
case e'_3
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
⊢ ↑1⁻¹ - (↑n)⁻¹ = (↑n')⁻¹
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
⊢ (↑n')⁻¹ - q⁻¹ = (↑p')⁻¹

Tactic:
hp'

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
⊢ (↑n')⁻¹ - q⁻¹ = ↑p⁻¹ - (↑n)⁻¹
Module: Mathlib.Analysis.InnerProductSpace.MeanErgodic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : LipschitzWith 1 ⇑f
g : E →L[𝕜] ↥(f.eqLocus 1)
hg_proj : ∀ (x : ↥(f.eqLocus 1)), g ↑x = x
hg_ker : ↑(↑g).ker ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(f - 1).range
y : E
hy : g y = 0
z : E
hz : IsFixedPt (⇑f) z
this✝ :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    {x | Tendsto (fun x_1 ↦ birkhoffAverage 𝕜 (⇑f) _root_.id x_1 x) atTop (𝓝 0)}
x : E
this : Bornology.IsBounded (Set.range fun x_1 ↦ _root_.id ((⇑f)^[x_1] x))
⊢ (f - 1) x ∈ {x | Tendsto (fun x_1 ↦ birkhoffAverage 𝕜 (⇑f) _root_.id x_1 x) atTop (𝓝 0)}

Tactic:
have H : ∀ n x y, f^[n] (x - y) = f^[n] x - f^[n] y := iterate_map_sub (f : E →+ E)

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : LipschitzWith 1 ⇑f
g : E →L[𝕜] ↥(f.eqLocus 1)
hg_proj : ∀ (x : ↥(f.eqLocus 1)), g ↑x = x
hg_ker : ↑(↑g).ker ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(f - 1).range
y : E
hy : g y = 0
z : E
hz : IsFixedPt (⇑f) z
this✝ :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    {x | Tendsto (fun x_1 ↦ birkhoffAverage 𝕜 (⇑f) _root_.id x_1 x) atTop (𝓝 0)}
x : E
this : Bornology.IsBounded (Set.range fun x_1 ↦ _root_.id ((⇑f)^[x_1] x))
H : ∀ (n : ℕ) (x y : E), (⇑f)^[n] (x - y) = (⇑f)^[n] x - (⇑f)^[n] y
⊢ (f - 1) x ∈ {x | Tendsto (fun x_1 ↦ birkhoffAverage 𝕜 (⇑f) _root_.id x_1 x) atTop (𝓝 0)}
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:
Submodule.eq_top_iff'

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
⊢ ∀ (x : E), x ∈ A†.domain
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case pos
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
⊢ (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / ↑p') ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ

Tactic:
h3u,

Goal state after:
case pos
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
⊢ 0 ^ (1 / ↑p') ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: case mp
𝕜 : 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
g : Submodule 𝕜 (E × F)
x : F × E
⊢ (∃ y,
      (∀ (u : WithLp 2 (F × E)) (x : E) (x_1 : F),
          (x, x_1) ∈ g → toLp 2 (x_1, -x) = u → ⟪u.fst, y.fst⟫ + ⟪u.snd, y.snd⟫ = 0) ∧
        y.ofLp = x) →
    ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0

pp: case mpr
𝕜 : 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
g : Submodule 𝕜 (E × F)
x : F × E
⊢ (∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0) →
    ∃ y,
      (∀ (u : WithLp 2 (F × E)) (x : E) (x_1 : F),
          (x, x_1) ∈ g → toLp 2 (x_1, -x) = u → ⟪u.fst, y.fst⟫ + ⟪u.snd, y.snd⟫ = 0) ∧
        y.ofLp = x

Tactic:
· rintro ⟨y, h1, h2⟩ a b hab
    rw [← h2, WithLp.ofLp_fst, WithLp.ofLp_snd]
    specialize h1 (toLp 2 (b, -a)) a b hab rfl
    dsimp at h1
    simp only [inner_neg_left, ← sub_eq_add_neg] at h1
    exact h1

Goal state after:
case mpr
𝕜 : 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
g : Submodule 𝕜 (E × F)
x : F × E
⊢ (∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0) →
    ∃ y,
      (∀ (u : WithLp 2 (F × E)) (x : E) (x_1 : F),
          (x, x_1) ∈ g → toLp 2 (x_1, -x) = u → ⟪u.fst, y.fst⟫ + ⟪u.snd, y.snd⟫ = 0) ∧
        y.ofLp = x