mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case succ
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ (∑ x ∈ (n + 1).divisorsAntidiagonal, μ x.1 • if x.2 = 0 then 0 else g x.2) = f (n + 1) ↔
    ∑ x ∈ (n + 1).divisorsAntidiagonal, μ x.1 • g x.2 = f (n + 1)

Tactic:
rw [sum_congr rfl fun x hx => ?_]

Goal state after:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
x : ℕ × ℕ
hx : x ∈ (n + 1).divisorsAntidiagonal
⊢ (μ x.1 • if x.2 = 0 then 0 else g x.2) = μ x.1 • g x.2
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
G : ℕ → R := fun n ↦ ∑ i ∈ n.divisors, f i
n : ℕ
hn : n > 0
⊢ n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
hnP

Goal state after:
case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
G : ℕ → R := fun n ↦ ∑ i ∈ n.divisors, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
⊢ ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
F : ℕ → R := fun n ↦ ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2
n : ℕ
hn : n > 0
⊢ n ∈ s → ∑ i ∈ n.divisors, f i = g n

Tactic:
hnP

Goal state after:
case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
F : ℕ → R := fun n ↦ ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2
n : ℕ
hn : n > 0
hnP : n ∈ s
⊢ ∑ i ∈ n.divisors, f i = g n
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case neg
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
⊢ (ζ ^ (↑i * i.gcdA k + ↑k * i.gcdB k)) ^ l = 1

Tactic:
zpow_add,

Goal state after:
case neg
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
⊢ (ζ ^ (↑i * i.gcdA k) * ζ ^ (↑k * i.gcdB k)) ^ l = 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case left
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
inst✝ : CommRing R
ζ : Rˣ
h✝ h : IsPrimitiveRoot ζ k
i : ZMod k
hi :
  (((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
        ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)
      i =
    0
⊢ i = 0

Tactic:
Subtype.ext_iff

Goal state after:
case left
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
inst✝ : CommRing R
ζ : Rˣ
h✝ h : IsPrimitiveRoot ζ k
i : ZMod k
hi :
  ↑((((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
          ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)
        i) =
    ↑0
⊢ i = 0
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case refine_2
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
hk0 : 0 < ↑k
i : ℤ := n % ↑k
i₀ : ℕ
hi₀ : ↑i₀ = i
⊢ ζ ^ i = ζ ^ (n % ↑k + ↑k * (n / ↑k))

Tactic:
zpow_add,

Goal state after:
case refine_2
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
hk0 : 0 < ↑k
i : ℤ := n % ↑k
i₀ : ℕ
hi₀ : ↑i₀ = i
⊢ ζ ^ i = ζ ^ (n % ↑k) * ζ ^ (↑k * (n / ↑k))
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (Int.castRingHom R) (cyclotomic n ℤ).leadingCoeff ≠ 0

Tactic:
simp only [(int_cyclotomic_spec n).right.right, eq_intCast, Monic.leadingCoeff, Int.cast_one,
    Ne, not_false_iff, one_ne_zero]

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

Goal state before:
pp: case refine_1.refine_2
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
S : Type u_7
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
ζ₁ ζ₂ : R
k₁ k₂ : ℕ
hζ₁ : IsPrimitiveRoot ζ₁ k₁
hζ₂ : IsPrimitiveRoot ζ₂ k₂
hk₁ : k₁ ≠ 0
hk₂ : k₂ ≠ 0
ζ : R
hζ : IsPrimitiveRoot ζ (k₁.lcm k₂)
this : NeZero (k₁.lcm k₂)
⊢ ζ₂ ∈ ↑S[ζ]

Tactic:
· obtain ⟨_, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one <|
        (hζ₂.pow_eq_one_iff_dvd _).mpr <| k₁.dvd_lcm_right k₂
      exact Subalgebra.pow_mem _ (Algebra.self_mem_adjoin_singleton S _) _

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

Goal state before:
pp: case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ φ k = #(primitiveRoots k R)

Tactic:
refine Finset.card_bij (fun i _ ↦ ζ ^ i) ?_ ?_ ?_

Goal state after:
case neg.refine_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ ∀ a ∈ {a ∈ range k | k.Coprime a}, ζ ^ a ∈ primitiveRoots k R

case neg.refine_2
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ ∀ a₁ ∈ {a ∈ range k | k.Coprime a}, ∀ a₂ ∈ {a ∈ range k | k.Coprime a}, ζ ^ a₁ = ζ ^ a₂ → a₁ = a₂

case neg.refine_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ ∀ b ∈ primitiveRoots k R, ∃ a, ∃ (_ : a ∈ {a ∈ range k | k.Coprime a}), ζ ^ a = b
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
⊢ #(primitiveRoots k R) = φ k

Tactic:
by_cases h0 : k = 0
  · simp [h0]
  have : NeZero k := ⟨h0⟩
  symm
  refine Finset.card_bij (fun i _ ↦ ζ ^ i) ?_ ?_ ?_
  · simp only [and_imp, mem_filter, mem_range]
    rintro i - hi
    rw [mem_primitiveRoots (Nat.pos_of_ne_zero h0)]
    exact h.pow_of_coprime i hi.symm
  · simp only [and_imp, mem_filter, mem_range]
    rintro i hi - j hj - H
    exact h.pow_inj hi hj H
  · simp only [exists_prop, mem_filter, mem_range]
    intro ξ hξ
    rw [mem_primitiveRoots (Nat.pos_of_ne_zero h0), h.isPrimitiveRoot_iff] at hξ
    rcases hξ with ⟨i, hin, hi, H⟩
    exact ⟨i, ⟨hin, hi.symm⟩, H⟩

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ : ℕ
⊢ IsPrimitiveRoot μ n✝ → Nat.Coprime 0 n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ 0)

Tactic:
intro h hn

Goal state after:
case refine_1
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ : ℕ
h : IsPrimitiveRoot μ n✝
hn : Nat.Coprime 0 n✝
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ 0)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
⊢ (cyclotomic n K).IsRoot μ ↔ IsPrimitiveRoot μ n

Tactic:
by
  -- in this proof, `o` stands for `orderOf μ`
  have hnpos : 0 < n := (NeZero.of_neZero_natCast K).out.bot_lt
  refine ⟨fun hμ => ?_, IsPrimitiveRoot.isRoot_cyclotomic hnpos⟩
  have hμn : μ ^ n = 1 := by
    rw [isRoot_of_unity_iff hnpos _]
    exact ⟨n, n.mem_divisors_self hnpos.ne', hμ⟩
  by_contra hnμ
  have ho : 0 < orderOf μ := (isOfFinOrder_iff_pow_eq_one.2 <| ⟨n, hnpos, hμn⟩).orderOf_pos
  have := pow_orderOf_eq_one μ
  rw [isRoot_of_unity_iff ho] at this
  obtain ⟨i, hio, hiμ⟩ := this
  replace hio := Nat.dvd_of_mem_divisors hio
  rw [IsPrimitiveRoot.not_iff] at hnμ
  rw [← orderOf_dvd_iff_pow_eq_one] at hμn
  have key : i < n := (Nat.le_of_dvd ho hio).trans_lt ((Nat.le_of_dvd hnpos hμn).lt_of_ne hnμ)
  have key' : i ∣ n := hio.trans hμn
  rw [← Polynomial.dvd_iff_isRoot] at hμ hiμ
  have hni : {i, n} ⊆ n.divisors := by simpa [Finset.insert_subset_iff, key'] using hnpos.ne'
  obtain ⟨k, hk⟩ := hiμ
  obtain ⟨j, hj⟩ := hμ
  have := prod_cyclotomic_eq_X_pow_sub_one hnpos K
  rw [← Finset.prod_sdiff hni, Finset.prod_pair key.ne, hk, hj] at this
  have hn := (X_pow_sub_one_separable_iff.mpr <| NeZero.natCast_ne n K).squarefree
  rw [← this, Squarefree] at hn
  specialize hn (X - C μ) ⟨(∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) * k * j, by ring⟩
  simp [Polynomial.isUnit_iff_degree_eq_zero] at hn

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

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

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

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

Goal state before:
pp: K : Type u_1
F : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
inst✝¹ : Field F
inst✝ : Algebra F K
⊢ (Polynomial.map (algebraMap F K) (X ^ Fintype.card K - X)).Splits

Tactic:
by
    have h : (X ^ Fintype.card K - X : K[X]).natDegree = Fintype.card K :=
      FiniteField.X_pow_card_sub_X_natDegree_eq K Fintype.one_lt_card
    rw [splits_iff_card_roots, Polynomial.map_sub, Polynomial.map_pow,
      map_X, h, FiniteField.roots_X_pow_card_sub_X K, ← Finset.card_def, Finset.card_univ]

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

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝ : Ring R
n : ℕ
h✝ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
h : eval 1 (cyclotomic n ℤ) = -1
⊢ eval 1 (cyclotomic n R) = 1

Tactic:
exfalso

Goal state after:
case inr.inr
R : Type u_1
inst✝ : Ring R
n : ℕ
h✝ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
h : eval 1 (cyclotomic n ℤ) = -1
⊢ False
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✝ : IsCyclotomicExtension S A B
⊢ Algebra.IsIntegral A B

Tactic:
rw [← (Subalgebra.equivOfEq _ _ ((IsCyclotomicExtension.iff_adjoin_eq_top S A B).1 ‹_›).2
    |>.trans Subalgebra.topEquiv).isIntegral_iff]

Goal state after:
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsCyclotomicExtension S A B
⊢ Algebra.IsIntegral A ↥(adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case inl.inr.inl
a : ℤ
ha : a ≠ 0
h : a < 0
⊢ IsUnit a.sign

Tactic:
simp only [Int.sign_eq_neg_one_of_neg h, IsUnit.neg_iff, isUnit_one]

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

Goal state before:
pp: n : ℕ
inst✝² : NeZero n
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
hm✝ : HasEnoughRootsOfUnity M n
e : ↥(rootsOfUnity n M) ≃* ↥(rootsOfUnity n N)
m : M
hm : IsPrimitiveRoot m n
⊢ ∃ m, IsPrimitiveRoot m n

Tactic:
use (e hm.toRootsOfUnity).val.val

Goal state after:
case h
n : ℕ
inst✝² : NeZero n
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
hm✝ : HasEnoughRootsOfUnity M n
e : ↥(rootsOfUnity n M) ≃* ↥(rootsOfUnity n N)
m : M
hm : IsPrimitiveRoot m n
⊢ IsPrimitiveRoot (↑↑(e hm.toRootsOfUnity)) n
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
x : Rˣ
h₁ : χ ↑x = 1
⊢ (χ ↑x)⁻¹ʳ = χ ↑x

pp: case inr.inr
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : χ ↑x = -1
⊢ (χ ↑x)⁻¹ʳ = χ ↑x

Tactic:
· rw [h₁, Ring.inverse_one]

Goal state after:
case inr.inr
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : χ ↑x = -1
⊢ (χ ↑x)⁻¹ʳ = χ ↑x
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:
(isCyclotomicExtension_singleton_iff_eq_adjoin n₁ C₁ hζ₁).mp 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 ↥(C₂ ⊔ A[(algebraMap (↥C₁) B) ζ₁])
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ (fun x' ↦ ‖x'‖ ^ p - ‖0‖ ^ p - 0 (x' - 0)) =o[𝓝 0] fun x' ↦ x' - 0

Tactic:
calc (fun x : E ↦ ‖x‖ ^ p - ‖(0 : E)‖ ^ p - 0)
        = (fun x : E ↦ ‖x‖ ^ p) := by simp [zero_lt_one.trans hp |>.ne']
      _ = (fun x : E ↦ ‖x‖ * ‖x‖ ^ (p - 1)) := by
          ext x
          rw [← rpow_one_add' (norm_nonneg x) (by positivity)]
          ring_nf
      _ =o[𝓝 0] (fun x : E ↦ ‖x‖ * 1) := by
        refine (isBigO_refl _ _).mul_isLittleO <| (isLittleO_const_iff <| by simp).mpr ?_
        convert! continuousAt_id.norm.rpow_const (.inr h2p.le) |>.tendsto
        simp [h2p.ne']
      _ =O[𝓝 0] (fun (x : E) ↦ x - 0) := by
        simp_rw [mul_one, isBigO_norm_left (f' := fun x ↦ x), sub_zero, isBigO_refl]

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
p q : E →ₗ[𝕜] E
hp : p.IsSymmetricProjection
hq : q.IsSymmetricProjection
x✝ : p ≤ q
a : E
ha : a ∈ p.range
h1 : (q - p).IsSymmetric
hh : ∀ {T : E →ₗ[𝕜] E}, T.IsSymmetricProjection → re ⟪T a, a⟫ = ‖T a‖ ^ 2
h2 : ‖a‖ ^ 2 ≤ ‖q a‖ ^ 2
⊢ a ∈ q.range

Tactic:
sq_le_sq,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : p.IsSymmetricProjection
hq : q.IsSymmetricProjection
x✝ : p ≤ q
a : E
ha : a ∈ p.range
h1 : (q - p).IsSymmetric
hh : ∀ {T : E →ₗ[𝕜] E}, T.IsSymmetricProjection → re ⟪T a, a⟫ = ‖T a‖ ^ 2
h2 : |‖a‖| ≤ |‖q a‖|
⊢ a ∈ q.range
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
hf : f.IsClosable
hfg : g ≤ f
⊢ g.IsClosable

Tactic:
obtain ⟨f', hf⟩ := hf

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : f.graph.topologicalClosure = f'.graph
⊢ g.IsClosable
Module: Mathlib.Dynamics.BirkhoffSum.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
f : α → α
g : α → M
m n : ℕ
x : α
⊢ birkhoffSum f g (m + n) x = birkhoffSum f g m x + birkhoffSum f g n (f^[m] x)

Tactic:
birkhoffSum,

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
f : α → α
g : α → M
m n : ℕ
x : α
⊢ ∑ k ∈ range (m + n), g (f^[k] x) = ∑ k ∈ range m, g (f^[k] x) + ∑ k ∈ range n, g (f^[k] (f^[m] x))
Module: Mathlib.Dynamics.BirkhoffSum.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
f : α → α
g : α → M
m n : ℕ
x : α
⊢ birkhoffSum f g (m + n) x = birkhoffSum f g m x + birkhoffSum f g n (f^[m] x)

Tactic:
simp_rw [birkhoffSum, sum_range_add, add_comm m, iterate_add_apply]

Goal state after:
Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace

Goal state before:
pp: case h
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace X
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε : ∀ (x y : X), (x, y) ∈ {p | edist p.1 p.2 ≤ δ} → (g x, g y) ∈ {p | dist p.1 p.2 ≤ ε}
x y : X
h : edist x y < δ
n k : ℕ
a✝ : k ∈ Finset.range n
⊢ dist (g (f^[k] x)) (g (f^[k] y)) ≤ ε

Tactic:
refine hδε _ _ ?_

Goal state after:
case h
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace X
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε : ∀ (x y : X), (x, y) ∈ {p | edist p.1 p.2 ≤ δ} → (g x, g y) ∈ {p | dist p.1 p.2 ≤ ε}
x y : X
h : edist x y < δ
n k : ℕ
a✝ : k ∈ Finset.range n
⊢ (f^[k] x, f^[k] y) ∈ {p | edist p.1 p.2 ≤ δ}
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

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
x x' : E
y y' : F
⊢ ‖x ⊗ₜ[𝕜] y - x' ⊗ₜ[𝕜] y'‖ ≤ ‖x‖ * ‖y‖ + ‖x'‖ * ‖y'‖

Tactic:
norm_sub_le

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
x x' : E
y y' : F
⊢ ‖x ⊗ₜ[𝕜] y‖ + ‖x' ⊗ₜ[𝕜] y'‖ ≤ ‖x‖ * ‖y‖ + ‖x'‖ * ‖y'‖
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : ⨆ d, ⨆ (_ : μH[↑d] s = ∞), ↑d < ↑d
d' : ℝ≥0
hsd' : ⨆ d, ⨆ (_ : μH[↑d] s = ∞), ↑d < ↑d'
hd'd : ↑d' < ↑d
⊢ μH[↑d] s = 0

Tactic:
exact (hausdorffMeasure_zero_or_top hd'd s).resolve_right fun h₂ => hsd'.not_ge <|
    le_iSup₂ (α := ℝ≥0∞) d' h₂

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
S : Set (Set X)
hS : S.Countable
⊢ dimH (⋃₀ S) = ⨆ s ∈ S, dimH s

Tactic:
by
  rw [sUnion_eq_biUnion, dimH_bUnion hS]

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case refine_2
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ ↑(finrank ℝ E) ≤ dimH (⇑e '' s)

Tactic:
have : e '' s ∈ 𝓝 (e x) := by rw [← e.map_nhds_eq]; exact image_mem_map h

Goal state after:
case refine_2
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
this : ⇑e '' s ∈ 𝓝 (e x)
⊢ ↑(finrank ℝ E) ≤ dimH (⇑e '' s)
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : InnerProductSpace 𝕜 W
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
⊢ (g ∘ₗ f).normDet = (g.domRestrict f.range).normDet * f.normDet

Tactic:
by
  by_cases hf : f.ker = ⊥
  · let bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
    obtain ⟨bv⟩ := (f.normDet_ne_zero_tfae.out 1 3).mp hf
    by_cases hgf : (g ∘ₗ f).ker = ⊥
    · obtain ⟨bw⟩ := ((g ∘ₗ f).normDet_ne_zero_tfae.out 1 3).mp hgf
      let bw' : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 (g.domRestrict f.range).range :=
        bw.map (LinearIsometryEquiv.ofEq _ _ (by simp [LinearMap.range_comp]))
      rw [(g ∘ₗ f).normDet_eq_norm_det_toMatrix_rangeRestrict bu bw,
        f.normDet_eq_norm_det_toMatrix_rangeRestrict bu bv,
        (g.domRestrict f.range).normDet_eq_norm_det_toMatrix_rangeRestrict bv bw']
      rw [← norm_mul, ← Matrix.det_mul, ← LinearMap.toMatrix_comp]
      rfl
    · have hg : (g.domRestrict f.range).ker ≠ ⊥ := by
        contrapose hf with hgf'
        rw [← LinearMap.ker_rangeRestrict, ← LinearMap.ker_comp_of_ker_eq_bot _ hgf']
        exact hgf
      simp [normDet_eq_zero_iff_ker_ne_bot.mpr hgf, normDet_eq_zero_iff_ker_ne_bot.mpr hg]
  · have hgf : (g ∘ₗ f).ker ≠ ⊥ := by
      contrapose hf with hbot
      simpa [hbot] using ker_le_ker_comp f g
    simp [normDet_eq_zero_iff_ker_ne_bot.mpr hf, normDet_eq_zero_iff_ker_ne_bot.mpr hgf]

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

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup U
inst✝⁴ : InnerProductSpace 𝕜 U
inst✝³ : FiniteDimensional 𝕜 U
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : FiniteDimensional 𝕜 V
f : U →ₗ[𝕜] V
⊢ f.normDet = ∏ i ∈ Finset.range (finrank 𝕜 U), f.singularValues i

Tactic:
← sq_eq_sq₀ f.normDet_nonneg (Finset.prod_nonneg fun i _ ↦ f.singularValues_nonneg i),

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup U
inst✝⁴ : InnerProductSpace 𝕜 U
inst✝³ : FiniteDimensional 𝕜 U
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : FiniteDimensional 𝕜 V
f : U →ₗ[𝕜] V
⊢ f.normDet ^ 2 = (∏ i ∈ Finset.range (finrank 𝕜 U), f.singularValues i) ^ 2
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℝ
hd : 0 < d
⊢ NullSingletonClass μH[d]

Tactic:
refine ⟨fun x => ?_⟩
  rw [← nonpos_iff_eq_zero, hausdorffMeasure_apply]
  refine iSup₂_le fun ε _ => iInf₂_le_of_le (fun _ => {x}) ?_ <| iInf_le_of_le (fun _ => ?_) ?_
  · exact subset_iUnion (fun _ => {x} : ℕ → Set X) 0
  · simp only [ediam_singleton, zero_le]
  · simp [hd]

Goal state after: