harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Basic.lean
theorem length_eq_length_filter_add {l : List (α)} (f : α → Bool) :
    l.length = (l.filter f).length + (l.filter (! f ·)).length

Proof state:
α : Type u
l : List α
f : α → Bool
⊢ l.length = (filter f l).length + (filter (fun x => !f x) l).length

Tactic:
simp_rw [← List.countP_eq_length_filter, l.length_eq_countP_add_countP f, Bool.not_eq_true,
  Bool.decide_eq_false]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem hasFDerivWithinAt_singleton (f : E → F) (x : E) :
    HasFDerivWithinAt f (0 : E →L[𝕜] F) {x} x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ HasFDerivWithinAt f 0 {x} x

Tactic:
simp only [HasFDerivWithinAt, nhdsWithin_singleton, hasFDerivAtFilter_iff_isLittleO,
  isLittleO_pure, ContinuousLinearMap.zero_apply, sub_self]

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
theorem lt_add_right (ha : a ≠ ∞) (hb : b ≠ 0) : a < a + b

Proof state:
a b : ℝ≥0∞
ha : a ≠ ⊤
hb : b ≠ 0
⊢ a < a + b

Tactic:
rwa [← pos_iff_ne_zero, ← ENNReal.add_lt_add_iff_left ha, add_zero] at hb

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem bool_iff_false {b : Bool} : ¬b ↔ b = false

Proof state:
b : Bool
⊢ ¬b = true ↔ b = false

Tactic:
cases b <;> decide

Result:
no goals
-- Mathlib/Algebra/Homology/QuasiIso.lean
lemma quasiIso_map_iff_of_preservesHomology [F.ReflectsIsomorphisms] :
    QuasiIso ((F.mapHomologicalComplex c).map φ) ↔ QuasiIso φ

Proof state:
ι : Type u_1
c : ComplexShape ι
C₁ : Type u_2
C₂ : Type u_3
inst✝¹⁰ : Category.{u_4, u_2} C₁
inst✝⁹ : Category.{u_5, u_3} C₂
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
K L : HomologicalComplex C₁ c
φ : K ⟶ L
F : C₁ ⥤ C₂
inst✝⁶ : F.Additive
inst✝⁵ : F.PreservesHomology
inst✝⁴ : ∀ (i : ι), K.HasHomology i
inst✝³ : ∀ (i : ι), L.HasHomology i
inst✝² : ∀ (i : ι), ((F.mapHomologicalComplex c).obj K).HasHomology i
inst✝¹ : ∀ (i : ι), ((F.mapHomologicalComplex c).obj L).HasHomology i
inst✝ : F.ReflectsIsomorphisms
⊢ QuasiIso ((F.mapHomologicalComplex c).map φ) ↔ QuasiIso φ

Tactic:
simp only [quasiIso_iff, quasiIsoAt_map_iff_of_preservesHomology φ F]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Finset.lean
lemma cons_mem_piFinset_cons {x_zero : α 0} {x_tail : (i : Fin n) → α i.succ}
    {s_zero : Finset (α 0)} {s_tail : (i : Fin n) → Finset (α i.succ)} :
    cons x_zero x_tail ∈ piFinset (cons s_zero s_tail) ↔
      x_zero ∈ s_zero ∧ x_tail ∈ piFinset s_tail

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
x_zero : α 0
x_tail : (i : Fin n) → α i.succ
s_zero : Finset (α 0)
s_tail : (i : Fin n) → Finset (α i.succ)
⊢ cons x_zero x_tail ∈ piFinset (cons s_zero s_tail) ↔ x_zero ∈ s_zero ∧ x_tail ∈ piFinset s_tail

Tactic:
simp_rw [mem_piFinset_iff_zero_tail, cons_zero, tail_cons]

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem emptyOn_dual_eq : (emptyOn α)✶ = emptyOn α

Proof state:
α : Type u_1
⊢ (emptyOn α)✶.E = ∅

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
⊢ (emptyOn α)✶ = emptyOn α

Tactic:
rw [← ground_eq_empty_iff]

Result:
α : Type u_1
⊢ (emptyOn α)✶.E = ∅
-- Mathlib/Data/Finset/Powerset.lean
theorem mem_powerset_self (s : Finset α) : s ∈ powerset s

Proof state:
α : Type u_1
s : Finset α
⊢ s ∈ s.powerset

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem eq_of_inv_eq_inv {f g : X ⟶ Y} [IsIso f] [IsIso g] (p : inv f = inv g) : f = g

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : IsIso g
p : inv f = inv g
⊢ inv f ≫ f = inv f ≫ g

Tactic:
rw [inv_hom_id, p, inv_hom_id]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : IsIso g
p : inv f = inv g
⊢ f = g

Tactic:
apply (cancel_epi (inv f)).1

Result:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : IsIso g
p : inv f = inv g
⊢ inv f ≫ f = inv f ≫ g
-- Mathlib/Data/Real/Pi/Bounds.lean
theorem pi_gt_d4 : 3.1415 < π

Proof state:
⊢ 3.1415 < π

Tactic:
pi_lower_bound [
  1970 / 1393, 3010 / 1629, 11689 / 5959, 10127 / 5088, 33997 / 17019, 23235 / 11621]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
theorem go_isPrefix_aig {aig : AIG β} :
    IsPrefix aig.decls (go aig expr atomHandler).val.aig.decls

Proof state:
case idx_eq
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
idx : Nat
h : idx < aig.decls.size
⊢ (go aig expr atomHandler).val.aig.decls[idx] = aig.decls[idx]

Tactic:
apply ofBoolExprCached.go_decl_eq

Result:
no goals

Proof state:
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ IsPrefix aig.decls (go aig expr atomHandler).val.aig.decls

Tactic:
apply IsPrefix.of

Result:
case idx_eq
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ ∀ (idx : Nat) (h : idx < aig.decls.size), (go aig expr atomHandler).val.aig.decls[idx] = aig.decls[idx]

case size_le
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ aig.decls.size ≤ (go aig expr atomHandler).val.aig.decls.size

Proof state:
case idx_eq
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ ∀ (idx : Nat) (h : idx < aig.decls.size), (go aig expr atomHandler).val.aig.decls[idx] = aig.decls[idx]

Tactic:
intro idx h

Result:
case idx_eq
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
idx : Nat
h : idx < aig.decls.size
⊢ (go aig expr atomHandler).val.aig.decls[idx] = aig.decls[idx]

Proof state:
case size_le
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ aig.decls.size ≤ (go aig expr atomHandler).val.aig.decls.size

Tactic:
apply go_le_size

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_insertIfNew [LawfulBEq α] (h : m.1.WF) {k a : α} [Inhabited (β a)] {v : β k} :
    (m.insertIfNew k v).get! a =
      if h : k == a ∧ m.contains k = false then cast (congrArg β (eq_of_beq h.1)) v
      else m.get! a

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
k a : α
inst✝ : Inhabited (β a)
v : β k
⊢ (m.insertIfNew k v).get! a = if h : (k == a) = true ∧ m.contains k = false then cast ⋯ v else m.get! a

Tactic:
simp_to_model [insertIfNew] using List.getValueCast!_insertEntryIfNew

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Erase.lean
theorem mem_of_mem_eraseIdx {l : Vector α n} {i : Nat} {h} {a : α} (h : a ∈ l.eraseIdx i) : a ∈ l

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h✝ : i < n
a : α
h : a ∈ l.eraseIdx i h✝
⊢ a ∈ l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
i : Nat
a : α
l : Array α
h✝ : i < l.size
h : a ∈ { toArray := l, size_toArray := ⋯ }.eraseIdx i h✝
⊢ a ∈ { toArray := l, size_toArray := ⋯ }

Proof state:
α : Type u_1
i : Nat
a : α
l : Array α
h✝ : i < l.size
h : a ∈ { toArray := l, size_toArray := ⋯ }.eraseIdx i h✝
⊢ a ∈ l.eraseIdx ?m.16514 ?m.16515

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
α : Type u_1
i : Nat
a : α
l : Array α
h✝ : i < l.size
h : a ∈ { toArray := l, size_toArray := ⋯ }.eraseIdx i h✝
⊢ a ∈ { toArray := l, size_toArray := ⋯ }

Tactic:
simpa using Array.mem_of_mem_eraseIdx (by simpa using h)

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
theorem _root_.Filter.EventuallyEq.lieBracketWithin_vectorField_eq
    (hV : V₁ =ᶠ[𝓝[s] x] V) (hxV : V₁ x = V x) (hW : W₁ =ᶠ[𝓝[s] x] W) (hxW : W₁ x = W x) :
    lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
s : Set E
x : E
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
⊢ lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x

Tactic:
simp only [lieBracketWithin, hV.fderivWithin_eq hxV, hW.fderivWithin_eq hxW, hxV, hxW]

Result:
no goals
-- Mathlib/Order/WithBot.lean
theorem some_eq_map_iff {f : α → β} {y : β} {v : WithTop α} :
    .some y = WithTop.map f v ↔ ∃ x, v = .some x ∧ f x = y

Proof state:
α : Type u_1
β : Type u_2
f : α → β
y : β
v : WithTop α
⊢ ↑y = map f v ↔ ∃ x, v = ↑x ∧ f x = y

Tactic:
cases v <;> simp [eq_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem length_eraseIdx_of_lt {l : List α} {i} (h : i < length l) :
    (l.eraseIdx i).length = length l - 1

Proof state:
α : Type u_1
l : List α
i : Nat
h : i < l.length
⊢ (l.eraseIdx i).length = l.length - 1

Tactic:
simp [length_eraseIdx, h]

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem Set.Subsingleton.maximal_mem_iff (h : s.Subsingleton) : Maximal (· ∈ s) x ↔ x ∈ s

Proof state:
α : Type u_1
x : α
s : Set α
inst✝ : Preorder α
h : s.Subsingleton
⊢ Maximal (fun x => x ∈ s) x ↔ x ∈ s

Tactic:
obtain (rfl | ⟨x, rfl⟩) := h.eq_empty_or_singleton <;> simp

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Maximal/Localization.lean
theorem toPiLocalization_not_surjective_of_infinite [Infinite ι] :
    ¬ Function.Surjective (toPiLocalization (Π i, R i)) :=
  fun surj ↦ MaximalSpectrum.toPiLocalization_not_surjective_of_infinite R <| by
    rw [← piLocalizationToMaximal_comp_toPiLocalization]
    exact (piLocalizationToMaximal_surjective _).comp surj

Proof state:
ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
⊢ Function.Surjective ⇑(MaximalSpectrum.toPiLocalization ((i : ι) → R i))

Tactic:
rw [← piLocalizationToMaximal_comp_toPiLocalization]

Result:
ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
⊢ Function.Surjective ⇑((piLocalizationToMaximal ((i : ι) → R i)).comp (toPiLocalization ((i : ι) → R i)))

Proof state:
ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
⊢ Function.Surjective ⇑((piLocalizationToMaximal ((i : ι) → R i)).comp (toPiLocalization ((i : ι) → R i)))

Tactic:
exact (piLocalizationToMaximal_surjective _).comp surj

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBasis.isBasis_union_of_subset (hI : M.IsBasis I X) (hJ : M.Indep J) (hIJ : I ⊆ J) :
    M.IsBasis J (J ∪ X)

Proof state:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
⊢ M.Indep J

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
⊢ M.IsBasis J (J ∪ X)

Tactic:
convert hJ.isBasis_self.union_isBasis_union hI _ <;>
rw [union_eq_self_of_subset_right hIJ]

Result:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
⊢ M.Indep J
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem isoIsPullback_inv_snd (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) :
    (h.isoIsPullback _ _ h').inv ≫ snd = snd'

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
P' : C
fst' : P' ⟶ X
snd' : P' ⟶ Y
h : IsPullback fst snd f g
h' : IsPullback fst' snd' f g
⊢ (isoIsPullback X Y h h').inv ≫ snd = snd'

Tactic:
simp only [Iso.inv_comp_eq, isoIsPullback_hom_snd]

Result:
no goals
-- Mathlib/Data/Int/Basic.lean
/-- If an integer with larger absolute value divides an integer, it is zero. -/
lemma eq_zero_of_dvd_of_natAbs_lt_natAbs (hmn : m ∣ n) (hnm : natAbs n < natAbs m) : n = 0

Proof state:
m n : ℤ
hmn : m ∣ n
hnm : n.natAbs < m.natAbs
⊢ n = 0

Tactic:
rw [← natAbs_dvd, ← dvd_natAbs, natCast_dvd_natCast] at hmn

Result:
m n : ℤ
hmn : m.natAbs ∣ n.natAbs
hnm : n.natAbs < m.natAbs
⊢ n = 0

Proof state:
m n : ℤ
hmn : m.natAbs ∣ n.natAbs
hnm : n.natAbs < m.natAbs
⊢ n = 0

Tactic:
rw [← natAbs_eq_zero]

Result:
m n : ℤ
hmn : m.natAbs ∣ n.natAbs
hnm : n.natAbs < m.natAbs
⊢ n.natAbs = 0

Proof state:
m n : ℤ
hmn : m.natAbs ∣ n.natAbs
hnm : n.natAbs < m.natAbs
⊢ n.natAbs = 0

Tactic:
exact Nat.eq_zero_of_dvd_of_lt hmn hnm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_insertManyIfNewUnit_list_of_mem
    [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k : α} {h'} (mem : k ∈ m) :
    getKey (insertManyIfNewUnit m l) k h' = getKey m k mem

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k : α
h' : k ∈ insertManyIfNewUnit m l
mem : k ∈ m
⊢ (insertManyIfNewUnit m l).getKey k h' = m.getKey k mem

Tactic:
simp_to_raw using Raw₀.Const.getKey_insertManyIfNewUnit_list_of_contains

Result:
no goals
-- Mathlib/Data/Int/ConditionallyCompleteOrder.lean
theorem csSup_empty : sSup (∅ : Set ℤ) = 0 :=
  dif_neg (by simp)

Proof state:
⊢ ¬(∅.Nonempty ∧ BddAbove ∅)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/ODE/PicardLindelof.lean
theorem exists_solution [CompleteSpace E] :
    ∃ f : ℝ → E, f v.t₀ = v.x₀ ∧ ∀ t ∈ Icc v.tMin v.tMax,
      HasDerivWithinAt f (v t (f t)) (Icc v.tMin v.tMax) t

Proof state:
case intro.refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
f : v.FunSpace
hf : f.next = f
t : ℝ
ht : t ∈ Icc v.tMin v.tMax
⊢ HasDerivWithinAt (f.toFun ∘ v.proj) (v.toFun t (f.toFun (v.proj t))) (Icc v.tMin v.tMax) t

Tactic:
lift t to Icc v.tMin v.tMax using ht

Result:
case intro.refine_2.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
f : v.FunSpace
hf : f.next = f
t : { x // x ∈ Icc v.tMin v.tMax }
⊢ HasDerivWithinAt (f.toFun ∘ v.proj) (v.toFun (↑t) (f.toFun (v.proj ↑t))) (Icc v.tMin v.tMax) ↑t

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
⊢ ∃ f, f ↑v.t₀ = v.x₀ ∧ ∀ t ∈ Icc v.tMin v.tMax, HasDerivWithinAt f (v.toFun t (f t)) (Icc v.tMin v.tMax) t

Tactic:
rcases v.exists_fixed with ⟨f, hf⟩

Result:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
f : v.FunSpace
hf : f.next = f
⊢ ∃ f, f ↑v.t₀ = v.x₀ ∧ ∀ t ∈ Icc v.tMin v.tMax, HasDerivWithinAt f (v.toFun t (f t)) (Icc v.tMin v.tMax) t

Proof state:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
f : v.FunSpace
hf : f.next = f
⊢ ∃ f, f ↑v.t₀ = v.x₀ ∧ ∀ t ∈ Icc v.tMin v.tMax, HasDerivWithinAt f (v.toFun t (f t)) (Icc v.tMin v.tMax) t

Tactic:
refine ⟨f ∘ v.proj, ?_, fun t ht => ?_⟩

Result:
case intro.refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
f : v.FunSpace
hf : f.next = f
⊢ (f.toFun ∘ v.proj) ↑v.t₀ = v.x₀

case intro.refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
f : v.FunSpace
hf : f.next = f
t : ℝ
ht : t ∈ Icc v.tMin v.tMax
⊢ HasDerivWithinAt (f.toFun ∘ v.proj) (v.toFun t ((f.toFun ∘ v.proj) t)) (Icc v.tMin v.tMax) t

Proof state:
case intro.refine_2.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : PicardLindelof E
inst✝ : CompleteSpace E
f : v.FunSpace
hf : f.next = f
t : { x // x ∈ Icc v.tMin v.tMax }
⊢ HasDerivWithinAt (f.toFun ∘ v.proj) (v.toFun (↑t) (f.toFun (v.proj ↑t))) (Icc v.tMin v.tMax) ↑t

Tactic:
simpa only [hf, v.proj_coe] using f.hasDerivWithinAt_next t

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem expand_char (f : R[X]) : map (frobenius R p) (expand R p f) = f ^ p

Proof state:
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
⊢ map (frobenius R p) ((expand R p) f) = f ^ p

Tactic:
refine f.induction_on' (fun a b ha hb => ?_) fun n a => ?_

Result:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f a b : R[X]
ha : map (frobenius R p) ((expand R p) a) = a ^ p
hb : map (frobenius R p) ((expand R p) b) = b ^ p
⊢ map (frobenius R p) ((expand R p) (a + b)) = (a + b) ^ p

case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ map (frobenius R p) ((expand R p) ((monomial n) a)) = (monomial n) a ^ p

Proof state:
case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ map (frobenius R p) ((expand R p) ((monomial n) a)) = (monomial n) a ^ p

Tactic:
rw [expand_monomial, map_monomial, ← C_mul_X_pow_eq_monomial, ← C_mul_X_pow_eq_monomial,
  mul_pow, ← C.map_pow, frobenius_def]

Result:
case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ C (a ^ p) * X ^ (n * p) = C (a ^ p) * (X ^ n) ^ p

Proof state:
case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ C (a ^ p) * X ^ (n * p) = C (a ^ p) * (X ^ n) ^ p

Tactic:
ring

Result:
no goals

Proof state:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f a b : R[X]
ha : map (frobenius R p) ((expand R p) a) = a ^ p
hb : map (frobenius R p) ((expand R p) b) = b ^ p
⊢ map (frobenius R p) ((expand R p) (a + b)) = (a + b) ^ p

Tactic:
rw [map_add, Polynomial.map_add, ha, hb, add_pow_expChar]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem map_comap {β} (f : α → β) (m : OuterMeasure β) : map f (comap f m) = restrict (range f) m :=
  ext fun s => congr_arg m <| by simp only [image_preimage_eq_inter_range, Subtype.range_coe]

Proof state:
α : Type u_1
β : Type u_3
f : α → β
m : OuterMeasure β
s : Set β
⊢ f '' (f ⁻¹' s) = Subtype.val '' (Subtype.val ⁻¹' s)

Tactic:
simp only [image_preimage_eq_inter_range, Subtype.range_coe]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@[simp]
lemma map_polynomialX : (W'.map f).toJacobian.polynomialX = MvPolynomial.map f W'.polynomialX

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
⊢ (map W' f).toJacobian.polynomialX = (MvPolynomial.map f) W'.polynomialX

Tactic:
simp only [polynomialX, map_polynomial, pderiv_map]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem comp_smulₛₗ [SMulCommClass R₂ R₂ M₂] [SMulCommClass R₃ R₃ M₃] [ContinuousConstSMul R₂ M₂]
    [ContinuousConstSMul R₃ M₃] (h : M₂ →SL[σ₂₃] M₃) (c : R₂) (f : M →SL[σ₁₂] M₂) :
    h.comp (c • f) = σ₂₃ c • h.comp f

Proof state:
case h
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁶ : Semiring R
inst✝¹⁵ : Semiring R₂
inst✝¹⁴ : Semiring R₃
M : Type u_6
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
M₂ : Type u_7
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
M₃ : Type u_8
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝³ : SMulCommClass R₂ R₂ M₂
inst✝² : SMulCommClass R₃ R₃ M₃
inst✝¹ : ContinuousConstSMul R₂ M₂
inst✝ : ContinuousConstSMul R₃ M₃
h : M₂ →SL[σ₂₃] M₃
c : R₂
f : M →SL[σ₁₂] M₂
x : M
⊢ (h.comp (c • f)) x = (σ₂₃ c • h.comp f) x

Tactic:
simp only [coe_smul', coe_comp', Function.comp_apply, Pi.smul_apply,
  ContinuousLinearMap.map_smulₛₗ]

Result:
no goals

Proof state:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁶ : Semiring R
inst✝¹⁵ : Semiring R₂
inst✝¹⁴ : Semiring R₃
M : Type u_6
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
M₂ : Type u_7
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
M₃ : Type u_8
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝³ : SMulCommClass R₂ R₂ M₂
inst✝² : SMulCommClass R₃ R₃ M₃
inst✝¹ : ContinuousConstSMul R₂ M₂
inst✝ : ContinuousConstSMul R₃ M₃
h : M₂ →SL[σ₂₃] M₃
c : R₂
f : M →SL[σ₁₂] M₂
⊢ h.comp (c • f) = σ₂₃ c • h.comp f

Tactic:
ext x

Result:
case h
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁶ : Semiring R
inst✝¹⁵ : Semiring R₂
inst✝¹⁴ : Semiring R₃
M : Type u_6
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
M₂ : Type u_7
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
M₃ : Type u_8
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝³ : SMulCommClass R₂ R₂ M₂
inst✝² : SMulCommClass R₃ R₃ M₃
inst✝¹ : ContinuousConstSMul R₂ M₂
inst✝ : ContinuousConstSMul R₃ M₃
h : M₂ →SL[σ₂₃] M₃
c : R₂
f : M →SL[σ₁₂] M₂
x : M
⊢ (h.comp (c • f)) x = (σ₂₃ c • h.comp f) x
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
/-- See `MulAction.isBlock_subgroup` for a version that works for the left action of a group on
itself. -/
@[to_additive "See `AddAction.isBlock_subgroup` for a version that works for the left action
of a group on itself."]
lemma isBlock_subgroup' : IsBlock G (s : Set H)

Proof state:
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G Hᵐᵒᵖ H
⊢ IsBlock G ↑s

Tactic:
simp only [IsBlock, disjoint_left]

Result:
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G Hᵐᵒᵖ H
⊢ ∀ ⦃g₁ g₂ : G⦄, g₁ • ↑s ≠ g₂ • ↑s → ∀ ⦃a : H⦄, a ∈ g₁ • ↑s → a ∉ g₂ • ↑s

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ False

Tactic:
refine hab ?_

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ a • ↑s = b • ↑s

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ a • ↑s = b • ↑s

Tactic:
rw [← op_smul_coe_set hc, ← smul_assoc, ← op_smul, ← hcd, op_smul, smul_assoc, op_smul_coe_set hc,
  op_smul_coe_set hd]

Result:
no goals

Proof state:
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G Hᵐᵒᵖ H
⊢ ∀ ⦃g₁ g₂ : G⦄, g₁ • ↑s ≠ g₂ • ↑s → ∀ ⦃a : H⦄, a ∈ g₁ • ↑s → a ∉ g₂ • ↑s

Tactic:
rintro a b hab _ ⟨c, hc, rfl⟩ ⟨d, hd, (hcd : b • d = a • c)⟩

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ False