harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem all_filterMap {l : List α} {f : α → Option β} {p : β → Bool} :
    (filterMap f l).all p = l.all fun a => match f a with | some b => p b | none => true

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
h : α
t : List α
ih :
  (filterMap f t).all p =
    t.all fun a =>
      match f a with
      | some b => p b
      | none => true
⊢ (match f h with
        | none => filterMap f t
        | some b => b :: filterMap f t).all
      p =
    (h :: t).all fun a =>
      match f a with
      | some b => p b
      | none => true

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
h : α
t : List α
ih :
  (filterMap f t).all p =
    t.all fun a =>
      match f a with
      | some b => p b
      | none => true
⊢ (filterMap f (h :: t)).all p =
    (h :: t).all fun a =>
      match f a with
      | some b => p b
      | none => true

Tactic:
simp only [filterMap_cons]

Result:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
h : α
t : List α
ih :
  (filterMap f t).all p =
    t.all fun a =>
      match f a with
      | some b => p b
      | none => true
⊢ (match f h with
        | none => filterMap f t
        | some b => b :: filterMap f t).all
      p =
    (h :: t).all fun a =>
      match f a with
      | some b => p b
      | none => true

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → Option β
p : β → Bool
⊢ (filterMap f l).all p =
    l.all fun a =>
      match f a with
      | some b => p b
      | none => true

Tactic:
induction l with
| nil => rfl
| cons h t ih =>
  simp only [filterMap_cons]
  split <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
⊢ (filterMap f []).all p =
    [].all fun a =>
      match f a with
      | some b => p b
      | none => true

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem log_im (x : ℂ) : x.log.im = x.arg

Proof state:
x : ℂ
⊢ (log x).im = x.arg

Tactic:
simp [log]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem mapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : Array { x // p x }}
    {f : { x // p x } → m β} {g : α → m β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    l.mapM f = l.unattach.mapM g

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → m β
g : α → m β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
l : List { x // p x }
⊢ List.toArray <$> List.mapM f l = List.toArray <$> List.mapM g l.unattach

Tactic:
rw [List.mapM_subtype hf]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
l : Array { x // p x }
f : { x // p x } → m β
g : α → m β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ mapM f l = mapM g l.unattach

Tactic:
rcases l with ⟨l⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → m β
g : α → m β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
l : List { x // p x }
⊢ mapM f { toList := l } = mapM g { toList := l }.unattach

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → m β
g : α → m β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
l : List { x // p x }
⊢ mapM f { toList := l } = mapM g { toList := l }.unattach

Tactic:
simp

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → m β
g : α → m β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
l : List { x // p x }
⊢ List.toArray <$> List.mapM f l = List.toArray <$> List.mapM g l.unattach
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem changeOriginSeries_support {k l : ℕ} (h : k + l ≠ Fintype.card ι) :
    f.toFormalMultilinearSeries.changeOriginSeries k l = 0 :=
  Finset.sum_eq_zero fun _ _ ↦ by
    simp_rw [FormalMultilinearSeries.changeOriginSeriesTerm,
      toFormalMultilinearSeries, dif_neg h.symm, LinearIsometryEquiv.map_zero]

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
k l : ℕ
h : k + l ≠ Fintype.card ι
x✝¹ : { s // s.card = l }
x✝ : x✝¹ ∈ Finset.univ
⊢ f.toFormalMultilinearSeries.changeOriginSeriesTerm k l ↑x✝¹ ⋯ = 0

Tactic:
simp_rw [FormalMultilinearSeries.changeOriginSeriesTerm,
  toFormalMultilinearSeries, dif_neg h.symm, LinearIsometryEquiv.map_zero]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem eq_true_eq_not_eq_false (b : Bool) : (¬b = false) = (b = true)

Proof state:
b : Bool
⊢ (¬b = false) = (b = true)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/RCLike/Inner.lean
@[simp] lemma wInner_one_const_left (a : 𝕜) (f : ι → 𝕜) :
    ⟪const _ a, f⟫_[𝕜] = conj a * ∑ i, f i

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
a : 𝕜
f : ι → 𝕜
⊢ wInner 1 (const ι a) f = (starRingEnd 𝕜) a * ∑ i : ι, f i

Tactic:
simp [wInner_one_eq_sum, mul_sum]

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem xy_modEq_of_modEq {a b c} (a1 : 1 < a) (b1 : 1 < b) (h : a ≡ b [MOD c]) :
    ∀ n, xn a1 n ≡ xn b1 n [MOD c] ∧ yn a1 n ≡ yn b1 n [MOD c]
  | 0 => by constructor <;> rfl
  | 1 => by simpa using ⟨h, ModEq.refl 1⟩
  | n + 2 =>
    ⟨(xy_modEq_of_modEq a1 b1 h n).left.add_right_cancel <| by
        rw [xn_succ_succ a1, xn_succ_succ b1]
        exact (h.mul_left _).mul (xy_modEq_of_modEq _ _ h (n + 1)).left,
      (xy_modEq_of_modEq a1 b1 h n).right.add_right_cancel <| by
        rw [yn_succ_succ a1, yn_succ_succ b1]
        exact (h.mul_left _).mul (xy_modEq_of_modEq _ _ h (n + 1)).right⟩

Proof state:
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
⊢ xn a1 0 ≡ xn b1 0 [MOD c] ∧ yn a1 0 ≡ yn b1 0 [MOD c]

Tactic:
constructor <;> rfl

Result:
no goals

Proof state:
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ yn a1 (n + 2) + yn a1 n ≡ yn b1 (n + 2) + yn b1 n [MOD c]

Tactic:
rw [yn_succ_succ a1, yn_succ_succ b1]

Result:
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ 2 * a * yn a1 (n + 1) ≡ 2 * b * yn b1 (n + 1) [MOD c]

Proof state:
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ 2 * a * yn a1 (n + 1) ≡ 2 * b * yn b1 (n + 1) [MOD c]

Tactic:
exact (h.mul_left _).mul (xy_modEq_of_modEq _ _ h (n + 1)).right

Result:
no goals

Proof state:
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ xn a1 (n + 2) + xn a1 n ≡ xn b1 (n + 2) + xn b1 n [MOD c]

Tactic:
rw [xn_succ_succ a1, xn_succ_succ b1]

Result:
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ 2 * a * xn a1 (n + 1) ≡ 2 * b * xn b1 (n + 1) [MOD c]

Proof state:
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ 2 * a * xn a1 (n + 1) ≡ 2 * b * xn b1 (n + 1) [MOD c]

Tactic:
exact (h.mul_left _).mul (xy_modEq_of_modEq _ _ h (n + 1)).left

Result:
no goals

Proof state:
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
⊢ xn a1 1 ≡ xn b1 1 [MOD c] ∧ yn a1 1 ≡ yn b1 1 [MOD c]

Tactic:
simpa using ⟨h, ModEq.refl 1⟩

Result:
no goals
-- Mathlib/Topology/MetricSpace/Defs.lean
theorem MetricSpace.replaceTopology_eq {γ} [U : TopologicalSpace γ] (m : MetricSpace γ)
    (H : U = m.toPseudoMetricSpace.toUniformSpace.toTopologicalSpace) :
    m.replaceTopology H = m

Proof state:
γ : Type u_3
U : TopologicalSpace γ
m : MetricSpace γ
H : U = UniformSpace.toTopologicalSpace
⊢ m.replaceTopology H = m

Tactic:
ext

Result:
case h.dist.h.h
γ : Type u_3
U : TopologicalSpace γ
m : MetricSpace γ
H : U = UniformSpace.toTopologicalSpace
x✝¹ x✝ : γ
⊢ dist x✝¹ x✝ = dist x✝¹ x✝

Proof state:
case h.dist.h.h
γ : Type u_3
U : TopologicalSpace γ
m : MetricSpace γ
H : U = UniformSpace.toTopologicalSpace
x✝¹ x✝ : γ
⊢ dist x✝¹ x✝ = dist x✝¹ x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Interval/Finset/Defs.lean
@[simp] lemma toFinset_Ico (a b : α) [Fintype (Ico a b)] : (Ico a b).toFinset = Finset.Ico a b

Proof state:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Ico a b)
⊢ (Ico a b).toFinset = Finset.Ico a b

Tactic:
ext

Result:
case h
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Ico a b)
a✝ : α
⊢ a✝ ∈ (Ico a b).toFinset ↔ a✝ ∈ Finset.Ico a b

Proof state:
case h
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Ico a b)
a✝ : α
⊢ a✝ ∈ (Ico a b).toFinset ↔ a✝ ∈ Finset.Ico a b

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/SplittingField/Construction.lean
theorem natDegree_removeFactor (f : K[X]) : f.removeFactor.natDegree = f.natDegree - 1

Proof state:
K : Type v
inst✝ : Field K
f : K[X]
⊢ f.removeFactor.natDegree = f.natDegree - 1

Tactic:
rw [removeFactor, natDegree_divByMonic _ (monic_X_sub_C _), natDegree_map, natDegree_X_sub_C]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem LinearIndependent.group_smul_iff {G : Type*} [hG : Group G] [DistribMulAction G R]
    [DistribMulAction G M] [IsScalarTower G R M] [SMulCommClass G R M] (v : ι → M) (w : ι → G) :
    LinearIndependent R (w • v) ↔ LinearIndependent R v

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
w : ι → G
⊢ LinearIndependent R (w • v) ↔ LinearIndependent R v

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.group_smul w⟩

Result:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
w : ι → G
h : LinearIndependent R (w • v)
⊢ LinearIndependent R v

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
w : ι → G
h : LinearIndependent R (w • v)
⊢ LinearIndependent R v

Tactic:
convert h.group_smul (fun i ↦ (w i)⁻¹)

Result:
case h.e'_4
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
w : ι → G
h : LinearIndependent R (w • v)
⊢ v = (fun i => (w i)⁻¹) • w • v

Proof state:
case h.e'_4
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
w : ι → G
h : LinearIndependent R (w • v)
⊢ v = (fun i => (w i)⁻¹) • w • v

Tactic:
simp [funext_iff]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Defs.lean
@[simp, norm_cast] lemma cast_ofNat (n : ℕ) [n.AtLeastTwo] :
    ((ofNat(n) : ℚ) : α) = (ofNat(n) : α)

Proof state:
α : Type u_3
inst✝¹ : DivisionRing α
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑(OfNat.ofNat n) = OfNat.ofNat n

Tactic:
simp [cast_def]

Result:
no goals
-- Mathlib/CategoryTheory/Filtered/Final.lean
theorem Functor.initial_of_exists_of_isCofiltered [IsCofilteredOrEmpty C]
    (h₁ : ∀ d, ∃ c, Nonempty (F.obj c ⟶ d)) (h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d),
      ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s') : Functor.Initial F

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
h₁ : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
⊢ F.Initial

Tactic:
suffices ∀ d, IsCofiltered (CostructuredArrow F d) from
  initial_of_isCofiltered_costructuredArrow F

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
h₁ : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
⊢ ∀ (d : D), IsCofiltered (CostructuredArrow F d)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
h₁ : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
⊢ ∀ (d : D), IsCofiltered (CostructuredArrow F d)

Tactic:
exact isCofiltered_costructuredArrow_of_isCofiltered_of_exists F h₁ h₂

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
lemma isClique_empty : G.IsClique ∅

Proof state:
α : Type u_1
G : SimpleGraph α
⊢ G.IsClique ∅

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem leadingCoeff_zero : m.leadingCoeff (0 : MvPolynomial σ R) = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
⊢ m.leadingCoeff 0 = 0

Tactic:
simp [degree, leadingCoeff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_sublist {p : α → Bool} : ∀ (l : List α), filter p l <+ l
  | [] => .slnil
  | a :: l => by rw [filter]; split <;> simp [Sublist.cons, Sublist.cons₂, filter_sublist l]

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
⊢ filter p (a :: l) <+ a :: l

Tactic:
rw [filter]

Result:
α : Type u_1
p : α → Bool
a : α
l : List α
⊢ (match p a with
    | true => a :: filter p l
    | false => filter p l) <+
    a :: l

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
⊢ (match p a with
    | true => a :: filter p l
    | false => filter p l) <+
    a :: l

Tactic:
split <;> simp [Sublist.cons, Sublist.cons₂, filter_sublist l]

Result:
no goals
-- Mathlib/Analysis/Calculus/LocalExtr/Rolle.lean
theorem exists_deriv_eq_zero' (hab : a < b) (hfa : Tendsto f (𝓝[>] a) (𝓝 l))
    (hfb : Tendsto f (𝓝[<] b) (𝓝 l)) : ∃ c ∈ Ioo a b, deriv f c = 0

Proof state:
case neg.intro.intro
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
h : ¬∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
c : ℝ
hc : c ∈ Ioo a b
hcdiff : ¬DifferentiableAt ℝ f c
⊢ ∃ c ∈ Ioo a b, deriv f c = 0

Tactic:
exact ⟨c, hc, deriv_zero_of_not_differentiableAt hcdiff⟩

Result:
no goals

Proof state:
case neg
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
h : ¬∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
⊢ ∃ c ∈ Ioo a b, deriv f c = 0

Tactic:
obtain ⟨c, hc, hcdiff⟩ : ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x := by
  push_neg at h; exact h

Result:
case neg.intro.intro
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
h : ¬∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
c : ℝ
hc : c ∈ Ioo a b
hcdiff : ¬DifferentiableAt ℝ f c
⊢ ∃ c ∈ Ioo a b, deriv f c = 0

Proof state:
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
h : ¬∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
⊢ ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x

Tactic:
push_neg at h

Result:
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
h : ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x
⊢ ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x

Proof state:
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
⊢ ∃ c ∈ Ioo a b, deriv f c = 0

Tactic:
by_cases h : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x

Result:
case pos
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
h : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
⊢ ∃ c ∈ Ioo a b, deriv f c = 0

case neg
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
h : ¬∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
⊢ ∃ c ∈ Ioo a b, deriv f c = 0

Proof state:
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
h : ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x
⊢ ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x

Tactic:
exact h

Result:
no goals

Proof state:
case pos
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
h : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
⊢ ∃ c ∈ Ioo a b, deriv f c = 0

Tactic:
exact exists_hasDerivAt_eq_zero' hab hfa hfb fun x hx => (h x hx).hasDerivAt

Result:
no goals
-- Mathlib/LinearAlgebra/TensorPower/Basic.lean
theorem algebraMap₀_mul {n} (r : R) (a : ⨂[R]^n M) :
    cast R M (zero_add _) (algebraMap₀ r ₜ* a) = r • a

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : ⨂[R]^n M
⊢ (cast R M ⋯) (GradedMonoid.GMul.mul (algebraMap₀ r) a) = r • a

Tactic:
rw [gMul_eq_coe_linearMap, algebraMap₀_eq_smul_one, LinearMap.map_smul₂,
  LinearEquiv.map_smul, ← gMul_eq_coe_linearMap, one_mul]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem MDifferentiableAt.comp_mdifferentiableWithinAt_of_eq {y : M'}
    (hg : MDifferentiableAt I' I'' g y) (hf : MDifferentiableWithinAt I I' f s x) (hy : f x = y) :
    MDifferentiableWithinAt I I'' (g ∘ f) s x

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
hf : MDifferentiableWithinAt I I' f s x
hg : MDifferentiableAt I' I'' g (f x)
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x

Tactic:
exact hg.comp_mdifferentiableWithinAt _ hf

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
y : M'
hg : MDifferentiableAt I' I'' g y
hf : MDifferentiableWithinAt I I' f s x
hy : f x = y
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x

Tactic:
subst hy

Result:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
hf : MDifferentiableWithinAt I I' f s x
hg : MDifferentiableAt I' I'' g (f x)
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x
-- Mathlib/Analysis/Convex/Intrinsic.lean
theorem intrinsicInterior_union_intrinsicFrontier (s : Set P) :
    intrinsicInterior 𝕜 s ∪ intrinsicFrontier 𝕜 s = intrinsicClosure 𝕜 s

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 : Set P
⊢ intrinsicInterior 𝕜 s ∪ intrinsicFrontier 𝕜 s = intrinsicClosure 𝕜 s

Tactic:
simp [intrinsicClosure, intrinsicInterior, intrinsicFrontier, closure_eq_interior_union_frontier,
  image_union]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
theorem terminal.comp_from [HasTerminal C] {P Q : C} (f : P ⟶ Q) :
    f ≫ terminal.from Q = terminal.from P

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasTerminal C
P Q : C
f : P ⟶ Q
⊢ f ≫ «from» Q = «from» P

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx?_subtype {p : α → Prop} {l : List { x // p x }}
    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    l.findIdx? f = l.unattach.findIdx? g

Proof state:
α : Type u_1
p : α → Prop
l : List { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ findIdx? f l = findIdx? g l.unattach

Tactic:
unfold unattach

Result:
α : Type u_1
p : α → Prop
l : List { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ findIdx? f l = findIdx? g (map (fun x => x.val) l)

Proof state:
case nil
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ findIdx? f [] = findIdx? g (map (fun x => x.val) [])

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
l : List { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ findIdx? f l = findIdx? g (map (fun x => x.val) l)

Tactic:
induction l with
| nil => simp
| cons a l ih =>
  simp [hf, findIdx?_cons]
  split <;> simp [ih, Function.comp_def]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
a : { x // p x }
l : List { x // p x }
ih : findIdx? f l = findIdx? g (map (fun x => x.val) l)
⊢ (if g a.val = true then some 0 else Option.map (fun i => i + 1) (findIdx? f l)) =
    if g a.val = true then some 0 else Option.map (fun i => i + 1) (findIdx? g l.unattach)

Tactic:
split <;> simp [ih, Function.comp_def]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
a : { x // p x }
l : List { x // p x }
ih : findIdx? f l = findIdx? g (map (fun x => x.val) l)
⊢ findIdx? f (a :: l) = findIdx? g (map (fun x => x.val) (a :: l))

Tactic:
simp [hf, findIdx?_cons]

Result:
case cons
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
a : { x // p x }
l : List { x // p x }
ih : findIdx? f l = findIdx? g (map (fun x => x.val) l)
⊢ (if g a.val = true then some 0 else Option.map (fun i => i + 1) (findIdx? f l)) =
    if g a.val = true then some 0 else Option.map (fun i => i + 1) (findIdx? g l.unattach)
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem abs_rpow_of_nonneg {x y : ℝ} (hx_nonneg : 0 ≤ x) : |x ^ y| = |x| ^ y

Proof state:
x y : ℝ
hx_nonneg : 0 ≤ x
⊢ |x ^ y| = |x| ^ y

Tactic:
have h_rpow_nonneg : 0 ≤ x ^ y := Real.rpow_nonneg hx_nonneg _

Result:
x y : ℝ
hx_nonneg : 0 ≤ x
h_rpow_nonneg : 0 ≤ x ^ y
⊢ |x ^ y| = |x| ^ y

Proof state:
x y : ℝ
hx_nonneg : 0 ≤ x
h_rpow_nonneg : 0 ≤ x ^ y
⊢ |x ^ y| = |x| ^ y

Tactic:
rw [abs_eq_self.mpr hx_nonneg, abs_eq_self.mpr h_rpow_nonneg]

Result:
no goals