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

Goal state before:
pp: case intro
p✝¹ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝¹)
n✝ p✝ : ℕ
h_prime : Fact (Nat.Prime p✝)
n : ℕ
K✝ : Type u_1
inst✝⁵ : Field K✝
inst✝⁴ : Algebra (ZMod p✝) K✝
K : Type u_2
K' : Type u_3
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Finite K'
inst✝ : Algebra K K'
val✝ : Fintype K'
p : ℕ
hp : CharP K p
this : CharP K p
⊢ IsGalois K K'

Tactic:
have : CharP K' p := charP_of_injective_algebraMap' K p

Goal state after:
case intro
p✝¹ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝¹)
n✝ p✝ : ℕ
h_prime : Fact (Nat.Prime p✝)
n : ℕ
K✝ : Type u_1
inst✝⁵ : Field K✝
inst✝⁴ : Algebra (ZMod p✝) K✝
K : Type u_2
K' : Type u_3
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Finite K'
inst✝ : Algebra K K'
val✝ : Fintype K'
p : ℕ
hp : CharP K p
this✝ : CharP K p
this : CharP K' p
⊢ IsGalois K K'
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
K' : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field K'
inst✝³ : Fintype K
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
this✝ : CharP K p
this : CharP K' p
n : ℕ+
a : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
a' : Nat.Prime p
hK' : Fintype.card K' = p ^ ↑n'
⊢ K ≃ₐ[ZMod p] K'

Tactic:
hK,

Goal state after:
p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
K' : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field K'
inst✝³ : Fintype K
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
this✝ : CharP K p
this : CharP K' p
n : ℕ+
hKK' : p ^ ↑n = Fintype.card K'
a : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
a' : Nat.Prime p
hK' : Fintype.card K' = p ^ ↑n'
⊢ K ≃ₐ[ZMod p] K'
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝⁷ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑n
this✝¹ : NeZero ↑n
this✝ : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : (cyclotomic n K).degree ≠ 0
⊢ (map (algebraMap K (cyclotomic n K).SplittingField) (cyclotomic n K)).degree ≠ 0

Tactic:
by rwa [degree_map]

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

Goal state before:
pp: case refine_2
n : ℕ
inst✝⁷ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑n
this✝¹ : NeZero ↑n
this✝ : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : (cyclotomic n K).degree ≠ 0
ζ : (cyclotomic n K).SplittingField
hζ : IsPrimitiveRoot ζ n
⊢ ∀ (x : CyclotomicField n K), x ∈ adjoin K {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
← Algebra.eq_top_iff,

Goal state after:
case refine_2
n : ℕ
inst✝⁷ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑n
this✝¹ : NeZero ↑n
this✝ : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : (cyclotomic n K).degree ≠ 0
ζ : (cyclotomic n K).SplittingField
hζ : IsPrimitiveRoot ζ n
⊢ adjoin K {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1} = ⊤
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
ha : a ≠ 0
ζ : Rˣ
hζ₁ : ζ ∈ rootsOfUnity n R
hζ₂ : ↑ζ = χ a
⊢ ∃ k < n, χ a = μ ^ k

Tactic:
have hζ' : ζ.val ^ n = 1 := (mem_rootsOfUnity' n ↑ζ).mp hζ₁

Goal state after:
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
ha : a ≠ 0
ζ : Rˣ
hζ₁ : ζ ∈ rootsOfUnity n R
hζ₂ : ↑ζ = χ a
hζ' : ↑ζ ^ n = 1
⊢ ∃ k < n, χ a = μ ^ k
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
x✝ : χ.FactorsThrough 1
w✝ : 1 ∣ n
χ₀ : DirichletCharacter R 1
hχ₀ : χ = (changeLevel w✝) χ₀
⊢ χ = 1

Tactic:
rwa [level_one χ₀, changeLevel_one] at hχ₀

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ x, ∑ y, χ (y * x⁻¹) * ψ (y - x) = ↑(Fintype.card R)

Tactic:
simp_rw [gaussSum_mul_aux hχ ψ]

Goal state after:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ x, ∑ c, χ c * ψ (x * (c - 1)) = ↑(Fintype.card R)
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ HasFDerivAt (fun x ↦ ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
⊢ HasFDerivAt (fun x ↦ ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ HasFDerivAt (fun x ↦ ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x
Module: Mathlib.Order.Grade

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
s : Flag α
a b : ↥s
h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b
c : α
hac : ↑a < c
hcb : c < ↑b
d : α
hd : d ∈ s
⊢ c ≤ d ∨ d ≤ c

Tactic:
obtain hda | had := le_or_gt (⟨d, hd⟩ : s) a
  · exact .inr ((Subtype.coe_le_coe.2 hda).trans hac.le)
  obtain hbd | hdb := le_or_gt b ⟨d, hd⟩
  · exact .inl (hcb.le.trans hbd)
  · cases h had hdb

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
⊢ ContDiff ℝ 1 fun x ↦ ‖x‖ ^ p

Tactic:
rw [contDiff_one_iff_fderiv]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
⊢ (Differentiable ℝ fun x ↦ ‖x‖ ^ p) ∧
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (fderiv ℝ fun x ↦ ‖x‖ ^ p)
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
⊢ ContinuousAt (fderiv ℝ fun x ↦ ‖x‖ ^ p) x

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ ContinuousAt (fderiv ℝ fun x ↦ ‖x‖ ^ p) x

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : ¬x = 0
⊢ ContinuousAt (fderiv ℝ fun x ↦ ‖x‖ ^ p) x
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ Icc s t = {u ∈ t.powerset | s ⊆ u}

Tactic:
ext; simp [and_comm]

Goal state after:
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ Ico s t = {u ∈ t.ssubsets | s ⊆ u}

Tactic:
ext; simp [and_comm]

Goal state after:
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ Ioc s t = {u ∈ t.powerset | s ⊂ u}

Tactic:
ext; simp [and_comm]

Goal state after:
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ Ioo s t = {u ∈ t.ssubsets | s ⊂ u}

Tactic:
ext; simp [and_comm]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
this : q ⊔ qᗮ = ⊤
⊢ q ⊔ qᗮ ⊓ p = p

Tactic:
← sup_inf_assoc_of_le _ hq₂,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
this : q ⊔ qᗮ = ⊤
⊢ (q ⊔ qᗮ) ⊓ p = p
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
inst✝ : U.HasOrthogonalProjection
⊢ (U.starProjection ∘SL T ∘SL U.starProjection).IsPositive

Tactic:
simp only [isPositive_iff, IsSymmetric, toLinearMap_comp, LinearMap.coe_comp, coe_coe,
    Function.comp_apply, comp_apply]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
inst✝ : U.HasOrthogonalProjection
⊢ (∀ (x y : E), ⟪U.starProjection (T (U.starProjection x)), y⟫ = ⟪x, U.starProjection (T (U.starProjection y))⟫) ∧
    ∀ (x : E), 0 ≤ ⟪U.starProjection (T (U.starProjection x)), 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
T : E →L[𝕜] E
hT : T.IsPositive
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
⊢ (U.orthogonalProjectionOnto ∘SL T ∘SL U.subtypeL).IsPositive

Tactic:
simp only [isPositive_iff, IsSymmetric, toLinearMap_comp, LinearMap.coe_comp, coe_coe,
    Function.comp_apply, comp_apply]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
⊢ (∀ (x y : ↥U),
      ⟪U.orthogonalProjectionOnto (T (U.subtypeL x)), y⟫ = ⟪x, U.orthogonalProjectionOnto (T (U.subtypeL y))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪U.orthogonalProjectionOnto (T (U.subtypeL x)), 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 = 0

Tactic:
have : ‖x‖ ^ 2 * c = 0 := le_antisymm (by simpa only [hx (f x) ⟨x, rfl⟩, norm_zero] using h x)
    (by positivity)

Goal state after:
𝕜 : 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ᗮ
this : ‖x‖ ^ 2 * ↑c = 0
⊢ x = 0
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: case inr
X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℕ
h✝ : d₁ < d₂
s : Set X
h : μH[↑d₁] s = ⊤
⊢ (volume.addHaarScalarFactor μH[↑d₂] • μH[↑d₂]) s = 0 ∨ (volume.addHaarScalarFactor μH[↑d₁] • μH[↑d₁]) s = ⊤

Tactic:
right

Goal state after:
case inr
X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℕ
h✝ : d₁ < d₂
s : Set X
h : μH[↑d₁] s = ⊤
⊢ (volume.addHaarScalarFactor μH[↑d₁] • μH[↑d₁]) s = ⊤
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : EMetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : EMetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℕ
hf : Isometry f
⊢ map f μHE[d] = μHE[d].restrict (Set.range f)

Tactic:
simp_rw [euclideanHausdorffMeasure_def]
  rw [Measure.map_smul, map_hausdorffMeasure hf (by simp), Measure.restrict_smul]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: case e_f
V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
hs : Nonempty ↥s
t : Set P
ht : MeasurableSet t
p : ↥s
x : ↥s.direction
u : Set ↥(mk' (↑(x +ᵥ p)) s.directionᗮ) := Subtype.val ⁻¹' (t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ))
hu : MeasurableSet u
hinter : t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ) = Subtype.val '' u
hxp : ↑(x +ᵥ p) ∈ mk' (↑(x +ᵥ p)) s.directionᗮ
hrank : finrank ℝ ↥s.directionᗮ = finrank ℝ ↥(mk' (↑(x +ᵥ p)) s.directionᗮ).direction
⊢ volume (Prod.mk x ⁻¹' ⇑(s.direction.measurableEquivProd ↑p).symm ⁻¹' t) =
    μHE[finrank ℝ ↥s.directionᗮ] (Subtype.val '' u)

Tactic:
euclideanHausdorffMeasure_coe_image,

Goal state after:
case e_f
V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
hs : Nonempty ↥s
t : Set P
ht : MeasurableSet t
p : ↥s
x : ↥s.direction
u : Set ↥(mk' (↑(x +ᵥ p)) s.directionᗮ) := Subtype.val ⁻¹' (t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ))
hu : MeasurableSet u
hinter : t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ) = Subtype.val '' u
hxp : ↑(x +ᵥ p) ∈ mk' (↑(x +ᵥ p)) s.directionᗮ
hrank : finrank ℝ ↥s.directionᗮ = finrank ℝ ↥(mk' (↑(x +ᵥ p)) s.directionᗮ).direction
⊢ volume (Prod.mk x ⁻¹' ⇑(s.direction.measurableEquivProd ↑p).symm ⁻¹' t) = μHE[finrank ℝ ↥s.directionᗮ] u
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: E : Type u_4
F : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h : ContDiff ℝ 1 f
⊢ dimH (range f) = dimH (f '' univ)

Tactic:
rw [image_univ]

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.gram 𝕜 fun x ↦ f.rangeRestrict (b x)).det

Tactic:
rw [Matrix.gram_eq_conjTranspose_mul bv, Matrix.det_mul, Matrix.det_conjTranspose]

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) =
    star (Matrix.of fun i j ↦ (bv.repr (f.rangeRestrict (b j))).ofLp i).det *
      (Matrix.of fun i j ↦ (bv.repr (f.rangeRestrict (b j))).ofLp i).det
Module: Mathlib.Analysis.InnerProductSpace.Reproducing

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : RKHS 𝕜 H X V
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace V
x y : X
⊢ ‖kernel H x y‖ ^ 2 ≤ ‖kernel H x x‖ * ‖kernel H y y‖

Tactic:
by
  grw [norm_kernel_le]; simp [mul_pow]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] star

Tactic:
simp_rw [continuous_iff, star_apply, ContinuousLinearMap.star_eq_adjoint,
      ContinuousLinearMap.adjoint_inner_right, coe_toCLM]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
⊢ ∀ (x y : F),
    Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x_1 ↦ ⟪x_1 y, x⟫_𝕜
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inr
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
iso_smul : Isometry ⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v))
⊢ ‖‖v‖‖₊ ^ 1 • μH[1] (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) '' s) = ‖v‖₊ • μH[1] s

