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

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
he' : e ≠ 1
hL : Continuous fun p ↦ (L p.1) p.2
hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0
v : V
⊢ ∀ ⦃y : V⦄,
    v ≠ y →
      ∃ f ∈ (fun f ↦ ⇑f) '' ↑(StarSubalgebra.map (toContinuousMapStarₐ ℂ) (charPoly he hL)).toSubalgebra, f v ≠ f y

Tactic:
v'

Goal state after:
V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
he' : e ≠ 1
hL : Continuous fun p ↦ (L p.1) p.2
hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0
v v' : V
⊢ v ≠ v' →
    ∃ f ∈ (fun f ↦ ⇑f) '' ↑(StarSubalgebra.map (toContinuousMapStarₐ ℂ) (charPoly he hL)).toSubalgebra, f v ≠ f v'
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n : ℕ+
⊢ (↑m).Coprime ↑n ↔ m.Coprime n

Tactic:
unfold Nat.Coprime Coprime

Goal state after:
m n : ℕ+
⊢ (↑m).gcd ↑n = 1 ↔ m.gcd n = 1
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n : ℕ+
⊢ (↑m).gcd ↑n = (↑n).gcd ↑m

Tactic:
apply Nat.gcd_comm

Goal state after:
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n k : ℕ+
h : k.Coprime m
⊢ m.gcd (k * n) = m.gcd n

Tactic:
iterate 2 rw [gcd_comm]; symm

Goal state after:
m n k : ℕ+
h : k.Coprime m
⊢ (k * n).gcd m = n.gcd m
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: ⊢ μ.IsMultiplicative

Tactic:
by
  rw [IsMultiplicative.iff_ne_zero]
  refine ⟨by simp, fun {n m} hn hm hnm => ?_⟩
  simp only [moebius, coe_mk, squarefree_mul hnm, ite_zero_mul_ite_zero, cardFactors_mul hn hm,
    pow_add]

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
⊢ ∏ i ∈ n.divisors, f i = g n ↔
    (∏ i ∈ n.divisors, if h : 0 < i then Units.mk0 (f i) ⋯ else 1) = if h : 0 < n then Units.mk0 (g n) ⋯ else 1

Tactic:
rw [dif_pos hn, ← Units.val_inj, ← Units.coeHom_apply, map_prod, Units.val_mk0,
      prod_congr rfl _]
    intro x hx
    rw [dif_pos (pos_of_mem_divisors hx), Units.coeHom_apply, Units.val_mk0]

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
⊢ n ∈ s → ∏ i ∈ n.divisors, f i = g n ↔
    n ∈ s → (∏ i ∈ n.divisors, if h : 0 < i then Units.mk0 (f i) ⋯ else 1) = if h : 0 < n then Units.mk0 (g n) ⋯ else 1

Tactic:
rw [dif_pos hn, ← Units.val_inj, ← Units.coeHom_apply, map_prod, Units.val_mk0,
      prod_congr rfl _]
    intro x hx
    rw [dif_pos (pos_of_mem_divisors hx), Units.coeHom_apply, Units.val_mk0]

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

Goal state before:
pp: M₀ : Type u_7
inst✝¹ : CommMonoidWithZero M₀
inst✝ : Nontrivial M₀
l : ℕ
hl : 0 ^ l = 1
⊢ 0 ∣ l

Tactic:
by simpa [zero_pow_eq] using hl

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

Goal state before:
pp: n : ℕ
K : Type u_1
inst✝ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ IsIntegral ℤ μ

Tactic:
by
  use X ^ n - 1
  constructor
  · exact monic_X_pow_sub_C 1 (ne_of_lt hpos).symm
  · simp only [((IsPrimitiveRoot.iff_def μ n).mp h).left, eval₂_one, eval₂_X_pow, eval₂_sub,
      sub_self]

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

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

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

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

Goal state before:
pp: case neg.h
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ Multiset.map (fun x ↦ ζ ^ x * α) (Multiset.range n) ≤ nthRoots n a

pp: case neg.a
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ (nthRoots n a).card ≤ (Multiset.map (fun x ↦ ζ ^ x * α) (Multiset.range n)).card

Tactic:
· rw [← Finset.range_val,
      ← Finset.image_val_of_injOn (hζ.injOn_pow_mul hα), Finset.val_le_iff_val_subset]
    intro x hx
    simp only [Finset.image_val, Finset.range_val, Multiset.mem_dedup, Multiset.mem_map,
      Multiset.mem_range] at hx
    obtain ⟨m, _, rfl⟩ := hx
    rw [mem_nthRoots hn, mul_pow, e, ← pow_mul, mul_comm m,
      pow_mul, hζ.pow_eq_one, one_pow, one_mul]

Goal state after:
case neg.a
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ (nthRoots n a).card ≤ (Multiset.map (fun x ↦ ζ ^ x * α) (Multiset.range n)).card
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: case neg.inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : ↑1 < emultiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
hfree : Squarefree (X ^ n - 1)
hunit : P.degree = 0
⊢ False

Tactic:
exact (minpoly.degree_pos (isIntegral h hpos)).ne' hunit

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

Goal state before:
pp: case inr.inl
n : ℕ
hnzero : n > 0
h : n ≠ 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic 0 ℚ)

pp: case inr.inr
n m : ℕ
h : n ≠ m
hnzero : n > 0
hmzero : m > 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)

Tactic:
· exact isCoprime_one_right

Goal state after:
case inr.inr
n m : ℕ
h : n ≠ m
hnzero : n > 0
hmzero : m > 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : (cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)
⊢ p.Coprime a

Tactic:
hprime.1.coprime_iff_not_dvd

Goal state after:
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : (cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)
⊢ ¬p ∣ a
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
⊢ IsCyclotomicExtension S A ↥(adjoin A {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})

Tactic:
refine ⟨fun {n} hn hn' => ?_, fun b => ?_⟩

Goal state after:
case refine_1
S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
n : ℕ
hn : n ∈ S
hn' : n ≠ 0
⊢ ∃ r, IsPrimitiveRoot r n

case refine_2
S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : ↥(adjoin A {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
⊢ b ∈ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}
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
this : NeZero n
y : L
hy : IsPrimitiveRoot y n
⊢ x ∈ ↑(IntermediateField.adjoin K (⇑i '' {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))

Tactic:
obtain ⟨m, -, rfl⟩ := (hy.map_of_injective i.injective).eq_pow_of_pow_eq_one h2

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} = ⊤
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
this : NeZero n
y : L
hy : IsPrimitiveRoot y n
m : ℕ
h2 : (i.toRingHom y ^ m) ^ n = 1
⊢ i.toRingHom y ^ m ∈ ↑(IntermediateField.adjoin K (⇑i '' {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : Fintype R
inst✝² : DecidableEq R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : ψ.IsPrimitive
⊢ ∑ x, ψ (x * b) = ↑(if b = 0 then Fintype.card R else 0)

Tactic:
split_ifs with h
  · -- case `b = 0`
    simp only [h, mul_zero, map_zero_eq_one, Finset.sum_const, Nat.smul_one_eq_cast]
    rfl
  · -- case `b ≠ 0`
    simp_rw [mul_comm]
    exact mod_cast sum_eq_zero_of_ne_one (hψ h)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ χ.conductor = 0 ↔ n = 0

Tactic:
by
  refine ⟨?_, ?_⟩
  · contrapose!
    exact fun h ↦ @conductor_ne_zero _ _ _ χ ⟨h⟩
  · rintro rfl
    exact Nat.sInf_eq_zero.mpr <| Or.inl <| level_mem_conductorSet χ

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
inst✝ : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
⊢ IsCyclotomicExtension S A ↥C ↔ C = adjoin A {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ h ▸ isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot S A B hS⟩
  have := congr_arg (Subalgebra.map C.val) ((IsCyclotomicExtension.iff_adjoin_eq_top _ _ _).mp h).2
  rw [← Subalgebra.range_val C, ← Algebra.map_top, ← this, AlgHom.map_adjoin]
  congr; ext
  simp only [Subalgebra.coe_val, ne_eq, ← Subalgebra.coe_eq_one, SubmonoidClass.coe_pow,
    Set.mem_image, Set.mem_ofPred_eq, Subtype.exists, exists_and_left, exists_prop,
    exists_eq_right_right, and_iff_left_iff_imp, forall_exists_index, and_imp]
  exact fun n hn₁ hn₂ hx ↦ h.mem_of_pow_eq_one S C hn₁ hn₂ hx

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

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
m : ℕ
χ : DirichletCharacter S m
hχ : χ.Odd
x✝ : ZMod m
⊢ -1 * χ x✝ = -χ x✝

Tactic:
neg_one_mul

Goal state after:
S : Type u_2
inst✝ : CommRing S
m : ℕ
χ : DirichletCharacter S m
hχ : χ.Odd
x✝ : ZMod m
⊢ -χ x✝ = -χ x✝
Module: Mathlib.Analysis.InnerProductSpace.NormPow

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

Tactic:
fun_prop (discharger := simp [hx])

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ Icc s t = image (fun x ↦ s ∪ x) (t \ s).powerset

Tactic:
by
  unfold Finset.Icc instLocallyFiniteOrder LocallyFiniteOrder.ofIcc
  ext
  simp [h, union_comm]

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
T : E →ₗ[𝕜] E
hT : IsIdempotentElem T
⊢ T.IsPositive ↔ T.IsSymmetric

Tactic:
refine ⟨fun h => h.isSymmetric, fun h => ⟨h, fun x => ?_⟩⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsIdempotentElem T
h : T.IsSymmetric
x : E
⊢ 0 ≤ re ⟪T x, x⟫
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, ‖u x‖ₑ ^ (1 / (↑#ι - 1)) ≤
    ∫⁻ (x : ι → ℝ), ∏ i, (∫⁻ (xᵢ : ℝ), ‖fderiv ℝ u (update x i xᵢ)‖ₑ) ^ (1 / (↑#ι - 1))

Tactic:
gcongr with x i

Goal state after:
case h₁
ι : 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
⊢ ‖u x‖ₑ ≤ ∫⁻ (xᵢ : ℝ), ‖fderiv ℝ u (update x i xᵢ)‖ₑ
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case h₁
ι : 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
⊢ ‖u x‖ₑ ≤ ∫⁻ (xᵢ : ℝ), ‖fderiv ℝ u (update x i xᵢ)‖ₑ

Tactic:
calc ‖u x‖ₑ
    _ ≤ ∫⁻ xᵢ in Iic (x i), ‖deriv (u ∘ update x i) xᵢ‖ₑ := by
        apply le_trans (by simp) (HasCompactSupport.enorm_le_lintegral_Ici_deriv _ _ _)
        · exact hu.comp (by convert! contDiff_update 1 x i)
        · exact h2u.comp_isClosedEmbedding (isClosedEmbedding_update x i)
    _ ≤ ∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖ₑ := ?_

Goal state after:
case h₁
ι : 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
⊢ ∫⁻ (xᵢ : ℝ) in Set.Iic (x i), ‖deriv (u ∘ update x i) xᵢ‖ₑ ≤ ∫⁻ (xᵢ : ℝ), ‖fderiv ℝ u (update x i xᵢ)‖ₑ
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
g : Submodule 𝕜 (E × F)
x : F × E
h : ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0
u : WithLp 2 (F × E)
a : E
b : F
⊢ (a, b) ∈ g → toLp 2 (b, -a) = u → ⟪u.fst, (toLp 2 x).fst⟫ + ⟪u.snd, (toLp 2 x).snd⟫ = 0

Tactic:
hab

Goal state after:
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
g : Submodule 𝕜 (E × F)
x : F × E
h : ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0
u : WithLp 2 (F × E)
a : E
b : F
hab : (a, b) ∈ g
⊢ toLp 2 (b, -a) = u → ⟪u.fst, (toLp 2 x).fst⟫ + ⟪u.snd, (toLp 2 x).snd⟫ = 0
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
⊢ MeasurableSpace.generateFrom {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} ≤ μ.caratheodory

Tactic:
refine MeasurableSpace.generateFrom_le fun t ht => μ.isCaratheodory_iff_le.2 fun s => ?_

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s
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
⊢ 1 ≤
    ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ 0

Tactic:
simp only [ENNReal.rpow_zero, le_iInf_iff]

Goal state after:
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
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 p1 p2 p3 : Prop
htfae : h → [p1, p2, p3].TFAE
tfae_1_to_2 : h ∧ p1 → h ∧ p2
tfae_2_to_3 : h ∧ p2 → h ∧ p3
⊢ [h ∧ p1, h ∧ p2, h ∧ p3].TFAE

Tactic:
tfae_have 3 → 1 := fun ⟨h, t⟩ ↦ ⟨h, ((htfae h).out 2 0).mp t⟩

Goal state after:
𝕜 : 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 p1 p2 p3 : Prop
htfae : h → [p1, p2, p3].TFAE
tfae_1_to_2 : h ∧ p1 → h ∧ p2
tfae_2_to_3 : h ∧ p2 → h ∧ p3
tfae_3_to_1 : h ∧ p3 → h ∧ p1
⊢ [h ∧ p1, h ∧ p2, h ∧ p3].TFAE
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : ↑K ^ d ≠ 0
hKd : ↑K ^ d ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
⊢ 0 < ε / ↑K

Tactic:
simp [ε0.ne']

Goal state after:
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
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
f : OfKernel K
h : (ContinuousLinearMap.pi fun x ↦ adjoint (kerFun K x)) f = 0
ff : H₀ K
⊢ ⟪↑ff, f⟫_𝕜 = 0

Tactic:
induction ff using Finsupp.induction with

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

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ μH[d] (⇑(AffineMap.homothety x c) '' s) = ‖c‖₊ ^ d • μH[d] s

Tactic:
suffices
    μH[d] (IsometryEquiv.vaddConst x '' (c • ·) '' (IsometryEquiv.vaddConst x).symm '' s) =
      ‖c‖₊ ^ d • μH[d] s by
    simpa only [Set.image_image]

Goal state after:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ μH[d] (⇑(IsometryEquiv.vaddConst x) '' (fun x ↦ c • x) '' ⇑(IsometryEquiv.vaddConst x).symm '' s) = ‖c‖₊ ^ d • μH[d] s
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)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ φ (o.rightAngleRotation x) = o.rightAngleRotation (φ x)

Tactic:
by
  convert! (o.rightAngleRotation_map φ (φ x)).symm
  · simp
  · symm
    rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ
    rw [@Fact.out (finrank ℝ E = 2), Fintype.card_fin]

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

Goal state before:
pp: t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ ‖1 + ↑t * z‖⁻¹ ≤ (1 - ‖z‖)⁻¹

Tactic:
refine inv_anti₀ (by linarith) ?_

Goal state after:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - ‖z‖ ≤ ‖1 + ↑t * z‖
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ (b : ℝ), e ≤ b → ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
⊢ ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi (max e 1)), ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d

Tactic:
refine (ae_restrict_mem measurableSet_Ioi).mono fun t ht => ?_

Goal state after:
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ (b : ℝ), e ≤ b → ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
t : ℝ
ht : t ∈ Ioi (max e 1)
⊢ ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - ‖z‖ ≤ ‖1 + ↑t * z‖

Tactic:
calc 1 - ‖z‖
    _ ≤ 1 - t * ‖z‖ := by
      nlinarith [norm_nonneg z]
    _ = 1 - ‖t * z‖ := by
      rw [norm_mul, Complex.norm_of_nonneg ht.1]
    _ ≤ ‖1 + t * z‖ := by
      rw [← norm_neg (t * z), ← sub_neg_eq_add]
      convert! norm_sub_norm_le 1 (-(t * z))
      exact norm_one.symm

Goal state after:
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
f' : ℂ → ℂ := fun z ↦ (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (fun t ↦ f' (0 + ↑t * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹
⊢ ∀ᵐ (t : ℝ), t ∈ Set.Ioc 0 1 → ‖↑t ^ n * (1 + ↑t * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹

Tactic:
filter_upwards with t ⟨ht₀, ht₁⟩

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)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (fun t ↦ f' (0 + ↑t * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹
t : ℝ
ht₀ : 0 < t
ht₁ : t ≤ 1
⊢ ‖↑t ^ n * (1 + ↑t * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