mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
⊢ Basis (Fin (minpoly K x).natDegree) K ↥K[x]

Tactic:
by
  have hST : Function.Injective (algebraMap (K[(x : S)]) S) := Subtype.coe_injective
  have hx' :
    IsIntegral K (⟨x, subset_adjoin (Set.mem_singleton x)⟩ : K[(x : S)]) := by
    apply (isIntegral_algebraMap_iff hST).mp
    convert! hx
  apply Basis.mk (v := fun i : Fin _ ↦ ⟨x, subset_adjoin (Set.mem_singleton x)⟩ ^ (i : ℕ))
  · have : LinearIndependent K _ := linearIndependent_pow
      (⟨x, self_mem_adjoin_singleton _ _⟩ : K[x])
    rwa [← minpoly.algebraMap_eq hST] at this
  · rintro ⟨y, hy⟩ _
    have := hx'.mem_span_pow (y := ⟨y, hy⟩)
    rw [← minpoly.algebraMap_eq hST] at this
    apply this
    rw [adjoin_singleton_eq_range_aeval] at hy
    obtain ⟨f, rfl⟩ := (aeval x).mem_range.mp hy
    use f
    ext
    exact aeval_algebraMap_apply S (⟨x, _⟩ : K[x]) _

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

Goal state before:
pp: n : ℕ
hn : 2 < n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
this : NeZero n
h0 : (cyclotomic n ℝ).coeff 0 = 1
⊢ 0 < eval (-1) (cyclotomic n ℝ)

Tactic:
coeff_zero_eq_eval_zero

Goal state after:
n : ℕ
hn : 2 < n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
this : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
⊢ 0 < eval (-1) (cyclotomic n ℝ)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ (cyclotomic n ℤ).natDegree * p ≤ (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree

Tactic:
natDegree_cyclotomic,

Goal state after:
case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ n.totient * p ≤ (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ n.totient * p ≤ (cyclotomic (n * p) ℤ).natDegree + (cyclotomic n ℤ).natDegree

Tactic:
natDegree_cyclotomic,

Goal state after:
case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ n.totient * p ≤ (n * p).totient + (cyclotomic n ℤ).natDegree
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ n.totient * p ≤ (n * p).totient + (cyclotomic n ℤ).natDegree

Tactic:
natDegree_cyclotomic,

Goal state after:
case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ n.totient * p ≤ (n * p).totient + n.totient
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
⊢ (cyclotomic n ℤ).natDegree * p ≤ (cyclotomic (n * p) ℤ).natDegree

Tactic:
natDegree_cyclotomic,

Goal state after:
case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
⊢ n.totient * p ≤ (cyclotomic (n * p) ℤ).natDegree
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
⊢ n.totient * p ≤ (cyclotomic (n * p) ℤ).natDegree

Tactic:
natDegree_cyclotomic,

Goal state after:
case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
⊢ n.totient * p ≤ (n * p).totient
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case neg.refine_2
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
⊢ ⊤ ≤ adjoin A {b | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
rw [← ((iff_adjoin_eq_top _ _ _).mp hB).2]
    exact Algebra.adjoin_mono (by aesop)

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

Goal state before:
pp: p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
s : ℕ
hs : s ≤ k
hodd : p ≠ 2
h : p ^ (k - s + 1) = 2
⊢ False

Tactic:
rw [← pow_one 2] at h

Goal state after:
p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
s : ℕ
hs : s ≤ k
hodd : p ≠ 2
h : p ^ (k - s + 1) = 2 ^ 1
⊢ False
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case succ.refine_5
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ ∀
    x ∈
      Subring.closure
        (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
          (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField),
    (aeval x) (X ^ (n✝ + 1) ^ n - X) = 0 → (aeval (-x)) (X ^ (n✝ + 1) ^ n - X) = 0

Tactic:
intro x _ hx
    simp only [g_poly, sub_eq_zero, aeval_X_pow, aeval_X, map_sub, sub_neg_eq_add] at *
    rw [neg_pow, hx, neg_one_pow_char_pow]
    simp

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case inr
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit ↑a₀
u : (ZMod N)ˣ
hu : (castHom ⋯ (ZMod N₀)) ↑u = ↑a₀
⊢ (castHom ⋯ (ZMod N₀)) ↑u = ↑(↑u).val

Tactic:
natCast_val,

Goal state after:
case inr
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit ↑a₀
u : (ZMod N)ˣ
hu : (castHom ⋯ (ZMod N₀)) ↑u = ↑a₀
⊢ (castHom ⋯ (ZMod N₀)) ↑u = (↑u).cast
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
⊢ χ₄ ↑(n % ↑4) = χ₄ ↑(n % 4)

Tactic:
Nat.cast_ofNat

Goal state after:
n : ℤ
⊢ χ₄ ↑(n % 4) = χ₄ ↑(n % 4)
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
⊢ χ₈ ↑(n % ↑8) = χ₈ ↑(n % 8)

Tactic:
Nat.cast_ofNat

Goal state after:
n : ℤ
⊢ χ₈ ↑(n % 8) = χ₈ ↑(n % 8)
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m d : ℕ
hm : n ∣ m
hd : m ∣ d
⊢ (changeLevel ⋯) χ = (changeLevel hd) ((changeLevel hm) χ)

Tactic:
by
  simp [changeLevel_def, MonoidHom.comp_assoc, ZMod.unitsMap_comp]

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

Goal state before:
pp: case neg
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
⊢ ¬IsUnit a → χ⁻¹ a = χ a⁻¹ʳ

Tactic:
nontriviality R

Goal state after:
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
a✝ : Nontrivial R
⊢ ¬IsUnit a → χ⁻¹ a = χ a⁻¹ʳ
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
n : ℕ
hn : Even (2 * n)
⊢ (χ ^ 2) ^ n = 1

Tactic:
hχ.sq_eq_one,

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
hn : Even (2 * n)
⊢ 1 ^ n = 1
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₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension S A ↥C₁
h₂ : IsCyclotomicExtension S A ↥C₂
hC : ∀ n ∈ S, n ≠ 0 → ∃ x, IsPrimitiveRoot x n
⊢ adjoin A {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = C₂

Tactic:
(isCyclotomicExtension_iff_eq_adjoin S C₂ hC).mp h₂

Goal state after:
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension S A ↥C₁
h₂ : IsCyclotomicExtension S A ↥C₂
hC : ∀ n ∈ S, n ≠ 0 → ∃ x, IsPrimitiveRoot x n
⊢ adjoin A {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = adjoin A {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
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₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension S A ↥C₁
h₂ : IsCyclotomicExtension S A ↥C₂
⊢ C₁ = C₂

Tactic:
by
  have hC (n) (hn₁ : n ∈ S) (hn₂ : n ≠ 0) : ∃ x : B, IsPrimitiveRoot x n := by
    obtain ⟨ζ, hζ⟩ := h₁.1 hn₁ hn₂
    exact ⟨ζ, IsPrimitiveRoot.coe_submonoidClass_iff.mpr hζ⟩
  rw [(isCyclotomicExtension_iff_eq_adjoin S C₁ hC).mp h₁,
    (isCyclotomicExtension_iff_eq_adjoin S C₂ hC).mp h₂]

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

Goal state before:
pp: A : Type u
B : Type v
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension {n₁} A ↥C₁
h₂ : IsCyclotomicExtension {n₂} A ↥C₂
inst✝¹ : NeZero n₁
inst✝ : NeZero n₂
⊢ IsCyclotomicExtension {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)

Tactic:
obtain ⟨ζ₁, hζ₁⟩ := h₁.1 rfl (NeZero.ne n₁)
  obtain ⟨ζ₂, hζ₂⟩ := h₂.1 rfl (NeZero.ne n₂)
  replace hζ₁ := hζ₁.map_of_injective (FaithfulSMul.algebraMap_injective C₁ B)
  replace hζ₂ := hζ₂.map_of_injective (FaithfulSMul.algebraMap_injective C₂ B)
  have hζ := hζ₁.pow_mul_pow_lcm hζ₂ (NeZero.ne n₁) (NeZero.ne n₂)
  rw [sup_comm, (isCyclotomicExtension_singleton_iff_eq_adjoin n₁ C₁ hζ₁).mp h₁,
    (isCyclotomicExtension_singleton_iff_eq_adjoin n₂ C₂ hζ₂).mp h₂, ← adjoin_union,
    Set.union_singleton, hζ₁.adjoin_pair_eq A hζ₂ (NeZero.ne _) (NeZero.ne _) hζ]
  have : NeZero (n₁.lcm n₂) := ⟨Nat.lcm_ne_zero (NeZero.ne _) (NeZero.ne _)⟩
  exact (hζ₁.pow_mul_pow_lcm hζ₂ (NeZero.ne n₁) (NeZero.ne n₂)).adjoin_isCyclotomicExtension A

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

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

Tactic:
hχ.sq_eq_one,

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ (ψ.mulShift ↑p) = 1 ↑p * gaussSum χ (ψ.mulShift ↑p)
Module: Mathlib.Analysis.Hofer

Goal state before:
pp: X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H : ∀ ε' > 0, ∀ (x' : X), ε' ≤ ε → d x' x ≤ 2 * ε → ε * ϕ x ≤ ε' * ϕ x' → ∃ y, d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
x' : X
k : ℕ
⊢ ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'

Tactic:
rw [div_mul_eq_mul_div, le_div_iff₀, mul_assoc, mul_le_mul_iff_right₀ ε_pos, mul_comm]

Goal state after:
X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H : ∀ ε' > 0, ∀ (x' : X), ε' ≤ ε → d x' x ≤ 2 * ε → ε * ϕ x ≤ ε' * ϕ x' → ∃ y, d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
x' : X
k : ℕ
⊢ 0 < 2 ^ k
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✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ T μ p (∫⋯∫⁻_(insert i s)ᶜ, f ∂μ) (insert i s) ≤ T μ p (∫⋯∫⁻_sᶜ, f ∂μ) s

Tactic:
convert! T_insert_le_T_lmarginal_singleton μ hp₀ s ?_ i hi (hf.lmarginal μ) using 2

Goal state after:
case e'_4
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
p : ℝ
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ ∫⋯∫⁻_sᶜ, f ∂μ = ∫⋯∫⁻_{i}, ∫⋯∫⁻_(insert i s)ᶜ, f ∂μ ∂μ

case convert_1
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
p : ℝ
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ ↑(#s) * p ≤ 1
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 ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : (↑#ι).HolderConjugate p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
⊢ 1 < #ι

Tactic:
exact_mod_cast hp.lt

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
⊢ 2 ≤ ↑#ι

Tactic:
exact_mod_cast hp.lt

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
hA : A.IsSymmetric
hB : B.IsSymmetric
i j : 𝕜 × 𝕜
hij : i ≠ j
v : E
x✝ : v ∈ eigenspace A i.2 ⊓ eigenspace B i.1
hv1 : v ∈ ↑(eigenspace A i.2)
hv2 : v ∈ ↑(eigenspace B i.1)
⊢ i.1 ≠ j.1 ∨ i.2 ≠ j.2

Tactic:
by rwa [Ne.eq_def, Prod.ext_iff, not_and_or] at hij

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

Goal state before:
pp: F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp✝ : (↑(finrank ℝ E)).HolderConjugate p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : (↑#ι).HolderConjugate p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)
hc : 0 < c
h2c : μ = c • Measure.map (⇑e.symm) volume
h3c : ↑c ≠ 0
⊢ C =
    μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume) * ‖↑e.symm‖₊ ^ p *
      (μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume) ^ p)⁻¹

Tactic:
ι,

Goal state after:
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp✝ : (↑(finrank ℝ E)).HolderConjugate p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : (↑#ι).HolderConjugate p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)
hc : 0 < c
h2c : μ = c • Measure.map (⇑e.symm) volume
h3c : ↑c ≠ 0
⊢ C =
    μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume) * ‖↑e.symm‖₊ ^ p *
      (μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume) ^ p)⁻¹
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: 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 : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
n : ℕ
⊢ μ (s ∩ t ∪ s \ t) = μ s

Tactic:
rw [inter_union_sdiff]

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
g₁ g₂ : G →L[𝕜] H
⊢ mapL f (g₁ + g₂) = mapL f g₁ + mapL f g₂

Tactic:
by ext; simp [map_add_right]

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

Goal state before:
pp: case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
h : dimH s < ⨅ d, ⨅ (_ : μH[↑d] s = 0), ↑d
⊢ False

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 h with ⟨d', hdim_lt, hlt⟩

Goal state after:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
h : dimH s < ⨅ d, ⨅ (_ : μH[↑d] s = 0), ↑d
d' : ℝ≥0
hdim_lt : dimH s < ↑d'
hlt : ↑d' < ⨅ d, ⨅ (_ : μH[↑d] s = 0), ↑d
⊢ False
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case refine_2
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
⊢ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets ≤ ⨆ x, limsup dimH (𝓝[s] x).smallSets

Tactic:
exact iSup₂_le_iSup _ _

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
s : Set E
hs : dimH s < ↑(finrank ℝ E)
⊢ Dense sᶜ

Tactic:
refine fun x => mem_closure_iff_nhds.2 fun t ht => nonempty_iff_ne_empty.2 fun he => hs.not_ge ?_
  rw [← sdiff_eq, sdiff_eq_empty] at he
  rw [← Real.dimH_of_mem_nhds ht]
  exact dimH_mono he

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℚ
⊢ innerProp' E ↑r

Tactic:
by
  intro x y
  let hom : 𝕜 →ₗ[ℚ] 𝕜 := AddMonoidHom.toRatLinearMap <|
    AddMonoidHom.mk' (fun r ↦ inner_ 𝕜 (r • x) y) <| fun a b ↦ by
      simpa [add_smul] using add_left (a • x) (b • x) y
  simpa [hom, Rat.smul_def] using map_smul hom r 1

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : I = 0
⊢ innerProp' E I

Tactic:
rw [hI]
    simpa using real_prop (𝕜 := 𝕜) 0

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

Goal state before:
pp: H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x y : H
⊢ (starRingEnd ℝ) ⟪y, x⟫.re = ⟪x, y⟫.re

Tactic:
simp only [← ipc.conj_inner_symm x y, conj_trivial]
    rfl

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
x : X
v : V
⊢ ‖K x x‖ * ‖v‖ * ‖v‖ ≤ (√‖K x x‖ * ‖v‖) ^ 2

Tactic:
by simp [mul_pow, mul_assoc, ← sq]

Goal state after:
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)
a b : E
⊢ ⟪a, b⟫ ^ 2 + (o.areaForm a) b ^ 2 = ‖a‖ ^ 2 * ‖b‖ ^ 2

Tactic:
simpa [sq, real_inner_self_eq_norm_sq] using o.inner_mul_inner_add_areaForm_mul_areaForm a b b

Goal state after:
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: ⊢ rexp '' univ = Ioi 0

Tactic:
Set.image_univ,

Goal state after:
⊢ range rexp = Ioi 0
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ cexp (-(↑s.re + ↑s.im * I) * ↑u) • f (rexp (-u)) = cexp (-↑s.im * ↑u * I) • rexp (-s.re * u) • f (rexp (-u))

Tactic:
rw [neg_add, add_mul, Complex.exp_add, mul_comm, ← smul_eq_mul, smul_assoc]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ cexp (-(↑s.im * I) * ↑u) • cexp (-↑s.re * ↑u) • f (rexp (-u)) =
    cexp (-↑s.im * ↑u * I) • rexp (-s.re * u) • f (rexp (-u))
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
hE : CompleteSpace E
⊢ mellin (fun t ↦ f (t ^ 0)) s = |0|⁻¹ • mellin f (s / ↑0)

pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
hE : ¬CompleteSpace E
⊢ mellin (fun t ↦ f (t ^ 0)) s = |0|⁻¹ • mellin f (s / ↑0)

Tactic:
· simp [integral_smul_const, mellin, setIntegral_Ioi_zero_cpow]

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
hE : ¬CompleteSpace E
⊢ mellin (fun t ↦ f (t ^ 0)) s = |0|⁻¹ • mellin f (s / ↑0)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case hf
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ 0 - 1 < u.re - 1

Tactic:
sub_lt_sub_iff_right

Goal state after:
case hf
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ 0 < u.re
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: x : ℝ
hx : x ∈ Ioi 0
m : ℕ
⊢ x ≠ -↑m

Tactic:
exact (neg_lt_iff_pos_add.mpr (add_pos_of_pos_of_nonneg (mem_Ioi.mp hx) (Nat.cast_nonneg m))).ne'

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e_a
n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in π / 2 - π / 2..π / 2, cos x ^ n = ∫ (x : ℝ) in 0..π / 2, sin x ^ n

Tactic:
(by ring : π / 2 = π / 2 - 0)

Goal state after:
case e_a
n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in π / 2 - π / 2..π / 2 - 0, cos x ^ n = ∫ (x : ℝ) in 0..π / 2, sin x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : 2 ≤ n
hx : 0 < x
⊢ f ↑n + x * log (↑n - 1) ≤ f (↑n + x)

Tactic:
have npos : 0 < (n : ℝ) - 1 := by rw [← Nat.cast_one, sub_pos, Nat.cast_lt]; lia

Goal state after:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : 2 ≤ n
hx : 0 < x
npos : 0 < ↑n - 1
⊢ f ↑n + x * log (↑n - 1) ≤ f (↑n + x)