Tactic:
nnnorm_norm,

Goal state after:
case inr
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
iso_smul : Isometry ⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v))
⊢ ‖v‖₊ ^ 1 • μH[1] (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) '' s) = ‖v‖₊ • μH[1] s
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case refine_1.inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
h : 0 = ‖o.rightAngleRotationAux₁ x‖
⊢ ‖o.rightAngleRotationAux₁ x‖ ≤ ‖x‖

pp: case refine_1.inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
h : 0 < ‖o.rightAngleRotationAux₁ x‖
⊢ ‖o.rightAngleRotationAux₁ x‖ ≤ ‖x‖

Tactic:
· rw [← h]
          positivity

Goal state after:
case refine_1.inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
h : 0 < ‖o.rightAngleRotationAux₁ x‖
⊢ ‖o.rightAngleRotationAux₁ x‖ ≤ ‖x‖
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ 0 ≤ ⟪x, y⟫ ∧ (o.areaForm x) y = 0 ↔ SameRay ℝ x y

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : x = 0
⊢ 0 ≤ ⟪x, y⟫ ∧ (o.areaForm x) y = 0 ↔ SameRay ℝ x y

case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
⊢ 0 ≤ ⟪x, y⟫ ∧ (o.areaForm x) y = 0 ↔ SameRay ℝ x y
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖y‖ = 0
⊢ x = 0 ∨ y = 0

Tactic:
right

Goal state after:
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖y‖ = 0
⊢ y = 0
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
hf : MellinConvergent f s
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
inst✝² : SMulZeroClass 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : SMulCommClass ℂ 𝕜 E
c : 𝕜
⊢ MellinConvergent (fun t ↦ c • f t) s

Tactic:
simpa only [MellinConvergent, smul_comm] using! hf.smul c

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • f (t ^ a) = (↑(t ^ (a - 1)) * ↑(t ^ a) ^ (s / ↑a - 1)) • f (t ^ a)

Tactic:
← cpow_mul_ofReal_nonneg (le_of_lt ht),

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • f (t ^ a) = (↑(t ^ (a - 1)) * ↑t ^ (↑a * (s / ↑a - 1))) • f (t ^ a)
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • f (t ^ a) = (↑t ^ ↑(a - 1) * ↑(t ^ a) ^ (s / ↑a - 1)) • f (t ^ a)

Tactic:
← cpow_mul_ofReal_nonneg (le_of_lt ht),

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • f (t ^ a) = (↑t ^ ↑(a - 1) * ↑t ^ (↑a * (s / ↑a - 1))) • f (t ^ a)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case e'_9
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
hz' : -z ≠ 1
⊢ (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - ∑ j ∈ Finset.range n, (-1) ^ j * z ^ j

Tactic:
← mul_pow,

Goal state after:
case e'_9
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
hz' : -z ≠ 1
⊢ (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - ∑ x ∈ Finset.range n, (-1 * z) ^ x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: case succ
s✝ : ℂ
hs✝ : ∀ (m : ℕ), s✝ ≠ -↑m
n : ℕ
IH : ∀ (s : ℂ), -↑n < s.re → (∀ (m : ℕ), s ≠ -↑m) → DifferentiableAt ℂ Gamma s
s : ℂ
hsre : -↑(n + 1) < s.re
hs : ∀ (m : ℕ), s ≠ -↑m
hsne : s ≠ 0
⊢ DifferentiableAt ℂ Gamma s

Tactic:
specialize IH (s + 1) (by grind [add_re, one_re]) (fun m ↦ by grind [hs (m + 1)])

Goal state after:
case succ
s✝ : ℂ
hs✝ : ∀ (m : ℕ), s✝ ≠ -↑m
n : ℕ
s : ℂ
IH : DifferentiableAt ℂ Gamma (s + 1)
hsre : -↑(n + 1) < s.re
hs : ∀ (m : ℕ), s ≠ -↑m
hsne : s ≠ 0
⊢ DifferentiableAt ℂ Gamma s