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

Goal state before:
pp: case mpr
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ) → IsPrimitiveRoot ζ n

pp: case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n → ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ

Tactic:
· rintro ⟨i, -, hi, rfl⟩; exact isPrimitiveRoot_exp_of_coprime i n hn hi

Goal state after:
case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n → ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : ↑l' = -l
⊢ ζ ^ (-l) = 1⁻¹ ↔ ζ ^ l' = 1

Tactic:
← hl',

Goal state after:
case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : ↑l' = -l
⊢ ζ ^ ↑l' = 1⁻¹ ↔ ζ ^ l' = 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ cyclotomic' n K =
    (cyclotomic' n K * ∏ x ∈ n.properDivisors, cyclotomic' x K) /ₘ ∏ i ∈ n.properDivisors, cyclotomic' i K

Tactic:
(div_modByMonic_unique (cyclotomic' n K) 0 prod_monic _).1

Goal state after:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ cyclotomic' n K = cyclotomic' n K

K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ 0 + (∏ i ∈ n.properDivisors, cyclotomic' i K) * cyclotomic' n K =
      cyclotomic' n K * ∏ x ∈ n.properDivisors, cyclotomic' x K ∧
    degree 0 < (∏ i ∈ n.properDivisors, cyclotomic' i K).degree
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := ⋯
hfrob : map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) ((expand ℤ p) Q)
⊢ minpoly ℤ μ ∣ (expand ℤ p) Q

Tactic:
exact minpoly_dvd_expand h hdiv

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

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
h : Nat.card ↥(rootsOfUnity n R) = n
ζ : Rˣ
hζ' : ζ ∈ rootsOfUnity n R
hζ : IsPrimitiveRoot (↑⟨ζ, hζ'⟩) n
⊢ ∃ ζ, IsPrimitiveRoot ζ n

Tactic:
← IsPrimitiveRoot.coe_units_iff

Goal state after:
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
h : Nat.card ↥(rootsOfUnity n R) = n
ζ : Rˣ
hζ' : ζ ∈ rootsOfUnity n R
hζ : IsPrimitiveRoot (↑↑⟨ζ, hζ'⟩) n
⊢ ∃ ζ, IsPrimitiveRoot ζ n
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ n.divisors
h : (cyclotomic i R).IsRoot ζ
⊢ ζ ^ n = 1

Tactic:
by
  rcases n.eq_zero_or_pos with (rfl | hn)
  · exact pow_zero _
  have := congr_arg (eval ζ) (prod_cyclotomic_eq_X_pow_sub_one hn R).symm
  rw [eval_sub, eval_X_pow, eval_one] at this
  convert! eq_add_of_sub_eq' this
  convert! (add_zero (M := R) _).symm
  apply eval_eq_zero_of_dvd_of_eval_eq_zero _ h
  exact Finset.dvd_prod_of_mem _ hi

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

Goal state before:
pp: M : Type u_7
inst✝¹ : CommMonoid M
n : ℕ
inst✝ : NeZero n
a : ZMod n
ha : a ≠ 0
ζ : M
hζ : IsPrimitiveRoot ζ n
⊢ n = Nat.card (Multiplicative (ZMod n))

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_multiplicative, card]

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

Goal state before:
pp: S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
⊢ ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (B.gen ^ n)) i)

Tactic:
by
  intro i
  nontriviality S
  let Q := X ^ n %ₘ minpoly R B.gen
  have : B.gen ^ n = aeval B.gen Q := by
    rw [← @aeval_X_pow R _ _ _ _ B.gen, ← modByMonic_add_div (X ^ n) (minpoly R B.gen)]
    simp [Q]
  by_cases hQ : Q = 0
  · simp [this, hQ, isIntegral_zero]
  have hlt : Q.natDegree < B.dim := by
    rw [← B.natDegree_minpoly, hmin, (minpoly.monic hB).natDegree_map,
      natDegree_lt_natDegree_iff hQ]
    let : Nontrivial R := Nontrivial.of_polynomial_ne hQ
    exact degree_modByMonic_lt _ (minpoly.monic hB)
  rw [this, aeval_eq_sum_range' hlt]
  simp only [map_sum, Finset.sum_apply']
  refine IsIntegral.sum _ fun j hj => ?_
  replace hj := Finset.mem_range.1 hj
  rw [← Fin.val_mk hj, ← B.basis_eq_pow, Algebra.smul_def, IsScalarTower.algebraMap_apply R S A, ←
    Algebra.smul_def, map_smul]
  simp only [algebraMap_smul, Finsupp.coe_smul, Pi.smul_apply, B.basis.repr_self_apply]
  by_cases hij : (⟨j, hj⟩ : Fin _) = i
  · simp only [hij, if_true]
    rw [Algebra.smul_def, mul_one]
    exact isIntegral_algebraMap
  · simp [hij, isIntegral_zero]

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

Goal state before:
pp: case inr
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
⊢ (expand ℤ p) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ

Tactic:
refine eq_of_monic_of_dvd_of_natDegree_le (cyclotomic.monic _ ℤ)
    ((cyclotomic.monic n ℤ).expand hp.pos) ?_ ?_

Goal state after:
case inr.refine_1
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
⊢ cyclotomic (n * p) ℤ ∣ (expand ℤ p) (cyclotomic n ℤ)

case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
⊢ ((expand ℤ p) (cyclotomic n ℤ)).natDegree ≤ (cyclotomic (n * p) ℤ).natDegree
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

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

Tactic:
by
  convert! aeval_zeta n A B using 0
  rw [IsRoot.def, aeval_def, eval₂_eq_eval_map, map_cyclotomic]

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
⊢ Algebra.adjoin F ↑univ = ⊤

Tactic:
coe_univ,

Goal state after:
K : Type u_1
F : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
inst✝¹ : Field F
inst✝ : Algebra F K
⊢ Algebra.adjoin F Set.univ = ⊤
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case e'_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ q = ‖q‖

Tactic:
Real.norm_of_nonneg (zero_le_one.trans_lt hq').le

Goal state after:
case e'_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ q = q
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
h : 0 ≤ -ζ.re ∧ (-ζ).im = 0
⊢ False

Tactic:
neg_nonneg,

Goal state after:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
h : ζ.re ≤ 0 ∧ (-ζ).im = 0
⊢ False
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

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

Tactic:
refine ⟨fun h => not_imp_comm.mp (@hψ a) ?_, fun ha => by rw [ha, map_zero_eq_one]⟩
  rw [zmod_char_ne_one_iff n (mulShift ψ a), mulShift_apply, mul_one, h, Classical.not_not]

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

Goal state before:
pp: 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 (↑hm.toRootsOfUnity) n

Tactic:
← IsPrimitiveRoot.coe_units_iff

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 (↑↑hm.toRootsOfUnity) n
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 4 → χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1
⊢ χ₄ ↑(n % ↑4) = if n % 4 % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1

Tactic:
exact help (n % 4) (Int.emod_nonneg n (by lia)) (Int.emod_lt_abs n (by lia))

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
⊢ ∃ r, IsPrimitiveRoot r a

Tactic:
have := h a ha ha'

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, IsPrimitiveRoot r a
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
⊢ χ = 1 ↔ ∀ (a : Rˣ), χ ↑a = 1

Tactic:
by
  simp only [MulChar.ext_iff, one_apply_coe]

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

Goal state before:
pp: R' : Type u_2
inst✝² : CommRing R'
R'' : Type u_3
inst✝¹ : CommRing R''
R : Type u_4
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
f : R' →+* R''
a✝ : Rˣ
⊢ (χ.ringHomComp f)⁻¹ ↑a✝ = (χ⁻¹.ringHomComp f) ↑a✝

Tactic:
simp only [inv_apply, Ring.inverse_unit, ringHomComp_apply]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
χ : MulChar R R'
f : R' →+* R''
⊢ χ.ringHomComp f ^ 0 = (χ ^ 0).ringHomComp f

Tactic:
simp only [pow_zero, ringHomComp_one]

Goal state after:
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₂
this : NeZero n₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot ((algebraMap (↥C₂) B) ζ₂) n₂
d : ℕ
hd : n₂ = n₁ * d
⊢ n₂ = ?m.112 * ?m.113

Tactic:
rwa [mul_comm]

Goal state after:
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
⊢ auxDFT (Φ₁ + Φ₂) = auxDFT Φ₁ + auxDFT Φ₂

Tactic:
ext; simp only [auxDFT, Pi.add_def, smul_add, sum_add_distrib]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
f : α → α
φ : α → M
h : φ ∘ f = φ
n : ℕ
⊢ birkhoffSum f φ n = n • φ

Tactic:
funext x
  suffices ∀ k, φ (f^[k] x) = φ x by simp [birkhoffSum, this]
  intro k
  exact congrFun (iterate_invariant h k) x

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
i : ℕ
⊢ 0 < T.singularValues i ↔ T.singularValues i ≠ 0

Tactic:
grind [T.singularValues_nonneg i]

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 →ₗᵢ[𝕜] G
g : F →ₗᵢ[𝕜] H
x y : E ⊗[𝕜] F
⊢ inner 𝕜 ((map f.toLinearMap g.toLinearMap) 0) ((map f.toLinearMap g.toLinearMap) y) = inner 𝕜 0 y

Tactic:
by simp [inner_def]

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 →ₗᵢ[𝕜] G
g : F →ₗᵢ[𝕜] H
x y : E ⊗[𝕜] F
⊢ ∀ (x : E) (y : F),
    inner 𝕜 ((map f.toLinearMap g.toLinearMap) (x ⊗ₜ[𝕜] y)) ((map f.toLinearMap g.toLinearMap) 0) =
      inner 𝕜 (x ⊗ₜ[𝕜] y) 0

Tactic:
by simp [inner_def]

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
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
a : E ⊗[𝕜] F
x✝³ : G
c : E ⊗[𝕜] F
x✝² : G
x✝¹ x✝ : E ⊗[𝕜] F
h1 :
  inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (x✝¹ ⊗ₜ[𝕜] x✝³)) ((TensorProduct.assoc 𝕜 E F G) (c ⊗ₜ[𝕜] x✝²)) =
    inner 𝕜 (x✝¹ ⊗ₜ[𝕜] x✝³) (c ⊗ₜ[𝕜] x✝²)
h2 :
  inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (x✝ ⊗ₜ[𝕜] x✝³)) ((TensorProduct.assoc 𝕜 E F G) (c ⊗ₜ[𝕜] x✝²)) =
    inner 𝕜 (x✝ ⊗ₜ[𝕜] x✝³) (c ⊗ₜ[𝕜] x✝²)
⊢ inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) ((x✝¹ + x✝) ⊗ₜ[𝕜] x✝³)) ((TensorProduct.assoc 𝕜 E F G) (c ⊗ₜ[𝕜] x✝²)) =
    inner 𝕜 ((x✝¹ + x✝) ⊗ₜ[𝕜] x✝³) (c ⊗ₜ[𝕜] x✝²)

Tactic:
simp only [add_tmul, inner_add_left, map_add, h1, h2]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case insert
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
s : ι → Set X
i : ι
I : Finset ι
hiI : i ∉ I
ihI : (∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)) → μ (⋃ i ∈ I, s i) = ∑ i ∈ I, μ (s i)
hI : ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ I → ∀ (j : ι), j = i ∨ j ∈ I → i_1 ≠ j → AreSeparated (s i_1) (s j)
⊢ μ (⋃ i_1 ∈ insert i I, s i_1) = ∑ i ∈ insert i I, μ (s i)

Tactic:
rw [Finset.set_biUnion_insert, hm, ihI, Finset.sum_insert hiI]

Goal state after:
case insert
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
s : ι → Set X
i : ι
I : Finset ι
hiI : i ∉ I
ihI : (∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)) → μ (⋃ i ∈ I, s i) = ∑ i ∈ I, μ (s i)
hI : ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ I → ∀ (j : ι), j = i ∨ j ∈ I → i_1 ≠ j → AreSeparated (s i_1) (s j)
⊢ ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)

case insert.a
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
s : ι → Set X
i : ι
I : Finset ι
hiI : i ∉ I
ihI : (∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)) → μ (⋃ i ∈ I, s i) = ∑ i ∈ I, μ (s i)
hI : ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ I → ∀ (j : ι), j = i ∨ j ∈ I → i_1 ≠ j → AreSeparated (s i_1) (s j)
⊢ AreSeparated (s i) (⋃ x ∈ I, s x)
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:
rw [ENNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hd'd

Goal state after:
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
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℕ
r : 𝕜
hr : r ≠ 0
s : Set E
⊢ μHE[d] (r • s) = ‖r‖₊ ^ d • μHE[d] s

Tactic:
rw [euclideanHausdorffMeasure_def, Measure.smul_apply, hausdorffMeasure_smul₀ (by simp) hr,
    Measure.smul_apply, smul_comm]

Goal state after:
𝕜 : Type u_3
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℕ
r : 𝕜
hr : r ≠ 0
s : Set E
⊢ ‖r‖₊ ^ ↑d • volume.addHaarScalarFactor μH[↑d] • μH[↑d] s = ‖r‖₊ ^ d • volume.addHaarScalarFactor μH[↑d] • μH[↑d] s
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
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 ↥f.range
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
h : Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
h1 : bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis * (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis = 1
h2 : (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis * bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis = 1
⊢ ‖(bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis * h.some.toBasis.toMatrix ⇑bv.toBasis *
          (toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖ =
    ‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖

Tactic:
Matrix.det_mul,

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
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 ↥f.range
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
h : Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
h1 : bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis * (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis = 1
h2 : (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis * bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis = 1
⊢ ‖(bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis * h.some.toBasis.toMatrix ⇑bv.toBasis).det *
        ((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖ =
    ‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
hf : ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, HolderOnWith C r f t
⊢ dimH (f '' s) ≤ dimH s / ↑r

Tactic:
by
  choose! C t htn hC using hf
  rcases countable_cover_nhdsWithin htn with ⟨u, hus, huc, huU⟩
  replace huU := inter_eq_self_of_subset_left huU; rw [inter_iUnion₂] at huU
  rw [← huU, image_iUnion₂, dimH_bUnion huc, dimH_bUnion huc]; simp only [ENNReal.iSup_div]
  exact iSup₂_mono fun x hx => ((hC x (hus hx)).mono inter_subset_right).dimH_image_le hr

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

Goal state before:
pp: case pos
𝕜 : 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
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
b : OrthonormalBasis ι 𝕜 U
h : f.ker = ⊥
bv : OrthonormalBasis ι 𝕜 ↥f.range := orthonormalBasis_range h b
⊢ ↑(f.normDet ^ 2) =
    ((Matrix.of fun i j ↦ (bv.repr (f.rangeRestrict (b j))).ofLp i).conjTranspose *
        Matrix.of fun i j ↦ (bv.repr (f.rangeRestrict (b j))).ofLp i).det

Tactic:
Matrix.det_mul,

Goal state after:
case pos
𝕜 : 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
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
b : OrthonormalBasis ι 𝕜 U
h : f.ker = ⊥
bv : OrthonormalBasis ι 𝕜 ↥f.range := orthonormalBasis_range h b
⊢ ↑(f.normDet ^ 2) =
    (Matrix.of fun i j ↦ (bv.repr (f.rangeRestrict (b j))).ofLp i).conjTranspose.det *
      (Matrix.of fun i j ↦ (bv.repr (f.rangeRestrict (b j))).ofLp i).det
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝³ : EMetricSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst✝ : ∀ (n : β), Countable (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
⊢ (mkMetric m) s ≤ liminf (fun n ↦ ∑' (i : ι n), m (ediam (t n i))) l

Tactic:
simp only [mkMetric_apply]

Goal state after:
X : Type u_2
inst✝³ : EMetricSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst✝ : ∀ (n : β), Countable (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
⊢ ⨆ r,
      ⨆ (_ : 0 < r),
        ⨅ t,
          ⨅ (_ : s ⊆ iUnion t),
            ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)) ≤
    liminf (fun n ↦ ∑' (i : ι n), m (ediam (t n i))) l
Module: Mathlib.Analysis.InnerProductSpace.OfNorm

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y : E
⊢ Continuous fun r ↦ inner_ 𝕜 (↑r • x) y

Tactic:
exact (continuous_ofReal.smul continuous_const).inner_ continuous_const

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

Goal state before:
pp: case mp
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
h : ∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0
y : H
hy : y ∈ S
hiy : y ∈ S → inner ℝ (I • y) x = 0
⊢ ⟪y, x⟫.im = 0

Tactic:
simpa [inner_real_eq_re_inner] using! hiy hy

Goal state after: