harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/MellinTransform.lean
theorem mellinConvergent_of_isBigO_rpow [NormedSpace ℂ E] {a b : ℝ} {f : ℝ → E} {s : ℂ}
    (hfc : LocallyIntegrableOn f <| Ioi 0) (hf_top : f =O[atTop] (· ^ (-a)))
    (hs_top : s.re < a) (hf_bot : f =O[𝓝[>] 0] (· ^ (-b))) (hs_bot : b < s.re) :
    MellinConvergent f s

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x => x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x => x ^ (-b)
hs_bot : b < s.re
⊢ MellinConvergent f s

Tactic:
rw [MellinConvergent,
  mellin_convergent_iff_norm Subset.rfl measurableSet_Ioi hfc.aestronglyMeasurable]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x => x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x => x ^ (-b)
hs_bot : b < s.re
⊢ IntegrableOn (fun t => t ^ (s.re - 1) * ‖f t‖) (Ioi 0) volume

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x => x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x => x ^ (-b)
hs_bot : b < s.re
⊢ IntegrableOn (fun t => t ^ (s.re - 1) * ‖f t‖) (Ioi 0) volume

Tactic:
exact mellin_convergent_of_isBigO_scalar hfc.norm hf_top.norm_left hs_top hf_bot.norm_left hs_bot

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
theorem HasFPowerSeriesWithinAt.add
    (hf : HasFPowerSeriesWithinAt f pf s x) (hg : HasFPowerSeriesWithinAt g pg s x) :
    HasFPowerSeriesWithinAt (f + g) (pf + pg) s x

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f pf s x
hg : HasFPowerSeriesWithinAt g pg s x
⊢ HasFPowerSeriesWithinAt (f + g) (pf + pg) s x

Tactic:
rcases (hf.eventually.and hg.eventually).exists with ⟨r, hr⟩

Result:
case intro
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f pf s x
hg : HasFPowerSeriesWithinAt g pg s x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f pf s x r ∧ HasFPowerSeriesWithinOnBall g pg s x r
⊢ HasFPowerSeriesWithinAt (f + g) (pf + pg) s x

Proof state:
case intro
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f pf s x
hg : HasFPowerSeriesWithinAt g pg s x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f pf s x r ∧ HasFPowerSeriesWithinOnBall g pg s x r
⊢ HasFPowerSeriesWithinAt (f + g) (pf + pg) s x

Tactic:
exact ⟨r, hr.1.add hr.2⟩

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem card_iSup_le_sum_card {ι : Type u} (f : ι → Ordinal.{max u v}) :
    (⨆ i, f i).card ≤ Cardinal.sum (fun i ↦ (f i).card)

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
this : Cardinal.lift.{u, max u v} (⨆ i, f i).card ≤ sum fun i => (f i).card
⊢ (⨆ i, f i).card ≤ sum fun i => (f i).card

Tactic:
rwa [Cardinal.lift_id'] at this

Result:
no goals

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (⨆ i, f i).card ≤ sum fun i => (f i).card

Tactic:
have := lift_card_iSup_le_sum_card f

Result:
ι : Type u
f : ι → Ordinal.{max u v}
this : Cardinal.lift.{u, max u v} (⨆ i, f i).card ≤ sum fun i => (f i).card
⊢ (⨆ i, f i).card ≤ sum fun i => (f i).card
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
theorem Walk.isPath_of_length_eq_dist (p : G.Walk u v) (hp : p.length = G.dist u v) :
    p.IsPath

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
⊢ p.IsPath

Tactic:
have : p.bypass = p := by
  apply Walk.bypass_eq_self_of_length_le
  calc p.length
    _ = G.dist u v := hp
    _ ≤ p.bypass.length := dist_le p.bypass

Result:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
this : p.bypass = p
⊢ p.IsPath

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
this : p.bypass = p
⊢ p.bypass.IsPath

Tactic:
apply Walk.bypass_isPath

Result:
no goals

Proof state:
case h
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
⊢ p.length ≤ p.bypass.length

Tactic:
calc p.length
  _ = G.dist u v := hp
  _ ≤ p.bypass.length := dist_le p.bypass

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
⊢ p.bypass = p

Tactic:
apply Walk.bypass_eq_self_of_length_le

Result:
case h
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
⊢ p.length ≤ p.bypass.length

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
⊢ p.IsPath

Tactic:
classical
have : p.bypass = p := by
  apply Walk.bypass_eq_self_of_length_le
  calc p.length
    _ = G.dist u v := hp
    _ ≤ p.bypass.length := dist_le p.bypass
rw [← this]
apply Walk.bypass_isPath

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
this : p.bypass = p
⊢ p.IsPath

Tactic:
rw [← this]

Result:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
this : p.bypass = p
⊢ p.bypass.IsPath
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_modify [LawfulBEq α] {k : α} {f : β k → β k} (h : m.WF) :
    (m.modify k f).size = m.size

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).size = m.size

Tactic:
simp_to_raw using Raw₀.size_modify

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseP_eq_iff {p} {l : Array α} :
    l.eraseP p = l' ↔
      ((∀ a ∈ l, ¬ p a) ∧ l = l') ∨
        ∃ a l₁ l₂, (∀ b ∈ l₁, ¬ p b) ∧ p a ∧ l = l₁.push a ++ l₂ ∧ l' = l₁ ++ l₂

Proof state:
case mk.mk.mp
α : Type u_1
p : α → Bool
l l' : List α
⊢ ((∀ (a : α), a ∈ l → p a = false) ∧ l = l' ∨
      ∃ a l₁, (∀ (b : α), b ∈ l₁ → p b = false) ∧ p a = true ∧ ∃ x, l = l₁ ++ a :: x ∧ l' = l₁ ++ x) →
    (∀ (a : α), a ∈ l → p a = false) ∧ l = l' ∨
      ∃ a l₁,
        (∀ (b : α), b ∈ l₁ → p b = false) ∧
          p a = true ∧ ∃ x, l = l₁.toList ++ a :: x.toList ∧ l' = l₁.toList ++ x.toList

Tactic:
rintro (h | ⟨a, l₁, h₁, h₂, ⟨x, rfl, rfl⟩⟩)

Result:
case mk.mk.mp.inl
α : Type u_1
p : α → Bool
l l' : List α
h : (∀ (a : α), a ∈ l → p a = false) ∧ l = l'
⊢ (∀ (a : α), a ∈ l → p a = false) ∧ l = l' ∨
    ∃ a l₁,
      (∀ (b : α), b ∈ l₁ → p b = false) ∧ p a = true ∧ ∃ x, l = l₁.toList ++ a :: x.toList ∧ l' = l₁.toList ++ x.toList

case mk.mk.mp.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
p : α → Bool
a : α
l₁ : List α
h₁ : ∀ (b : α), b ∈ l₁ → p b = false
h₂ : p a = true
x : List α
⊢ (∀ (a_1 : α), a_1 ∈ l₁ ++ a :: x → p a_1 = false) ∧ l₁ ++ a :: x = l₁ ++ x ∨
    ∃ a_1 l₁_1,
      (∀ (b : α), b ∈ l₁_1 → p b = false) ∧
        p a_1 = true ∧ ∃ x_1, l₁ ++ a :: x = l₁_1.toList ++ a_1 :: x_1.toList ∧ l₁ ++ x = l₁_1.toList ++ x_1.toList

Proof state:
case mk.mk
α : Type u_1
p : α → Bool
l l' : List α
⊢ { toList := l }.eraseP p = { toList := l' } ↔
    (∀ (a : α), a ∈ { toList := l } → ¬p a = true) ∧ { toList := l } = { toList := l' } ∨
      ∃ a l₁ l₂,
        (∀ (b : α), b ∈ l₁ → ¬p b = true) ∧ p a = true ∧ { toList := l } = l₁.push a ++ l₂ ∧ { toList := l' } = l₁ ++ l₂

Tactic:
simp [List.eraseP_eq_iff]

Result:
case mk.mk
α : Type u_1
p : α → Bool
l l' : List α
⊢ ((∀ (a : α), a ∈ l → p a = false) ∧ l = l' ∨
      ∃ a l₁, (∀ (b : α), b ∈ l₁ → p b = false) ∧ p a = true ∧ ∃ x, l = l₁ ++ a :: x ∧ l' = l₁ ++ x) ↔
    (∀ (a : α), a ∈ l → p a = false) ∧ l = l' ∨
      ∃ a l₁,
        (∀ (b : α), b ∈ l₁ → p b = false) ∧
          p a = true ∧ ∃ x, l = l₁.toList ++ a :: x.toList ∧ l' = l₁.toList ++ x.toList
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
theorem mul_nonneg_iff_of_pos_right [MulPosStrictMono α]
    (h : 0 < c) : 0 ≤ b * c ↔ 0 ≤ b

Proof state:
α : Type u
inst✝² : Semiring α
inst✝¹ : LinearOrder α
b c : α
inst✝ : MulPosStrictMono α
h : 0 < c
⊢ 0 ≤ b * c ↔ 0 ≤ b

Tactic:
simpa using (mul_le_mul_right h : 0 * c ≤ b * c ↔ 0 ≤ b)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Time/Date/Unit/Month.lean
theorem valid_clipDay : Valid leap month (clipDay leap month day)

Proof state:
case isTrue
leap : Bool
month : Ordinal
day : Day.Ordinal
h✝ : (days leap month).val < day.val
⊢ (days leap month).val ≤ (days leap month).val

case isFalse
leap : Bool
month : Ordinal
day : Day.Ordinal
h✝ : ¬(days leap month).val < day.val
⊢ day.val ≤ (days leap month).val

Tactic:
exact Int.le_refl (days leap month).val

Result:
case isFalse
leap : Bool
month : Ordinal
day : Day.Ordinal
h✝ : ¬(days leap month).val < day.val
⊢ day.val ≤ (days leap month).val

Proof state:
leap : Bool
month : Ordinal
day : Day.Ordinal
⊢ Valid leap month (clipDay leap month day)

Tactic:
simp [Valid, clipDay]

Result:
leap : Bool
month : Ordinal
day : Day.Ordinal
⊢ (if (days leap month).val < day.val then days leap month else day).val ≤ (days leap month).val

Proof state:
case isFalse
leap : Bool
month : Ordinal
day : Day.Ordinal
h✝ : ¬(days leap month).val < day.val
⊢ day.val ≤ (days leap month).val

Tactic:
next h => exact Int.not_lt.mp h

Result:
no goals

Proof state:
leap : Bool
month : Ordinal
day : Day.Ordinal
h : ¬(days leap month).val < day.val
⊢ day.val ≤ (days leap month).val

Tactic:
exact Int.not_lt.mp h

Result:
no goals

Proof state:
leap : Bool
month : Ordinal
day : Day.Ordinal
⊢ (if (days leap month).val < day.val then days leap month else day).val ≤ (days leap month).val

Tactic:
split

Result:
case isTrue
leap : Bool
month : Ordinal
day : Day.Ordinal
h✝ : (days leap month).val < day.val
⊢ (days leap month).val ≤ (days leap month).val

case isFalse
leap : Bool
month : Ordinal
day : Day.Ordinal
h✝ : ¬(days leap month).val < day.val
⊢ day.val ≤ (days leap month).val
-- Mathlib/Data/Setoid/Partition.lean
theorem IsPartition.sUnion_eq_univ {c : Set (Set α)} (hc : IsPartition c) : ⋃₀ c = Set.univ :=
  Set.eq_univ_of_forall fun x =>
    Set.mem_sUnion.2 <|
      let ⟨t, ht⟩ := hc.2 x
      ⟨t, by
        simp only [existsUnique_iff_exists] at ht
        tauto⟩

Proof state:
α : Type u_1
c : Set (Set α)
hc : IsPartition c
x : α
t : Set α
ht : (t ∈ c ∧ x ∈ t) ∧ ∀ (y : Set α), y ∈ c ∧ x ∈ y → y = t
⊢ t ∈ c ∧ x ∈ t

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
c : Set (Set α)
hc : IsPartition c
x : α
t : Set α
ht : (fun b => b ∈ c ∧ x ∈ b) t ∧ ∀ (y : Set α), (fun b => b ∈ c ∧ x ∈ b) y → y = t
⊢ t ∈ c ∧ x ∈ t

Tactic:
simp only [existsUnique_iff_exists] at ht

Result:
α : Type u_1
c : Set (Set α)
hc : IsPartition c
x : α
t : Set α
ht : (t ∈ c ∧ x ∈ t) ∧ ∀ (y : Set α), y ∈ c ∧ x ∈ y → y = t
⊢ t ∈ c ∧ x ∈ t
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem List.measurable_prod' (l : List (α → M)) (hl : ∀ f ∈ l, Measurable f) :
    Measurable l.prod

Proof state:
case cons
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, Measurable f) → Measurable l.prod
hl : ∀ f_1 ∈ f :: l, Measurable f_1
⊢ Measurable (f :: l).prod

Tactic:
rw [List.forall_mem_cons] at hl

Result:
case cons
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, Measurable f) → Measurable l.prod
hl : Measurable f ∧ ∀ x ∈ l, Measurable x
⊢ Measurable (f :: l).prod

Proof state:
case cons
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, Measurable f) → Measurable l.prod
hl : Measurable f ∧ ∀ x ∈ l, Measurable x
⊢ Measurable (f :: l).prod

Tactic:
rw [List.prod_cons]

Result:
case cons
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, Measurable f) → Measurable l.prod
hl : Measurable f ∧ ∀ x ∈ l, Measurable x
⊢ Measurable (f * l.prod)

Proof state:
case nil
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
hl : ∀ f ∈ [], Measurable f
⊢ Measurable [].prod

Tactic:
exact measurable_one

Result:
no goals

Proof state:
case cons
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, Measurable f) → Measurable l.prod
hl : Measurable f ∧ ∀ x ∈ l, Measurable x
⊢ Measurable (f * l.prod)

Tactic:
exact hl.1.mul (ihl hl.2)

Result:
no goals

Proof state:
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
l : List (α → M)
hl : ∀ f ∈ l, Measurable f
⊢ Measurable l.prod

Tactic:
induction' l with f l ihl

Result:
case nil
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
hl : ∀ f ∈ [], Measurable f
⊢ Measurable [].prod

case cons
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, Measurable f) → Measurable l.prod
hl : ∀ f_1 ∈ f :: l, Measurable f_1
⊢ Measurable (f :: l).prod
-- Mathlib/Data/Real/Hyperreal.lean
theorem IsSt.isSt_st {x : ℝ*} {r : ℝ} (hxr : IsSt x r) : IsSt x (st x)

Proof state:
x : ℝ*
r : ℝ
hxr : x.IsSt r
⊢ x.IsSt x.st

Tactic:
rwa [hxr.st_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean
theorem nonneg (x : ℝ) : 0 ≤ expNegInvGlue x

Proof state:
x : ℝ
⊢ 0 ≤ expNegInvGlue x

Tactic:
cases le_or_gt x 0 with
| inl h => exact ge_of_eq (zero_of_nonpos h)
| inr h => exact le_of_lt (pos_of_pos h)

Result:
no goals

Proof state:
case inr
x : ℝ
h : x > 0
⊢ 0 ≤ expNegInvGlue x

Tactic:
exact le_of_lt (pos_of_pos h)

Result:
no goals

Proof state:
case inl
x : ℝ
h : x ≤ 0
⊢ 0 ≤ expNegInvGlue x

Tactic:
exact ge_of_eq (zero_of_nonpos h)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem ne_and_not_mem_of_not_mem_push {a y : α} {l : Vector α n} : a ∉ l.push y → a ≠ y ∧ a ∉ l

Proof state:
α : Type u_1
n : Nat
a y : α
l : Vector α n
⊢ ¬a ∈ l.push y → a ≠ y ∧ ¬a ∈ l

Tactic:
simp +contextual

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem Filter.EventuallyEq.deriv_eq (hL : f₁ =ᶠ[𝓝 x] f) : deriv f₁ x = deriv f x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
hL : f₁ =ᶠ[𝓝 x] f
⊢ deriv f₁ x = deriv f x

Tactic:
unfold deriv

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
hL : f₁ =ᶠ[𝓝 x] f
⊢ (fderiv 𝕜 f₁ x) 1 = (fderiv 𝕜 f x) 1

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
hL : f₁ =ᶠ[𝓝 x] f
⊢ (fderiv 𝕜 f₁ x) 1 = (fderiv 𝕜 f x) 1

Tactic:
rwa [Filter.EventuallyEq.fderiv_eq]

Result:
no goals
-- Mathlib/Data/Fin/Rev.lean
theorem cast_rev (i : Fin n) (h : n = m) :
    i.rev.cast h = (i.cast h).rev

Proof state:
n : ℕ
i : Fin n
⊢ Fin.cast ⋯ i.rev = (Fin.cast ⋯ i).rev

Tactic:
simp

Result:
no goals

Proof state:
n m : ℕ
i : Fin n
h : n = m
⊢ Fin.cast h i.rev = (Fin.cast h i).rev

Tactic:
subst h

Result:
n : ℕ
i : Fin n
⊢ Fin.cast ⋯ i.rev = (Fin.cast ⋯ i).rev
-- Mathlib/Data/Finmap.lean
theorem keys_erase (a : α) (s : Finmap β) : (erase a s).keys = s.keys.erase a :=
  induction_on s fun s => by simp

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s✝ : Finmap β
s : AList β
⊢ (erase a ⟦s⟧).keys = ⟦s⟧.keys.erase a

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/Valued/LocallyCompact.lean
/-- An element is in the valuation ring if the norm is bounded by 1. This is a variant of
`Valuation.mem_integer_iff`, phrased using norms instead of the valuation. -/
lemma mem_iff {x : K} : x ∈ 𝒪[K] ↔ ‖x‖ ≤ 1

Proof state:
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : K
⊢ x ∈ 𝒪[K] ↔ ‖x‖ ≤ 1

Tactic:
simp [Valuation.mem_integer_iff, ← NNReal.coe_le_coe]

Result:
no goals
-- Mathlib/Analysis/Complex/Isometry.lean
theorem LinearIsometry.im_apply_eq_im_or_neg_of_re_apply_eq_re {f : ℂ →ₗᵢ[ℝ] ℂ}
    (h₂ : ∀ z, (f z).re = z.re) (z : ℂ) : (f z).im = z.im ∨ (f z).im = -z.im

Proof state:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), (f z).re = z.re
z : ℂ
h₁ : ‖f z‖ = ‖z‖
⊢ (f z).im = z.im ∨ (f z).im = -z.im

Tactic:
simp only [norm_def] at h₁

Result:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), (f z).re = z.re
z : ℂ
h₁ : √(normSq (f z)) = √(normSq z)
⊢ (f z).im = z.im ∨ (f z).im = -z.im

Proof state:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), (f z).re = z.re
z : ℂ
⊢ (f z).im = z.im ∨ (f z).im = -z.im

Tactic:
have h₁ := f.norm_map z

Result:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), (f z).re = z.re
z : ℂ
h₁ : ‖f z‖ = ‖z‖
⊢ (f z).im = z.im ∨ (f z).im = -z.im

Proof state:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), (f z).re = z.re
z : ℂ
h₁ : √(normSq (f z)) = √(normSq z)
⊢ (f z).im = z.im ∨ (f z).im = -z.im

Tactic:
rwa [Real.sqrt_inj (normSq_nonneg _) (normSq_nonneg _), normSq_apply (f z), normSq_apply z,
  h₂, add_left_cancel_iff, mul_self_eq_mul_self_iff] at h₁

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
lemma mapRingHom_comp_C {R S : Type*} [Semiring R] [Semiring S] (f : R →+* S) :
    (mapRingHom f).comp C = C.comp f

Proof state:
case a.a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x✝ : R
n✝ : ℕ
⊢ (((mapRingHom f).comp C) x✝).coeff n✝ = ((C.comp f) x✝).coeff n✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
⊢ (mapRingHom f).comp C = C.comp f

Tactic:
ext

Result:
case a.a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x✝ : R
n✝ : ℕ
⊢ (((mapRingHom f).comp C) x✝).coeff n✝ = ((C.comp f) x✝).coeff n✝
-- Mathlib/Analysis/NormedSpace/IndicatorFunction.lean
theorem enorm_indicator_le_enorm_self : ‖indicator s f a‖ₑ ≤ ‖f a‖ₑ

Proof state:
α : Type u_1
E : Type u_2
inst✝ : SeminormedAddCommGroup E
s : Set α
f : α → E
a : α
⊢ s.indicator (fun a => ‖f a‖ₑ) a ≤ ‖f a‖ₑ

Tactic:
apply indicator_enorm_le_enorm_self

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝ : SeminormedAddCommGroup E
s : Set α
f : α → E
a : α
⊢ ‖s.indicator f a‖ₑ ≤ ‖f a‖ₑ

Tactic:
rw [enorm_indicator_eq_indicator_enorm]

Result:
α : Type u_1
E : Type u_2
inst✝ : SeminormedAddCommGroup E
s : Set α
f : α → E
a : α
⊢ s.indicator (fun a => ‖f a‖ₑ) a ≤ ‖f a‖ₑ
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_alterKey [EquivBEq α] {k k' : α} {f : Option β → Option β} (l : List ((_ : α) × β))
    (hl : DistinctKeys l) :
    getKey? k' (alterKey k f l) =
      if k == k' then
        if (f (getValue? k l)).isSome then some k else none
      else
        getKey? k' l

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ getKey? k' (alterKey k f l) =
    if (k == k') = true then if (f (getValue? k l)).isSome = true then some k else none else getKey? k' l

Tactic:
rw [alterKey]

Result:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ getKey? k'
      (match f (getValue? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l) =
    if (k == k') = true then if (f (getValue? k l)).isSome = true then some k else none else getKey? k' l

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
x✝ : Option β
v✝ : β
heq : f (getValue? k l) = some v✝
⊢ getKey? k' (insertEntry k v✝ l) =
    if (k == k') = true then if (f (getValue? k l)).isSome = true then some k else none else getKey? k' l

Tactic:
simp [hl, heq, getKey?_eraseKey, getKey?_insertEntry]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ getKey? k'
      (match f (getValue? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l) =
    if (k == k') = true then if (f (getValue? k l)).isSome = true then some k else none else getKey? k' l

Tactic:
split <;> next heq => simp [hl, heq, getKey?_eraseKey, getKey?_insertEntry]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Contracting.lean
theorem one_sub_K_pos' (hf : ContractingWith K f) : (0 : ℝ≥0∞) < 1 - K

Proof state:
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
⊢ 0 < 1 - ↑K

Tactic:
simp [hf.1]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Pointwise.lean
theorem image_smul_setₛₗ :
    h '' (c • s) = σ c • h '' s

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_6
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
σ : R → S
inst✝³ : MulAction R M
inst✝² : MulAction S N
F : Type u_7
h : F
inst✝¹ : FunLike F M N
inst✝ : MulActionSemiHomClass F σ M N
c : R
s : Set M
⊢ ⇑h '' (c • s) = σ c • ⇑h '' s

Tactic:
simp only [← image_smul, image_image, map_smulₛₗ h]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem ext_fourfold {g h : ((M ⊗[R] N) ⊗[R] P) ⊗[R] Q →ₗ[R] S}
    (H : ∀ w x y z, g (w ⊗ₜ x ⊗ₜ y ⊗ₜ z) = h (w ⊗ₜ x ⊗ₜ y ⊗ₜ z)) : g = h

Proof state:
case H.H.H.h.h.h.h
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : AddCommMonoid S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R Q
inst✝¹ : Module R S
inst✝ : Module R P
g h : ((M ⊗[R] N) ⊗[R] P) ⊗[R] Q →ₗ[R] S
H : ∀ (w : M) (x : N) (y : P) (z : Q), g (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) = h (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)
w : M
x : N
y : P
z : Q
⊢ (((((mk R M N).compr₂ ((mk R (M ⊗[R] N) P).compr₂ ((mk R ((M ⊗[R] N) ⊗[R] P) Q).compr₂ g))) w) x) y) z =
    (((((mk R M N).compr₂ ((mk R (M ⊗[R] N) P).compr₂ ((mk R ((M ⊗[R] N) ⊗[R] P) Q).compr₂ h))) w) x) y) z

Tactic:
exact H w x y z

Result:
no goals

Proof state:
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : AddCommMonoid S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R Q
inst✝¹ : Module R S
inst✝ : Module R P
g h : ((M ⊗[R] N) ⊗[R] P) ⊗[R] Q →ₗ[R] S
H : ∀ (w : M) (x : N) (y : P) (z : Q), g (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) = h (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)
⊢ g = h

Tactic:
ext w x y z

Result:
case H.H.H.h.h.h.h
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : AddCommMonoid S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R Q
inst✝¹ : Module R S
inst✝ : Module R P
g h : ((M ⊗[R] N) ⊗[R] P) ⊗[R] Q →ₗ[R] S
H : ∀ (w : M) (x : N) (y : P) (z : Q), g (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) = h (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)
w : M
x : N
y : P
z : Q
⊢ (((((mk R M N).compr₂ ((mk R (M ⊗[R] N) P).compr₂ ((mk R ((M ⊗[R] N) ⊗[R] P) Q).compr₂ g))) w) x) y) z =
    (((((mk R M N).compr₂ ((mk R (M ⊗[R] N) P).compr₂ ((mk R ((M ⊗[R] N) ⊗[R] P) Q).compr₂ h))) w) x) y) z