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
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
v : V
hv : R + 1 < ‖v‖
⊢ 1 / 2 ≤ ‖w‖

Tactic:
refine le_trans (le_add_of_nonneg_right <| one_div_nonneg.mpr <| ?_) hw_bd

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
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
v : V
hv : R + 1 < ‖v‖
⊢ 0 ≤ 2 * δ
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
S : Type u_7
F : Type u_8
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
ζ : R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
f : F
hf : Function.Injective ⇑f
⊢ Subgroup.map (Units.map ↑f) (rootsOfUnity n R) = rootsOfUnity n S

Tactic:
let : CommMonoid Sˣ := inferInstance
  replace hζ := hζ.isUnit_unit NeZero.out
  rw [← hζ.zpowers_eq,
    ← (hζ.map_of_injective (Units.map_injective (f := (f : R →* S)) hf)).zpowers_eq,
    MonoidHom.map_zpowers]

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

Goal state before:
pp: K : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
⊢ ∃! P, map (Int.castRingHom K) P = cyclotomic' (↑n) K

Tactic:
obtain ⟨P, hP⟩ := int_coeff_of_cyclotomic' h

Goal state after:
K : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
P : ℤ[X]
hP : map (Int.castRingHom K) P = cyclotomic' (↑n) K ∧ P.degree = (cyclotomic' (↑n) K).degree ∧ P.Monic
⊢ ∃! P, map (Int.castRingHom K) P = cyclotomic' (↑n) K
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ X - 1 = map (Int.castRingHom R) (X - 1)

Tactic:
simp only [map_X, Polynomial.map_one, Polynomial.map_sub]

Goal state after:
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
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 : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • g v) - 0‖ < ε / 2
⊢ ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) - ∫ (v : V), 𝐞 (-⟪v, w⟫) • g v‖ ≤ ∫ (x : V), ‖f x - g x‖

Tactic:
← integral_sub ((Real.fourierIntegral_convergent_iff w).2 hfi)
      ((Real.fourierIntegral_convergent_iff w).2 (hg_cont.integrable_of_hasCompactSupport hg_supp)),

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
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 : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • g v) - 0‖ < ε / 2
⊢ ‖∫ (a : V), 𝐞 (-⟪a, w⟫) • f a - 𝐞 (-⟪a, w⟫) • g a ∂volume‖ ≤ ∫ (x : V), ‖f x - g x‖
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
⊢ ∑ i, ↑(α i) * ζ ^ ↑i = 0 ↔ ∀ (i j : Fin p), α i = α j

Tactic:
have hP (i : Fin p) : α i = P.coeff i := by simp [P, ← Fin.ext_iff]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
⊢ ∑ i, ↑(α i) * ζ ^ ↑i = 0 ↔ ∀ (i j : Fin p), α i = α j
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : eval ((Nat.castRingHom (ZMod p)) a) (cyclotomic n (ZMod p)) = 0
h : ↑a = 0
⊢ False

Tactic:
eq_natCast,

Goal state after:
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : eval (↑a) (cyclotomic n (ZMod p)) = 0
h : ↑a = 0
⊢ False
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case h
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 (∏ i ∈ n.divisors.erase 1, cyclotomic i R) = eval x (∑ i ∈ range n, X ^ i)
⊢ 0 < eval x (cyclotomic n R)

Tactic:
← cons_self_properDivisors hn'.ne',

Goal state after:
case h
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 (∏ i ∈ (cons n n.properDivisors ⋯).erase 1, cyclotomic i R) = eval x (∑ i ∈ range n, X ^ i)
⊢ 0 < eval x (cyclotomic n R)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
this✝ : Fact (Nat.Prime p)
t : ℤ
this :
  ↑n =
    ↑p ^ padicValNat p n * ↑p *
      (t *
        ∏ x ∈ (n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ))
ht : eval 1 (cyclotomic n ℤ) = ↑p * t
⊢ False

Tactic:
have : (p : ℤ) ^ padicValNat p n * p ∣ n := ⟨_, this⟩

Goal state after:
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
this✝¹ : Fact (Nat.Prime p)
t : ℤ
this✝ :
  ↑n =
    ↑p ^ padicValNat p n * ↑p *
      (t *
        ∏ x ∈ (n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ))
