mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
hδ2 : ∀ ⦃a b : V⦄, ‖a - b‖ < δ → ‖f a - f b‖ < ε / ↑B
x : V
x✝ : x ∈ A
⊢ 1 / 2 / δ < ‖w‖

Tactic:
div_div

Goal state after:
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
hδ2 : ∀ ⦃a b : V⦄, ‖a - b‖ < δ → ‖f a - f b‖ < ε / ↑B
x : V
x✝ : x ∈ A
⊢ 1 / (2 * δ) < ‖w‖
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
ζ : R
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
⊢ Nat.card ↥(rootsOfUnity n R) = n

Tactic:
obtain ⟨ζ, hζ⟩ := h.isUnit NeZero.out

Goal state after:
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
ζ✝ : R
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ✝ n
ζ : Rˣ
hζ : ↑ζ = ζ✝
⊢ Nat.card ↥(rootsOfUnity n R) = n
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: case pos
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hfi : Integrable f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2
hg_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
⊢ ∀ᶠ (x : V) in cocompact V, dist (∫ (v : V), 𝐞 (-⟪v, x⟫) • f v) 0 < ε

Tactic:
refine
    ((Metric.tendsto_nhds.mp
            (tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support hg_cont
              hg_supp))
          _ (div_pos hε two_pos)).mp
      (Eventually.of_forall fun w hI => ?_)

Goal state after:
case pos
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hfi : Integrable f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2
hg_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
w : V
hI : dist (∫ (v : V), 𝐞 (-⟪v, w⟫) • g v) 0 < ε / 2
⊢ dist (∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) 0 < ε
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
⊢ 2 ≠ 1 ∧ 2 ∈ n.properDivisors

Tactic:
mem_properDivisors

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
⊢ 2 ≠ 1 ∧ 2 ∣ n ∧ 2 < n
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
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, Subtype.exists, ←
      NNReal.coe_lt_coe, ← Units.val_lt_val, Units.val_mk0 _, coe_nnnorm]
    simpa [hq'.le, Real.coe_toNNReal', max_eq_left, sub_nonneg] using hex

Goal state after:
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
h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
n : ℕ
hn1 : n ∈ S
hn2 : n ≠ 0
⊢ ∃ r, IsPrimitiveRoot r n

Tactic:
obtain ⟨r, hr1, hr2⟩ := h n hn1 hn2

Goal state after:
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
n : ℕ
hn1 : n ∈ S
hn2 : n ≠ 0
r : B
hr1 : r ^ n = 1
hr2 : ∀ (l : ℕ), r ^ l = 1 → n ∣ l
⊢ ∃ r, IsPrimitiveRoot r n
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n✝ : ℕ
inst✝⁴ : NeZero n✝
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n✝} A B
b : B
x✝ : b ∈ {b | ∃ n ∈ {n✝}, n ≠ 0 ∧ b ^ n = 1}
n : ℕ
hb : n = n✝ ∧ n ≠ 0 ∧ b ^ n = 1
⊢ eval₂ (algebraMap A B) b (X ^ n - 1) = 0

Tactic:
by simpa [sub_eq_zero] using hb.2.2

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

Goal state before:
pp: case refine_2
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 ∈ {ζ}
⊢ x ∈ (cyclotomic n A).rootSet B

Tactic:
simp only [mem_singleton_iff] at hx
    simpa only [hx, mem_rootSet', map_cyclotomic, ← eval_map_algebraMap, IsRoot] using
      And.intro (cyclotomic_ne_zero n B) (hζ.isRoot_cyclotomic (NeZero.pos n))

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
n : ℕ
inst✝¹ : NeZero n
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ A[ζ] = ⊤

Tactic:
← adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic hζ

Goal state after:
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
n : ℕ
inst✝¹ : NeZero n
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ adjoin A ((cyclotomic n A).rootSet B) = ⊤
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
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
x✝ : ↥A[ζ]
x : B
hx : x ∈ A[ζ]
b : B
hb✝ : b ∈ {ζ}
hb : b = ζ
⊢ n ≠ 0 ∧ ⟨ζ, ⋯⟩ ^ n = 1

Tactic:
rw [← Subalgebra.coe_eq_one, Subalgebra.coe_pow, Subtype.coe_mk]

Goal state after:
case refine_1
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
x✝ : ↥A[ζ]
x : B
hx : x ∈ A[ζ]
b : B
hb✝ : b ∈ {ζ}
hb : b = ζ
⊢ n ≠ 0 ∧ ζ ^ n = 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
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
x✝ : ↥A[ζ]
x : B
hx : x ∈ A[ζ]
⊢ ⟨x, hx⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
by
      refine
        adjoin_induction
          (hx := hx) (fun b hb => ?_) (fun a => ?_) (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)
          (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)
      · rw [Set.mem_singleton_iff] at hb
        refine subset_adjoin ?_
        simp only [mem_singleton_iff, exists_eq_left, mem_ofPred_eq, hb]
        rw [← Subalgebra.coe_eq_one, Subalgebra.coe_pow, Subtype.coe_mk]
        exact ⟨NeZero.ne n, ((IsPrimitiveRoot.iff_def ζ n).1 h).1⟩
      · exact Subalgebra.algebraMap_mem _ _
      · exact Subalgebra.add_mem _ hb₁ hb₂
      · exact Subalgebra.mul_mem _ hb₁ hb₂

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x✝ : ↥(rootsOfUnity n ℂ)
w : ℂˣ
hw : w ∈ rootsOfUnity n ℂ
j : ℕ
hj1 : j < n
hj2 : cexp (2 * ↑π * I * (↑j / ↑n)) = ↑w
⊢ ∃ a, (⇑(rootsOfUnityCircleEquiv n) ∘ ⇑(ZMod.rootsOfUnityAddChar n)) a = ⟨w, hw⟩

Tactic:
exact ⟨j, by simp [Units.ext_iff, Subtype.ext_iff, ← hj2, ZMod.toCircle_natCast, mul_div_assoc]⟩

Goal state after:
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
⊢ 1⁻¹ʳ = 1

Tactic:
Ring.inverse_one

Goal state after:
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
⊢ 1 = 1
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = -1
⊢ (-1) ^ p = -1

Tactic:
· exact neg_one_pow_char R' p

Goal state after:
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'
x a : R
x✝ : a ∈ univ
⊢ χ x * φ a * ψ (x + a) = χ x * φ (a + x - x) * ψ (a + x)

Tactic:
rw [add_sub_cancel_right, add_comm]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case zero
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ ψ ^ p ^ 0 = χ (↑p ^ 0) * gaussSum χ ψ

Tactic:
rw [pow_zero, pow_one, pow_zero, MulChar.map_one, one_mul]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
n : ℕ
ih : gaussSum χ ψ ^ p ^ n = χ (↑p ^ n) * gaussSum χ ψ
⊢ χ (↑p ^ n) ^ p * χ ↑p * gaussSum χ ψ = χ (↑p ^ n) * χ ↑p * gaussSum χ ψ

Tactic:
← pow_apply' χ fp.1.ne_zero ((p : R) ^ n),

Goal state after:
case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
n : ℕ
ih : gaussSum χ ψ ^ p ^ n = χ (↑p ^ n) * gaussSum χ ψ
⊢ (χ ^ p) (↑p ^ n) * χ ↑p * gaussSum χ ψ = χ (↑p ^ n) * χ ↑p * gaussSum χ ψ
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
⊢ (fun Φ k ↦ (↑N)⁻¹ • auxDFT Φ (-k)) (auxDFT Φ) = Φ

Tactic:
by
    simp only [auxDFT_auxDFT, neg_neg, ← mul_smul, inv_mul_cancel₀ (NeZero.ne _), one_smul]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
h : ∀ (x : H), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫‖
x : H
⊢ ‖x‖ * ↑c ≤ ‖f x‖

Tactic:
sq,

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * ‖x‖ * ↑c ≤ ‖⟪f x, x⟫‖
⊢ ‖x‖ * ↑c ≤ ‖f x‖
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case neg
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
⊢ eLpNorm u (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ

Tactic:
have h2n : (0 : ℝ) < n - 1 := by simp_rw [sub_pos]; exact hn.coe.lt

Goal state after:
case neg
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
⊢ eLpNorm u (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ
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
x : E
⊢ Tendsto (fun x_1 ↦ birkhoffAverage 𝕜 (⇑f) _root_.id x_1 x) atTop (𝓝 ↑(g x))

Tactic:
obtain ⟨y, hy, z, hz, rfl⟩ : ∃ y, g y = 0 ∧ ∃ z, IsFixedPt f z ∧ x = y + z :=
    ⟨x - g x, by simp [hg_proj], g x, (g x).2, by simp⟩

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
⊢ Tendsto (fun x ↦ birkhoffAverage 𝕜 (⇑f) _root_.id x (y + z)) atTop (𝓝 ↑(g (y + z)))
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
hS : ∀ m ∈ T.singularValues.support, m < finrank 𝕜 E
hT : (adjoint T ∘ₗ T).IsSymmetric
this : T.singularValues.support.attachFin hS = {i | ↑(hT.eigenvalues ⋯ i) = 0}ᶜ
⊢ T.singularValues.support.card = finrank 𝕜 ↥T.range

Tactic:
← T.singularValues.support.card_attachFin hS,

Goal state after:
𝕜 : 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
hS : ∀ m ∈ T.singularValues.support, m < finrank 𝕜 E
hT : (adjoint T ∘ₗ T).IsSymmetric
this : T.singularValues.support.attachFin hS = {i | ↑(hT.eigenvalues ⋯ i) = 0}ᶜ
⊢ (T.singularValues.support.attachFin hS).card = finrank 𝕜 ↥T.range
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
E' : Submodule 𝕜 E
F' : Submodule 𝕜 F
iE' : Module.Finite 𝕜 ↥E'
iF' : Module.Finite 𝕜 ↥F'
y : ↥E' ⊗[𝕜] ↥F'
hx : inner 𝕜 ((mapIncl E' F') y) ((mapIncl E' F') y) = 0
hz : {(mapIncl E' F') y} ⊆ ↑(mapIncl E' F').range
e : OrthonormalBasis (Fin (finrank 𝕜 ↥E')) 𝕜 ↥E'
f : OrthonormalBasis (Fin (finrank 𝕜 ↥F')) 𝕜 ↥F'
this : ∀ (i : Fin (finrank 𝕜 ↥E')) (j : Fin (finrank 𝕜 ↥F')), ((e.toBasis.tensorProduct f.toBasis).repr y) (i, j) = 0
⊢ y = 0

Tactic:
simp [(e.toBasis.tensorProduct f.toBasis).ext_elem_iff, this]

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

Goal state before:
pp: case mp
𝕜 : 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
h : T.singularValues = 0
⊢ T = 0

Tactic:
rw [← range_eq_bot, ← Submodule.finrank_eq_zero, ← Nat.le_zero,
      ← singularValues_eq_zero_iff_le_finrank_range, h, Finsupp.zero_apply]

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

Goal state before:
pp: F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖↑e.symm‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ ↑p
C₂ : ℝ≥0 := ‖↑e‖₊
v : E → F' := ⇑e ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this : eLpNorm v (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ v) (↑p) μ
h4v : ∀ (x : E), ‖fderiv ℝ v x‖ ≤ ↑C₂ * ‖fderiv ℝ u x‖
⊢ ↑C₁ * eLpNorm v (↑p') μ ≤ ↑C₁ * ↑C * eLpNorm (fderiv ℝ v) (↑p) μ

Tactic:
rw [mul_assoc]

Goal state after:
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖↑e.symm‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ ↑p
C₂ : ℝ≥0 := ‖↑e‖₊
v : E → F' := ⇑e ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this : eLpNorm v (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ v) (↑p) μ
h4v : ∀ (x : E), ‖fderiv ℝ v x‖ ≤ ↑C₂ * ‖fderiv ℝ u x‖
⊢ ↑C₁ * eLpNorm v (↑p') μ ≤ ↑C₁ * (↑C * eLpNorm (fderiv ℝ v) (↑p) μ)
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
⊢ f.normDet = ‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖

Tactic:
have hrank : finrank 𝕜 U = finrank 𝕜 f.range := by
    rw [finrank_eq_nat_card_basis bu.toBasis, finrank_eq_nat_card_basis bv.toBasis]
  have h : Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 f.range) := by
    rw [hrank]
    exact ⟨stdOrthonormalBasis 𝕜 f.range⟩
  simp only [normDet, h, ↓reduceDIte]
  rw [← basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix (stdOrthonormalBasis 𝕜 U).toBasis
    bu.toBasis h.some.toBasis bv.toBasis]
  have h1 : bu.toBasis.toMatrix (stdOrthonormalBasis 𝕜 U).toBasis *
      (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix bu.toBasis = 1 :=
    Basis.toMatrix_mul_toMatrix_flip _ _
  have h2 : (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix bu.toBasis *
      bu.toBasis.toMatrix (stdOrthonormalBasis 𝕜 U).toBasis = 1 :=
    Basis.toMatrix_mul_toMatrix_flip _ _
  rw [← Matrix.det_comm' h1 h2, ← Matrix.mul_assoc, Matrix.det_mul, norm_mul]
  suffices ‖(bu.toBasis.toMatrix (stdOrthonormalBasis 𝕜 U).toBasis *
      h.some.toBasis.toMatrix ⇑bv.toBasis).det‖ = 1 by
    rw [this, one_mul]
  refine CStarRing.norm_of_mem_unitary <| Matrix.det_of_mem_unitary ?_
  rw [Matrix.mem_unitaryGroup_iff, Matrix.star_eq_conjTranspose, Matrix.conjTranspose_mul,
    ← Matrix.mul_assoc, Matrix.mul_assoc (bu.toBasis.toMatrix (stdOrthonormalBasis 𝕜 U).toBasis)]
  simp

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
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
⊢ f.normDet = ‖((toMatrix bu.toBasis bv.toBasis) f).det‖

Tactic:
by_cases! hrank : finrank 𝕜 U = finrank 𝕜 f.range

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
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
⊢ f.normDet = ‖((toMatrix bu.toBasis bv.toBasis) f).det‖

case neg
𝕜 : 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 ι 𝕜 V
this : FiniteDimensional 𝕜 V
hrank : finrank 𝕜 U ≠ finrank 𝕜 ↥f.range
⊢ f.normDet = ‖((toMatrix bu.toBasis bv.toBasis) f).det‖
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case neg
𝕜 : 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 = ⊥
⊢ ↑(f.normDet ^ 2) = (Matrix.gram 𝕜 fun x ↦ f.rangeRestrict (b x)).det

Tactic:
· trans 0
    · simp [show f.normDet = 0 from (f.normDet_eq_zero_tfae.out 1 0).mp h]
    have hrank := (f.normDet_eq_zero_tfae.out 1 3).mp h
    symm
    contrapose! hrank with h0
    rw [finrank_eq_card_basis b.toBasis]
    exact (Matrix.linearIndependent_of_det_gram_ne_zero h0).fintype_card_le_finrank

Goal state after: