mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case succ.refine_1.inr
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x✝ : GaloisField (n✝ + 1) n
hx✝ :
  x✝ ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
x : GaloisField (n✝ + 1) n
hx : x ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField
⊢ (aeval x) (X ^ (n✝ + 1) ^ n - X) = 0

Tactic:
mem_rootSet_of_ne aux

Goal state after:
case succ.refine_1.inr
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x✝ : GaloisField (n✝ + 1) n
hx✝ :
  x✝ ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
x : GaloisField (n✝ + 1) n
hx : (aeval x) (X ^ (n✝ + 1) ^ n - X) = 0
⊢ (aeval x) (X ^ (n✝ + 1) ^ n - X) = 0
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
n : ℕ
inst✝¹ : NeZero n
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : x ∈ (cyclotomic n A).rootSet B
⊢ x ^ n = 1

Tactic:
refine (isRoot_of_unity_iff (NeZero.pos n) B).2 ?_

Goal state after:
case refine_1
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
n : ℕ
inst✝¹ : NeZero n
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : x ∈ (cyclotomic n A).rootSet B
⊢ ∃ i ∈ n.divisors, (cyclotomic i B).IsRoot x
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case pos
p : ℕ
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s = 0
hs : s = k
⊢ (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s

Tactic:
simp only [hp, hs] at hζ hirr hcycl ⊢

Goal state after:
case pos
p : ℕ
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hpri : Fact (Nat.Prime p)
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s = 0
hs : s = k
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
hcycl : IsCyclotomicExtension {2 ^ (k + 1)} K L
⊢ (Algebra.norm K) (ζ ^ 2 ^ k - 1) = ↑2 ^ 2 ^ k
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
hζ : ζ ^ n = 1
a : ℕ
⊢ (zmodChar n hζ) ↑a = ζ ^ (a % n)

Tactic:
zmodChar_apply,

Goal state after:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
hζ : ζ ^ n = 1
a : ℕ
⊢ ζ ^ (↑a).val = ζ ^ (a % n)
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: C : Type v
inst✝ : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ψ a = 1 → a = 0
⊢ ψ.IsPrimitive

Tactic:
intro a ha hf

Goal state after:
C : Type v
inst✝ : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ψ a = 1 → a = 0
a : ZMod n
ha : a ≠ 0
hf : ψ.mulShift a = 1
⊢ False
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
a : ZMod n
ha : (zmodChar n ⋯) a = 1
⊢ a = 0

Tactic:
zmodChar_apply,

Goal state after:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
a : ZMod n
ha : ζ ^ a.val = 1
⊢ a = 0
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Algebra K K'
inst✝ : Finite K'
this✝ : Finite K
this : Fintype K'ˣ
x✝ : K'ˣ
⊢ x✝ ∈ ↑(Units.map (Algebra.norm K)).ker ↔ x✝ ∈ ↑{a | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1}

Tactic:
simp [Units.ext_iff, ← (algebraMap K K').injective.eq_iff, algebraMap_norm_eq_pow]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : Fintype R
inst✝² : DecidableEq R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : ψ.IsPrimitive
h : ¬b = 0
⊢ ∑ x, ψ (b * x) = ↑0

Tactic:
exact mod_cast sum_eq_zero_of_ne_one (hψ h)

Goal state after:
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
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ζ : (cyclotomic n (cyclotomic n K).SplittingField).IsRoot ζ
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)

Tactic:
isRoot_cyclotomic_iff

Goal state after:
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
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
⊢ toCircle j = Circle.exp (2 * π * (↑j.val / ↑N))

Tactic:
by
  ext
  rw [toCircle_apply, Circle.coe_exp]
  push_cast
  congr; ring

Goal state after:
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'
h : ∀ (a : Rˣ), χ ↑a = χ' ↑a
a : R
ha : ¬IsUnit a
⊢ χ a = χ' a

Tactic:
· rw [map_nonunit χ ha, map_nonunit χ' ha]

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : Fintype M
inst✝¹ : DecidableEq M
R : Type u_2
inst✝ : CommMonoidWithZero R
ζ : Rˣ
hζ : ζ ∈ rootsOfUnity (Fintype.card Mˣ) R
g : Mˣ
hg : ∀ (x : Mˣ), x ∈ Subgroup.zpowers g
⊢ (ofRootOfUnity hζ hg) ↑g = ↑ζ

Tactic:
simp only [ofRootOfUnity, ofUnitHom_eq, equivToUnitHom_symm_coe,
    monoidHomOfForallMemZpowers_apply_gen]

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

Goal state before:
pp: S : Set ℕ
K : Type w
inst✝¹ : Field K
inst✝ : IsSepClosed K
h : ∀ a ∈ S, a ≠ 0 → NeZero ↑a
a : ℕ
ha : a ∈ S
ha' : a ≠ 0
this : NeZero ↑a
r : K
hr : (cyclotomic a K).IsRoot r
⊢ IsPrimitiveRoot r a

Tactic:
isRoot_cyclotomic_iff

Goal state after:
S : Set ℕ
K : Type w
inst✝¹ : Field K
inst✝ : IsSepClosed K
h : ∀ a ∈ S, a ≠ 0 → NeZero ↑a
a : ℕ
ha : a ∈ S
ha' : a ≠ 0
this : NeZero ↑a
r : K
hr : IsPrimitiveRoot r a
⊢ IsPrimitiveRoot r a
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
χ : MulChar R R'
hχ : χ.IsQuadratic
f : R' →+* R''
a : R
⊢ (χ.ringHomComp f) a = 0 ∨ (χ.ringHomComp f) a = 1 ∨ (χ.ringHomComp f) a = -1

Tactic:
rcases hχ a with (ha | ha | ha)

Goal state after:
case inl
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
χ : MulChar R R'
hχ : χ.IsQuadratic
f : R' →+* R''
a : R
ha : χ a = 0
⊢ (χ.ringHomComp f) a = 0 ∨ (χ.ringHomComp f) a = 1 ∨ (χ.ringHomComp f) a = -1

case inr.inl
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
χ : MulChar R R'
hχ : χ.IsQuadratic
f : R' →+* R''
a : R
ha : χ a = 1
⊢ (χ.ringHomComp f) a = 0 ∨ (χ.ringHomComp f) a = 1 ∨ (χ.ringHomComp f) a = -1

case inr.inr
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
χ : MulChar R R'
hχ : χ.IsQuadratic
f : R' →+* R''
a : R
ha : χ a = -1
⊢ (χ.ringHomComp f) a = 0 ∨ (χ.ringHomComp f) a = 1 ∨ (χ.ringHomComp f) a = -1
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: A : Type u
B : Type v
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension {n₁} A ↥C₁
h₂ : IsCyclotomicExtension {n₂} A ↥C₂
inst✝¹ : NeZero n₁
inst✝ : NeZero n₂
ζ₁ : ↥C₁
ζ₂ : ↥C₂
hζ₁ : IsPrimitiveRoot ((algebraMap (↥C₁) B) ζ₁) n₁
hζ₂ : IsPrimitiveRoot ((algebraMap (↥C₂) B) ζ₂) n₂
hζ :
  IsPrimitiveRoot
    ((algebraMap (↥C₁) B) ζ₁ ^ (n₁ / n₁.factorizationLCMLeft n₂) *
      (algebraMap (↥C₂) B) ζ₂ ^ (n₂ / n₁.factorizationLCMRight n₂))
    (n₁.lcm n₂)
⊢ IsCyclotomicExtension {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)

Tactic:
rw [sup_comm, (isCyclotomicExtension_singleton_iff_eq_adjoin n₁ C₁ hζ₁).mp h₁,
    (isCyclotomicExtension_singleton_iff_eq_adjoin n₂ C₂ hζ₂).mp h₂, ← adjoin_union,
    Set.union_singleton, hζ₁.adjoin_pair_eq A hζ₂ (NeZero.ne _) (NeZero.ne _) hζ]

Goal state after:
A : Type u
B : Type v
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension {n₁} A ↥C₁
h₂ : IsCyclotomicExtension {n₂} A ↥C₂
inst✝¹ : NeZero n₁
inst✝ : NeZero n₂
ζ₁ : ↥C₁
ζ₂ : ↥C₂
hζ₁ : IsPrimitiveRoot ((algebraMap (↥C₁) B) ζ₁) n₁
hζ₂ : IsPrimitiveRoot ((algebraMap (↥C₂) B) ζ₂) n₂
hζ :
  IsPrimitiveRoot
    ((algebraMap (↥C₁) B) ζ₁ ^ (n₁ / n₁.factorizationLCMLeft n₂) *
      (algebraMap (↥C₂) B) ζ₂ ^ (n₂ / n₁.factorizationLCMRight n₂))
    (n₁.lcm n₂)
⊢ IsCyclotomicExtension {n₁.lcm n₂} A
    ↥A[(algebraMap (↥C₁) B) ζ₁ ^ (n₁ / n₁.factorizationLCMLeft n₂) *
          (algebraMap (↥C₂) B) ζ₂ ^ (n₂ / n₁.factorizationLCMRight n₂)]
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
⊢ ∑ x, χ x * ↑(if x - 1 = 0 then Fintype.card R else 0) = ↑(Fintype.card R)

Tactic:
sub_eq_zero,

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, χ x * ↑(if x = 1 then Fintype.card R else 0) = ↑(Fintype.card R)
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
u : (ZMod N)ˣ
k : ZMod N
⊢ 𝓕 (fun j ↦ Φ (↑u * j)) k = 𝓕 Φ (↑u⁻¹ * k)

Tactic:
by
  refine Fintype.sum_equiv u.mulLeft _ _ fun x ↦ ?_
  simp only [mul_comm u.val, u.mulLeft_apply, ← mul_assoc, u.mul_inv_cancel_right]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : χ (-1) = 1
hq : χ.IsQuadratic
h₁ : (fun a ↦ ↑(χ₈ a) * τ ^ ↑a) = fun a ↦ χ a * ψ₈char a
⊢ ↑0 * τ ^ ↑0 + ↑1 * τ ^ ↑1 + ↑0 * τ ^ ↑2 + ↑(-1) * τ ^ 3 + ↑0 * τ ^ ↑4 + ↑(-1) * τ ^ ↑5 + ↑0 * τ ^ ↑6 + ↑1 * τ ^ ↑7 =
    2 * (τ - τ ^ 3)

Tactic:
show ((5 : Fin 8) : ℕ) = 5 from rfl,

Goal state after:
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : χ (-1) = 1
hq : χ.IsQuadratic
h₁ : (fun a ↦ ↑(χ₈ a) * τ ^ ↑a) = fun a ↦ χ a * ψ₈char a
⊢ ↑0 * τ ^ ↑0 + ↑1 * τ ^ ↑1 + ↑0 * τ ^ ↑2 + ↑(-1) * τ ^ 3 + ↑0 * τ ^ ↑4 + ↑(-1) * τ ^ 5 + ↑0 * τ ^ ↑6 + ↑1 * τ ^ ↑7 =
    2 * (τ - τ ^ 3)
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
⊢ (t₁ • (b -ᵥ a) +ᵥ a) -ᵥ (t₂ • (c -ᵥ a) +ᵥ a) = t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a)

Tactic:
vadd_vsub_vadd_cancel_right

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
⊢ t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a) = t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a)
Module: Mathlib.Analysis.Hofer

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

Tactic:
rwa [tendsto_add_atTop_iff_nat] at this

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

Goal state before:
pp: case hpq
ι : 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
⊢ 1 - k * p + ∑ i ∈ s, p = 1

Tactic:
simp only [sum_const, nsmul_eq_mul]

Goal state after:
case hpq
ι : 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
⊢ 1 - k * p + ↑(#s) * p = 1
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x y z : E
⊢ (adjoint comul) ((LinearMap.rTensor E (adjoint comul)) (x ⊗ₜ[𝕜] y ⊗ₜ[𝕜] z)) =
    (adjoint comul) (x ⊗ₜ[𝕜] (adjoint comul) (y ⊗ₜ[𝕜] z))

Tactic:
← comp_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x y z : E
⊢ (adjoint comul ∘ₗ LinearMap.rTensor E (adjoint comul)) (x ⊗ₜ[𝕜] y ⊗ₜ[𝕜] z) =
    (adjoint comul) (x ⊗ₜ[𝕜] (adjoint comul) (y ⊗ₜ[𝕜] z))
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x : E
⊢ (adjoint comul) ((LinearMap.rTensor E (adjoint counit)) (One.one ⊗ₜ[𝕜] x)) = x

Tactic:
← comp_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x : E
⊢ (adjoint comul ∘ₗ LinearMap.rTensor E (adjoint counit)) (One.one ⊗ₜ[𝕜] x) = x
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x : E
⊢ (adjoint comul) ((LinearMap.lTensor E (adjoint counit)) (x ⊗ₜ[𝕜] One.one)) = x

Tactic:
← comp_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x : E
⊢ (adjoint comul ∘ₗ LinearMap.lTensor E (adjoint counit)) (x ⊗ₜ[𝕜] One.one) = x
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x y : 𝕜
⊢ (adjoint counit) (x * y) = (adjoint comul) ((adjoint (map counit counit)) (x ⊗ₜ[𝕜] y))

Tactic:
← comp_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x y : 𝕜
⊢ (adjoint counit) (x * y) = (adjoint comul ∘ₗ adjoint (map counit counit)) (x ⊗ₜ[𝕜] y)
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
r : 𝕜
x : E
⊢ (adjoint comul) ((adjoint (LinearMap.rTensor E counit)) (r ⊗ₜ[𝕜] x)) =
    (adjoint comul) ((adjoint (LinearMap.lTensor E counit)) (x ⊗ₜ[𝕜] r))

Tactic:
← comp_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
r : 𝕜
x : E
⊢ (adjoint comul ∘ₗ adjoint (LinearMap.rTensor E counit)) (r ⊗ₜ[𝕜] x) =
    (adjoint comul ∘ₗ adjoint (LinearMap.lTensor E counit)) (x ⊗ₜ[𝕜] r)
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
r : 𝕜
x : E
⊢ r • x = (adjoint comul) ((adjoint (LinearMap.rTensor E counit)) (r ⊗ₜ[𝕜] x))

Tactic:
← comp_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
r : 𝕜
x : E
⊢ r • x = (adjoint comul ∘ₗ adjoint (LinearMap.rTensor E counit)) (r ⊗ₜ[𝕜] x)
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
⊢ 0 ≤ f ↔ f.IsPositive

Tactic:
simpa using le_def 0 f

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

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
ι : Type u_2
inst✝ : LinearOrder ι
v : ι → E
hv : Orthonormal ℝ v
s t : ↑(Set.powersetCard ι n)
⊢ (innerProductForm (ιMulti_family ℝ n v s)) (ιMulti_family ℝ n v t) = if s = t then 1 else 0

Tactic:
by
  simp only [ιMulti_family]
  split_ifs with h
  · subst h
    simp [gram_eq_one_iff_orthonormal.mpr (hv.comp _ (RelEmbedding.injective _))]
  · rw [innerProductForm_ιMulti_ιMulti]
    obtain ⟨x, hxt, hxs⟩ := (Set.powersetCard.exists_mem_notMem_iff_ne t s).mp (.symm h)
    simp only [Set.mem_range, not_exists,
      ← Set.powersetCard.mem_range_ofFinEmbEquiv_symm_iff_mem] at hxs hxt
    obtain ⟨i, rfl⟩ := hxt
    exact det_eq_zero_of_row_eq_zero i (fun j ↦ hv.inner_eq_zero (hxs j))

Goal state after:
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
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
i : ι
a✝ : i ∈ Finset.univ
⊢ HasCompactSupport (u ∘ update x i)

Tactic:
exact h2u.comp_isClosedEmbedding (isClosedEmbedding_update x i)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : E →L[𝕜] E
⊢ 0 ≤ f ↔ f.IsPositive

Tactic:
simpa using le_def 0 f

Goal state after:
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
⊢ 0 ≤ re ⟪↑T.symm x, x⟫

Tactic:
have := by simpa using hT.2 (T.symm.toLinearMap x)

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.Dynamics.BirkhoffSum.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝ : AddCommGroup G
f : α → α
g : α → G
n : ℕ
x : α
⊢ birkhoffSum f g n (f x) - birkhoffSum f g (n + 1) x + g (f^[n] x) =
    g (f^[n] x) - birkhoffSum f g (n + 1) x + birkhoffSum f g n (f x)

Tactic:
sub_add_comm

Goal state after:
α : Type u_1
G : Type u_2
inst✝ : AddCommGroup G
f : α → α
g : α → G
n : ℕ
x : α
⊢ g (f^[n] x) - birkhoffSum f g (n + 1) x + birkhoffSum f g n (f x) =
    g (f^[n] x) - birkhoffSum f g (n + 1) x + birkhoffSum f g n (f x)
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_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.LinearPMap

Goal state before:
pp: 𝕜 : 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
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
hT : Dense ↑T.domain
⊢ _root_.IsClosed ↑T.graph.adjoint

Tactic:
Submodule.adjoint

Goal state after:
𝕜 : 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
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
hT : Dense ↑T.domain
⊢ _root_.IsClosed
    ↑(Submodule.map (↑(WithLp.linearEquiv 2 𝕜 (F × E)))
        (Submodule.map (↑((LinearEquiv.skewSwap 𝕜 F E).symm.trans (WithLp.linearEquiv 2 𝕜 (F × E)).symm)) T.graph)ᗮ)