harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Iio_union_Ioo (h : min c d < b) : Iio b ∪ Ioo c d = Iio (max b d)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h : c ⊓ d < b
⊢ Iio b ∪ Ioo c d = Iio (b ⊔ d)

Tactic:
rcases le_total c d with hcd | hcd <;> simp [hcd] at h

Result:
case inl
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : c ≤ d
h : c < b
⊢ Iio b ∪ Ioo c d = Iio (b ⊔ d)

case inr
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : d ≤ c
h : d < b
⊢ Iio b ∪ Ioo c d = Iio (b ⊔ d)

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : c ≤ d
h : c < b
⊢ Iio b ∪ Ioo c d = Iio (b ⊔ d)

Tactic:
exact Iio_union_Ioo' h

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : d ≤ c
h : d < b
⊢ Iio b ∪ Ioo c d = Iio (b ⊔ d)

Tactic:
rw [max_comm]

Result:
case inr
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : d ≤ c
h : d < b
⊢ Iio b ∪ Ioo c d = Iio (d ⊔ b)

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : d ≤ c
h : d < b
⊢ Iio b ∪ Ioo c d = Iio (d ⊔ b)

Tactic:
simp [*, max_eq_right_of_lt h]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma IsCycle.three_le_length {v : V} {p : G.Walk v v} (hp : p.IsCycle) : 3 ≤ p.length

Proof state:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
v✝ : V
h✝¹ : G.Adj v v✝
h✝ : G.Adj v✝ v
hp✝ : (cons h✝¹ (cons h✝ nil)).IsCycle
hp : (cons h✝¹ (cons h✝ nil)).IsTrail
hp' : cons h✝¹ (cons h✝ nil) ≠ nil
support_nodup✝ : (cons h✝¹ (cons h✝ nil)).support.tail.Nodup
⊢ 3 ≤ (cons h✝¹ (cons h✝ nil)).length

Tactic:
simp at hp

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
v✝² : V
h✝² : G.Adj v v✝²
v✝¹ : V
h✝¹ : G.Adj v✝² v✝¹
v✝ : V
h✝ : G.Adj v✝¹ v✝
p✝ : G.Walk v✝ v
hp✝ : (cons h✝² (cons h✝¹ (cons h✝ p✝))).IsCycle
hp : (cons h✝² (cons h✝¹ (cons h✝ p✝))).IsTrail
hp' : cons h✝² (cons h✝¹ (cons h✝ p✝)) ≠ nil
support_nodup✝ : (cons h✝² (cons h✝¹ (cons h✝ p✝))).support.tail.Nodup
⊢ 3 ≤ p✝.length + 1 + 1 + 1

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
hp : p.IsCycle
⊢ 3 ≤ p.length

Tactic:
have ⟨⟨hp, hp'⟩, _⟩ := hp

Result:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
hp✝ : p.IsCycle
hp : p.IsTrail
hp' : p ≠ nil
support_nodup✝ : p.support.tail.Nodup
⊢ 3 ≤ p.length

Proof state:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
h : G.Adj v v
hp✝ : (cons h nil).IsCycle
hp : (cons h nil).IsTrail
hp' : cons h nil ≠ nil
support_nodup✝ : (cons h nil).support.tail.Nodup
⊢ 3 ≤ (cons h nil).length

Tactic:
simp at h

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
hp✝ : nil.IsCycle
hp : nil.IsTrail
hp' : nil ≠ nil
support_nodup✝ : nil.support.tail.Nodup
⊢ 3 ≤ nil.length

Tactic:
simp at hp'

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
hp✝ : p.IsCycle
hp : p.IsTrail
hp' : p ≠ nil
support_nodup✝ : p.support.tail.Nodup
⊢ 3 ≤ p.length

Tactic:
match p with
| .nil => simp at hp'
| .cons h .nil => simp at h
| .cons _ (.cons _ .nil) => simp at hp
| .cons _ (.cons _ (.cons _ _)) => simp_rw [SimpleGraph.Walk.length_cons]; omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
v✝² : V
h✝² : G.Adj v v✝²
v✝¹ : V
h✝¹ : G.Adj v✝² v✝¹
v✝ : V
h✝ : G.Adj v✝¹ v✝
p✝ : G.Walk v✝ v
hp✝ : (cons h✝² (cons h✝¹ (cons h✝ p✝))).IsCycle
hp : (cons h✝² (cons h✝¹ (cons h✝ p✝))).IsTrail
hp' : cons h✝² (cons h✝¹ (cons h✝ p✝)) ≠ nil
support_nodup✝ : (cons h✝² (cons h✝¹ (cons h✝ p✝))).support.tail.Nodup
⊢ 3 ≤ (cons h✝² (cons h✝¹ (cons h✝ p✝))).length

Tactic:
simp_rw [SimpleGraph.Walk.length_cons]

Result:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
v✝² : V
h✝² : G.Adj v v✝²
v✝¹ : V
h✝¹ : G.Adj v✝² v✝¹
v✝ : V
h✝ : G.Adj v✝¹ v✝
p✝ : G.Walk v✝ v
hp✝ : (cons h✝² (cons h✝¹ (cons h✝ p✝))).IsCycle
hp : (cons h✝² (cons h✝¹ (cons h✝ p✝))).IsTrail
hp' : cons h✝² (cons h✝¹ (cons h✝ p✝)) ≠ nil
support_nodup✝ : (cons h✝² (cons h✝¹ (cons h✝ p✝))).support.tail.Nodup
⊢ 3 ≤ p✝.length + 1 + 1 + 1
-- Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean
lemma CompactlySupportedContinuousMap.monotone_of_nnreal : Monotone Λ

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
⊢ Monotone ⇑Λ

Tactic:
intro f₁ f₂ h

Result:
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f₁ f₂ : X →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ Λ f₁ ≤ Λ f₂

Proof state:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f₁ f₂ : X →C_c ℝ≥0
h : f₁ ≤ f₂
g : X →C_c ℝ≥0
hg : f₁ + g = f₂
⊢ Λ f₁ ≤ Λ f₂

Tactic:
rw [← hg]

Result:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f₁ f₂ : X →C_c ℝ≥0
h : f₁ ≤ f₂
g : X →C_c ℝ≥0
hg : f₁ + g = f₂
⊢ Λ f₁ ≤ Λ (f₁ + g)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f₁ f₂ : X →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ Λ f₁ ≤ Λ f₂

Tactic:
obtain ⟨g, hg⟩ := CompactlySupportedContinuousMap.exists_add_of_le h

Result:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f₁ f₂ : X →C_c ℝ≥0
h : f₁ ≤ f₂
g : X →C_c ℝ≥0
hg : f₁ + g = f₂
⊢ Λ f₁ ≤ Λ f₂

Proof state:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f₁ f₂ : X →C_c ℝ≥0
h : f₁ ≤ f₂
g : X →C_c ℝ≥0
hg : f₁ + g = f₂
⊢ Λ f₁ ≤ Λ (f₁ + g)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
/-- When `n` is either a natural number or `ω`, one can characterize the property of being `C^n`
as the existence of a neighborhood on which there is a Taylor series up to order `n`,
requiring in addition that its terms are analytic in the `ω` case. -/
lemma contDiffWithinAt_iff_of_ne_infty (hn : n ≠ ∞) :
    ContDiffWithinAt 𝕜 n f s x ↔ ∃ u ∈ 𝓝[insert x s] x,
      ∃ p : E → FormalMultilinearSeries 𝕜 E F, HasFTaylorSeriesUpToOn n f p u ∧
        (n = ω → ∀ i, AnalyticOn 𝕜 (fun x ↦ p x i) u)

Proof state:
𝕜 : 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
x : E
n✝ : WithTop ℕ∞
n : ℕ
hn : ↑n ≠ ∞
⊢ ContDiffWithinAt 𝕜 (↑n) f s x ↔
    ∃ u ∈ 𝓝[insert x s] x,
      ∃ p, HasFTaylorSeriesUpToOn (↑n) f p u ∧ (↑n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u)

Tactic:
simp [contDiffWithinAt_nat]

Result:
no goals

Proof state:
𝕜 : 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
x : E
n : WithTop ℕ∞
hn : n ≠ ∞
⊢ ContDiffWithinAt 𝕜 n f s x ↔
    ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn n f p u ∧ (n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u)

Tactic:
match n with
| ω => simp [ContDiffWithinAt]
| ∞ => simp at hn
| (n : ℕ) => simp [contDiffWithinAt_nat]

Result:
no goals

Proof state:
𝕜 : 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
x : E
n : WithTop ℕ∞
hn : ω ≠ ∞
⊢ ContDiffWithinAt 𝕜 ω f s x ↔
    ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn ω f p u ∧ (ω = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u)

Tactic:
simp [ContDiffWithinAt]

Result:
no goals

Proof state:
𝕜 : 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
x : E
n : WithTop ℕ∞
hn : ∞ ≠ ∞
⊢ ContDiffWithinAt 𝕜 ∞ f s x ↔
    ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn ∞ f p u ∧ (∞ = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u)

Tactic:
simp at hn

Result:
no goals
-- Mathlib/Data/Nat/Pairing.lean
theorem unpair_pair (a b : ℕ) : unpair (pair a b) = (a, b)

Proof state:
case pos
a b : ℕ
h : a < b
be : (b * b + a).sqrt = b
⊢ unpair (b * b + a) = (a, b)

Tactic:
simp [unpair, be, Nat.add_sub_cancel_left, h]

Result:
no goals

Proof state:
a b : ℕ
⊢ unpair (pair a b) = (a, b)

Tactic:
dsimp only [pair]

Result:
a b : ℕ
⊢ unpair (if a < b then b * b + a else a * a + a + b) = (a, b)

Proof state:
case neg
a b : ℕ
h : ¬a < b
ae : (a * a + (a + b)).sqrt = a
⊢ unpair (a * a + a + b) = (a, b)

Tactic:
simp [unpair, ae, Nat.not_lt_zero, Nat.add_assoc, Nat.add_sub_cancel_left]

Result:
no goals

Proof state:
case neg
a b : ℕ
h : ¬a < b
⊢ unpair (a * a + a + b) = (a, b)

Tactic:
have ae : sqrt (a * a + (a + b)) = a := by
  rw [sqrt_add_eq]
  exact Nat.add_le_add_left (le_of_not_gt h) _

Result:
case neg
a b : ℕ
h : ¬a < b
ae : (a * a + (a + b)).sqrt = a
⊢ unpair (a * a + a + b) = (a, b)

Proof state:
a b : ℕ
⊢ unpair (if a < b then b * b + a else a * a + a + b) = (a, b)

Tactic:
split_ifs with h

Result:
case pos
a b : ℕ
h : a < b
⊢ unpair (b * b + a) = (a, b)

case neg
a b : ℕ
h : ¬a < b
⊢ unpair (a * a + a + b) = (a, b)

Proof state:
case pos
a b : ℕ
h : a < b
⊢ unpair (b * b + a) = (a, b)

Tactic:
have be : sqrt (b * b + a) = b := sqrt_add_eq _ (le_trans (le_of_lt h) (Nat.le_add_left _ _))

Result:
case pos
a b : ℕ
h : a < b
be : (b * b + a).sqrt = b
⊢ unpair (b * b + a) = (a, b)

Proof state:
case h
a b : ℕ
h : ¬a < b
⊢ a + b ≤ a + a

Tactic:
exact Nat.add_le_add_left (le_of_not_gt h) _

Result:
no goals

Proof state:
a b : ℕ
h : ¬a < b
⊢ (a * a + (a + b)).sqrt = a

Tactic:
rw [sqrt_add_eq]

Result:
case h
a b : ℕ
h : ¬a < b
⊢ a + b ≤ a + a
-- Mathlib/Data/Fin/Tuple/Take.lean
theorem take_repeat {α : Type*} {n' : ℕ} (m : ℕ) (h : m ≤ n) (a : Fin n' → α) :
    take (m * n') (Nat.mul_le_mul_right n' h) (Fin.repeat n a) = Fin.repeat m a

Proof state:
case h
n : ℕ
α : Type u_2
n' m : ℕ
h : m ≤ n
a : Fin n' → α
i : Fin (m * n')
⊢ take (m * n') ⋯ («repeat» n a) i = «repeat» m a i

Tactic:
simp only [take, repeat_apply, modNat, coe_castLE]

Result:
no goals

Proof state:
n : ℕ
α : Type u_2
n' m : ℕ
h : m ≤ n
a : Fin n' → α
⊢ take (m * n') ⋯ («repeat» n a) = «repeat» m a

Tactic:
ext i

Result:
case h
n : ℕ
α : Type u_2
n' m : ℕ
h : m ≤ n
a : Fin n' → α
i : Fin (m * n')
⊢ take (m * n') ⋯ («repeat» n a) i = «repeat» m a i
-- Mathlib/Data/Part.lean
theorem inter_get_eq [Inter α] (a b : Part α) (hab : Dom (a ∩ b)) :
    (a ∩ b).get hab = a.get (left_dom_of_inter_dom hab) ∩ b.get (right_dom_of_inter_dom hab)

Proof state:
α : Type u_1
inst✝ : Inter α
a b : Part α
hab : (a ∩ b).Dom
⊢ (a.bind fun y => map (fun x => y ∩ x) b).get ⋯ = a.get ⋯ ∩ b.get ⋯

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Inter α
a b : Part α
hab : (a ∩ b).Dom
⊢ (a ∩ b).get hab = a.get ⋯ ∩ b.get ⋯

Tactic:
simp [inter_def]

Result:
α : Type u_1
inst✝ : Inter α
a b : Part α
hab : (a ∩ b).Dom
⊢ (a.bind fun y => map (fun x => y ∩ x) b).get ⋯ = a.get ⋯ ∩ b.get ⋯
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem sInf_toNonUnitalSubsemiring (S : Set (NonUnitalSubalgebra R A)) :
    (sInf S).toNonUnitalSubsemiring = sInf (NonUnitalSubalgebra.toNonUnitalSubsemiring '' S) :=
  SetLike.coe_injective <| by simp

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : Set (NonUnitalSubalgebra R A)
⊢ ↑(sInf S).toNonUnitalSubsemiring = ↑(sInf (NonUnitalSubalgebra.toNonUnitalSubsemiring '' S))

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Germ/Basic.lean
/-- If a germ `f : Germ l β` is constant, where `l : Filter α`,
and a function `g : γ → α` tends to `l` along `lc : Filter γ`,
the germ of the composition `f ∘ g` is also constant. -/
lemma isConstant_compTendsto {f : Germ l β} {lc : Filter γ} {g : γ → α}
    (hf : f.IsConstant) (hg : Tendsto g lc l) : (f.compTendsto g hg).IsConstant

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : l.Germ β
lc : Filter γ
g : γ → α
hf : f.IsConstant
hg : Tendsto g lc l
⊢ (f.compTendsto g hg).IsConstant

Tactic:
induction f using Quotient.inductionOn with | _ f => ?_

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
lc : Filter γ
g : γ → α
hg : Tendsto g lc l
f : α → β
hf : IsConstant ⟦f⟧
⊢ (compTendsto ⟦f⟧ g hg).IsConstant

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
lc : Filter γ
g : γ → α
hg : Tendsto g lc l
f : α → β
hf : IsConstant ⟦f⟧
⊢ (compTendsto ⟦f⟧ g hg).IsConstant

Tactic:
exact isConstant_comp_tendsto hf hg

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem trans [Monoid M] : ∀ {x y z : M}, x ~ᵤ y → y ~ᵤ z → x ~ᵤ z
  | x, _, _, ⟨u, rfl⟩, ⟨v, rfl⟩ => ⟨u * v, by rw [Units.val_mul, mul_assoc]⟩

Proof state:
M : Type u_1
inst✝ : Monoid M
x : M
u v : Mˣ
⊢ x * ↑(u * v) = x * ↑u * ↑v

Tactic:
rw [Units.val_mul, mul_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List (α × β)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Prod.fst)
    {h'} :
    (insertMany m l).getKey k' h' = k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Prod.fst l
h' : k' ∈ insertMany m l
⊢ (insertMany m l).getKey k' h' = k

Tactic:
simp_to_raw using Raw₀.Const.getKey_insertMany_list_of_mem

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/LevelOne.lean
lemma levelOne_neg_weight_eq_zero (hk : k < 0) (f : F) : ⇑f = 0

Proof state:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k < 0
f : F
⊢ ⇑f = 0

Tactic:
have hf := levelOne_nonpos_wt_const hk.le f

Result:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k < 0
f : F
hf : ⇑f = Function.const ℍ (SlashInvariantFormClass.cuspFunction 1 f 0)
⊢ ⇑f = 0

Proof state:
case inr
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k < 0
f : F
hf : ⇑f = Function.const ℍ (SlashInvariantFormClass.cuspFunction 1 f 0)
hf₀ : SlashInvariantFormClass.cuspFunction 1 f 0 = 0
⊢ ⇑f = 0

Tactic:
rw [hf, hf₀, const_zero]

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k < 0
f : F
hf : ⇑f = Function.const ℍ (SlashInvariantFormClass.cuspFunction 1 f 0)
⊢ ⇑f = 0

Tactic:
rcases wt_eq_zero_of_eq_const k hf with rfl | hf₀

Result:
case inl
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
hf : ⇑f = Function.const ℍ (SlashInvariantFormClass.cuspFunction 1 f 0)
inst✝ : ModularFormClass F Γ(1) 0
hk : 0 < 0
⊢ ⇑f = 0

case inr
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k < 0
f : F
hf : ⇑f = Function.const ℍ (SlashInvariantFormClass.cuspFunction 1 f 0)
hf₀ : SlashInvariantFormClass.cuspFunction 1 f 0 = 0
⊢ ⇑f = 0

Proof state:
case inl
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
hf : ⇑f = Function.const ℍ (SlashInvariantFormClass.cuspFunction 1 f 0)
inst✝ : ModularFormClass F Γ(1) 0
hk : 0 < 0
⊢ ⇑f = 0

Tactic:
exact (lt_irrefl _ hk).elim

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem not_isSome : isSome a = false ↔ a.isNone = true

Proof state:
α✝ : Type u_1
a : Option α✝
⊢ a.isSome = false ↔ a.isNone = true

Tactic:
cases a <;> simp

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Convergence.lean
lemma LSeriesSummable_lt_re_of_abscissaOfAbsConv_lt_re {f : ℕ → ℂ} {s : ℂ}
    (hs : abscissaOfAbsConv f < s.re) :
    ∃ x : ℝ, x < s.re ∧ LSeriesSummable f x

Proof state:
f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < ↑s.re
⊢ ∃ x < s.re, LSeriesSummable f ↑x

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := EReal.exists_between_coe_real hs

Result:
case intro.intro
f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < ↑s.re
x : ℝ
hx₁ : abscissaOfAbsConv f < ↑x
hx₂ : ↑x < ↑s.re
⊢ ∃ x < s.re, LSeriesSummable f ↑x

Proof state:
case intro.intro
f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < ↑s.re
x : ℝ
hx₁ : abscissaOfAbsConv f < ↑x
hx₂ : ↑x < ↑s.re
⊢ ∃ x < s.re, LSeriesSummable f ↑x

Tactic:
exact ⟨x, by simpa using hx₂, LSeriesSummable_of_abscissaOfAbsConv_lt_re hx₁⟩

Result:
no goals

Proof state:
f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < ↑s.re
x : ℝ
hx₁ : abscissaOfAbsConv f < ↑x
hx₂ : ↑x < ↑s.re
⊢ x < s.re

Tactic:
simpa using hx₂

Result:
no goals
-- Mathlib/Data/Multiset/UnionInter.lean
lemma add_union_distrib (s t u : Multiset α) : s + (t ∪ u) = s + t ∪ (s + u)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s + (t ∪ u) = s + t ∪ (s + u)

Tactic:
rw [Multiset.add_comm, union_add_distrib, s.add_comm, s.add_comm]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_map_div (f g : R → R) (a : A) (hg' : ∀ x ∈ spectrum R a, g x ≠ 0)
    (hf : ContinuousOn f (spectrum R a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : HasContinuousInv₀ R
f g : R → R
a : A
hg' : ∀ x ∈ spectrum R a, g x ≠ 0
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => f x * (g x)⁻¹) a = cfc f a * Ring.inverse (cfc g a)

Tactic:
rw [cfc_mul .., cfc_inv g a hg']

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : HasContinuousInv₀ R
f g : R → R
a : A
hg' : ∀ x ∈ spectrum R a, g x ≠ 0
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => f x / g x) a = cfc f a * Ring.inverse (cfc g a)

Tactic:
simp only [div_eq_mul_inv]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : HasContinuousInv₀ R
f g : R → R
a : A
hg' : ∀ x ∈ spectrum R a, g x ≠ 0
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => f x * (g x)⁻¹) a = cfc f a * Ring.inverse (cfc g a)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Erase.lean
theorem eraseIdx_eq_take_drop_succ (l : Vector α n) (i : Nat) (h) :
    l.eraseIdx i = (l.take i ++ l.drop (i + 1)).cast (by omega)

Proof state:
α : Type ?u.12
n : Nat
l : Vector α n
i : Nat
h : i < n
⊢ min i n + (n - (i + 1)) = n - 1

Tactic:
omega

Result:
no goals

Proof state:
case mk
α : Type u_1
i : Nat
l : Array α
h : i < l.size
⊢ { toArray := l, size_toArray := ⋯ }.eraseIdx i h =
    Vector.cast ⋯ ({ toArray := l, size_toArray := ⋯ }.take i ++ { toArray := l, size_toArray := ⋯ }.drop (i + 1))

Tactic:
simp [Array.eraseIdx_eq_take_drop_succ, *]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
⊢ l.eraseIdx i h = Vector.cast ⋯ (l.take i ++ l.drop (i + 1))

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
i : Nat
l : Array α
h : i < l.size
⊢ { toArray := l, size_toArray := ⋯ }.eraseIdx i h =
    Vector.cast ⋯ ({ toArray := l, size_toArray := ⋯ }.take i ++ { toArray := l, size_toArray := ⋯ }.drop (i + 1))
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem op_smul_finset_smul_eq_smul_smul_finset (a : α) (s : Finset β) (t : Finset γ)
    (h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c) : (op a • s) • t = s • a • t

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq β
inst✝³ : DecidableEq γ
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Finset β
t : Finset γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
⊢ (op a • s) • t = s • a • t

Tactic:
ext

Result:
case h
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq β
inst✝³ : DecidableEq γ
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Finset β
t : Finset γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
a✝ : γ
⊢ a✝ ∈ (op a • s) • t ↔ a✝ ∈ s • a • t

Proof state:
case h
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq β
inst✝³ : DecidableEq γ
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Finset β
t : Finset γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
a✝ : γ
⊢ a✝ ∈ (op a • s) • t ↔ a✝ ∈ s • a • t

Tactic:
simp [mem_smul, mem_smul_finset, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lex.lean
theorem le_iff_exists [DecidableEq α] [LT α] [DecidableLT α]
    [Std.Irrefl (· < · : α → α → Prop)]
    [Std.Asymm (· < · : α → α → Prop)]
    [Std.Antisymm (¬ · < · : α → α → Prop)] {l₁ l₂ : Vector α n} :
    l₁ ≤ l₂ ↔
      (l₁ = l₂) ∨
        (∃ (i : Nat) (h : i < n), (∀ j, (hj : j < i) → l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i])

Proof state:
case mk.mk
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : Array α
n₂ : l₂.size = l₁.size
⊢ { toArray := l₁, size_toArray := ⋯ } ≤ { toArray := l₂, size_toArray := n₂ } ↔
    { toArray := l₁, size_toArray := ⋯ } = { toArray := l₂, size_toArray := n₂ } ∨
      ∃ i h,
        (∀ (j : Nat) (hj : j < i), { toArray := l₁, size_toArray := ⋯ }[j] = { toArray := l₂, size_toArray := n₂ }[j]) ∧
          { toArray := l₁, size_toArray := ⋯ }[i] < { toArray := l₂, size_toArray := n₂ }[i]

Tactic:
simp [Array.le_iff_exists, ← n₂]

Result:
no goals

Proof state:
case mk
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ : Array α
l₂ : Vector α l₁.size
⊢ { toArray := l₁, size_toArray := ⋯ } ≤ l₂ ↔
    { toArray := l₁, size_toArray := ⋯ } = l₂ ∨
      ∃ i h,
        (∀ (j : Nat) (hj : j < i), { toArray := l₁, size_toArray := ⋯ }[j] = l₂[j]) ∧
          { toArray := l₁, size_toArray := ⋯ }[i] < l₂[i]

Tactic:
rcases l₂ with ⟨l₂, n₂⟩

Result:
case mk.mk
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : Array α
n₂ : l₂.size = l₁.size
⊢ { toArray := l₁, size_toArray := ⋯ } ≤ { toArray := l₂, size_toArray := n₂ } ↔
    { toArray := l₁, size_toArray := ⋯ } = { toArray := l₂, size_toArray := n₂ } ∨
      ∃ i h,
        (∀ (j : Nat) (hj : j < i), { toArray := l₁, size_toArray := ⋯ }[j] = { toArray := l₂, size_toArray := n₂ }[j]) ∧
          { toArray := l₁, size_toArray := ⋯ }[i] < { toArray := l₂, size_toArray := n₂ }[i]

Proof state:
α : Type u_1
n : Nat
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ : Vector α n
⊢ l₁ ≤ l₂ ↔ l₁ = l₂ ∨ ∃ i h, (∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]

Tactic:
rcases l₁ with ⟨l₁, rfl⟩

Result:
case mk
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ : Array α
l₂ : Vector α l₁.size
⊢ { toArray := l₁, size_toArray := ⋯ } ≤ l₂ ↔
    { toArray := l₁, size_toArray := ⋯ } = l₂ ∨
      ∃ i h,
        (∀ (j : Nat) (hj : j < i), { toArray := l₁, size_toArray := ⋯ }[j] = l₂[j]) ∧
          { toArray := l₁, size_toArray := ⋯ }[i] < l₂[i]