mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
⊢ ∫ (v : ι → ℝ), cexp (∑ x, -(b x * ↑(v x) ^ 2) + ∑ i, c i * ↑(v i)) =
    ∏ i, (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i))

Tactic:
← Finset.sum_add_distrib,

Goal state after:
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
⊢ ∫ (v : ι → ℝ), cexp (∑ x, (-(b x * ↑(v x) ^ 2) + c x * ↑(v x))) =
    ∏ i, (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i))
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: case e'_3
d : Type u_1
inst✝ : Fintype d
a : d → ℝ
this :
  Measure.map (fun x i ↦ ↑(x i)) (Measure.map Subtype.val (Measure.comap Subtype.val volume)) =
    Measure.map (fun x i ↦ ↑(↑x i)) (Measure.comap Subtype.val volume)
⊢ Measure.map Subtype.val (Measure.comap Subtype.val volume) = Measure.pi fun i ↦ volume.restrict (Ioc (a i) (a i + 1))

Tactic:
convert!
    (map_comap_subtype_coe (MeasurableSet.univ_pi' (fun i => measurableSet_Ioc (a := a i))) volume)
    convert! (Measure.restrict_pi_pi (fun i => volume) (fun i => Ioc (a i) (a i + 1))).symm
    grind

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (mFourierCoeff ⇑f)
⊢ HasSum (fun i ↦ mFourierCoeff (⇑f) i • mFourier i) f

Tactic:
have sum_L2 := hasSum_mFourier_series_L2 (ContinuousMap.toLp 2 volume ℂ f)
  simp only [mFourierCoeff_toLp] at sum_L2
  refine ContinuousMap.hasSum_of_hasSum_Lp (.of_norm ?_) sum_L2
  simpa only [norm_smul, mFourier_norm, mul_one] using h.norm

Goal state after:
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m : E
⊢ MemSobolev (s - 1) 2 (∂_{m} f)

Tactic:
rw [SubNegMonoid.sub_eq_add_neg s 1, add_comm, ← memSobolev_besselPotential_iff,
    besselPotential_neg_one_lineDerivOp_eq f]

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m : E
⊢ MemSobolev s 2 ((2 * ↑π * Complex.I) • (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x m * (1 + ‖x‖ ^ 2) ^ (-1 / 2))) f)
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
⊢ ∫ (x : ℝ), e x * f x = 𝓕 ⇑f ↑m

Tactic:
by
      rw [fourier_real_eq_integral_exp_smul]
      congr 1 with x : 1
      rw [smul_eq_mul, comp_apply, coe_mk, coe_mk, ContinuousMap.toFun_eq_coe, fourier_coe_apply]
      congr 2
      push_cast
      ring

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

Goal state before:
pp: m n : ℕ+
⊢ n.gcd m = m ↔ m ∣ n

Tactic:
rw [gcd_comm]

Goal state after:
m n : ℕ+
⊢ m.gcd n = m ↔ m ∣ n
Module: Mathlib.Data.PNat.Prime

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

Tactic:
rw [gcd_comm]

Goal state after:
m n k : ℕ+
h : k.Coprime m
⊢ (k * n).gcd m = m.gcd n
Module: Mathlib.Data.PNat.Prime

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

Tactic:
rw [gcd_comm]

Goal state after:
m n k : ℕ+
h : k.Coprime m
⊢ n.gcd m = (k * n).gcd m
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: n : ℕ+
⊢ n.gcd 1 = 1

Tactic:
rw [gcd_comm]

Goal state after:
n : ℕ+
⊢ gcd 1 n = 1
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n : ℕ+
⊢ m.gcd n = 1 → n.gcd m = 1

Tactic:
rw [gcd_comm]

Goal state after:
m n : ℕ+
⊢ n.gcd m = 1 → n.gcd m = 1
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
⊢ (a * b).gcd m = a.gcd m

Tactic:
apply Coprime.gcd_mul_right_cancel a

Goal state after:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
⊢ b.Coprime m
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = m.gcd (a * b)

Tactic:
rw [gcd_comm]

Goal state after:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (a * b).gcd m
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = m.gcd (b * a)

Tactic:
rw [gcd_comm]

Goal state after:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (b * a).gcd m
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
⊢ Subgroup.zpowers ζ = rootsOfUnity k R

Tactic:
apply Subgroup.eq_of_le_of_card_ge (Subgroup.zpowers_le_of_mem h.pow_eq_one)

Goal state after:
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
⊢ Nat.card ↥(rootsOfUnity k R) ≤ Nat.card ↥(Subgroup.zpowers ζ)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
S : Type u_7
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
ζ₁ ζ₂ : R
k₁ k₂ : ℕ
hζ₁ : IsPrimitiveRoot ζ₁ k₁
hζ₂ : IsPrimitiveRoot ζ₂ k₂
hk₁ : k₁ ≠ 0
hk₂ : k₂ ≠ 0
ζ : R
hζ : IsPrimitiveRoot ζ (k₁.lcm k₂)
⊢ S[ζ₁, ζ₂] = S[ζ]

Tactic:
have : NeZero (k₁.lcm k₂) := ⟨Nat.lcm_ne_zero hk₁ hk₂⟩
  refine le_antisymm (Algebra.adjoin_le ?_) (Algebra.adjoin_le ?_)
  · refine Set.pair_subset_iff.mpr ⟨?_, ?_⟩
    · obtain ⟨_, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one <|
        (hζ₁.pow_eq_one_iff_dvd _).mpr <| k₁.dvd_lcm_left k₂
      exact Subalgebra.pow_mem _ (Algebra.self_mem_adjoin_singleton S _) _
    · obtain ⟨_, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one <|
        (hζ₂.pow_eq_one_iff_dvd _).mpr <| k₁.dvd_lcm_right k₂
      exact Subalgebra.pow_mem _ (Algebra.self_mem_adjoin_singleton S _) _
  · have hζ' := IsPrimitiveRoot.pow_mul_pow_lcm hζ₁ hζ₂ hk₁ hk₂
    obtain ⟨_, _, rfl⟩ := hζ'.eq_pow_of_pow_eq_one hζ.pow_eq_one
    aesop

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n → ∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R)) (cyclotomic i R) = (algebraMap R[X] (RatFunc R)) (X ^ n - 1)
⊢ ∀ (n : ℕ), 0 < n → ¬X ^ n - 1 = 0

Tactic:
· intro n hn
    apply Monic.ne_zero
    apply monic_X_pow_sub_C _ (ne_of_gt hn)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hz : IsPrimitiveRoot ζ n
⊢ cyclotomic n K = ∏ μ ∈ primitiveRoots n K, (X - C μ)

Tactic:
rw [← cyclotomic']

Goal state after:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hz : IsPrimitiveRoot ζ n
⊢ cyclotomic n K = cyclotomic' n K
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hz : IsPrimitiveRoot ζ n
⊢ cyclotomic n K = cyclotomic' n K

Tactic:
induction n using Nat.strong_induction_on generalizing ζ with | _ k hk
   =>  _ 

Goal state after:
case h
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
⊢ cyclotomic k K = cyclotomic' k K
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case inl
m : ℕ
h : 0 ≠ m
⊢ IsCoprime (cyclotomic 0 ℚ) (cyclotomic m ℚ)

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

Tactic:
· exact isCoprime_one_left

Goal state after:
case inr
n m : ℕ
h : n ≠ m
hnzero : n > 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
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
⊢ 0 < eval (↑(-1)) (cyclotomic n ℝ)

Tactic:
simp only [Int.cast_one, Int.cast_neg]

Goal state after:
n : ℕ
hn : 2 < n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
this : NeZero n
⊢ 0 < eval (-1) (cyclotomic n ℝ)
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:
rw [coeff_zero_eq_eval_zero] at h0

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.Eval

Goal state before:
pp: case h.inl.hb
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 (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Odd n ∨ 0 < x + 1
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
⊢ 0 ≤ eval x (cyclotomic i R)

Tactic:
rcases h with hk | hx

Goal state after:
case h.inl.hb.inl
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 (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hk : Odd n
⊢ 0 ≤ eval x (cyclotomic i R)

case h.inl.hb.inr
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 (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hx : 0 < x + 1
⊢ 0 ≤ eval x (cyclotomic i R)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ⋯
⊢ (fun x ↦ cyclotomic n (ZMod p) * x) (cyclotomic (n * p) (ZMod p)) =
    (fun x ↦ cyclotomic n (ZMod p) * x) (cyclotomic n (ZMod p) ^ (p - 1))

Tactic:
dsimp

Goal state after:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic n (ZMod p) * cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) * cyclotomic n (ZMod p) ^ (p - 1)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) = (expand (ZMod p) p) (cyclotomic n (ZMod p))

Tactic:
← map_cyclotomic_int n,

Goal state after:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) = (expand (ZMod p) p) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))
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
h : IsCyclotomicExtension {1} A B
x : B
⊢ x ∈ ⊥

Tactic:
by
    simpa [adjoin_singleton_one] using ((isCyclotomicExtension_iff _ _ _).1 h).2 x

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

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝¹ : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝ : FiniteDimensional K L := finiteDimensional {n} K L
this : IsGalois K L := isGalois {n} K L
| ∏ σ, σ (ζ - 1)

Tactic:
congr
    rfl
    ext
    rw [← neg_sub, map_neg, map_sub, map_one, neg_eq_neg_one_mul]

Goal state after:
case f
n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝¹ : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝ : FiniteDimensional K L := finiteDimensional {n} K L
this : IsGalois K L := isGalois {n} K L
x✝ : L →ₐ[K] E
| -1 * (1 - x✝ ζ)
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
C : Type u_1
inst✝¹ : CommRing C
inst✝ : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
this✝ : Algebra B C := (↑f).toAlgebra
this : IsCyclotomicExtension {1} B C
⊢ IsCyclotomicExtension S A C

Tactic:
have : IsScalarTower A B C := IsScalarTower.of_algHom f.toAlgHom

Goal state after:
S : Set ℕ
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
C : Type u_1
inst✝¹ : CommRing C
inst✝ : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
this✝¹ : Algebra B C := (↑f).toAlgebra
this✝ : IsCyclotomicExtension {1} B C
this : IsScalarTower A B C
⊢ IsCyclotomicExtension S A C
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case mem
S : Set ℕ
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsCyclotomicExtension S A B
inst✝ : IsDomain B
f g : B ≃ₐ[A] B
H : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n ∧ f r = g r
x y : B
hy : y ∈ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}
⊢ f y = g y

Tactic:
| mem y hy =>

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

Goal state before:
pp: case refine_2
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
x✝ : ↥A[ζ]
x : B
hx : x ∈ A[ζ]
a : A
⊢ ⟨(algebraMap A B) a, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
exact Subalgebra.algebraMap_mem _ _

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

Goal state before:
pp: case h
n : ℕ
inst✝⁴ : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ X ^ n - 1 = cyclotomic n K * ∏ i ∈ n.properDivisors, cyclotomic i K

Tactic:
(eq_cyclotomic_iff (NeZero.pos _) _).1 rfl

Goal state after:
case h
n : ℕ
inst✝⁴ : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ X ^ n - 1 = X ^ n - 1
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S : Set ℕ
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
key : ∀ b ∈ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}, IsAlgebraic K b
⊢ IsCyclotomicExtension S K ↥(IntermediateField.adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}).toSubalgebra

Tactic:
rw [congr(IsCyclotomicExtension S K $(IntermediateField.adjoin_toSubalgebra_of_isAlgebraic key))]

Goal state after:
S : Set ℕ
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
key : ∀ b ∈ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}, IsAlgebraic K b
⊢ IsCyclotomicExtension S K ↥(adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: N : ℕ
a : ZMod N
⊢ ∃ d, d ∣ N ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Tactic:
by
  rcases eq_or_ne N 0 with rfl | hN
  -- Silly special case : N = 0. Of no mathematical interest, but true, so let's prove it.
  · change ℤ at a
    rcases eq_or_ne a 0 with rfl | ha
    · refine ⟨0, dvd_zero _, 1, isUnit_one, by rw [Nat.cast_zero, mul_zero]⟩
    refine ⟨a.natAbs, dvd_zero _, Int.sign a, ?_, (Int.sign_mul_natAbs a).symm⟩
    rcases lt_or_gt_of_ne ha with h | h
    · simp only [Int.sign_eq_neg_one_of_neg h, IsUnit.neg_iff, isUnit_one]
    · simp only [Int.sign_eq_one_of_pos h, isUnit_one]
  -- now the interesting case
  have : NeZero N := ⟨hN⟩
  -- Define `d` as the GCD of a lift of `a` and `N`.
  let d := a.val.gcd N
  have hd : d ≠ 0 := Nat.gcd_ne_zero_right hN
  obtain ⟨a₀, (ha₀ : _ = d * _)⟩ := a.val.gcd_dvd_left N
  obtain ⟨N₀, (hN₀ : _ = d * _)⟩ := a.val.gcd_dvd_right N
  refine ⟨d, ⟨N₀, hN₀⟩, ?_⟩
  -- Show `a` is a unit mod `N / d`.
  have hu₀ : IsUnit (a₀ : ZMod N₀) := by
    refine (isUnit_iff_coprime _ _).mpr (Nat.isCoprime_iff_coprime.mp ?_)
    obtain ⟨p, q, hpq⟩ : ∃ (p q : ℤ), d = a.val * p + N * q := ⟨_, _, Nat.gcd_eq_gcd_ab _ _⟩
    rw [ha₀, hN₀, Nat.cast_mul, Nat.cast_mul, mul_assoc, mul_assoc, ← mul_add, eq_comm,
      mul_comm _ p, mul_comm _ q] at hpq
    exact ⟨p, q, Int.eq_one_of_mul_eq_self_right (Nat.cast_ne_zero.mpr hd) hpq⟩
  -- Lift it arbitrarily to a unit mod `N`.
  obtain ⟨u, hu⟩ := (unitsMap_surjective (⟨d, mul_comm d N₀ ▸ hN₀⟩ : N₀ ∣ N)) hu₀.unit
  rw [unitsMap_def, ← Units.val_inj, Units.coe_map, IsUnit.unit_spec, MonoidHom.coe_coe] at hu
  refine ⟨u.val, u.isUnit, ?_⟩
  rw [← natCast_zmod_val a, ← natCast_zmod_val u.1, ha₀, ← Nat.cast_mul,
    natCast_eq_natCast_iff, mul_comm _ d, Nat.ModEq]
  simp only [hN₀, Nat.mul_mod_mul_left, Nat.mul_right_inj hd]
  rw [← Nat.ModEq, ← natCast_eq_natCast_iff, ← hu, natCast_val, castHom_apply]

Goal state after:
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case refine_2
F : Type u_3
K : Type u_4
L : Type u_5
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this✝⁴ : Finite F
this✝³ : Fintype F
this✝² : Module.Finite F K
this✝¹ : Finite K
this✝ : Fintype K
this : Fintype L
⊢ Polynomial.map (algebraMap F L) (X ^ Fintype.card K - X) ∣ Polynomial.map (algebraMap F L) (X ^ Fintype.card L - X)

Tactic:
Module.card_eq_pow_finrank (K := F),

Goal state after:
case refine_2
F : Type u_3
K : Type u_4
L : Type u_5
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this✝⁴ : Finite F
this✝³ : Fintype F
this✝² : Module.Finite F K
this✝¹ : Finite K
this✝ : Fintype K
this : Fintype L
⊢ Polynomial.map (algebraMap F L) (X ^ Fintype.card F ^ Module.finrank F K - X) ∣
    Polynomial.map (algebraMap F L) (X ^ Fintype.card L - X)
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: case hbc
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ ‖f x‖ ^ (p - 2) * ‖(innerSL ℝ) (f x) ∘SL fderiv ℝ f x‖ ≤ ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖

Tactic:
refine mul_le_mul_of_nonneg_left (ContinuousLinearMap.opNorm_comp_le ..) (by positivity)
    |>.trans_eq ?_

Goal state after:
case hbc
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ ‖f x‖ ^ (p - 2) * (‖(innerSL ℝ) (f x)‖ * ‖fderiv ℝ f x‖) = ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
r : 𝕜
x : E
⊢ { toFun := ⇑(adjoint counit), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x =
    x * { toFun := ⇑(adjoint counit), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r

Tactic:
dsimp

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
r : 𝕜
x : E
⊢ (adjoint comul) ((adjoint counit) r ⊗ₜ[𝕜] x) = (adjoint comul) (x ⊗ₜ[𝕜] (adjoint counit) r)
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
r : 𝕜
x : E
⊢ r • x = { toFun := ⇑(adjoint counit), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x

Tactic:
dsimp

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
r : 𝕜
x : E
⊢ r • x = (adjoint comul) ((adjoint counit) r ⊗ₜ[𝕜] x)
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
f' : F →ₗ.[R] E
h : f.inverse.graph.topologicalClosure = f'.graph
x : E
hx : x ∈ f.closure.domain
hx' : (x, 0) ∈ closure[instTopologicalSpaceProd] ↑f.graph
⊢ (0, x) ∈ (Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph).topologicalClosure

Tactic:
apply image_closure_subset_closure_image continuous_swap

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
f' : F →ₗ.[R] E
h : f.inverse.graph.topologicalClosure = f'.graph
x : E
hx : x ∈ f.closure.domain
hx' : (x, 0) ∈ closure[instTopologicalSpaceProd] ↑f.graph
⊢ (0, x) ∈ Prod.swap '' closure[instTopologicalSpaceProd] ↑f.graph
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:

Tactic:
μ (s ∩ t) + μ (s \ t) = μ (s ∩ t) + μ (⋃ n, S n) := by rw [iUnion_S]
    _ ≤ μ (s ∩ t) + ⨆ n, μ (S n) := by gcongr
    _ = ⨆ n, μ (s ∩ t) + μ (S n) := ENNReal.add_iSup ..
    _ ≤ μ s := iSup_le hSs

Goal state after:
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
s : Set Y
⊢ μHE[d] (f ⁻¹' s) = μHE[d] (s ∩ Set.range f)

Tactic:
by
  simp_rw [euclideanHausdorffMeasure_def, Measure.smul_apply]
  rw [Isometry.hausdorffMeasure_preimage hf (by simp)]

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

Goal state before:
pp: ⊢ dimH univ = 1

Tactic:
rw [dimH_univ_eq_finrank ℝ, Module.finrank_self, Nat.cast_one]

Goal state after: