harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
theorem ContinuousMultilinearMap.curry_uncurryRight
    (f : ContinuousMultilinearMap 𝕜 (fun i : Fin n => Ei <| castSucc i) (Ei (last n) →L[𝕜] G)) :
    f.uncurryRight.curryRight = f

Proof state:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 (fun i => Ei i.castSucc) (Ei (last n) →L[𝕜] G)
⊢ f.uncurryRight.curryRight = f

Tactic:
ext m x

Result:
case H.h
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 (fun i => Ei i.castSucc) (Ei (last n) →L[𝕜] G)
m : (i : Fin n) → Ei i.castSucc
x : Ei (last n)
⊢ (f.uncurryRight.curryRight m) x = (f m) x

Proof state:
case H.h
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 (fun i => Ei i.castSucc) (Ei (last n) →L[𝕜] G)
m : (i : Fin n) → Ei i.castSucc
x : Ei (last n)
⊢ (f.uncurryRight.curryRight m) x = (f m) x

Tactic:
rw [ContinuousMultilinearMap.curryRight_apply, ContinuousMultilinearMap.uncurryRight_apply,
  snoc_last, init_snoc]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_neg_self_right {x : V} (hx : x ≠ 0) : o.oangle x (-x) = π

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
⊢ o.oangle x (-x) = ↑π

Tactic:
simp [oangle_neg_right, hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem not_mem_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
    m.isEmpty → ¬a ∈ m

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a : α
⊢ m.isEmpty = true → ¬a ∈ m

Tactic:
simpa [mem_iff_contains] using contains_of_isEmpty h

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
theorem ι_range_map_lift (f : M →ₗ[R] A) (cond : ∀ m, f m * f m = algebraMap _ _ (Q m)) :
    (ι Q).range.map (lift Q ⟨f, cond⟩).toLinearMap = LinearMap.range f

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)
⊢ Submodule.map ((lift Q) ⟨f, cond⟩).toLinearMap (LinearMap.range (ι Q)) = LinearMap.range f

Tactic:
rw [← LinearMap.range_comp, ι_comp_lift]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem IsTopologicalGroup.of_comm_of_nhds_one {G : Type u} [CommGroup G] [TopologicalSpace G]
    (hmul : Tendsto (uncurry ((· * ·) : G → G → G)) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1))
    (hinv : Tendsto (fun x : G => x⁻¹) (𝓝 1) (𝓝 1))
    (hleft : ∀ x₀ : G, 𝓝 x₀ = map (x₀ * ·) (𝓝 1)) : IsTopologicalGroup G :=
  IsTopologicalGroup.of_nhds_one hmul hinv hleft (by simpa using tendsto_id)

Proof state:
G : Type u
inst✝¹ : CommGroup G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
⊢ ∀ (x₀ : G), Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)

Tactic:
simpa using tendsto_id

Result:
no goals
-- Mathlib/Order/SupClosed.lean
lemma supClosed_range [FunLike F α β] [SupHomClass F α β] (f : F) : SupClosed (Set.range f)

Proof state:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
⊢ SupClosed (range ⇑f)

Tactic:
simpa using supClosed_univ.image f

Result:
no goals
-- Mathlib/Algebra/Ring/NegOnePow.lean
theorem abs_negOnePow (n : ℤ) : |(n.negOnePow : ℤ)| = 1

Proof state:
n : ℤ
⊢ |↑n.negOnePow| = 1

Tactic:
rw [abs_eq_natAbs, Int.units_natAbs, Nat.cast_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_mul' (a m n : Nat) : a ^ (m * n) = (a ^ n) ^ m

Proof state:
a m n : Nat
⊢ a ^ (m * n) = (a ^ n) ^ m

Tactic:
rw [← Nat.pow_mul, Nat.mul_comm]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem finite_spans_dense [DecidableEq E] (b : HilbertBasis ι 𝕜 E) :
    (⨆ J : Finset ι, span 𝕜 (J.image b : Set E)).topologicalClosure = ⊤ :=
  eq_top_iff.mpr <| b.dense_span.ge.trans (by
    simp_rw [← Submodule.span_iUnion]
    exact topologicalClosure_mono (span_mono <| Set.range_subset_iff.mpr fun i =>
      Set.mem_iUnion_of_mem {i} <| Finset.mem_coe.mpr <| Finset.mem_image_of_mem _ <|
      Finset.mem_singleton_self i))

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
b : HilbertBasis ι 𝕜 E
⊢ (span 𝕜 (Set.range ⇑b)).topologicalClosure ≤ (⨆ J, span 𝕜 ↑(Finset.image (⇑b) J)).topologicalClosure

Tactic:
simp_rw [← Submodule.span_iUnion]

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
b : HilbertBasis ι 𝕜 E
⊢ (span 𝕜 (Set.range ⇑b)).topologicalClosure ≤ (span 𝕜 (⋃ i, ↑(Finset.image (⇑b) i))).topologicalClosure

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
b : HilbertBasis ι 𝕜 E
⊢ (span 𝕜 (Set.range ⇑b)).topologicalClosure ≤ (span 𝕜 (⋃ i, ↑(Finset.image (⇑b) i))).topologicalClosure

Tactic:
exact topologicalClosure_mono (span_mono <| Set.range_subset_iff.mpr fun i =>
  Set.mem_iUnion_of_mem {i} <| Finset.mem_coe.mpr <| Finset.mem_image_of_mem _ <|
  Finset.mem_singleton_self i)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem zero_xor (x : Nat) : 0 ^^^ x = x

Proof state:
case pred
x : Nat
⊢ ∀ (i : Nat), (0 ^^^ x).testBit i = x.testBit i

Tactic:
simp

Result:
no goals

Proof state:
x : Nat
⊢ 0 ^^^ x = x

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
x : Nat
⊢ ∀ (i : Nat), (0 ^^^ x).testBit i = x.testBit i
-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
@[to_additive]
lemma closure_pow_le : ∀ {n}, n ≠ 0 → closure (s ^ n) ≤ closure s
  | 1, _ => by simp
  | n + 2, _ =>
    calc
      closure (s ^ (n + 2))
      _ = closure (s ^ (n + 1) * s)

Proof state:
M : Type u_3
inst✝ : Monoid M
s : Set M
n : ℕ
x✝ : n + 2 ≠ 0
⊢ closure (s ^ (n + 1)) ⊔ closure s ≤ closure s ⊔ closure s

Tactic:
gcongr ?_ ⊔ _

Result:
case h₁
M : Type u_3
inst✝ : Monoid M
s : Set M
n : ℕ
x✝ : n + 2 ≠ 0
⊢ closure (s ^ (n + 1)) ≤ closure s

Proof state:
M : Type u_3
inst✝ : Monoid M
s : Set M
n : ℕ
x✝ : n + 2 ≠ 0
⊢ closure (s ^ (n + 2)) = closure (s ^ (n + 1) * s)

Tactic:
rw [pow_succ]

Result:
no goals

Proof state:
M : Type u_3
inst✝ : Monoid M
s : Set M
x✝ : 1 ≠ 0
⊢ closure (s ^ 1) ≤ closure s

Tactic:
simp

Result:
no goals

Proof state:
case h₁
M : Type u_3
inst✝ : Monoid M
s : Set M
n : ℕ
x✝ : n + 2 ≠ 0
⊢ closure (s ^ (n + 1)) ≤ closure s

Tactic:
exact closure_pow_le n.succ_ne_zero

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem Ico_succ_left : Ico a.succ b = Ioo a b

Proof state:
case h
a b x : ℕ
⊢ x ∈ Ico a.succ b ↔ x ∈ Ioo a b

Tactic:
rw [mem_Ico, mem_Ioo, succ_le_iff]

Result:
no goals

Proof state:
a b : ℕ
⊢ Ico a.succ b = Ioo a b

Tactic:
ext x

Result:
case h
a b x : ℕ
⊢ x ∈ Ico a.succ b ↔ x ∈ Ioo a b
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem sum_apply_of_countable [Countable ι] (f : ι → Measure α) (s : Set α) :
    sum f s = ∑' i, f i s

Proof state:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst✝ : Countable ι
f : ι → Measure α
s t : Set α
hst : s ⊆ t
htm : MeasurableSet t
ht : ∀ (i : ι), (f i) t = (f i) s
⊢ ∑' (i : ι), (f i) t = ∑' (i : ι), (f i) s

Tactic:
simp [ht]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst✝ : Countable ι
f : ι → Measure α
s : Set α
⊢ (sum f) s = ∑' (i : ι), (f i) s

Tactic:
apply le_antisymm ?_ (le_sum_apply _ _)

Result:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst✝ : Countable ι
f : ι → Measure α
s : Set α
⊢ (sum f) s ≤ ∑' (i : ι), (f i) s

Proof state:
case intro.intro.intro
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst✝ : Countable ι
f : ι → Measure α
s t : Set α
hst : s ⊆ t
htm : MeasurableSet t
ht : ∀ (i : ι), (f i) t = (f i) s
⊢ (sum f) s ≤ ∑' (i : ι), (f i) s

Tactic:
calc
sum f s ≤ sum f t := measure_mono hst
_ = ∑' i, f i t := sum_apply _ htm
_ = ∑' i, f i s := by simp [ht]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst✝ : Countable ι
f : ι → Measure α
s : Set α
⊢ (sum f) s ≤ ∑' (i : ι), (f i) s

Tactic:
rcases exists_measurable_superset_forall_eq f s with ⟨t, hst, htm, ht⟩

Result:
case intro.intro.intro
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst✝ : Countable ι
f : ι → Measure α
s t : Set α
hst : s ⊆ t
htm : MeasurableSet t
ht : ∀ (i : ι), (f i) t = (f i) s
⊢ (sum f) s ≤ ∑' (i : ι), (f i) s
-- Mathlib/Data/Nat/PartENat.lean
theorem add_right_cancel_iff {a b c : PartENat} (hc : c ≠ ⊤) : a + c = b + c ↔ a = b

Proof state:
case intro.refine_2.refine_2
a b : PartENat
c : ℕ
hc : ↑c ≠ ⊤
⊢ ∀ (n n_1 : ℕ), ↑n_1 + ↑c = ↑n + ↑c ↔ n_1 = n

Tactic:
simp only [← Nat.cast_add, add_left_cancel_iff, PartENat.natCast_inj, add_comm, forall_const]

Result:
no goals

Proof state:
a b c : PartENat
hc : c ≠ ⊤
⊢ a + c = b + c ↔ a = b

Tactic:
rcases ne_top_iff.1 hc with ⟨c, rfl⟩

Result:
case intro
a b : PartENat
c : ℕ
hc : ↑c ≠ ⊤
⊢ a + ↑c = b + ↑c ↔ a = b

Proof state:
case intro
a b : PartENat
c : ℕ
hc : ↑c ≠ ⊤
⊢ a + ↑c = b + ↑c ↔ a = b

Tactic:
refine PartENat.casesOn a ?_ ?_
<;> refine PartENat.casesOn b ?_ ?_
<;> simp [add_eq_top_iff, natCast_ne_top, @eq_comm _ (⊤ : PartENat), top_add]

Result:
case intro.refine_2.refine_2
a b : PartENat
c : ℕ
hc : ↑c ≠ ⊤
⊢ ∀ (n n_1 : ℕ), ↑n_1 + ↑c = ↑n + ↑c ↔ n_1 = n
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem norm_le_of_forall_le' [Nonempty α] {f : lp E ∞} (C : ℝ) (hCf : ∀ i, ‖f i‖ ≤ C) :
    ‖f‖ ≤ C

Proof state:
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Nonempty α
f : ↥(lp E ⊤)
C : ℝ
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
⊢ C ∈ upperBounds (Set.range fun i => ‖↑f i‖)

Tactic:
rintro - ⟨i, rfl⟩

Result:
case intro
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Nonempty α
f : ↥(lp E ⊤)
C : ℝ
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
i : α
⊢ (fun i => ‖↑f i‖) i ≤ C

Proof state:
case intro
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Nonempty α
f : ↥(lp E ⊤)
C : ℝ
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
i : α
⊢ (fun i => ‖↑f i‖) i ≤ C

Tactic:
exact hCf i

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Nonempty α
f : ↥(lp E ⊤)
C : ℝ
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
⊢ ‖f‖ ≤ C

Tactic:
refine (isLUB_norm f).2 ?_

Result:
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Nonempty α
f : ↥(lp E ⊤)
C : ℝ
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
⊢ C ∈ upperBounds (Set.range fun i => ‖↑f i‖)
-- Mathlib/Data/Finset/Lattice/Basic.lean
theorem union_right_comm (s t u : Finset α) : s ∪ t ∪ u = s ∪ u ∪ t :=
  ext fun x => by simp only [mem_union, or_assoc, @or_comm (x ∈ t)]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
x : α
⊢ x ∈ s ∪ t ∪ u ↔ x ∈ s ∪ u ∪ t

Tactic:
simp only [mem_union, or_assoc, @or_comm (x ∈ t)]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Span.lean
theorem factors_decreasing [IsDomain α] (b₁ b₂ : α) (h₁ : b₁ ≠ 0) (h₂ : ¬IsUnit b₂) :
    span ({b₁ * b₂} : Set α) < span {b₁} :=
  lt_of_le_not_le
    (Ideal.span_le.2 <| singleton_subset_iff.2 <| Ideal.mem_span_singleton.2 ⟨b₂, rfl⟩) fun h =>
    h₂ <| isUnit_of_dvd_one <|
        (mul_dvd_mul_iff_left h₁).1 <| by rwa [mul_one, ← Ideal.span_singleton_le_span_singleton]

Proof state:
α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
b₁ b₂ : α
h₁ : b₁ ≠ 0
h₂ : ¬IsUnit b₂
h : span {b₁} ≤ span {b₁ * b₂}
⊢ b₁ * b₂ ∣ b₁ * 1

Tactic:
rwa [mul_one, ← Ideal.span_singleton_le_span_singleton]

Result:
no goals
-- Mathlib/GroupTheory/DoubleCoset.lean
theorem mk_eq_of_doset_eq {H K : Subgroup G} {a b : G} (h : doset a H K = doset b H K) :
    mk H K a = mk H K b

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : doset a ↑H ↑K = doset b ↑H ↑K
⊢ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k

Tactic:
exact mem_doset.mp (h.symm ▸ mem_doset_self H K b)

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : doset a ↑H ↑K = doset b ↑H ↑K
⊢ mk H K a = mk H K b

Tactic:
rw [eq]

Result:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : doset a ↑H ↑K = doset b ↑H ↑K
⊢ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem map_one_snd_of_isMulTwoCocycle {f : G × G → M} (hf : IsMulTwoCocycle f) (g : G) :
    f (g, 1) = g • f (1, 1)

Proof state:
G : Type u_1
M : Type u_2
inst✝² : Monoid G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G × G → M
hf : IsMulTwoCocycle f
g : G
⊢ f (g, 1) = g • f (1, 1)

Tactic:
simpa only [mul_one, mul_left_inj] using hf g 1 1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem alterKey_append_of_containsKey_right_eq_false {a : α} {f : Option (β a) → Option (β a)}
    {l l' : List ((a : α) × β a)} (hc : containsKey a l' = false) :
    alterKey a f (l ++ l') = alterKey a f l ++ l'

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l l' : List ((a : α) × β a)
hc : containsKey a l' = false
⊢ alterKey a f (l ++ l') = alterKey a f l ++ l'

Tactic:
simp only [alterKey, getValueCast?_append_of_containsKey_eq_false hc,
  eraseKey_append_of_containsKey_right_eq_false hc, insertEntry_append_of_not_contains_right hc]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l l' : List ((a : α) × β a)
hc : containsKey a l' = false
⊢ (match f (getValueCast? a l) with
    | none => eraseKey a l ++ l'
    | some v => insertEntry a v l ++ l') =
    (match f (getValueCast? a l) with
      | none => eraseKey a l
      | some v => insertEntry a v l) ++
      l'

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l l' : List ((a : α) × β a)
hc : containsKey a l' = false
⊢ (match f (getValueCast? a l) with
    | none => eraseKey a l ++ l'
    | some v => insertEntry a v l ++ l') =
    (match f (getValueCast? a l) with
      | none => eraseKey a l
      | some v => insertEntry a v l) ++
      l'

Tactic:
split <;> rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sin_eq_real_sin_iff_eq_or_add_eq_pi {θ : Angle} {ψ : ℝ} :
    sin θ = Real.sin ψ ↔ θ = ψ ∨ θ + ψ = π

Proof state:
case h
ψ x✝ : ℝ
⊢ (↑x✝).sin = Real.sin ψ ↔ ↑x✝ = ↑ψ ∨ ↑x✝ + ↑ψ = ↑π

Tactic:
exact sin_eq_iff_coe_eq_or_add_eq_pi

Result:
no goals

Proof state:
θ : Angle
ψ : ℝ
⊢ θ.sin = Real.sin ψ ↔ θ = ↑ψ ∨ θ + ↑ψ = ↑π

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
ψ x✝ : ℝ
⊢ (↑x✝).sin = Real.sin ψ ↔ ↑x✝ = ↑ψ ∨ ↑x✝ + ↑ψ = ↑π
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem hasFTaylorSeriesUpToOn_top_iff_add (hN : ∞ ≤ N) (k : ℕ) :
    HasFTaylorSeriesUpToOn N f p s ↔ ∀ n : ℕ, HasFTaylorSeriesUpToOn (n + k : ℕ) f p s

Proof state:
case mpr.fderivWithin
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
k : ℕ
H : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k)) f p s
⊢ ∀ (m : ℕ), ↑m < N → ∀ x ∈ s, HasFDerivWithinAt (fun x => p x m) (p x m.succ).curryLeft s x

Tactic:
intro m _

Result:
case mpr.fderivWithin
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
k : ℕ
H : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k)) f p s
m : ℕ
a✝ : ↑m < N
⊢ ∀ x ∈ s, HasFDerivWithinAt (fun x => p x m) (p x m.succ).curryLeft s x

Proof state:
case mpr.cont
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
k : ℕ
H : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k)) f p s
⊢ ∀ (m : ℕ), ↑m ≤ N → ContinuousOn (fun x => p x m) s

Tactic:
intro m _

Result:
case mpr.cont
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
k : ℕ
H : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k)) f p s
m : ℕ
a✝ : ↑m ≤ N
⊢ ContinuousOn (fun x => p x m) s

Proof state:
case mpr.zero_eq
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
k : ℕ
H : ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k)) f p s
⊢ ∀ x ∈ s, (p x 0).curry0 = f x

Tactic:
exact (H 0).zero_eq

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_trim {X} {m m0 : MeasurableSpace X} {μ : Measure X} (hm : m ≤ m0) {f : X → E}
    (hf_meas : StronglyMeasurable[m] f) {s : Set X} (hs : MeasurableSet[m] s) :
    ∫ x in s, f x ∂μ = ∫ x in s, f x ∂μ.trim hm

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
X : Type u_5
m m0 : MeasurableSpace X
μ : Measure X
hm : m ≤ m0
f : X → E
hf_meas : StronglyMeasurable f
s : Set X
hs : MeasurableSet s
⊢ ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, f x ∂μ.trim hm

Tactic:
rwa [integral_trim hm hf_meas, restrict_trim hm μ]

Result:
no goals
-- Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean
theorem strictConcaveOn_cos_Icc : StrictConcaveOn ℝ (Icc (-(π / 2)) (π / 2)) cos

Proof state:
⊢ StrictConcaveOn ℝ (Icc (-(π / 2)) (π / 2)) cos

Tactic:
apply strictConcaveOn_of_deriv2_neg (convex_Icc _ _) continuousOn_cos fun x hx => ?_

Result:
x : ℝ
hx : x ∈ interior (Icc (-(π / 2)) (π / 2))
⊢ deriv^[2] cos x < 0

Proof state:
x : ℝ
hx : x ∈ interior (Icc (-(π / 2)) (π / 2))
⊢ deriv^[2] cos x < 0

Tactic:
rw [interior_Icc] at hx

Result:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ deriv^[2] cos x < 0

Proof state:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ deriv^[2] cos x < 0

Tactic:
simp [cos_pos_of_mem_Ioo hx]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive]
lemma mem_smul_finset {x : β} : x ∈ a • s ↔ ∃ y, y ∈ s ∧ a • y = x

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : SMul α β
s : Finset β
a : α
x : β
⊢ x ∈ a • s ↔ ∃ y ∈ s, a • y = x

Tactic:
simp only [Finset.smul_finset_def, and_assoc, mem_image, exists_prop, Prod.exists, mem_product]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem mem_powers_of_prime_card {p : ℕ} [hp : Fact p.Prime]
    (h : Nat.card G = p) {g g' : G} (hg : g ≠ 1) : g' ∈ Submonoid.powers g

Proof state:
G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
this : Finite G
⊢ g' ∈ Submonoid.powers g

Tactic:
rw [mem_powers_iff_mem_zpowers]

Result:
G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
this : Finite G
⊢ g' ∈ zpowers g

Proof state:
G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
⊢ g' ∈ Submonoid.powers g

Tactic:
have : Finite G := Nat.finite_of_card_ne_zero (h ▸ hp.1.ne_zero)

Result:
G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
this : Finite G
⊢ g' ∈ Submonoid.powers g

Proof state:
G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
this : Finite G
⊢ g' ∈ zpowers g

Tactic:
exact mem_zpowers_of_prime_card h hg

Result:
no goals
-- Mathlib/Data/Nat/Pairing.lean
theorem left_le_pair (a b : ℕ) : a ≤ pair a b

Proof state:
a b : ℕ
⊢ a ≤ pair a b

Tactic:
simpa using unpair_left_le (pair a b)

Result:
no goals
-- Mathlib/FieldTheory/Cardinality.lean
theorem Field.nonempty_iff {α : Type u} : Nonempty (Field α) ↔ IsPrimePow #α

Proof state:
case inr
α : Type u
h : Infinite α
⊢ Nonempty (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ n, #α = ↑n ∧ IsPrimePow n

Tactic:
simpa only [← Cardinal.infinite_iff, h, true_or, iff_true] using Infinite.nonempty_field

Result:
no goals

Proof state:
case inl
α : Type u
h : Fintype α
⊢ Nonempty (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ n, #α = ↑n ∧ IsPrimePow n

Tactic:
simpa only [Cardinal.mk_fintype, Nat.cast_inj, exists_eq_left',
  (Cardinal.nat_lt_aleph0 _).not_le, false_or] using Fintype.nonempty_field_iff

Result:
no goals

Proof state:
α : Type u
⊢ Nonempty (Field α) ↔ IsPrimePow #α

Tactic:
rw [Cardinal.isPrimePow_iff]

Result:
α : Type u
⊢ Nonempty (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ n, #α = ↑n ∧ IsPrimePow n

Proof state:
α : Type u
⊢ Nonempty (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ n, #α = ↑n ∧ IsPrimePow n

Tactic:
obtain h | h := fintypeOrInfinite α

Result:
case inl
α : Type u
h : Fintype α
⊢ Nonempty (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ n, #α = ↑n ∧ IsPrimePow n

case inr
α : Type u
h : Infinite α
⊢ Nonempty (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ n, #α = ↑n ∧ IsPrimePow n
-- Mathlib/CategoryTheory/GradedObject.lean
lemma congr_mapMap (φ₁ φ₂ : X ⟶ Y) (h : φ₁ = φ₂) : mapMap φ₁ p = mapMap φ₂ p

Proof state:
I : Type u_1
J : Type u_2
C : Type u_4
inst✝² : Category.{u_5, u_4} C
X Y : GradedObject I C
p : I → J
inst✝¹ : X.HasMap p
inst✝ : Y.HasMap p
φ₁ : X ⟶ Y
⊢ mapMap φ₁ p = mapMap φ₁ p

Tactic:
rfl

Result:
no goals

Proof state:
I : Type u_1
J : Type u_2
C : Type u_4
inst✝² : Category.{u_5, u_4} C
X Y : GradedObject I C
p : I → J
inst✝¹ : X.HasMap p
inst✝ : Y.HasMap p
φ₁ φ₂ : X ⟶ Y
h : φ₁ = φ₂
⊢ mapMap φ₁ p = mapMap φ₂ p

Tactic:
subst h

Result:
I : Type u_1
J : Type u_2
C : Type u_4
inst✝² : Category.{u_5, u_4} C
X Y : GradedObject I C
p : I → J
inst✝¹ : X.HasMap p
inst✝ : Y.HasMap p
φ₁ : X ⟶ Y
⊢ mapMap φ₁ p = mapMap φ₁ p
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_one_add_X_pow (R : Type*) [Semiring R] (n k : ℕ) :
    ((1 + X) ^ n).coeff k = (n.choose k : R)

Proof state:
R : Type u_1
inst✝ : Semiring R
n k : ℕ
⊢ ((1 + X) ^ n).coeff k = ↑(n.choose k)

Tactic:
rw [add_comm _ X, coeff_X_add_one_pow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Dvd.lean
theorem mod_mod_of_dvd (a : Nat) (h : c ∣ b) : a % b % c = a % c

Proof state:
c b a : Nat
h : c ∣ b
⊢ a % b % c = (a % b + b * (a / b)) % c

Tactic:
have ⟨x, h⟩ := h

Result:
c b a : Nat
h✝ : c ∣ b
x : Nat
h : b = c * x
⊢ a % b % c = (a % b + b * (a / b)) % c

Proof state:
c b a : Nat
h : c ∣ b
⊢ a % b % c = a % c

Tactic:
rw (occs := [2]) [← mod_add_div a b]

Result:
c b a : Nat
h : c ∣ b
⊢ a % b % c = (a % b + b * (a / b)) % c

Proof state:
c a x : Nat
h : c ∣ c * x
⊢ a % (c * x) % c = (a % (c * x) + c * x * (a / (c * x))) % c

Tactic:
rw [Nat.mul_assoc, add_mul_mod_self_left]

Result:
no goals

Proof state:
c b a : Nat
h✝ : c ∣ b
x : Nat
h : b = c * x
⊢ a % b % c = (a % b + b * (a / b)) % c

Tactic:
subst h

Result:
c a x : Nat
h : c ∣ c * x
⊢ a % (c * x) % c = (a % (c * x) + c * x * (a / (c * x))) % c