harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma degree_norm_smul_basis [IsDomain R] (p q : R[X]) :
    (Algebra.norm R[X] <| p • (1 : W.CoordinateRing) + q • mk W Y).degree =
      max (2 • p.degree) (2 • q.degree + 3)

Proof state:
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ 2 * dq + 3 < 2 * dp

Tactic:
linarith only [hpq]

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
theorem Finset.centerMass_pair (hne : i ≠ j) :
    ({i, j} : Finset ι).centerMass w z = (w i / (w i + w j)) • z i + (w j / (w i + w j)) • z j

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i j : ι
w : ι → R
z : ι → E
hne : i ≠ j
⊢ {i, j}.centerMass w z = (w i / (w i + w j)) • z i + (w j / (w i + w j)) • z j

Tactic:
simp only [centerMass, sum_pair hne]

Result:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i j : ι
w : ι → R
z : ι → E
hne : i ≠ j
⊢ (w i + w j)⁻¹ • (w i • z i + w j • z j) = (w i / (w i + w j)) • z i + (w j / (w i + w j)) • z j

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i j : ι
w : ι → R
z : ι → E
hne : i ≠ j
⊢ (w i + w j)⁻¹ • (w i • z i + w j • z j) = (w i / (w i + w j)) • z i + (w j / (w i + w j)) • z j

Tactic:
module

Result:
no goals
-- Mathlib/Data/Set/Opposite.lean
theorem singleton_op_unop (x : α) : ({op x} : Set αᵒᵖ).unop = {x}

Proof state:
α : Type u_1
x : α
⊢ {op x}.unop = {x}

Tactic:
ext

Result:
case h
α : Type u_1
x x✝ : α
⊢ x✝ ∈ {op x}.unop ↔ x✝ ∈ {x}

Proof state:
case h
α : Type u_1
x x✝ : α
⊢ x✝ ∈ {op x}.unop ↔ x✝ ∈ {x}

Tactic:
constructor

Result:
case h.mp
α : Type u_1
x x✝ : α
⊢ x✝ ∈ {op x}.unop → x✝ ∈ {x}

case h.mpr
α : Type u_1
x x✝ : α
⊢ x✝ ∈ {x} → x✝ ∈ {op x}.unop

Proof state:
case h.mpr
α : Type u_1
x x✝ : α
⊢ x✝ ∈ {x} → x✝ ∈ {op x}.unop

Tactic:
apply unop_injective

Result:
no goals

Proof state:
case h.mp
α : Type u_1
x x✝ : α
⊢ x✝ ∈ {op x}.unop → x✝ ∈ {x}

Tactic:
apply op_injective

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem ite_false_true {_ : Decidable p} : (ite p False True) = ¬p

Proof state:
p : Prop
x✝ : Decidable p
⊢ (if p then False else True) = ¬p

Tactic:
by_cases p <;> simp

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoUniformlyOnFilter.congr {F' : ι → α → β} (hf : TendstoUniformlyOnFilter F f p p')
    (hff' : ∀ᶠ n : ι × α in p ×ˢ p', F n.fst n.snd = F' n.fst n.snd) :
    TendstoUniformlyOnFilter F' f p p'

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p p'
hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', F n.1 n.2 = F' n.1 n.2
u : Set (β × β)
hu : u ∈ 𝓤 β
n : ι × α
h : (f n.2, F n.1 n.2) ∈ u ∧ F n.1 n.2 = F' n.1 n.2
⊢ (f n.2, F n.1 n.2) ∈ u

Tactic:
exact h.left

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p p'
hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', F n.1 n.2 = F' n.1 n.2
⊢ TendstoUniformlyOnFilter F' f p p'

Tactic:
refine fun u hu => ((hf u hu).and hff').mono fun n h => ?_

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p p'
hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', F n.1 n.2 = F' n.1 n.2
u : Set (β × β)
hu : u ∈ 𝓤 β
n : ι × α
h : (f n.2, F n.1 n.2) ∈ u ∧ F n.1 n.2 = F' n.1 n.2
⊢ (f n.2, F' n.1 n.2) ∈ u

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p p'
hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', F n.1 n.2 = F' n.1 n.2
u : Set (β × β)
hu : u ∈ 𝓤 β
n : ι × α
h : (f n.2, F n.1 n.2) ∈ u ∧ F n.1 n.2 = F' n.1 n.2
⊢ (f n.2, F' n.1 n.2) ∈ u

Tactic:
rw [← h.right]

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p p'
hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', F n.1 n.2 = F' n.1 n.2
u : Set (β × β)
hu : u ∈ 𝓤 β
n : ι × α
h : (f n.2, F n.1 n.2) ∈ u ∧ F n.1 n.2 = F' n.1 n.2
⊢ (f n.2, F n.1 n.2) ∈ u
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem map_fval {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] {x y : ZFSet.{u}}
    (h : y ∈ x) : (ZFSet.map f x ′ y : Class.{u}) = f y :=
  Class.iota_val _ _ fun z => by
    rw [Class.toSet_of_ZFSet, Class.coe_apply, mem_map]
    exact
      ⟨fun ⟨w, _, pr⟩ => by
        let ⟨wy, fw⟩ := ZFSet.pair_injective pr
        rw [← fw, wy], fun e => by
        subst e
        exact ⟨_, h, rfl⟩⟩

Proof state:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
⊢ Class.ToSet (fun x_1 => ↑(map f x) (x_1.pair z)) ↑y ↔ z = f y

Tactic:
rw [Class.toSet_of_ZFSet, Class.coe_apply, mem_map]

Result:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
⊢ (∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z) ↔ z = f y

Proof state:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
e : z = f y
⊢ ∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z

Tactic:
subst e

Result:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
⊢ ∃ z ∈ x, z.pair (f z) = y.pair (f y)

Proof state:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
⊢ ∃ z ∈ x, z.pair (f z) = y.pair (f y)

Tactic:
exact ⟨_, h, rfl⟩

Result:
no goals

Proof state:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
x✝ : ∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z
w : ZFSet.{u}
left✝ : w ∈ x
pr : w.pair (f w) = y.pair z
wy : w = y
fw : f w = z
⊢ z = f y

Tactic:
rw [← fw, wy]

Result:
no goals

Proof state:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
x✝ : ∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z
w : ZFSet.{u}
left✝ : w ∈ x
pr : w.pair (f w) = y.pair z
⊢ z = f y

Tactic:
let ⟨wy, fw⟩ := ZFSet.pair_injective pr

Result:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
x✝ : ∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z
w : ZFSet.{u}
left✝ : w ∈ x
pr : w.pair (f w) = y.pair z
wy : w = y
fw : f w = z
⊢ z = f y

Proof state:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
⊢ (∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z) ↔ z = f y

Tactic:
exact
  ⟨fun ⟨w, _, pr⟩ => by
    let ⟨wy, fw⟩ := ZFSet.pair_injective pr
    rw [← fw, wy], fun e => by
    subst e
    exact ⟨_, h, rfl⟩⟩

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Killing.lean
lemma exists_isSl2Triple_of_weight_isNonZero {α : Weight K H L} (hα : α.IsNonZero) :
    ∃ h e f : L, IsSl2Triple h e f ∧ e ∈ rootSpace H α ∧ f ∈ rootSpace H (- α)

Proof state:
case intro.intro.intro.intro.refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e : L
heα : e ∈ rootSpace H ⇑α
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-⇑α)
hf : ((killingForm K L) e) f' ≠ 0
hef✝ : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H := ⟨⁅e, f'⁆, ⋯⟩
hh : α h ≠ 0
f : L := (2 * (α h)⁻¹) • f'
hef : ⁅⁅e, f⁆, e⁆ = 2 • e
contra : ⁅e, f⁆ = 0
⊢ False

Tactic:
rw [contra] at hef

Result:
case intro.intro.intro.intro.refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e : L
heα : e ∈ rootSpace H ⇑α
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-⇑α)
hf : ((killingForm K L) e) f' ≠ 0
hef✝ : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H := ⟨⁅e, f'⁆, ⋯⟩
hh : α h ≠ 0
f : L := (2 * (α h)⁻¹) • f'
hef : ⁅0, e⁆ = 2 • e
contra : ⁅e, f⁆ = 0
⊢ False
-- Mathlib/RingTheory/Idempotents.lean
lemma OrthogonalIdempotents.equiv {J} (i : J ≃ I) :
    OrthogonalIdempotents (e ∘ i) ↔ OrthogonalIdempotents e

Proof state:
R : Type u_1
inst✝ : Semiring R
I : Type u_3
e : I → R
J : Type u_4
i : J ≃ I
⊢ OrthogonalIdempotents (e ∘ ⇑i) ↔ OrthogonalIdempotents e

Tactic:
simp [iff_mul_eq, i.forall_congr_left]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
I : Type u_3
e : I → R
J : Type u_4
i : J ≃ I
⊢ OrthogonalIdempotents (e ∘ ⇑i) ↔ OrthogonalIdempotents e

Tactic:
classical
simp [iff_mul_eq, i.forall_congr_left]

Result:
no goals
-- Mathlib/CategoryTheory/CofilteredSystem.lean
theorem nonempty_sections_of_finite_inverse_system {J : Type u} [Preorder J] [IsDirected J (· ≤ ·)]
    (F : Jᵒᵖ ⥤ Type v) [∀ j : Jᵒᵖ, Finite (F.obj j)] [∀ j : Jᵒᵖ, Nonempty (F.obj j)] :
    F.sections.Nonempty

Proof state:
case inl
J : Type u
inst✝³ : Preorder J
inst✝² : IsDirected J fun x1 x2 => x1 ≤ x2
F : Jᵒᵖ ⥤ Type v
inst✝¹ : ∀ (j : Jᵒᵖ), Finite (F.obj j)
inst✝ : ∀ (j : Jᵒᵖ), Nonempty (F.obj j)
h✝ : IsEmpty J
this : IsEmpty Jᵒᵖ
⊢ F.sections.Nonempty

Tactic:
exact ⟨isEmptyElim, by apply isEmptyElim⟩

Result:
no goals

Proof state:
case inl
J : Type u
inst✝³ : Preorder J
inst✝² : IsDirected J fun x1 x2 => x1 ≤ x2
F : Jᵒᵖ ⥤ Type v
inst✝¹ : ∀ (j : Jᵒᵖ), Finite (F.obj j)
inst✝ : ∀ (j : Jᵒᵖ), Nonempty (F.obj j)
h✝ : IsEmpty J
⊢ F.sections.Nonempty

Tactic:
haveI : IsEmpty Jᵒᵖ := ⟨fun j => isEmptyElim j.unop⟩

Result:
case inl
J : Type u
inst✝³ : Preorder J
inst✝² : IsDirected J fun x1 x2 => x1 ≤ x2
F : Jᵒᵖ ⥤ Type v
inst✝¹ : ∀ (j : Jᵒᵖ), Finite (F.obj j)
inst✝ : ∀ (j : Jᵒᵖ), Nonempty (F.obj j)
h✝ : IsEmpty J
this : IsEmpty Jᵒᵖ
⊢ F.sections.Nonempty

Proof state:
case inr
J : Type u
inst✝³ : Preorder J
inst✝² : IsDirected J fun x1 x2 => x1 ≤ x2
F : Jᵒᵖ ⥤ Type v
inst✝¹ : ∀ (j : Jᵒᵖ), Finite (F.obj j)
inst✝ : ∀ (j : Jᵒᵖ), Nonempty (F.obj j)
h✝ : Nonempty J
⊢ F.sections.Nonempty

Tactic:
exact nonempty_sections_of_finite_cofiltered_system _

Result:
no goals

Proof state:
J : Type u
inst✝³ : Preorder J
inst✝² : IsDirected J fun x1 x2 => x1 ≤ x2
F : Jᵒᵖ ⥤ Type v
inst✝¹ : ∀ (j : Jᵒᵖ), Finite (F.obj j)
inst✝ : ∀ (j : Jᵒᵖ), Nonempty (F.obj j)
h✝ : IsEmpty J
this : IsEmpty Jᵒᵖ
⊢ (fun a => isEmptyElim a) ∈ F.sections

Tactic:
apply isEmptyElim

Result:
no goals

Proof state:
J : Type u
inst✝³ : Preorder J
inst✝² : IsDirected J fun x1 x2 => x1 ≤ x2
F : Jᵒᵖ ⥤ Type v
inst✝¹ : ∀ (j : Jᵒᵖ), Finite (F.obj j)
inst✝ : ∀ (j : Jᵒᵖ), Nonempty (F.obj j)
⊢ F.sections.Nonempty

Tactic:
cases isEmpty_or_nonempty J

Result:
case inl
J : Type u
inst✝³ : Preorder J
inst✝² : IsDirected J fun x1 x2 => x1 ≤ x2
F : Jᵒᵖ ⥤ Type v
inst✝¹ : ∀ (j : Jᵒᵖ), Finite (F.obj j)
inst✝ : ∀ (j : Jᵒᵖ), Nonempty (F.obj j)
h✝ : IsEmpty J
⊢ F.sections.Nonempty

case inr
J : Type u
inst✝³ : Preorder J
inst✝² : IsDirected J fun x1 x2 => x1 ≤ x2
F : Jᵒᵖ ⥤ Type v
inst✝¹ : ∀ (j : Jᵒᵖ), Finite (F.obj j)
inst✝ : ∀ (j : Jᵒᵖ), Nonempty (F.obj j)
h✝ : Nonempty J
⊢ F.sections.Nonempty
-- Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
@[simp]
lemma volume_closedBall_fin_two (x : EuclideanSpace ℝ (Fin 2)) (r : ℝ) :
    volume (closedBall x r) = .ofReal r ^ 2 * .ofReal π

Proof state:
x : EuclideanSpace ℝ (Fin 2)
r : ℝ
⊢ volume (closedBall x r) = ENNReal.ofReal r ^ 2 * ENNReal.ofReal π

Tactic:
rw [addHaar_closedBall_eq_addHaar_ball, volume_ball_fin_two x r]

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircleMulti.lean
theorem orthonormal_mFourier : Orthonormal ℂ (mFourierLp (d := d) 2)

Proof state:
d : Type u_1
inst✝ : Fintype d
⊢ ∀ (i j : d → ℤ), inner (mFourierLp 2 i) (mFourierLp 2 j) = if i = j then 1 else 0

Tactic:
intro m n

Result:
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
⊢ inner (mFourierLp 2 m) (mFourierLp 2 n) = if m = n then 1 else 0

Proof state:
case neg.intro
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
h : ¬m = n
i : d
hi : m i ≠ n i
⊢ ∫ (x : UnitAddCircle), (fourier ((-m + n) i)) x = 0

Tactic:
simpa only [eq_false_intro hi, if_false, ContinuousMap.inner_toLp, ← fourier_neg,
  ← fourier_add] using (orthonormal_iff_ite.mp <| orthonormal_fourier) (m i) (n i)

Result:
no goals

Proof state:
case pos
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
h : m = n
⊢ ∫ (x : UnitAddTorus d), (mFourier (-m + n)) x = 1

Tactic:
simpa only [h, neg_add_cancel, mFourier_zero, measure_univ, ENNReal.one_toReal, one_smul] using
  integral_const (α := UnitAddTorus d) (μ := volume) (1 : ℂ)

Result:
no goals

Proof state:
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
⊢ inner (mFourierLp 2 m) (mFourierLp 2 n) = if m = n then 1 else 0

Tactic:
simp only [ContinuousMap.inner_toLp, ← mFourier_neg, ← mFourier_add]

Result:
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
⊢ ∫ (x : UnitAddTorus d), (mFourier (-m + n)) x = if m = n then 1 else 0

Proof state:
case neg
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
h : ¬m = n
⊢ ∏ i : d, ∫ (x : UnitAddCircle), (fourier ((-m + n) i)) x = 0

Tactic:
obtain ⟨i, hi⟩ := Function.ne_iff.mp h

Result:
case neg.intro
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
h : ¬m = n
i : d
hi : m i ≠ n i
⊢ ∏ i : d, ∫ (x : UnitAddCircle), (fourier ((-m + n) i)) x = 0

Proof state:
d : Type u_1
inst✝ : Fintype d
⊢ Orthonormal ℂ (mFourierLp 2)

Tactic:
rw [orthonormal_iff_ite]

Result:
d : Type u_1
inst✝ : Fintype d
⊢ ∀ (i j : d → ℤ), inner (mFourierLp 2 i) (mFourierLp 2 j) = if i = j then 1 else 0

Proof state:
case neg.intro
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
h : ¬m = n
i : d
hi : m i ≠ n i
⊢ ∏ i : d, ∫ (x : UnitAddCircle), (fourier ((-m + n) i)) x = 0

Tactic:
apply Finset.prod_eq_zero (Finset.mem_univ i)

Result:
case neg.intro
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
h : ¬m = n
i : d
hi : m i ≠ n i
⊢ ∫ (x : UnitAddCircle), (fourier ((-m + n) i)) x = 0

Proof state:
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
⊢ ∫ (x : UnitAddTorus d), (mFourier (-m + n)) x = if m = n then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
h : m = n
⊢ ∫ (x : UnitAddTorus d), (mFourier (-m + n)) x = 1

case neg
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
h : ¬m = n
⊢ ∫ (x : UnitAddTorus d), (mFourier (-m + n)) x = 0

Proof state:
case neg
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
h : ¬m = n
⊢ ∫ (x : UnitAddTorus d), (mFourier (-m + n)) x = 0

Tactic:
rw [mFourier, ContinuousMap.coe_mk, MeasureTheory.integral_fintype_prod_eq_prod]

Result:
case neg
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
h : ¬m = n
⊢ ∏ i : d, ∫ (x : UnitAddCircle), (fourier ((-m + n) i)) x = 0
-- Mathlib/Data/Nat/Totient.lean
theorem totient_mul_prod_primeFactors (n : ℕ) :
    (φ n * ∏ p ∈ n.primeFactors, p) = n * ∏ p ∈ n.primeFactors, (p - 1)

Proof state:
case pos
n : ℕ
hn : n = 0
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
simp [hn]

Result:
no goals

Proof state:
case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : 0 < n.factorization p
⊢ p ^ (n.factorization p - 1) * (p - 1) * p = p ^ n.factorization p * (p - 1)

Tactic:
rw [mul_comm, ← mul_assoc, ← pow_succ', Nat.sub_one, Nat.succ_pred_eq_of_pos hp]

Result:
no goals

Proof state:
case neg
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun p k => p ^ (k - 1) * (p - 1)) * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
nth_rw 3 [← factorization_prod_pow_eq_self hn]

Result:
case neg
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun p k => p ^ (k - 1) * (p - 1)) * ∏ p ∈ n.primeFactors, p =
    (n.factorization.prod fun x1 x2 => x1 ^ x2) * ∏ p ∈ n.primeFactors, (p - 1)

Proof state:
case neg
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun a b => a ^ (b - 1) * (a - 1) * a) = n.factorization.prod fun a b => a ^ b * (a - 1)

Tactic:
refine Finsupp.prod_congr (M := ℕ) (N := ℕ) fun p hp => ?_

Result:
case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : p ∈ n.factorization.support
⊢ p ^ (n.factorization p - 1) * (p - 1) * p = p ^ n.factorization p * (p - 1)

Proof state:
case neg
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun p k => p ^ (k - 1) * (p - 1)) * ∏ p ∈ n.primeFactors, p =
    (n.factorization.prod fun x1 x2 => x1 ^ x2) * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
simp only [prod_primeFactors_prod_factorization, ← Finsupp.prod_mul]

Result:
case neg
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun a b => a ^ (b - 1) * (a - 1) * a) = n.factorization.prod fun a b => a ^ b * (a - 1)

Proof state:
case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : p ∈ n.factorization.support
⊢ p ^ (n.factorization p - 1) * (p - 1) * p = p ^ n.factorization p * (p - 1)

Tactic:
rw [Finsupp.mem_support_iff, ← zero_lt_iff] at hp

Result:
case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : 0 < n.factorization p
⊢ p ^ (n.factorization p - 1) * (p - 1) * p = p ^ n.factorization p * (p - 1)

Proof state:
n : ℕ
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
by_cases hn : n = 0

Result:
case pos
n : ℕ
hn : n = 0
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

case neg
n : ℕ
hn : ¬n = 0
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

Proof state:
case neg
n : ℕ
hn : ¬n = 0
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
rw [totient_eq_prod_factorization hn]

Result:
case neg
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun p k => p ^ (k - 1) * (p - 1)) * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)
-- Mathlib/RingTheory/DedekindDomain/Dvr.lean
theorem IsLocalization.AtPrime.not_isField {P : Ideal A} (hP : P ≠ ⊥) [pP : P.IsPrime] (Aₘ : Type*)
    [CommRing Aₘ] [Algebra A Aₘ] [IsLocalization.AtPrime Aₘ P] : ¬ IsField Aₘ

Proof state:
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
h : IsField Aₘ
⊢ False

Tactic:
letI := h.toField

Result:
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
h : IsField Aₘ
this : Field Aₘ := h.toField
⊢ False

Proof state:
case intro.intro
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
h : IsField Aₘ
this : Field Aₘ := h.toField
x : A
x_mem : x ∈ P
x_ne : x ≠ 0
⊢ False

Tactic:
exact
  (IsLocalRing.maximalIdeal.isMaximal _).ne_top
    (Ideal.eq_top_of_isUnit_mem _
      ((IsLocalization.AtPrime.to_map_mem_maximal_iff Aₘ P _).mpr x_mem)
      (isUnit_iff_ne_zero.mpr
        ((map_ne_zero_iff (algebraMap A Aₘ)
              (IsLocalization.injective Aₘ P.primeCompl_le_nonZeroDivisors)).mpr
          x_ne)))

Result:
no goals

Proof state:
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
⊢ ¬IsField Aₘ

Tactic:
intro h

Result:
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
h : IsField Aₘ
⊢ False

Proof state:
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
h : IsField Aₘ
this : Field Aₘ := h.toField
⊢ False

Tactic:
obtain ⟨x, x_mem, x_ne⟩ := P.ne_bot_iff.mp hP

Result:
case intro.intro
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
h : IsField Aₘ
this : Field Aₘ := h.toField
x : A
x_mem : x ∈ P
x_ne : x ≠ 0
⊢ False
-- Mathlib/CategoryTheory/Functor/Category.lean
theorem congr_app {α β : F ⟶ G} (h : α = β) (X : C) : α.app X = β.app X

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α β : F ⟶ G
h : α = β
X : C
⊢ α.app X = β.app X

Tactic:
rw [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem modCore_eq_mod (n m : Nat) : Nat.modCore n m = n % m

Proof state:
case false
n m n✝ x✝ : Nat
h : ¬x✝ ≤ n✝ + 1
⊢ (n✝ + 1).modCore x✝ = n✝ + 1

Tactic:
rw [Nat.modCore]

Result:
case false
n m n✝ x✝ : Nat
h : ¬x✝ ≤ n✝ + 1
⊢ ite (0 < x✝ ∧ x✝ ≤ n✝ + 1) ((n✝ + 1 - x✝).modCore x✝) (n✝ + 1) = n✝ + 1

Proof state:
n m x✝ : Nat
⊢ ite (0 < x✝ ∧ x✝ ≤ 0) ((0 - x✝).modCore x✝) 0 = Nat.mod 0 x✝

Tactic:
exact if_neg fun ⟨hlt, hle⟩ => Nat.lt_irrefl _ (Nat.lt_of_lt_of_le hlt hle)

Result:
no goals

Proof state:
n m n✝ x✝ : Nat
⊢ (n✝ + 1).modCore x✝ = ite (x✝ ≤ n✝ + 1) ((n✝ + 1).modCore x✝) (n✝ + 1)

Tactic:
refine iteInduction (fun _ => rfl) (fun h => ?false)

Result:
case false
n m n✝ x✝ : Nat
h : ¬x✝ ≤ n✝ + 1
⊢ (n✝ + 1).modCore x✝ = n✝ + 1

Proof state:
n m : Nat
⊢ n.modCore m = n.mod m

Tactic:
match n, m with
| 0, _ =>
  rw [Nat.modCore]
  exact if_neg fun ⟨hlt, hle⟩ => Nat.lt_irrefl _ (Nat.lt_of_lt_of_le hlt hle)
| (_ + 1), _ =>
  rw [Nat.mod]; dsimp
  refine iteInduction (fun _ => rfl) (fun h => ?false) rw [Nat.modCore]
  exact if_neg fun ⟨_hlt, hle⟩ => h hle

Result:
no goals

Proof state:
n m n✝ x✝ : Nat
⊢ (n✝ + 1).modCore x✝ = (n✝ + 1).mod x✝

Tactic:
rw [Nat.mod]

Result:
n m n✝ x✝ : Nat
⊢ (n✝ + 1).modCore x✝ = ite (x✝ ≤ n✝.succ) (n✝.succ.modCore x✝) n✝.succ

Proof state:
n m x✝ : Nat
⊢ Nat.modCore 0 x✝ = Nat.mod 0 x✝

Tactic:
rw [Nat.modCore]

Result:
n m x✝ : Nat
⊢ ite (0 < x✝ ∧ x✝ ≤ 0) ((0 - x✝).modCore x✝) 0 = Nat.mod 0 x✝

Proof state:
n m : Nat
⊢ n.modCore m = n % m

Tactic:
show Nat.modCore n m = Nat.mod n m

Result:
n m : Nat
⊢ n.modCore m = n.mod m

Proof state:
case false
n m n✝ x✝ : Nat
h : ¬x✝ ≤ n✝ + 1
⊢ ite (0 < x✝ ∧ x✝ ≤ n✝ + 1) ((n✝ + 1 - x✝).modCore x✝) (n✝ + 1) = n✝ + 1

Tactic:
exact if_neg fun ⟨_hlt, hle⟩ => h hle

Result:
no goals

Proof state:
n m n✝ x✝ : Nat
⊢ (n✝ + 1).modCore x✝ = ite (x✝ ≤ n✝.succ) (n✝.succ.modCore x✝) n✝.succ

Tactic:
dsimp

Result:
n m n✝ x✝ : Nat
⊢ (n✝ + 1).modCore x✝ = ite (x✝ ≤ n✝ + 1) ((n✝ + 1).modCore x✝) (n✝ + 1)
-- Mathlib/Data/Option/Defs.lean
theorem mem_some_iff {α : Type*} {a b : α} : a ∈ some b ↔ b = a

Proof state:
α : Type u_3
a b : α
⊢ a ∈ some b ↔ b = a

Tactic:
simp

Result:
no goals