ht : eval 1 (cyclotomic n ℤ) = ↑p * t
this : ↑p ^ padicValNat p n * ↑p ∣ ↑n
⊢ False
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝ : Nontrivial R
a : ℤ
⊢ χ ↑a ≠ 0 ↔ IsCoprime a ↑n

Tactic:
by
  rw [MulChar.apply_ne_zero_iff, ZMod.coe_int_isUnit_iff_isCoprime, isCoprime_comm]

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : Odd n
hχ : χ ^ n = 1
⊢ χ (-1) ^ n = 1

Tactic:
← χ.pow_apply' (Nat.ne_of_odd_add hn),

Goal state after:
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : Odd n
hχ : χ ^ n = 1
⊢ (χ ^ n) (-1) = 1
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s : Multiset α
a : α
h : s ⋖ a ::ₘ s
⊢ s.card ⋖ (a ::ₘ s).card

Tactic:
card_cons

Goal state after:
α : Type u_1
s : Multiset α
a : α
h : s ⋖ a ::ₘ s
⊢ s.card ⋖ s.card + 1
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁ : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
n' : ℕ+
hp' : Nat.Prime (ringChar F')
hc' : Fintype.card F' = ringChar F' ^ ↑n'
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
hchar : ringChar F' = ringChar FF'
⊢ (χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2) = χ ↑(Fintype.card F')

Tactic:
apply (algebraMap F' FF').injective

Goal state after:
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁ : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
n' : ℕ+
hp' : Nat.Prime (ringChar F')
hc' : Fintype.card F' = ringChar F' ^ ↑n'
ψ : PrimitiveAddChar F F' := ⋯
FF' : Type u_2 := ⋯
hchar : ringChar F' = ringChar FF'
⊢ (algebraMap F' FF') ((χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2)) =
    (algebraMap F' FF') (χ ↑(Fintype.card F'))
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ (u ∈ if s ⊆ t then map { toFun := fun u ↦ (↑u).disjUnion s ⋯, inj' := ⋯ } (t \ s).powerset.attach else ∅) ↔
    s ⊆ u ∧ u ⊆ t

Tactic:
by_cases hst : s ⊆ t

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
hst : s ⊆ t
⊢ (u ∈ if s ⊆ t then map { toFun := fun u ↦ (↑u).disjUnion s ⋯, inj' := ⋯ } (t \ s).powerset.attach else ∅) ↔
    s ⊆ u ∧ u ⊆ t

case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
hst : ¬s ⊆ t
⊢ (u ∈ if s ⊆ t then map { toFun := fun u ↦ (↑u).disjUnion s ⋯, inj' := ⋯ } (t \ s).powerset.attach else ∅) ↔
    s ⊆ u ∧ u ⊆ t
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case refine_2
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
⊢ ¬ψ₈.char 1 ^ 4 = 1

Tactic:
rw [← map_nsmul_eq_pow ψ₈.char, ψ₈.prim.zmod_char_eq_one_iff]
      decide

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

Goal state before:
pp: case h₂.hg
ι : 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 := ⋯
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ⋯
hk' : 0 ≤ 1 - k * p
⊢ AEMeasurable (fun a ↦ f (X a)) (μ i)

Tactic:
exact hF₀.aemeasurable

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
n : ℕ
x : E
⊢ 0 ≤ ↑n * re ⟪x, x⟫

Tactic:
positivity [inner_self_nonneg (x := x) (𝕜 := 𝕜)]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst✝¹ : U.HasOrthogonalProjection
inst✝ : V.HasOrthogonalProjection
⊢ U.starProjection = V.starProjection ↔ U = V

Tactic:
by
  simp only [le_antisymm_iff, ← starProjection_le_starProjection_iff]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: case h'
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : E
h1 : x ∈ (f.closure.domRestrict f.domain).domain
h2 : x ∈ f.domain
⊢ ↑(f.closure.domRestrict f.domain) ⟨x, h1⟩ = ↑f ⟨x, h2⟩

Tactic:
let z : f.closure.domain := ⟨x, f.le_closure.1 h2⟩

Goal state after:
case h'
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : E
h1 : x ∈ (f.closure.domRestrict f.domain).domain
h2 : x ∈ f.domain
z : ↥f.closure.domain := ⟨x, ⋯⟩
⊢ ↑(f.closure.domRestrict f.domain) ⟨x, h1⟩ = ↑f ⟨x, h2⟩
Module: Mathlib.Dynamics.BirkhoffSum.Average

Goal state before:
pp: R : Type u_1
α : Type u_2
M : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α → α
g : α → M
h : g ∘ f = g
n : ℕ
hn : ↑n ≠ 0
x : α
⊢ (↑n)⁻¹ • n • g x = g x

Tactic:
rw [← Nat.cast_smul_eq_nsmul (R := R), ← mul_smul, inv_mul_cancel₀ hn, one_smul]

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

Goal state before:
pp: X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
⊢ μHE[0] = μH[0]

Tactic:
let basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) :=
    EuclideanSpace.basisFun (Fin 0) ℝ

Goal state after:
X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
⊢ μHE[0] = μH[0]
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
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace G
inst✝² : CompleteSpace (E ⊗[𝕜] G)
inst✝¹ : CompleteSpace (F ⊗[𝕜] G)
inst✝ : CompleteSpace F
f : E →L[𝕜] F
⊢ ContinuousLinearMap.adjoint (ContinuousLinearMap.rTensor G f) =
    ContinuousLinearMap.rTensor G (ContinuousLinearMap.adjoint f)

Tactic:
simp [ContinuousLinearMap.rTensor_eq_mapL]

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

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
s t : Set X
⊢ ⨆ i, dimH (bif i then s else t) = max (dimH s) (dimH t)

Tactic:
iSup_bool_eq,

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
s t : Set X
⊢ max (dimH (bif true then s else t)) (dimH (bif false then s else t)) = max (dimH s) (dimH t)
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
K : ℝ≥0
f : X → Y
hf : AntilipschitzWith K f
s : Set Y
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f ⁻¹' s) = ∞
this : μH[↑d] (f ⁻¹' s) ≤ ↑K ^ ↑d * μH[↑d] s
⊢ μH[↑d] s = ∞

Tactic:
rw [hd, top_le_iff] at this

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
K : ℝ≥0
f : X → Y
hf : AntilipschitzWith K f
s : Set Y
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f ⁻¹' s) = ∞
this : ↑K ^ ↑d * μH[↑d] s = ∞
⊢ μH[↑d] s = ∞
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: 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
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction = 1
⊢ μHE[finrank ℝ V] t = ‖v‖ₑ * ∫⁻ (x : ℝ), μHE[finrank ℝ V - 1] (t ∩ ↑(AffineSubspace.mk' (x • v +ᵥ p) (ℝ ∙ v)ᗮ))

Tactic:
have hrank' : finrank ℝ (AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ V - 1 := by
    rw [← (AffineSubspace.mk' p (ℝ ∙ v)).direction.finrank_add_finrank_orthogonal, hrank,
      Nat.add_sub_cancel_left]

Goal state after:
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
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction = 1
hrank' : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ V - 1
⊢ μHE[finrank ℝ V] t = ‖v‖ₑ * ∫⁻ (x : ℝ), μHE[finrank ℝ V - 1] (t ∩ ↑(AffineSubspace.mk' (x • v +ᵥ p) (ℝ ∙ v)ᗮ))
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
m : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hc' : c ≠ 0
⊢ ⨆ r, ⨆ (_ : r > 0), boundedBy (extend fun s x ↦ (c • m) (ediam s)) =
    ⨆ i, ⨆ (_ : i > 0), c • boundedBy (extend fun s x ↦ m (ediam s))

Tactic:
smul_boundedBy hc,

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
m : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hc' : c ≠ 0
⊢ ⨆ r, ⨆ (_ : r > 0), boundedBy (extend fun s x ↦ (c • m) (ediam s)) =
    ⨆ i, ⨆ (_ : i > 0), boundedBy (c • extend fun s x ↦ m (ediam s))
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
μ : Measure X
ε : ℝ≥0∞
h₀ : 0 < ε
h : ∀ (s : Set X), ediam s ≤ ε → μ s ≤ m (ediam s)
⊢ μ.toOuterMeasure ≤ (mkMetric m).toOuterMeasure

Tactic:
mkMetric_toOuterMeasure

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
μ : Measure X
ε : ℝ≥0∞
h₀ : 0 < ε
h : ∀ (s : Set X), ediam s ≤ ε → μ s ≤ m (ediam s)
⊢ μ.toOuterMeasure ≤ OuterMeasure.mkMetric m
Module: Mathlib.Analysis.InnerProductSpace.OfNorm

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ (starRingEnd 𝕜) (inner_ 𝕜 y x) = inner_ 𝕜 x y

Tactic:
simp only [inner_, map_sub, map_add, map_mul, map_inv₀, map_ofNat, conj_ofReal, conj_I]
  rw [add_comm y x, norm_sub_rev]
  by_cases hI : (I : 𝕜) = 0
  · simp only [hI, neg_zero, zero_mul]
  have hI' := I_mul_I_of_nonzero hI
  have I_smul (v : E) : ‖(I : 𝕜) • v‖ = ‖v‖ := by rw [norm_smul, norm_I_of_ne_zero hI, one_mul]
  have h₁ : ‖(I : 𝕜) • y - x‖ = ‖(I : 𝕜) • x + y‖ := by
    convert I_smul ((I : 𝕜) • x + y)
    linear_combination (norm := module) -hI' • x
  have h₂ : ‖(I : 𝕜) • y + x‖ = ‖(I : 𝕜) • x - y‖ := by
    convert (I_smul ((I : 𝕜) • y + x)).symm
    linear_combination (norm := module) -hI' • y
  rw [h₁, h₂]
  ring

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

Goal state before:
pp: case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
⊢ ∀ (i : ℕ → Set X), {x} ⊆ ⋃ n, i n → (∀ (n : ℕ), ediam (i n) ≤ 1) → 1 ≤ ∑' (n : ℕ), ⨆ (_ : (i n).Nonempty), 1

Tactic:
intro t hst _

Goal state after:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
t : ℕ → Set X
hst : {x} ⊆ ⋃ n, t n
i✝ : ∀ (n : ℕ), ediam (t n) ≤ 1
⊢ 1 ≤ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), 1
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
inst✝ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
h : K.IsHermitian
f : X →₀ V →L[𝕜] V
⊢ IsSelfAdjoint (f.sum fun i xi ↦ f.sum fun j xj ↦ star xi * K i j * xj)

Tactic:
simp only [mul_assoc, isSelfAdjoint_iff, star_finsuppSum, Pi.star_apply, star_mul, h.apply,
    star_star]
  rw [Finsupp.sum_comm]

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

Goal state before:
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‖ * ‖o.rightAngleRotationAux₁ x‖ ≤ ‖x‖ * ‖o.rightAngleRotationAux₁ x‖

Tactic:
rw [← real_inner_self_eq_norm_mul_norm, o.inner_rightAngleRotationAux₁_left]

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.areaForm x) (o.rightAngleRotationAux₁ x) ≤ ‖x‖ * ‖o.rightAngleRotationAux₁ x‖
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: f : ℝ → ℂ
s a : ℂ
⊢ mellin (fun t ↦ f t / a) s = mellin f s / a

Tactic:
simp_rw [mellin, smul_eq_mul, ← mul_div_assoc, integral_div]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ ∀ (n : ℕ) (s : ℂ), -↑n < s.re → (∀ (m : ℕ), s ≠ -↑m) → DifferentiableAt ℂ Gamma s

Tactic:
intro n s hsre hs

Goal state after:
s✝ : ℂ
hs✝ : ∀ (m : ℕ), s✝ ≠ -↑m
n : ℕ
s : ℂ
hsre : -↑n < s.re
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ DifferentiableAt ℂ Gamma s
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z ↦ log (1 + z) - logTaylor (n + 1) z
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)

Tactic:
let f' (z : ℂ) : ℂ := (-z) ^ n * (1 + z)⁻¹

Goal state after:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z ↦ log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z ↦ (-z) ^ n * (1 + z)⁻¹
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun x ↦ ↑x * g x) atTop (𝓝 t)
⊢ (fun x ↦ (↑x * g x) ^ 2 * ↑x⁻¹) =O[atTop] fun x ↦ ↑x⁻¹

Tactic:
simpa using isBigO_const_of_tendsto hg (one_ne_zero (α := ℂ))
        |>.pow 2 |>.mul (isBigO_refl _ _)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1) ∂volume) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1) ∂volume
hst : 0 < (s + t).re
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
this : cexp (-↑x) = cexp (-↑y) * cexp (-(↑x - ↑y))
⊢ cexp (-↑y) * ↑y ^ (s - 1) * (cexp (-(↑x - ↑y)) * (↑x - ↑y) ^ (t - 1)) =
    cexp (-↑x) * (↑y ^ (s - 1) * (↑x - ↑y) ^ (t - 1))

Tactic:
rw [this]; ring

Goal state after: