harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem descPochhammer_eval_eq_descFactorial (n k : ℕ) :
    (descPochhammer R k).eval (n : R) = n.descFactorial k

Proof state:
case zero
R : Type u
inst✝ : Ring R
n : ℕ
⊢ eval (↑n) (descPochhammer R 0) = ↑(n.descFactorial 0)

Tactic:
rw [descPochhammer_zero, eval_one, Nat.descFactorial_zero, Nat.cast_one]

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
h : n < k
⊢ (↑n - ↑k) * ↑(n.descFactorial k) = ↑((n - k) * n.descFactorial k)

Tactic:
rw [Nat.descFactorial_eq_zero_iff_lt.mpr h, Nat.cast_zero, mul_zero, mul_zero, Nat.cast_zero]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
⊢ (↑n - ↑k) * ↑(n.descFactorial k) = ↑((n - k) * n.descFactorial k)

Tactic:
by_cases h : n < k

Result:
case pos
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
h : n < k
⊢ (↑n - ↑k) * ↑(n.descFactorial k) = ↑((n - k) * n.descFactorial k)

case neg
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
h : ¬n < k
⊢ (↑n - ↑k) * ↑(n.descFactorial k) = ↑((n - k) * n.descFactorial k)

Proof state:
case neg
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
h : ¬n < k
⊢ (↑n - ↑k) * ↑(n.descFactorial k) = ↑((n - k) * n.descFactorial k)

Tactic:
rw [Nat.cast_mul, Nat.cast_sub <| not_lt.mp h]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
⊢ eval (↑n) (descPochhammer R (k + 1)) = ↑(n.descFactorial (k + 1))

Tactic:
rw [descPochhammer_succ_right, Nat.descFactorial_succ, mul_sub, eval_sub, eval_mul_X,
  ← Nat.cast_comm k, eval_natCast_mul, ← Nat.cast_comm n, ← sub_mul, ih]

Result:
case succ
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
⊢ (↑n - ↑k) * ↑(n.descFactorial k) = ↑((n - k) * n.descFactorial k)
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem norm_setToSimpleFunc_le_integral_norm (T : Set α → E →L[ℝ] F) {C : ℝ}
    (hT_norm : ∀ s, MeasurableSet s → μ s < ∞ → ‖T s‖ ≤ C * (μ s).toReal) {f : α →ₛ E}
    (hf : Integrable f μ) : ‖f.setToSimpleFunc T‖ ≤ C * (f.map norm).integral μ :=
  calc
    ‖f.setToSimpleFunc T‖ ≤ C * ∑ x ∈ f.range, ENNReal.toReal (μ (f ⁻¹' {x})) * ‖x‖ :=
      norm_setToSimpleFunc_le_sum_mul_norm_of_integrable T hT_norm f hf
    _ = C * (f.map norm).integral μ

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
T : Set α → E →L[ℝ] F
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ C * ∑ x ∈ f.range, (μ (⇑f ⁻¹' {x})).toReal * ‖x‖ = C * ∑ x ∈ f.range, (μ (⇑f ⁻¹' {x})).toReal • ‖x‖

Tactic:
simp_rw [smul_eq_mul]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
T : Set α → E →L[ℝ] F
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ C * ∑ x ∈ f.range, (μ (⇑f ⁻¹' {x})).toReal * ‖x‖ = C * integral μ (map norm f)

Tactic:
rw [map_integral f norm hf norm_zero]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
T : Set α → E →L[ℝ] F
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ C * ∑ x ∈ f.range, (μ (⇑f ⁻¹' {x})).toReal * ‖x‖ = C * ∑ x ∈ f.range, (μ (⇑f ⁻¹' {x})).toReal • ‖x‖
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_two_right (n : ℕ) : choose n 2 = n * (n - 1) / 2

Proof state:
case zero

⊢ choose 0 2 = 0 * (0 - 1) / 2

Tactic:
simp

Result:
no goals

Proof state:
case succ
n : ℕ
ih : n.choose 2 = n * (n - 1) / 2
⊢ n.choose 1 + n * (n - 1) / 2 = n * (n - 1) / 2 + n

Tactic:
simp [Nat.add_comm]

Result:
no goals

Proof state:
case succ
n : ℕ
ih : n.choose 2 = n * (n - 1) / 2
⊢ (n + 1).choose 2 = (n + 1) * (n + 1 - 1) / 2

Tactic:
rw [triangle_succ n, choose, ih]

Result:
case succ
n : ℕ
ih : n.choose 2 = n * (n - 1) / 2
⊢ n.choose 1 + n * (n - 1) / 2 = n * (n - 1) / 2 + n

Proof state:
n : ℕ
⊢ n.choose 2 = n * (n - 1) / 2

Tactic:
induction' n with n ih

Result:
case zero

⊢ choose 0 2 = 0 * (0 - 1) / 2

case succ
n : ℕ
ih : n.choose 2 = n * (n - 1) / 2
⊢ (n + 1).choose 2 = (n + 1) * (n + 1 - 1) / 2
-- Mathlib/Order/CompleteLattice.lean
theorem le_iInf₂_iff {f : ∀ i, κ i → α} : (a ≤ ⨅ (i) (j), f i j) ↔ ∀ i j, a ≤ f i j

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLattice α
a : α
f : (i : ι) → κ i → α
⊢ a ≤ ⨅ i, ⨅ j, f i j ↔ ∀ (i : ι) (j : κ i), a ≤ f i j

Tactic:
simp_rw [le_iInf_iff]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem exists_lt_add {α} [hα : Nonempty α] {o : Ordinal} {f : α → Ordinal}
    (H : ∀ ⦃a⦄, a < o → ∃ i, a < f i) {b : Ordinal} ⦃a⦄ (h : a < b + o) : ∃ i, a < b + f i

Proof state:
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h : a < b + o
⊢ ∃ i, a < b + f i

Tactic:
rcases lt_or_le a b with h | h'

Result:
case inl
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h✝ : a < b + o
h : a < b
⊢ ∃ i, a < b + f i

case inr
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h : a < b + o
h' : b ≤ a
⊢ ∃ i, a < b + f i

Proof state:
case inl
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h✝ : a < b + o
h : a < b
⊢ ∃ i, a < b + f i

Tactic:
obtain ⟨i⟩ := id hα

Result:
case inl.intro
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h✝ : a < b + o
h : a < b
i : α
⊢ ∃ i, a < b + f i

Proof state:
case inr
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h : a < b + o
h' : b ≤ a
⊢ ∃ i, a < b + f i

Tactic:
rw [← Ordinal.add_sub_cancel_of_le h', add_lt_add_iff_left] at h

Result:
case inr
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h : a - b < o
h' : b ≤ a
⊢ ∃ i, a < b + f i

Proof state:
case inr
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h : a - b < o
h' : b ≤ a
⊢ ∃ i, a < b + f i

Tactic:
refine (H h).imp fun i H => ?_

Result:
case inr
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H✝ : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h : a - b < o
h' : b ≤ a
i : α
H : a - b < f i
⊢ a < b + f i

Proof state:
case inr
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H✝ : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h : a - b < o
h' : b ≤ a
i : α
H : a - b < f i
⊢ a < b + f i

Tactic:
rwa [← Ordinal.add_sub_cancel_of_le h', add_lt_add_iff_left]

Result:
no goals

Proof state:
case inl.intro
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h✝ : a < b + o
h : a < b
i : α
⊢ ∃ i, a < b + f i

Tactic:
exact ⟨i, h.trans_le (le_add_right _ _)⟩

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem tendsto_setToFun_approxOn_of_measurable_of_range_subset
    (hT : DominatedFinMeasAdditive μ T C) [MeasurableSpace E] [BorelSpace E] {f : α → E}
    (fmeas : Measurable f) (hf : Integrable f μ) (s : Set E) [SeparableSpace s]
    (hs : range f ∪ {0} ⊆ s) :
    Tendsto (fun n => setToFun μ T hT (SimpleFunc.approxOn f fmeas s 0 (hs <| by simp) n)) atTop
      (𝓝 <| setToFun μ T hT f)

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝³ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
s : Set E
inst✝ : SeparableSpace ↑s
hs : Set.range f ∪ {0} ⊆ s
⊢ Tendsto (fun n => setToFun μ T hT ⇑(SimpleFunc.approxOn f fmeas s 0 ⋯ n)) atTop (𝓝 (setToFun μ T hT f))

Tactic:
refine tendsto_setToFun_approxOn_of_measurable hT hf fmeas ?_ _ (integrable_zero _ _ _)

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝³ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
s : Set E
inst✝ : SeparableSpace ↑s
hs : Set.range f ∪ {0} ⊆ s
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ closure s

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
G : Type u_5
𝕜 : Type u_6
p : ℝ≥0∞
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup F'
inst✝⁵ : NormedSpace ℝ F'
inst✝⁴ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝³ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
hT : DominatedFinMeasAdditive μ T C
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
s : Set E
inst✝ : SeparableSpace ↑s
hs : Set.range f ∪ {0} ⊆ s
n : ℕ
⊢ 0 ∈ Set.range f ∪ {0}

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝³ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
s : Set E
inst✝ : SeparableSpace ↑s
hs : Set.range f ∪ {0} ⊆ s
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ closure s

Tactic:
exact Eventually.of_forall fun x => subset_closure (hs (Set.mem_union_left _ (mem_range_self _)))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_concat_succ {x : BitVec w} {i : Nat} (h : i + 1 < w + 1) :
    (concat x b)[i + 1] = x[i]

Proof state:
w : Nat
b : Bool
x : BitVec w
i : Nat
h✝ : i + 1 < w + 1
h : i < w
⊢ (x.concat b)[i + 1] = x[i]

Tactic:
simp [getElem_concat, h, getLsbD_eq_getElem]

Result:
no goals

Proof state:
w : Nat
b : Bool
x : BitVec w
i : Nat
h : i + 1 < w + 1
⊢ (x.concat b)[i + 1] = x[i]

Tactic:
simp only [Nat.add_lt_add_iff_right] at h

Result:
w : Nat
b : Bool
x : BitVec w
i : Nat
h✝ : i + 1 < w + 1
h : i < w
⊢ (x.concat b)[i + 1] = x[i]
-- Mathlib/Analysis/Convex/Intrinsic.lean
theorem intrinsicClosure_mono (h : s ⊆ t) : intrinsicClosure 𝕜 s ⊆ intrinsicClosure 𝕜 t

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
h : s ⊆ t
x : ↥(affineSpan 𝕜 s)
hx : x ∈ closure (Subtype.val ⁻¹' s)
⊢ Subtype.val ⁻¹' s ⊆ Set.inclusion ⋯ ⁻¹' (Subtype.val ⁻¹' t)

Tactic:
exact fun y hy => h hy

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
h : s ⊆ t
x : ↥(affineSpan 𝕜 s)
hx : x ∈ closure (Subtype.val ⁻¹' s)
⊢ x ∈ Subtype.val ⁻¹' intrinsicClosure 𝕜 t

Tactic:
refine ⟨Set.inclusion (affineSpan_mono _ h) x, ?_, rfl⟩

Result:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
h : s ⊆ t
x : ↥(affineSpan 𝕜 s)
hx : x ∈ closure (Subtype.val ⁻¹' s)
⊢ Set.inclusion ⋯ x ∈ closure (Subtype.val ⁻¹' t)

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
h : s ⊆ t
x : ↥(affineSpan 𝕜 s)
hx : x ∈ closure (Subtype.val ⁻¹' s)
⊢ Set.inclusion ⋯ x ∈ closure (Subtype.val ⁻¹' t)

Tactic:
refine (continuous_inclusion (affineSpan_mono _ h)).closure_preimage_subset _ (closure_mono ?_ hx)

Result:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
h : s ⊆ t
x : ↥(affineSpan 𝕜 s)
hx : x ∈ closure (Subtype.val ⁻¹' s)
⊢ Subtype.val ⁻¹' s ⊆ Set.inclusion ⋯ ⁻¹' (Subtype.val ⁻¹' t)

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
h : s ⊆ t
⊢ intrinsicClosure 𝕜 s ⊆ intrinsicClosure 𝕜 t

Tactic:
refine image_subset_iff.2 fun x hx => ?_

Result:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s t : Set P
h : s ⊆ t
x : ↥(affineSpan 𝕜 s)
hx : x ∈ closure (Subtype.val ⁻¹' s)
⊢ x ∈ Subtype.val ⁻¹' intrinsicClosure 𝕜 t
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem iUnion_Icc_zsmul : ⋃ n : ℤ, Icc (n • p) ((n + 1) • p) = univ

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
⊢ ⋃ n, Icc (n • p) ((n + 1) • p) = univ

Tactic:
simpa only [zero_add] using iUnion_Icc_add_zsmul hp 0

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourierSubalgebra_separatesPoints : (@fourierSubalgebra T).SeparatesPoints

Proof state:
T : ℝ
hT : Fact (0 < T)
⊢ fourierSubalgebra.SeparatesPoints

Tactic:
intro x y hxy

Result:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑fourierSubalgebra.toSubalgebra, f x ≠ f y

Proof state:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ (fourier 1) x ≠ (fourier 1) y

Tactic:
rw [fourier_one, fourier_one]

Result:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ ↑x.toCircle ≠ ↑y.toCircle

Proof state:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ (fun f => ⇑f) (fourier 1) x ≠ (fun f => ⇑f) (fourier 1) y

Tactic:
dsimp only

Result:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ (fourier 1) x ≠ (fourier 1) y

Proof state:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : ↑x.toCircle = ↑y.toCircle
⊢ x = y

Tactic:
rw [Subtype.coe_inj] at hxy

Result:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x.toCircle = y.toCircle
⊢ x = y

Proof state:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑fourierSubalgebra.toSubalgebra, f x ≠ f y

Tactic:
refine ⟨_, ⟨fourier 1, subset_adjoin ⟨1, rfl⟩, rfl⟩, ?_⟩

Result:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ (fun f => ⇑f) (fourier 1) x ≠ (fun f => ⇑f) (fourier 1) y

Proof state:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x.toCircle = y.toCircle
⊢ x = y

Tactic:
exact injective_toCircle hT.elim.ne' hxy

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ ↑x.toCircle ≠ ↑y.toCircle

Tactic:
contrapose! hxy

Result:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : ↑x.toCircle = ↑y.toCircle
⊢ x = y
-- Mathlib/GroupTheory/HNNExtension.lean
theorem unitsSMulGroup_snd (u : ℤˣ) (g : G) :
    (unitsSMulGroup φ d u g).2 = ((d.compl u).equiv g).2

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g : G
⊢ (unitsSMulGroup φ d u g).2 = (⋯.equiv g).2

Tactic:
rcases Int.units_eq_one_or u with rfl | rfl <;> rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
/-- The special-value formula `Γ(k + 1 + 1/2) = (2 * k + 1)‼ * √π / (2 ^ (k + 1))` for half-integer
values of the gamma function in terms of `Nat.doubleFactorial`. -/
lemma Real.Gamma_nat_add_one_add_half (k : ℕ) :
    Gamma (k + 1 + 1 / 2) = (2 * k + 1 : ℕ)‼ * √π / (2 ^ (k + 1))

Proof state:
case succ
k : ℕ
ih : Gamma (↑k + 1 + 1 / 2) = ↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)
⊢ Gamma (↑(k + 1) + 1 + 1 / 2) = ↑(2 * (k + 1) + 1)‼ * √π / 2 ^ (k + 1 + 1)

Tactic:
rw [add_right_comm, Gamma_add_one (by positivity), Nat.cast_add, Nat.cast_one, ih, Nat.mul_add]

Result:
case succ
k : ℕ
ih : Gamma (↑k + 1 + 1 / 2) = ↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)
⊢ (↑k + 1 + 1 / 2) * (↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)) = ↑(2 * k + 2 * 1 + 1)‼ * √π / 2 ^ (k + 1 + 1)

Proof state:
case zero

⊢ Gamma (↑0 + 1 + 1 / 2) = ↑(2 * 0 + 1)‼ * √π / 2 ^ (0 + 1)

Tactic:
simp [-one_div, add_comm (1 : ℝ), Gamma_add_one, Gamma_one_half_eq]

Result:
case zero

⊢ 1 / 2 * √π = √π / 2

Proof state:
case succ
k : ℕ
ih : Gamma (↑k + 1 + 1 / 2) = ↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)
⊢ ((↑k + 1) * 2 + 1) * (↑(2 * k + 1)‼ * √π) * 2 ^ (k + 1 + 1) =
    (2 * ↑k + 1 + 2) * ↑(2 * k + 1)‼ * √π * (2 * 2 ^ (k + 1))

Tactic:
ring

Result:
no goals

Proof state:
case succ
k : ℕ
ih : Gamma (↑k + 1 + 1 / 2) = ↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)
⊢ (↑k + 1 + 1 / 2) * (↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)) = ↑(2 * k + 2 * 1 + 1)‼ * √π / 2 ^ (k + 1 + 1)

Tactic:
field_simp

Result:
case succ
k : ℕ
ih : Gamma (↑k + 1 + 1 / 2) = ↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)
⊢ ((↑k + 1) * 2 + 1) * (↑(2 * k + 1)‼ * √π) * 2 ^ (k + 1 + 1) =
    (2 * ↑k + 1 + 2) * ↑(2 * k + 1)‼ * √π * (2 * 2 ^ (k + 1))

Proof state:
k : ℕ
⊢ Gamma (↑k + 1 + 1 / 2) = ↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)

Tactic:
induction k with
| zero => simp [-one_div, add_comm (1 : ℝ), Gamma_add_one, Gamma_one_half_eq]; ring
| succ k ih =>
  rw [add_right_comm, Gamma_add_one (by positivity), Nat.cast_add, Nat.cast_one, ih, Nat.mul_add]
  field_simp
  ring

Result:
no goals

Proof state:
case zero

⊢ 1 / 2 * √π = √π / 2

Tactic:
ring

Result:
no goals

Proof state:
k : ℕ
ih : Gamma (↑k + 1 + 1 / 2) = ↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)
⊢ ↑(k + 1) + 1 / 2 ≠ 0

Tactic:
positivity

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseIdx_eq_self : ∀ {l : List α} {k : Nat}, eraseIdx l k = l ↔ length l ≤ k
  | [], _ => by simp
  | a::l, 0 => by simp [(cons_ne_self _ _).symm]
  | a::l, k + 1 => by simp [eraseIdx_eq_self]

Proof state:
α : Type u_1
x✝ : Nat
⊢ [].eraseIdx x✝ = [] ↔ [].length ≤ x✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
l : List α
k : Nat
⊢ (a :: l).eraseIdx (k + 1) = a :: l ↔ (a :: l).length ≤ k + 1

Tactic:
simp [eraseIdx_eq_self]

Result:
no goals

Proof state:
α : Type u_1
a : α
l : List α
⊢ (a :: l).eraseIdx 0 = a :: l ↔ (a :: l).length ≤ 0

Tactic:
simp [(cons_ne_self _ _).symm]

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem div_rat (h : Irrational x) {q : ℚ} (hq : q ≠ 0) : Irrational (x / q)

Proof state:
x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x * ↑q⁻¹)

Tactic:
exact h.mul_rat (inv_ne_zero hq)

Result:
no goals

Proof state:
x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x / ↑q)

Tactic:
rw [div_eq_mul_inv, ← cast_inv]

Result:
x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x * ↑q⁻¹)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Compare.lean
theorem compare_ne_lt {a b : Nat} : compare a b ≠ .lt ↔ b ≤ a

Proof state:
a b : Nat
⊢ (if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt) ≠ Ordering.lt ↔ b ≤ a

Tactic:
repeat' split

Result:
case isTrue.isTrue
a b : Nat
h✝¹ : a ≤ b
h✝ : b ≤ a
⊢ Ordering.eq ≠ Ordering.lt ↔ b ≤ a

case isTrue.isFalse
a b : Nat
h✝¹ : a ≤ b
h✝ : ¬b ≤ a
⊢ Ordering.lt ≠ Ordering.lt ↔ b ≤ a

case isFalse
a b : Nat
h✝ : ¬a ≤ b
⊢ Ordering.gt ≠ Ordering.lt ↔ b ≤ a

Proof state:
a b : Nat
⊢ compare a b ≠ Ordering.lt ↔ b ≤ a

Tactic:
rw [compare_def_le]

Result:
a b : Nat
⊢ (if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt) ≠ Ordering.lt ↔ b ≤ a

Proof state:
a b : Nat
⊢ (if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt) ≠ Ordering.lt ↔ b ≤ a

Tactic:
(repeat' split) <;> simp [Nat.le_of_not_le, *]

Result:
no goals

Proof state:
case isTrue
a b : Nat
h✝ : a ≤ b
⊢ (if b ≤ a then Ordering.eq else Ordering.lt) ≠ Ordering.lt ↔ b ≤ a

Tactic:
split

Result:
case isTrue.isTrue
a b : Nat
h✝¹ : a ≤ b
h✝ : b ≤ a
⊢ Ordering.eq ≠ Ordering.lt ↔ b ≤ a

case isTrue.isFalse
a b : Nat
h✝¹ : a ≤ b
h✝ : ¬b ≤ a
⊢ Ordering.lt ≠ Ordering.lt ↔ b ≤ a
-- Mathlib/GroupTheory/Sylow.lean
theorem smul_eq_iff_mem_normalizer {g : G} {P : Sylow p G} :
    g • P = P ↔ g ∈ P.normalizer

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
g : G
P : Sylow p G
⊢ (∀ (x : G), x ∈ P ↔ x ∈ g • P) ↔ ∀ (h : G), h ∈ ↑P ↔ g⁻¹ * h * g ∈ ↑P

Tactic:
exact
  forall_congr' fun h =>
    iff_congr Iff.rfl
      ⟨fun ⟨a, b, c⟩ => c ▸ by simpa [mul_assoc] using b,
        fun hh => ⟨(MulAut.conj g)⁻¹ h, hh, MulAut.apply_inv_self G (MulAut.conj g) h⟩⟩

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
g : G
P : Sylow p G
h : G
x✝ : h ∈ g • P
a : G
b : a ∈ ↑↑P
c : ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) a = h
⊢ g⁻¹ * ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) a * g ∈ ↑P

Tactic:
simpa [mul_assoc] using b

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
g : G
P : Sylow p G
⊢ g • P = P ↔ g ∈ (↑P).normalizer

Tactic:
rw [eq_comm, SetLike.ext_iff, ← inv_mem_iff (G := G) (H := normalizer P.toSubgroup),
    mem_normalizer_iff, inv_inv]

Result:
p : ℕ
G : Type u_1
inst✝ : Group G
g : G
P : Sylow p G
⊢ (∀ (x : G), x ∈ P ↔ x ∈ g • P) ↔ ∀ (h : G), h ∈ ↑P ↔ g⁻¹ * h * g ∈ ↑P
-- Mathlib/Analysis/Calculus/FDeriv/Linear.lean
theorem ContinuousLinearMap.fderivWithin (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 e s x = e

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E →L[𝕜] F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 (⇑e) x = e

Tactic:
exact e.fderiv

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E →L[𝕜] F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (⇑e) s x = e

Tactic:
rw [DifferentiableAt.fderivWithin e.differentiableAt hxs]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E →L[𝕜] F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 (⇑e) x = e
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem ExprCnstr.eq_true_of_isValid (ctx : Context) (c : ExprCnstr) (h : c.toNormPoly.isValid) : c.denote ctx = True

Proof state:
ctx : Context
c : ExprCnstr
h : c.toNormPoly.isValid = true
this : PolyCnstr.denote ctx c.toNormPoly = True
⊢ denote ctx c = True

Tactic:
simp [-eq_iff_iff] at this

Result:
ctx : Context
c : ExprCnstr
h : c.toNormPoly.isValid = true
this : denote ctx c = True
⊢ denote ctx c = True

Proof state:
ctx : Context
c : ExprCnstr
h : c.toNormPoly.isValid = true
⊢ denote ctx c = True

Tactic:
have := PolyCnstr.eq_true_of_isValid ctx h

Result:
ctx : Context
c : ExprCnstr
h : c.toNormPoly.isValid = true
this : PolyCnstr.denote ctx c.toNormPoly = True
⊢ denote ctx c = True

Proof state:
ctx : Context
c : ExprCnstr
h : c.toNormPoly.isValid = true
this : denote ctx c = True
⊢ denote ctx c = True

Tactic:
assumption

Result:
no goals