mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
E : Type v := ⋯
z : E
hz : (cyclotomic n E).IsRoot z
⊢ (algebraMap K E) ((Algebra.norm K) (ζ - 1)) = (algebraMap K E) ↑(eval 1 (cyclotomic n ℤ))

Tactic:
let := IsCyclotomicExtension.finiteDimensional {n} K L

Goal state after:
n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝ : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this : FiniteDimensional K L := finiteDimensional {n} K L
⊢ (algebraMap K E) ((Algebra.norm K) (ζ - 1)) = (algebraMap K E) ↑(eval 1 (cyclotomic n ℤ))
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:
Subalgebra.coe_pow,

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: S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
⊢ Algebra.IsSeparable K L

Tactic:
by
  have := integral S K L
  have h := (IsCyclotomicExtension.iff_adjoin_eq_top S K L).1 ‹_› |>.2
  rw [← IntermediateField.adjoin_toSubalgebra_of_isAlgebraic
    fun b _ ↦ Algebra.IsAlgebraic.isAlgebraic b, ← IntermediateField.top_toSubalgebra] at h
  rw [← AlgEquiv.Algebra.isSeparable_iff <|
    (IntermediateField.equivOfEq (IntermediateField.toSubalgebra_injective h)).trans
      IntermediateField.topEquiv, IntermediateField.isSeparable_adjoin_iff_isSeparable]
  rintro b ⟨n, hn, h1, h2⟩
  have := NeZero.mk h1
  have := Polynomial.X_pow_sub_one_separable_iff.2 (neZero_of_mem' n S K L hn).out
  exact this.of_dvd <| minpoly.dvd K b <| by simp [h2]

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

Goal state before:
pp: case a
S : Set ℕ
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension S K L
M : Type u_1
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤
x : M
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : x ^ n = 1
⊢ x ∈ ↑(IntermediateField.adjoin K (⇑i '' {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))

Tactic:
have : NeZero n := ⟨h1⟩

Goal state after:
case a
S : Set ℕ
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension S K L
M : Type u_1
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsSepClosed M
this✝ : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤
x : M
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : x ^ n = 1
this : NeZero n
⊢ x ∈ ↑(IntermediateField.adjoin K (⇑i '' {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case right
S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
i : L ≃ₐ[K] ↥(IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
f : AlgebraicClosure K →ₐ[K] AlgebraicClosure K
x : AlgebraicClosure K
hx : ∃ x_1 ∈ (IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}).toSubalgebra, f x_1 = x
⊢ x ∈ IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

Tactic:
obtain ⟨y, hy, rfl⟩ := hx

Goal state after:
case right
S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
i : L ≃ₐ[K] ↥(IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
f : AlgebraicClosure K →ₐ[K] AlgebraicClosure K
y : AlgebraicClosure K
hy : y ∈ (IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}).toSubalgebra
⊢ f y ∈ IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
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✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x : CyclotomicField n K
hx : x ∈ adjoin A {b | b ^ n = 1}
y : CyclotomicField n K
hy : y ∈ {b | b ^ n = 1}
⊢ ↑(⟨y, ⋯⟩ ^ n) = 1

Tactic:
Subalgebra.coe_pow,

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✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x : CyclotomicField n K
hx : x ∈ adjoin A {b | b ^ n = 1}
y : CyclotomicField n K
hy : y ∈ {b | b ^ n = 1}
⊢ ↑⟨y, ⋯⟩ ^ n = 1
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✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x : CyclotomicField n K
hx : x ∈ adjoin A {b | b ^ n = 1}
y : CyclotomicField n K
hy : y ∈ {b | b ^ n = 1}
⊢ ⟨y, ⋯⟩ ^ n = 1

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

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
⊢ ∀ (a b : MulChar R R'), a * b = b * a

Tactic:
intro χ₁ χ₂

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ₁ χ₂ : MulChar R R'
⊢ χ₁ * χ₂ = χ₂ * χ₁
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
⊢ ∀ (a b : MulChar R R'), a * b = b * a

Tactic:
by
    intro χ₁ χ₂
    ext a
    simp only [mul_comm, Pi.mul_apply, MulChar.coeToFun_mul]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero n
ψ : DirichletCharacter R m
h : (changeLevel ⋯) χ = (changeLevel ⋯) ψ
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap ⋯).ker
⊢ (↑x).val ≡ 1 [MOD n.gcd m]

Tactic:
rwa [MonoidHom.mem_ker, Units.ext_iff, ZMod.unitsMap_val, ← ZMod.natCast_val,
      Units.val_one, ← Nat.cast_one, ZMod.natCast_eq_natCast_iff] at hx

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

Goal state before:
pp: 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ˣ
⊢ (χ ^ p) ↑x = χ ↑x

Tactic:
pow_apply_coe

Goal state after:
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ˣ
⊢ χ ↑x ^ p = χ ↑x
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: 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
⊢ χ ^ p = χ

Tactic:
by
  ext x
  rw [pow_apply_coe]
  rcases hχ x with (hx | hx | hx) <;> rw [hx]
  · rw [zero_pow (@Fact.out p.Prime).ne_zero]
  · rw [one_pow]
  · exact neg_one_pow_char R' p

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝³ : Field R
inst✝² : Fintype R
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
⊢ ∑ a ∈ {0}ᶜ, 1 a * ψ a + 1 = ∑ a ∈ {0}ᶜ, ψ a + ψ 0

Tactic:
by
    congr! <;> aesop (add simp MulChar.one_apply)

Goal state after:
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
h : ∀ {f : ZMod N → ℂ}, Function.Even f → Function.Even (𝓕 f)
⊢ Function.Even (𝓕 Φ) ↔ Function.Even Φ

Tactic:
refine ⟨fun hΦ x ↦ ?_, h⟩

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
h : ∀ {f : ZMod N → ℂ}, Function.Even f → Function.Even (𝓕 f)
hΦ : Function.Even (𝓕 Φ)
x : ZMod N
⊢ Φ (-x) = Φ x
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
h : ∀ {f : ZMod N → ℂ}, Function.Odd f → Function.Odd (𝓕 f)
⊢ Function.Odd (𝓕 Φ) ↔ Function.Odd Φ

Tactic:
refine ⟨fun hΦ x ↦ ?_, h⟩

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
h : ∀ {f : ZMod N → ℂ}, Function.Odd f → Function.Odd (𝓕 f)
hΦ : Function.Odd (𝓕 Φ)
x : ZMod N
⊢ Φ (-x) = -Φ x
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : 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
⊢ ∫⁻ (t : A i), (∫⋯∫⁻_{i}, f ∂μ) (X t) ^ p * (f (X t) ^ (1 - k * p) * ∏ j ∈ s, (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p) ∂μ i =
    (∫⋯∫⁻_{i}, f ∂μ) x ^ p * ∫⁻ (t : A i), f (X t) ^ (1 - k * p) * ∏ j ∈ s, (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p ∂μ i

Tactic:
by
              -- pull out this constant factor
              have : ∀ t, (∫⋯∫⁻_{i}, f ∂μ) (X t) = (∫⋯∫⁻_{i}, f ∂μ) x := by
                intro t
                rw [lmarginal_update_of_mem]
                exact Iff.mpr Finset.mem_singleton rfl
              simp_rw [this]
              rw [lintegral_const_mul]
              exact (hF₀.pow_const _).mul <| Finset.measurable_fun_prod _ fun _ _ ↦ hF₁.pow_const _

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
⊢ ContDiff ℝ 1 (u ∘ update x i)

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 hu.comp (by convert! contDiff_update 1 x i)

Goal state after:
ι : 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)
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: case pos
𝕜 : 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⟫‖
hx0 : x = 0
⊢ ‖x‖ * ↑c ≤ ‖f x‖

pp: case neg
𝕜 : 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⟫‖
hx0 : ¬x = 0
⊢ ‖x‖ * ↑c ≤ ‖f x‖

Tactic:
· simp [hx0]

Goal state after:
case neg
𝕜 : 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⟫‖
hx0 : ¬x = 0
⊢ ‖x‖ * ↑c ≤ ‖f 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
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫‖
h_anti : AntilipschitzWith c⁻¹ ⇑f
x : E
hx : x ∈ (↑f).rangeᗮ
⊢ ‖x‖ ^ 2 * ↑c ≤ 0

Tactic:
by simpa only [hx (f x) ⟨x, rfl⟩, norm_zero] using h x

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

Goal state before:
pp: V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ ∃ C, 0 < C ∧ AntilipschitzWith C ⇑(continuousLinearMapOfBilin B)

Tactic:
rcases coercive.bounded_below with ⟨C, C_pos, below_bound⟩
  refine ⟨C⁻¹.toNNReal, Real.toNNReal_pos.mpr (inv_pos.mpr C_pos), ?_⟩
  refine ContinuousLinearMap.antilipschitz_of_bound B♯ ?_
  simp_rw [Real.coe_toNNReal', max_eq_left_of_lt (inv_pos.mpr C_pos), ←
    inv_mul_le_iff₀ (inv_pos.mpr C_pos)]
  simpa using below_bound

Goal state after:
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
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
hcf : f.closure.toFun.ker = ⊥
⊢ ↑(Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph.topologicalClosure) =
    ↑(Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph).topologicalClosure

Tactic:
simp only [Submodule.topologicalClosure_coe, Submodule.map_coe, LinearEquiv.coe_coe,
    LinearEquiv.prodComm_apply]

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
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
hcf : f.closure.toFun.ker = ⊥
⊢ (fun a ↦ a.swap) '' closure[instTopologicalSpaceProd] ↑f.graph =
    closure[instTopologicalSpaceProd] ((fun a ↦ a.swap) '' ↑f.graph)
Module: Mathlib.Dynamics.BirkhoffSum.Average

Goal state before:
pp: R : Type u_1
α : Type u_2
M : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : α → α
g g' : α → M
⊢ birkhoffAverage R f (g - g') = birkhoffAverage R f g - birkhoffAverage R f g'

Tactic:
funext _ x
  simp [birkhoffAverage, birkhoffSum, smul_sub]

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
hT : Dense ↑T.domain
x : F × E
⊢ (∀ (a : E) (a_1 : a ∈ T.domain), ⟪↑T ⟨a, ⋯⟩, x.1⟫ - ⟪a, x.2⟫ = 0) → ∃ (x_1 : x.1 ∈ T†.domain), ↑T† ⟨x.1, ⋯⟩ = x.2

Tactic:
· intro h
    simp_rw [sub_eq_zero] at h
    have hx : x.fst ∈ T†.domain := by
      apply mem_adjoint_domain_of_exists
      use x.snd
      rintro ⟨a, ha⟩
      rw [← inner_conj_symm, ← h a ha, inner_conj_symm]
    use hx
    apply hT.eq_of_inner_right 𝕜
    rintro a ha
    rw [← h a ha, (adjoint_isFormalAdjoint hT).symm ⟨a, ha⟩ ⟨x.fst, hx⟩]

Goal state after:
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 y : E ⊗[𝕜] F
⊢ x = y ↔ ∀ (a : E) (b : F), inner 𝕜 (a ⊗ₜ[𝕜] b) x = inner 𝕜 (a ⊗ₜ[𝕜] b) y

Tactic:
simpa only [← inner_conj_symm x, ← inner_conj_symm y, starRingEnd_apply, star_inj] using
    TensorProduct.ext_iff_inner_right (x := x) (y := y)

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 →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ∀ (i j : Fin n),
    ‖f‖ ^ 2 • inner 𝕜 (e i) (e j) - (∑ i, Matrix.vecMulVec (A i) (star (A i))) i j = inner 𝕜 (f (e i)) (f (e j))
⊢ RCLike.re (∑ x, ∑ x_1, ‖f‖ ^ 2 • inner 𝕜 (e x_1) (e x) * inner 𝕜 (g x_1) (g x)) -
      RCLike.re (∑ x, ∑ x_1, (∑ i, Matrix.vecMulVec (A i) (star (A i))) x_1 x * inner 𝕜 (g x_1) (g x)) ≤
    RCLike.re (‖f‖ ^ 2 • ∑ x, ∑ i, inner 𝕜 (e i) (e x) * inner 𝕜 (g i) (g x))

Tactic:
Finset.smul_sum,

Goal state after:
𝕜 : 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 →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ∀ (i j : Fin n),
    ‖f‖ ^ 2 • inner 𝕜 (e i) (e j) - (∑ i, Matrix.vecMulVec (A i) (star (A i))) i j = inner 𝕜 (f (e i)) (f (e j))
⊢ RCLike.re (∑ x, ∑ x_1, ‖f‖ ^ 2 • inner 𝕜 (e x_1) (e x) * inner 𝕜 (g x_1) (g x)) -
      RCLike.re (∑ x, ∑ x_1, (∑ i, Matrix.vecMulVec (A i) (star (A i))) x_1 x * inner 𝕜 (g x_1) (g x)) ≤
    RCLike.re (∑ x, ∑ x_1, ‖f‖ ^ 2 • (inner 𝕜 (e x_1) (e x) * inner 𝕜 (g x_1) (g x)))
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 →L[𝕜] F
g : G →L[𝕜] H
⊢ ‖ContinuousLinearMap.rTensor H f‖ * ‖ContinuousLinearMap.lTensor E g‖ ≤ ‖f‖ * ‖g‖

Tactic:
ContinuousLinearMap.norm_rTensor_le,

Goal state after:
𝕜 : 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 →L[𝕜] F
g : G →L[𝕜] H
⊢ ‖f‖ * ‖ContinuousLinearMap.lTensor E g‖ ≤ ‖f‖ * ‖g‖
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
ι₁ : Type u_6
ι₂ : Type u_7
b₁ : ι₁ → E
b₂ : ι₂ → F
hb₁ : Orthonormal 𝕜 b₁
hb₂ : Orthonormal 𝕜 b₂
⊢ Orthonormal 𝕜 fun i ↦ b₁ i.1 ⊗ₜ[𝕜] b₂ i.2

Tactic:
rw [orthonormal_iff_ite]
  rintro ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
  simp [orthonormal_iff_ite.mp, hb₁, hb₂, ← ite_and, and_comm]

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 (⋃ i ∈ S, i) = ⨆ s ∈ S, dimH s

Tactic:
dimH_bUnion hS

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
S : Set (Set X)
hS : S.Countable
⊢ ⨆ i ∈ S, dimH i = ⨆ s ∈ S, dimH s
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case inr.refine_2
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
this : μH[↑(Fintype.card ι)] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
⊢ ENNReal.ofReal ((2 * r) ^ Fintype.card ι) ≠ ∞

Tactic:
· exact ENNReal.ofReal_ne_top

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

Goal state before:
pp: 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) → ℝ
⊢ ⇑e '' s ∈ 𝓝 (e x)

Tactic:
rw [← e.map_nhds_eq]

Goal state after:
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) → ℝ
⊢ ⇑e '' s ∈ Filter.map (⇑e) (𝓝 x)
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
f : U →ₗ[𝕜] V
c : 𝕜
hc : c = 0
⊢ (c • f).normDet = ‖c‖ ^ finrank 𝕜 U * f.normDet

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
f : U →ₗ[𝕜] V
c : 𝕜
hc : ¬c = 0
⊢ (c • f).normDet = ‖c‖ ^ finrank 𝕜 U * f.normDet

Tactic:
· nontriviality U
    simp [hc, zero_pow finrank_pos.ne.symm]

Goal state after:
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
f : U →ₗ[𝕜] V
c : 𝕜
hc : ¬c = 0
⊢ (c • f).normDet = ‖c‖ ^ finrank 𝕜 U * f.normDet
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: U : Type u_5
V : Type u_6
inst✝⁸ : NormedAddCommGroup U
inst✝⁷ : InnerProductSpace ℝ U
inst✝⁶ : FiniteDimensional ℝ U
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MeasurableSpace U
inst✝² : BorelSpace U
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : U →ₗ[ℝ] V
s : Set U
⊢ μH[↑(finrank ℝ U)] (⇑f '' s) = ENNReal.ofReal f.normDet * μH[↑(finrank ℝ U)] s

Tactic:
by
  by_cases h : f.ker = ⊥
  · have hrank : finrank ℝ ↥f.range = finrank ℝ U := (f.normDet_ne_zero_tfae.out 1 2).mp h
    obtain ⟨bv⟩ := (f.normDet_ne_zero_tfae.out 1 3).mp h
    let g : U ≃ₗᵢ[ℝ] f.range := (stdOrthonormalBasis ℝ U).equiv bv (Equiv.refl _)
    suffices μH[finrank ℝ U] ((f.range.subtypeₗᵢ.comp g.toLinearIsometry) ''
        ((g.symm.toLinearIsometry.toLinearMap ∘ₗ f.rangeRestrict) '' s)) =
        ENNReal.ofReal f.normDet * μH[finrank ℝ U] s by
      simpa [Set.image_image]
    rw [(LinearIsometry.isometry _).hausdorffMeasure_image (by simp),
      addHaar_image_linearMap μH[finrank ℝ U], ← normDet_eq_abs_det,
      normDet_comp_of_finrank_eq _ _ hrank.symm, g.symm.toLinearIsometry.normDet_eq_one]
    simp
  · suffices μH[finrank ℝ U] (f.range.subtypeₗᵢ '' (f.rangeRestrict '' s)) = 0 by
      simpa [(f.normDet_eq_zero_tfae.out 1 0).mp h, Set.image_image]
    rw [(LinearIsometry.isometry _).hausdorffMeasure_image (by simp)]
    have h : (finrank ℝ f.range : ℝ) < finrank ℝ U := by
      exact_mod_cast (f.normDet_eq_zero_tfae.out 1 3).mp h
    simp [Real.hausdorffMeasure_of_finrank_lt h]

Goal state after: