harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/ContextFreeGrammar.lean
protected lemma Rewrites.reverse : ∀ {u v}, r.Rewrites u v → r.reverse.Rewrites u.reverse v.reverse
  | _, _, head s => by simpa using .append_left .input_output _
  | _, _, @cons _ _ _ x u v h => by simpa using h.reverse.append_right _

Proof state:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
s : List (Symbol T N)
⊢ r.reverse.Rewrites (Symbol.nonterminal r.input :: s).reverse (r.output ++ s).reverse

Tactic:
simpa using .append_left .input_output _

Result:
no goals

Proof state:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
x : Symbol T N
u v : List (Symbol T N)
h : r.Rewrites u v
⊢ r.reverse.Rewrites (x :: u).reverse (x :: v).reverse

Tactic:
simpa using h.reverse.append_right _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem countP_le_size {l : Vector α n} : countP p l ≤ n

Proof state:
case mk
α : Type u_1
p : α → Bool
l : Array α
⊢ countP p { toArray := l, size_toArray := ⋯ } ≤ l.size

Tactic:
simp [Array.countP_le_size (p := p)]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
n : Nat
l : Vector α n
⊢ countP p l ≤ n

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
p : α → Bool
l : Array α
⊢ countP p { toArray := l, size_toArray := ⋯ } ≤ l.size
-- Mathlib/Topology/ContinuousMap/Algebra.lean
theorem Subalgebra.SeparatesPoints.strongly {s : Subalgebra 𝕜 C(α, 𝕜)} (h : s.SeparatesPoints) :
    (s : Set C(α, 𝕜)).SeparatesPointsStrongly := fun v x y => by
  by_cases n : x = y
  · subst n
    exact ⟨_, (v x • (1 : s) : s).prop, mul_one _, mul_one _⟩
  obtain ⟨_, ⟨f, hf, rfl⟩, hxy⟩ := h n
  replace hxy : f x - f y ≠ 0 := sub_ne_zero_of_ne hxy
  let a := v x
  let b := v y
  let f' : s :=
    ((b - a) * (f x - f y)⁻¹) • (algebraMap _ s (f x) - (⟨f, hf⟩ : s)) + algebraMap _ s a
  refine ⟨f', f'.prop, ?_, ?_⟩
  · simp [a, b, f']
  · simp [a, b, f', inv_mul_cancel_right₀ hxy]

Proof state:
case neg.intro.intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
inst✝¹ : Field 𝕜
inst✝ : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : f x - f y ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
f' : ↥s := ((b - a) * (f x - f y)⁻¹) • ((algebraMap 𝕜 ↥s) (f x) - ⟨f, hf⟩) + (algebraMap 𝕜 ↥s) a
⊢ ∃ f ∈ ↑s, f x = v x ∧ f y = v y

Tactic:
refine ⟨f', f'.prop, ?_, ?_⟩

Result:
case neg.intro.intro.intro.intro.refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
inst✝¹ : Field 𝕜
inst✝ : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : f x - f y ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
f' : ↥s := ((b - a) * (f x - f y)⁻¹) • ((algebraMap 𝕜 ↥s) (f x) - ⟨f, hf⟩) + (algebraMap 𝕜 ↥s) a
⊢ ↑f' x = v x

case neg.intro.intro.intro.intro.refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
inst✝¹ : Field 𝕜
inst✝ : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : f x - f y ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
f' : ↥s := ((b - a) * (f x - f y)⁻¹) • ((algebraMap 𝕜 ↥s) (f x) - ⟨f, hf⟩) + (algebraMap 𝕜 ↥s) a
⊢ ↑f' y = v y
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem preimage_mul_left_one : preimage 1 (a * ·) (mul_right_injective _).injOn = {a⁻¹}

Proof state:
α : Type u_2
inst✝ : Group α
a : α
⊢ preimage 1 (fun x => a * x) ⋯ = {a⁻¹}

Tactic:
rw [← image_mul_left', image_one, mul_one]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Group α
a : α
⊢ preimage 1 (fun x => a * x) ⋯ = {a⁻¹}

Tactic:
classical rw [← image_mul_left', image_one, mul_one]

Result:
no goals
-- Mathlib/ModelTheory/Order.lean
/-- This is not an instance because it would form a loop with
`FirstOrder.Language.order.instStrongHomClassOfOrderIsoClass`.
As both types are `Prop`s, it would only cause a slowdown. -/
lemma StrongHomClass.toOrderIsoClass
    (L : Language) [L.IsOrdered] (M : Type*) [L.Structure M] [LE M] [L.OrderedStructure M]
    (N : Type*) [L.Structure N] [LE N] [L.OrderedStructure N]
    (F : Type*) [EquivLike F M N] [L.StrongHomClass F M N] :
    OrderIsoClass F M N where
  map_le_map_iff f a b

Proof state:
L : Language
inst✝⁸ : L.IsOrdered
M : Type u_1
inst✝⁷ : L.Structure M
inst✝⁶ : LE M
inst✝⁵ : L.OrderedStructure M
N : Type u_2
inst✝⁴ : L.Structure N
inst✝³ : LE N
inst✝² : L.OrderedStructure N
F : Type u_3
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
f : F
a b : M
⊢ f a ≤ f b ↔ a ≤ b

Tactic:
have h := StrongHomClass.map_rel f leSymb ![a,b]

Result:
L : Language
inst✝⁸ : L.IsOrdered
M : Type u_1
inst✝⁷ : L.Structure M
inst✝⁶ : LE M
inst✝⁵ : L.OrderedStructure M
N : Type u_2
inst✝⁴ : L.Structure N
inst✝³ : LE N
inst✝² : L.OrderedStructure N
F : Type u_3
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
f : F
a b : M
h : RelMap leSymb (⇑f ∘ ![a, b]) ↔ RelMap leSymb ![a, b]
⊢ f a ≤ f b ↔ a ≤ b

Proof state:
L : Language
inst✝⁸ : L.IsOrdered
M : Type u_1
inst✝⁷ : L.Structure M
inst✝⁶ : LE M
inst✝⁵ : L.OrderedStructure M
N : Type u_2
inst✝⁴ : L.Structure N
inst✝³ : LE N
inst✝² : L.OrderedStructure N
F : Type u_3
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
f : F
a b : M
h : f a ≤ f b ↔ a ≤ b
⊢ f a ≤ f b ↔ a ≤ b

Tactic:
exact h

Result:
no goals

Proof state:
L : Language
inst✝⁸ : L.IsOrdered
M : Type u_1
inst✝⁷ : L.Structure M
inst✝⁶ : LE M
inst✝⁵ : L.OrderedStructure M
N : Type u_2
inst✝⁴ : L.Structure N
inst✝³ : LE N
inst✝² : L.OrderedStructure N
F : Type u_3
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
f : F
a b : M
h : RelMap leSymb (⇑f ∘ ![a, b]) ↔ RelMap leSymb ![a, b]
⊢ f a ≤ f b ↔ a ≤ b

Tactic:
simp only [relMap_leSymb, Fin.isValue, Function.comp_apply, Matrix.cons_val_zero,
  Matrix.cons_val_one, Matrix.head_cons] at h

Result:
L : Language
inst✝⁸ : L.IsOrdered
M : Type u_1
inst✝⁷ : L.Structure M
inst✝⁶ : LE M
inst✝⁵ : L.OrderedStructure M
N : Type u_2
inst✝⁴ : L.Structure N
inst✝³ : LE N
inst✝² : L.OrderedStructure N
F : Type u_3
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
f : F
a b : M
h : f a ≤ f b ↔ a ≤ b
⊢ f a ≤ f b ↔ a ≤ b
-- Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean
@[reassoc, to_app]
lemma mapComp_id_right_hom (f : a ⟶ b) : (F.mapComp f (𝟙 b)).hom =
    F.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b).inv

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : Pseudofunctor B C
a b : B
f : a ⟶ b
⊢ (F.mapComp f (𝟙 b)).hom = F.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b).inv

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Directed.lean
/-- If `f` is monotone and antitone on a directed set `s`, then `f` is constant on `s`. -/
lemma constant_of_monotoneOn_antitoneOn (hf : MonotoneOn f s) (hf' : AntitoneOn f s)
    (hs : DirectedOn (· ≤ ·) s) : ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → f a = f b

Proof state:
α : Type u
β : Type v
inst✝¹ : PartialOrder β
inst✝ : Preorder α
f : α → β
s : Set α
hf : MonotoneOn f s
hf' : AntitoneOn f s
hs : DirectedOn (fun x1 x2 => x1 ≤ x2) s
⊢ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → f a = f b

Tactic:
rintro a ha b hb

Result:
α : Type u
β : Type v
inst✝¹ : PartialOrder β
inst✝ : Preorder α
f : α → β
s : Set α
hf : MonotoneOn f s
hf' : AntitoneOn f s
hs : DirectedOn (fun x1 x2 => x1 ≤ x2) s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ f a = f b

Proof state:
case intro.intro.intro
α : Type u
β : Type v
inst✝¹ : PartialOrder β
inst✝ : Preorder α
f : α → β
s : Set α
hf : MonotoneOn f s
hf' : AntitoneOn f s
hs : DirectedOn (fun x1 x2 => x1 ≤ x2) s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hac : a ≤ c
hbc : b ≤ c
⊢ f a = f b

Tactic:
exact le_antisymm ((hf ha hc hac).trans <| hf' hb hc hbc) ((hf hb hc hbc).trans <| hf' ha hc hac)

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : PartialOrder β
inst✝ : Preorder α
f : α → β
s : Set α
hf : MonotoneOn f s
hf' : AntitoneOn f s
hs : DirectedOn (fun x1 x2 => x1 ≤ x2) s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ f a = f b

Tactic:
obtain ⟨c, hc, hac, hbc⟩ := hs _ ha _ hb

Result:
case intro.intro.intro
α : Type u
β : Type v
inst✝¹ : PartialOrder β
inst✝ : Preorder α
f : α → β
s : Set α
hf : MonotoneOn f s
hf' : AntitoneOn f s
hs : DirectedOn (fun x1 x2 => x1 ≤ x2) s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hac : a ≤ c
hbc : b ≤ c
⊢ f a = f b
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem eq_of_edist_zero_on {f f' : α → E} {s : Set α} (h : ∀ ⦃x⦄, x ∈ s → edist (f x) (f' x) = 0) :
    eVariationOn f s = eVariationOn f' s

Proof state:
case e_s.h.e_f.h
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f f' : α → E
s : Set α
h : ∀ ⦃x : α⦄, x ∈ s → edist (f x) (f' x) = 0
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
i : ℕ
⊢ edist (f (↑p.2 (i + 1))) (f (↑p.2 i)) = edist (f' (↑p.2 (i + 1))) (f' (↑p.2 i))

Tactic:
rw [edist_congr_right (h <| p.snd.prop.2 (i + 1)), edist_congr_left (h <| p.snd.prop.2 i)]

Result:
no goals

Proof state:
case e_s.h
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f f' : α → E
s : Set α
h : ∀ ⦃x : α⦄, x ∈ s → edist (f x) (f' x) = 0
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
⊢ ∑ i ∈ Finset.range p.1, edist (f (↑p.2 (i + 1))) (f (↑p.2 i)) =
    ∑ i ∈ Finset.range p.1, edist (f' (↑p.2 (i + 1))) (f' (↑p.2 i))

Tactic:
congr 1 with i : 1

Result:
case e_s.h.e_f.h
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f f' : α → E
s : Set α
h : ∀ ⦃x : α⦄, x ∈ s → edist (f x) (f' x) = 0
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
i : ℕ
⊢ edist (f (↑p.2 (i + 1))) (f (↑p.2 i)) = edist (f' (↑p.2 (i + 1))) (f' (↑p.2 i))

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f f' : α → E
s : Set α
h : ∀ ⦃x : α⦄, x ∈ s → edist (f x) (f' x) = 0
⊢ ⨆ p, ∑ i ∈ Finset.range p.1, edist (f (↑p.2 (i + 1))) (f (↑p.2 i)) =
    ⨆ p, ∑ i ∈ Finset.range p.1, edist (f' (↑p.2 (i + 1))) (f' (↑p.2 i))

Tactic:
congr 1 with p : 1

Result:
case e_s.h
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f f' : α → E
s : Set α
h : ∀ ⦃x : α⦄, x ∈ s → edist (f x) (f' x) = 0
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
⊢ ∑ i ∈ Finset.range p.1, edist (f (↑p.2 (i + 1))) (f (↑p.2 i)) =
    ∑ i ∈ Finset.range p.1, edist (f' (↑p.2 (i + 1))) (f' (↑p.2 i))

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f f' : α → E
s : Set α
h : ∀ ⦃x : α⦄, x ∈ s → edist (f x) (f' x) = 0
⊢ eVariationOn f s = eVariationOn f' s

Tactic:
dsimp only [eVariationOn]

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f f' : α → E
s : Set α
h : ∀ ⦃x : α⦄, x ∈ s → edist (f x) (f' x) = 0
⊢ ⨆ p, ∑ i ∈ Finset.range p.1, edist (f (↑p.2 (i + 1))) (f (↑p.2 i)) =
    ⨆ p, ∑ i ∈ Finset.range p.1, edist (f' (↑p.2 (i + 1))) (f' (↑p.2 i))
-- Mathlib/MeasureTheory/Integral/TorusIntegral.lean
theorem function_integrable [NormedSpace ℂ E] (hf : TorusIntegrable f c R) :
    IntegrableOn (fun θ : ℝⁿ => (∏ i, R i * exp (θ i * I) * I : ℂ) • f (torusMap c R θ))
      (Icc (0 : ℝⁿ) fun _ => 2 * π) volume

Proof state:
case refine_2
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst✝ : NormedSpace ℂ E
hf : TorusIntegrable f c R
⊢ ∀ᵐ (a : Fin n → ℝ) ∂volume.restrict (Icc 0 fun x => 2 * π),
    ‖(∏ i : Fin n, ↑(R i) * cexp (↑(a i) * I) * I) • f (torusMap c R a)‖ ≤ (∏ i : Fin n, |R i|) * ‖f (torusMap c R a)‖

Tactic:
simp [norm_smul, map_prod]

Result:
no goals

Proof state:
case refine_1
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst✝ : NormedSpace ℂ E
hf : TorusIntegrable f c R
⊢ AEStronglyMeasurable (fun θ => (∏ i : Fin n, ↑(R i) * cexp (↑(θ i) * I) * I) • f (torusMap c R θ))
    (volume.restrict (Icc 0 fun x => 2 * π))

Tactic:
refine (Continuous.aestronglyMeasurable ?_).smul hf.1

Result:
case refine_1
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst✝ : NormedSpace ℂ E
hf : TorusIntegrable f c R
⊢ Continuous fun θ => ∏ i : Fin n, ↑(R i) * cexp (↑(θ i) * I) * I

Proof state:
case refine_1
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst✝ : NormedSpace ℂ E
hf : TorusIntegrable f c R
⊢ Continuous fun θ => ∏ i : Fin n, ↑(R i) * cexp (↑(θ i) * I) * I

Tactic:
fun_prop

Result:
no goals

Proof state:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst✝ : NormedSpace ℂ E
hf : TorusIntegrable f c R
⊢ IntegrableOn (fun θ => (∏ i : Fin n, ↑(R i) * cexp (↑(θ i) * I) * I) • f (torusMap c R θ)) (Icc 0 fun x => 2 * π)
    volume

Tactic:
refine (hf.norm.const_mul (∏ i, |R i|)).mono' ?_ ?_

Result:
case refine_1
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst✝ : NormedSpace ℂ E
hf : TorusIntegrable f c R
⊢ AEStronglyMeasurable (fun θ => (∏ i : Fin n, ↑(R i) * cexp (↑(θ i) * I) * I) • f (torusMap c R θ))
    (volume.restrict (Icc 0 fun x => 2 * π))

case refine_2
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst✝ : NormedSpace ℂ E
hf : TorusIntegrable f c R
⊢ ∀ᵐ (a : Fin n → ℝ) ∂volume.restrict (Icc 0 fun x => 2 * π),
    ‖(∏ i : Fin n, ↑(R i) * cexp (↑(a i) * I) * I) • f (torusMap c R a)‖ ≤ (∏ i : Fin n, |R i|) * ‖f (torusMap c R a)‖
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_eq_singleton_iff {f : α → β} {l : Array α} {b : β} :
    map f l = #[b] ↔ ∃ a, l = #[a] ∧ f a = b

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
b : β
toList✝ : List α
⊢ map f { toList := toList✝ } = #[b] ↔ ∃ a, { toList := toList✝ } = #[a] ∧ f a = b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Array α
b : β
⊢ map f l = #[b] ↔ ∃ a, l = #[a] ∧ f a = b

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
b : β
toList✝ : List α
⊢ map f { toList := toList✝ } = #[b] ↔ ∃ a, { toList := toList✝ } = #[a] ∧ f a = b
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffOn_infty_iff_fderivWithin (hs : UniqueDiffOn 𝕜 s) :
    ContDiffOn 𝕜 ∞ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ∞ (fderivWithin 𝕜 f s) s

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
hs : UniqueDiffOn 𝕜 s
⊢ DifferentiableOn 𝕜 f s ∧ (∞ = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 ∞ (fderivWithin 𝕜 f s) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (∞ + 1) (fderivWithin 𝕜 f s) s

Tactic:
simp

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
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 ∞ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ∞ (fderivWithin 𝕜 f s) s

Tactic:
rw [← ENat.coe_top_add_one, contDiffOn_succ_iff_fderivWithin hs]

Result:
𝕜 : 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
hs : UniqueDiffOn 𝕜 s
⊢ DifferentiableOn 𝕜 f s ∧ (∞ = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 ∞ (fderivWithin 𝕜 f s) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (∞ + 1) (fderivWithin 𝕜 f s) s
-- Mathlib/MeasureTheory/Measure/AddContent.lean
/-- An `addContent C` on a `SetSemiring C` is monotone. -/
lemma addContent_mono (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C)
    (hst : s ⊆ t) :
    m s ≤ m t

Proof state:
case refine_2
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ (↑{s}).PairwiseDisjoint id

Tactic:
simp only [coe_singleton, pairwiseDisjoint_singleton]

Result:
no goals

Proof state:
case refine_4
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
h : ∑ u ∈ {s}, m u ≤ m t
⊢ m s ≤ m t

Tactic:
simpa only [sum_singleton] using h

Result:
no goals

Proof state:
case refine_3
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ∀ s_1 ∈ {s}, s_1 ⊆ t

Tactic:
simp [hst]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ↑{s} ⊆ C

Tactic:
rwa [singleton_subset_set_iff]

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ m s ≤ m t

Tactic:
have h := sum_addContent_le_of_subset (m := m) hC (I := {s}) ?_ ?_ ht ?_

Result:
case refine_4
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
h : ∑ u ∈ {s}, m u ≤ m t
⊢ m s ≤ m t

case refine_1
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ↑{s} ⊆ C

case refine_2
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ (↑{s}).PairwiseDisjoint id

case refine_3
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ∀ s_1 ∈ {s}, s_1 ⊆ t
-- Mathlib/Data/Finite/Prod.lean
theorem Finite.toFinset_prod {s : Set α} {t : Set β} (hs : s.Finite) (ht : t.Finite) :
    hs.toFinset ×ˢ ht.toFinset = (hs.prod ht).toFinset :=
  Finset.ext <| by simp

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
⊢ ∀ (a : α × β), a ∈ hs.toFinset ×ˢ ht.toFinset ↔ a ∈ ⋯.toFinset

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
lemma domain_eq (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] : p.obj a = R

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ p.obj a = R

Tactic:
subst_hom_lift p f φ

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsHomLift (p.map φ) φ
⊢ p.obj a✝ = p.obj a✝

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsHomLift (p.map φ) φ
⊢ p.obj a✝ = p.obj a✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/TietzeExtension.lean
theorem TietzeExtension.of_homeo {Y : Type v} {Z : Type w} [TopologicalSpace Y]
    [TopologicalSpace Z] [TietzeExtension.{u, w} Z] (e : Y ≃ₜ Z) :
    TietzeExtension.{u, v} Y :=
  .of_retract (e : C(Y, Z)) (e.symm : C(Z, Y)) <| by simp

Proof state:
Y : Type v
Z : Type w
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TietzeExtension Z
e : Y ≃ₜ Z
⊢ (↑e.symm).comp ↑e = ContinuousMap.id Y

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Factors.lean
theorem prime_of_mem_primeFactorsList {n : ℕ} : ∀ {p : ℕ}, p ∈ primeFactorsList n → Prime p

Proof state:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : p = m ∨ p ∈ ((k + 2) / m).primeFactorsList
⊢ Prime p

Tactic:
exact Or.casesOn h₁ (fun h₂ => h₂.symm ▸ minFac_prime (by simp)) prime_of_mem_primeFactorsList

Result:
no goals

Proof state:
n k : ℕ
⊢ ∀ {p : ℕ}, p ∈ (k + 2).primeFactorsList → Prime p

Tactic:
intro p h

Result:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
⊢ Prime p

Proof state:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : p = m ∨ p ∈ ((k + 2) / m).primeFactorsList
h₂ : p = m
⊢ k + 2 ≠ 1

Tactic:
simp

Result:
no goals

Proof state:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ p ∈ m :: ((k + 2) / m).primeFactorsList

Tactic:
rwa [primeFactorsList] at h

Result:
no goals

Proof state:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
⊢ Prime p

Tactic:
have : (k + 2) / m < (k + 2) := factors_lemma

Result:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ Prime p

Proof state:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ Prime p

Tactic:
have h₁ : p = m ∨ p ∈ primeFactorsList ((k + 2) / m) :=
  List.mem_cons.1 (by rwa [primeFactorsList] at h)

Result:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : p = m ∨ p ∈ ((k + 2) / m).primeFactorsList
⊢ Prime p

Proof state:
n : ℕ
⊢ ∀ {p : ℕ}, p ∈ n.primeFactorsList → Prime p

Tactic:
match n with
| 0 => simp
| 1 => simp
| k + 2 =>
    intro p h
    let m := minFac (k + 2)
    have : (k + 2) / m < (k + 2) := factors_lemma
    have h₁ : p = m ∨ p ∈ primeFactorsList ((k + 2) / m) :=
      List.mem_cons.1 (by rwa [primeFactorsList] at h)
    exact Or.casesOn h₁ (fun h₂ => h₂.symm ▸ minFac_prime (by simp)) prime_of_mem_primeFactorsList

Result:
no goals

Proof state:
n : ℕ
⊢ ∀ {p : ℕ}, p ∈ primeFactorsList 0 → Prime p

Tactic:
simp

Result:
no goals

Proof state:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
⊢ Prime p

Tactic:
let m := minFac (k + 2)

Result:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
⊢ Prime p

Proof state:
n : ℕ
⊢ ∀ {p : ℕ}, p ∈ primeFactorsList 1 → Prime p

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/IsConnected.lean
theorem constant_of_preserves_morphisms [IsPreconnected J] {α : Type u₂} (F : J → α)
    (h : ∀ (j₁ j₂ : J) (_ : j₁ ⟶ j₂), F j₁ = F j₂) (j j' : J) : F j = F j'

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → F j₁ = F j₂
j j' : J
⊢ F j = F j'

Tactic:
simpa using
  any_functor_const_on_obj
    { obj := Discrete.mk ∘ F
      map := fun f => eqToHom (by ext; exact h _ _ f) }
    j j'

Result:
no goals

Proof state:
case as
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → F j₁ = F j₂
j j' X✝ Y✝ : J
f : X✝ ⟶ Y✝
⊢ ((Discrete.mk ∘ F) X✝).as = ((Discrete.mk ∘ F) Y✝).as

Tactic:
exact h _ _ f

Result:
no goals

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → F j₁ = F j₂
j j' X✝ Y✝ : J
f : X✝ ⟶ Y✝
⊢ (Discrete.mk ∘ F) X✝ = (Discrete.mk ∘ F) Y✝

Tactic:
ext

Result:
case as
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → F j₁ = F j₂
j j' X✝ Y✝ : J
f : X✝ ⟶ Y✝
⊢ ((Discrete.mk ∘ F) X✝).as = ((Discrete.mk ∘ F) Y✝).as
-- Mathlib/Data/List/Basic.lean
theorem idxOf_get [DecidableEq α] {a : α} {l : List α} (h) : get l ⟨idxOf a l, h⟩ = a

Proof state:
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
h : idxOf a l < l.length
⊢ l.get ⟨idxOf a l, h⟩ = a

Tactic:
simp

Result:
no goals