harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/TypeVec.lean
theorem toSubtype_of_subtype {α : TypeVec n} (p : α ⟹ «repeat» n Prop) :
    toSubtype p ⊚ ofSubtype p = id

Proof state:
n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
⊢ toSubtype p ⊚ ofSubtype p = id

Tactic:
ext i x

Result:
case a.h
n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
i : Fin2 n
x : Subtype_ p i
⊢ (toSubtype p ⊚ ofSubtype p) i x = id i x

Proof state:
case a.h
n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
i : Fin2 n
x : Subtype_ p i
⊢ (toSubtype p ⊚ ofSubtype p) i x = id i x

Tactic:
induction i <;> simp only [id, toSubtype, comp, ofSubtype] at *

Result:
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec.{u_1} n✝} (p : α ⟹ «repeat» n✝ Prop) (x : Subtype_ p a✝), toSubtype p a✝ (ofSubtype p a✝ x) = x
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ p a✝.fs
⊢ toSubtype (dropFun p) a✝ (ofSubtype (dropFun p) a✝ x) = x

Proof state:
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec.{u_1} n✝} (p : α ⟹ «repeat» n✝ Prop) (x : Subtype_ p a✝), toSubtype p a✝ (ofSubtype p a✝ x) = x
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ p a✝.fs
⊢ toSubtype (dropFun p) a✝ (ofSubtype (dropFun p) a✝ x) = x

Tactic:
simp [*]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Subcanonical.lean
/-- See also `yonedaEquiv_naturality'` for a more general version. -/
lemma yonedaULiftEquiv_naturality {X Y : C} {F : Sheaf J (Type (max v v'))}
    (f : J.yonedaULift.obj X ⟶ F) (g : Y ⟶ X) :
      F.val.map g.op (J.yonedaULiftEquiv f) = J.yonedaULiftEquiv (J.yonedaULift.map g ≫ f)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type (max v v'))
f : (yonedaULift.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
⊢ F.val.map g.op (J.yonedaULiftEquiv f) = J.yonedaULiftEquiv ((yonedaULift.{v', v, u} J).map g ≫ f)

Tactic:
change (f.val.app (op X) ≫ F.val.map g.op) ⟨𝟙 X⟩ = f.val.app (op Y) ⟨𝟙 Y ≫ g⟩

Result:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type (max v v'))
f : (yonedaULift.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
⊢ (f.val.app (op X) ≫ F.val.map g.op) { down := 𝟙 X } = f.val.app (op Y) { down := 𝟙 Y ≫ g }

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type (max v v'))
f : (yonedaULift.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
⊢ (f.val.app (op X) ≫ F.val.map g.op) { down := 𝟙 X } = f.val.app (op Y) { down := 𝟙 Y ≫ g }

Tactic:
rw [← f.val.naturality]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type (max v v'))
f : (yonedaULift.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
⊢ (((yonedaULift.{v', v, u} J).obj X).val.map g.op ≫ f.val.app (op Y)) { down := 𝟙 X } =
    f.val.app (op Y) { down := 𝟙 Y ≫ g }

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type (max v v'))
f : (yonedaULift.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
⊢ (((yonedaULift.{v', v, u} J).obj X).val.map g.op ≫ f.val.app (op Y)) { down := 𝟙 X } =
    f.val.app (op Y) { down := 𝟙 Y ≫ g }

Tactic:
simp [yonedaULift]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
lemma measurableSet_eq_fun (hf : StronglyMeasurable[m] f) (hg : StronglyMeasurable[m] g) :
    MeasurableSet[m] {a | f a = g a}

Proof state:
α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ MeasurableSet {a | f a = g a}

Tactic:
borelize (E × E)

Result:
α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace (E × E) := borel (E × E)
this✝ : BorelSpace (E × E)
⊢ MeasurableSet {a | f a = g a}

Proof state:
α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace (E × E) := borel (E × E)
this✝ : BorelSpace (E × E)
⊢ MeasurableSet {a | f a = g a}

Tactic:
exact (hf.prod_mk hg).measurable isClosed_diagonal.measurableSet

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_atTop_zero [Nonempty β] [SemilatticeSup β] {f : β → ℝ≥0∞} :
    Tendsto f atTop (𝓝 0) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε :=
  .trans (atTop_basis.tendsto_iff nhds_zero_basis_Iic) (by simp only [true_and]; rfl)

Proof state:
β : Type u_2
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, True ∧ ∀ x ∈ Ici ia, f x ∈ Iic ib) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε

Tactic:
simp only [true_and]

Result:
β : Type u_2
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, ∀ x ∈ Ici ia, f x ∈ Iic ib) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε

Proof state:
β : Type u_2
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, ∀ x ∈ Ici ia, f x ∈ Iic ib) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Filter/CountableSeparatingOn.lean
theorem exists_singleton_mem_of_mem_of_forall_separating [Nonempty α] (p : Set α → Prop)
    {s : Set α} [HasCountableSeparatingOn α p s] (hs : s ∈ l) (hl : ∀ U, p U → U ∈ l ∨ Uᶜ ∈ l) :
    ∃ a, {a} ∈ l

Proof state:
α : Type u_1
l : Filter α
inst✝² : CountableInterFilter l
inst✝¹ : Nonempty α
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
⊢ ∃ a, {a} ∈ l

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hne

Result:
case inl
α : Type u_1
l : Filter α
inst✝² : CountableInterFilter l
inst✝¹ : Nonempty α
p : Set α → Prop
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
inst✝ : HasCountableSeparatingOn α p ∅
hs : ∅ ∈ l
⊢ ∃ a, {a} ∈ l

case inr
α : Type u_1
l : Filter α
inst✝² : CountableInterFilter l
inst✝¹ : Nonempty α
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
hne : s.Nonempty
⊢ ∃ a, {a} ∈ l

Proof state:
case inl
α : Type u_1
l : Filter α
inst✝² : CountableInterFilter l
inst✝¹ : Nonempty α
p : Set α → Prop
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
inst✝ : HasCountableSeparatingOn α p ∅
hs : ∅ ∈ l
⊢ ∃ a, {a} ∈ l

Tactic:
exact ‹Nonempty α›.elim fun a ↦ ⟨a, mem_of_superset hs (empty_subset _)⟩

Result:
no goals

Proof state:
case inr
α : Type u_1
l : Filter α
inst✝² : CountableInterFilter l
inst✝¹ : Nonempty α
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
hne : s.Nonempty
⊢ ∃ a, {a} ∈ l

Tactic:
exact (exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating p hs hne hl).imp fun _ ↦
  And.right

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Classes/SatisfiesM.lean
theorem SatisfiesM_ReaderT_eq [Monad m] :
    SatisfiesM (m := ReaderT ρ m) p x ↔ ∀ s, SatisfiesM p (x.run s) :=
  (exists_congr fun a => by exact ⟨fun eq _ => eq ▸ rfl, funext⟩).trans Classical.skolem.symm

Proof state:
m : Type u_1 → Type u_2
ρ α✝ : Type u_1
p : α✝ → Prop
x : ReaderT ρ m α✝
inst✝ : Monad m
a : ReaderT ρ m { a // p a }
⊢ Subtype.val <$> a = x ↔ ∀ (x_1 : ρ), Subtype.val <$> a x_1 = x.run x_1

Tactic:
exact ⟨fun eq _ => eq ▸ rfl, funext⟩

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem IsSt.lt {x y : ℝ*} {r s : ℝ} (hxr : IsSt x r) (hys : IsSt y s) (hrs : r < s) :
    x < y

Proof state:
case intro
y : ℝ*
r s : ℝ
hys : y.IsSt s
hrs : r < s
f : ℕ → ℝ
hxr : (ofSeq f).IsSt r
⊢ ofSeq f < y

Tactic:
rcases ofSeq_surjective y with ⟨g, rfl⟩

Result:
case intro.intro
r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : (ofSeq f).IsSt r
g : ℕ → ℝ
hys : (ofSeq g).IsSt s
⊢ ofSeq f < ofSeq g

Proof state:
case intro.intro
r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : (ofSeq f).IsSt r
g : ℕ → ℝ
hys : (ofSeq g).IsSt s
⊢ ofSeq f < ofSeq g

Tactic:
rw [isSt_ofSeq_iff_tendsto] at hxr hys

Result:
case intro.intro
r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)
g : ℕ → ℝ
hys : Tendsto g (↑(hyperfilter ℕ)) (𝓝 s)
⊢ ofSeq f < ofSeq g

Proof state:
case intro.intro
r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)
g : ℕ → ℝ
hys : Tendsto g (↑(hyperfilter ℕ)) (𝓝 s)
⊢ ofSeq f < ofSeq g

Tactic:
exact ofSeq_lt_ofSeq.2 <| hxr.eventually_lt hys hrs

Result:
no goals

Proof state:
x y : ℝ*
r s : ℝ
hxr : x.IsSt r
hys : y.IsSt s
hrs : r < s
⊢ x < y

Tactic:
rcases ofSeq_surjective x with ⟨f, rfl⟩

Result:
case intro
y : ℝ*
r s : ℝ
hys : y.IsSt s
hrs : r < s
f : ℕ → ℝ
hxr : (ofSeq f).IsSt r
⊢ ofSeq f < y
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma one_lt_ofENat {m : ℕ∞} : 1 < (m : Cardinal) ↔ 1 < m

Proof state:
m : ℕ∞
⊢ 1 < ↑m ↔ 1 < m

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem bihimp_top : a ⇔ ⊤ = a

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a : α
⊢ a ⇔ ⊤ = a

Tactic:
rw [bihimp, himp_top, top_himp, inf_top_eq]

Result:
no goals
-- Mathlib/Analysis/Analytic/Inverse.lean
theorem rightInv_coeff_one (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) :
    p.rightInv i x 1 = (continuousMultilinearCurryFin1 𝕜 F E).symm i.symm

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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
⊢ p.rightInv i x 1 = (continuousMultilinearCurryFin1 𝕜 F E).symm ↑i.symm

Tactic:
rw [rightInv]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem ofMul_multiset_prod (s : Multiset α) : ofMul s.prod = (s.map ofMul).sum

Proof state:
α : Type u_3
inst✝ : CommMonoid α
s : Multiset α
⊢ s.prod = s.sum

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_3
inst✝ : CommMonoid α
s : Multiset α
⊢ ofMul s.prod = (Multiset.map (⇑ofMul) s).sum

Tactic:
simp [ofMul]

Result:
α : Type u_3
inst✝ : CommMonoid α
s : Multiset α
⊢ s.prod = s.sum
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean
@[reassoc (attr := simp)]
lemma comp_add' (f : L.obj X ⟶ L.obj Y) (g₁ g₂ : L.obj Y ⟶ L.obj Z) :
    f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
⊢ f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)

Tactic:
obtain ⟨α, hα⟩ := exists_leftFraction L W f

Result:
case intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
α : W.LeftFraction X Y
hα : f = α.map L ⋯
⊢ f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)

Proof state:
case intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
α : W.LeftFraction X Y
hα : f = α.map L ⋯
β : W.LeftFraction₂ Y Z
hβ₁ : g₁ = β.fst.map L ⋯
hβ₂ : g₂ = β.snd.map L ⋯
γ : W.LeftFraction₂ α.Y' β.Y'
hγ₁ : (RightFraction₂.mk α.s ⋯ β.f β.f').f ≫ γ.s = (RightFraction₂.mk α.s ⋯ β.f β.f').s ≫ γ.f
hγ₂ : (RightFraction₂.mk α.s ⋯ β.f β.f').f' ≫ γ.s = (RightFraction₂.mk α.s ⋯ β.f β.f').s ≫ γ.f'
⊢ f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)

Tactic:
dsimp at hγ₁ hγ₂

Result:
case intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
α : W.LeftFraction X Y
hα : f = α.map L ⋯
β : W.LeftFraction₂ Y Z
hβ₁ : g₁ = β.fst.map L ⋯
hβ₂ : g₂ = β.snd.map L ⋯
γ : W.LeftFraction₂ α.Y' β.Y'
hγ₁ : β.f ≫ γ.s = α.s ≫ γ.f
hγ₂ : β.f' ≫ γ.s = α.s ≫ γ.f'
⊢ f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
α : W.LeftFraction X Y
hα : f = α.map L ⋯
β : W.LeftFraction₂ Y Z
hβ₁ : g₁ = β.fst.map L ⋯
hβ₂ : g₂ = β.snd.map L ⋯
γ : W.LeftFraction₂ α.Y' β.Y'
hγ₁ : β.f ≫ γ.s = α.s ≫ γ.f
hγ₂ : β.f' ≫ γ.s = α.s ≫ γ.f'
⊢ f ≫ g₁ = (LeftFraction₂.mk (α.f ≫ γ.f) (α.f ≫ γ.f') (β.s ≫ γ.s) ⋯).fst.map L ⋯

Tactic:
simpa only [hα, hβ₁] using LeftFraction.map_comp_map_eq_map α β.fst γ.fst hγ₁ L

Result:
no goals
-- Mathlib/Topology/UniformSpace/Completion.lean
theorem inseparable_iff_of_le_nhds {f g : CauchyFilter α} {a b : α}
    (ha : f.1 ≤ 𝓝 a) (hb : g.1 ≤ 𝓝 b) : Inseparable a b ↔ Inseparable f g

Proof state:
α : Type u
inst✝ : UniformSpace α
f g : CauchyFilter α
a b : α
ha : ↑f ≤ 𝓝 a
hb : ↑g ≤ 𝓝 b
⊢ Inseparable a b ↔ Inseparable f g

Tactic:
rw [← tendsto_id'] at ha hb

Result:
α : Type u
inst✝ : UniformSpace α
f g : CauchyFilter α
a b : α
ha : Tendsto id (↑f) (𝓝 a)
hb : Tendsto id (↑g) (𝓝 b)
⊢ Inseparable a b ↔ Inseparable f g

Proof state:
α : Type u
inst✝ : UniformSpace α
f g : CauchyFilter α
a b : α
ha : Tendsto id (↑f) (𝓝 a)
hb : Tendsto id (↑g) (𝓝 b)
⊢ Inseparable a b ↔ Inseparable f g

Tactic:
rw [inseparable_iff, (ha.comp tendsto_fst).inseparable_iff_uniformity (hb.comp tendsto_snd)]

Result:
α : Type u
inst✝ : UniformSpace α
f g : CauchyFilter α
a b : α
ha : Tendsto id (↑f) (𝓝 a)
hb : Tendsto id (↑g) (𝓝 b)
⊢ Tendsto (fun x => ((id ∘ Prod.fst) x, (id ∘ Prod.snd) x)) (↑f ×ˢ ↑g) (𝓤 α) ↔ ↑f ×ˢ ↑g ≤ 𝓤 α

Proof state:
α : Type u
inst✝ : UniformSpace α
f g : CauchyFilter α
a b : α
ha : Tendsto id (↑f) (𝓝 a)
hb : Tendsto id (↑g) (𝓝 b)
⊢ Tendsto (fun x => ((id ∘ Prod.fst) x, (id ∘ Prod.snd) x)) (↑f ×ˢ ↑g) (𝓤 α) ↔ ↑f ×ˢ ↑g ≤ 𝓤 α

Tactic:
simp only [Function.comp_apply, id_eq, Prod.mk.eta, ← Function.id_def, tendsto_id']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem find?_subtype {p : α → Prop} {l : Array { x // p x }}
    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    (l.find? f).map Subtype.val = l.unattach.find? g

Proof state:
case mk.cons
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
head✝ : { x // p x }
tail✝ : List { x // p x }
⊢ Option.map Subtype.val (Array.find? f { toList := head✝ :: tail✝ }) =
    Array.find? g { toList := head✝ :: tail✝ }.unattach

Tactic:
rw [Array.find?_subtype hf]

Result:
no goals

Proof state:
case mk.nil
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ Option.map Subtype.val (Array.find? f { toList := [] }) = Array.find? g { toList := [] }.unattach

case mk.cons
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
head✝ : { x // p x }
tail✝ : List { x // p x }
⊢ Option.map Subtype.val (Array.find? f { toList := head✝ :: tail✝ }) =
    Array.find? g { toList := head✝ :: tail✝ }.unattach

Tactic:
simp

Result:
case mk.cons
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
head✝ : { x // p x }
tail✝ : List { x // p x }
⊢ Option.map Subtype.val (Array.find? f { toList := head✝ :: tail✝ }) =
    Array.find? g { toList := head✝ :: tail✝ }.unattach

Proof state:
α : Type u_1
p : α → Prop
l : Array { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ Option.map Subtype.val (Array.find? f l) = Array.find? g l.unattach

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk.nil
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ Option.map Subtype.val (Array.find? f { toList := [] }) = Array.find? g { toList := [] }.unattach

case mk.cons
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
head✝ : { x // p x }
tail✝ : List { x // p x }
⊢ Option.map Subtype.val (Array.find? f { toList := head✝ :: tail✝ }) =
    Array.find? g { toList := head✝ :: tail✝ }.unattach
-- Mathlib/Data/Array/ExtractLemmas.lean
theorem extract_append_right {a b : Array α} {i j : Nat} (h : a.size ≤ i) :
    (a ++ b).extract i j = b.extract (i - a.size) (j - a.size)

Proof state:
case h₂
α : Type u
a b : Array α
i j : Nat
h : a.size ≤ i
⊢ ∀ (i_1 : Nat) (hi₁ : i_1 < ((a ++ b).extract i j).size) (hi₂ : i_1 < (b.extract (i - a.size) (j - a.size)).size),
    ((a ++ b).extract i j)[i_1] = (b.extract (i - a.size) (j - a.size))[i_1]

Tactic:
intro k hi h2

Result:
case h₂
α : Type u
a b : Array α
i j : Nat
h : a.size ≤ i
k : Nat
hi : k < ((a ++ b).extract i j).size
h2 : k < (b.extract (i - a.size) (j - a.size)).size
⊢ ((a ++ b).extract i j)[k] = (b.extract (i - a.size) (j - a.size))[k]

Proof state:
α : Type u
a b : Array α
i j : Nat
h : a.size ≤ i
k : Nat
hi : k < ((a ++ b).extract i j).size
h2 : k < (b.extract (i - a.size) (j - a.size)).size
⊢ a.size ≤ i + k

Tactic:
omega

Result:
no goals

Proof state:
case h₁
α : Type u
a b : Array α
i j : Nat
h : a.size ≤ i
⊢ min j (a.size + b.size) - i = min (j - a.size) b.size - (i - a.size)

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
a b : Array α
i j : Nat
h : a.size ≤ i
⊢ (a ++ b).extract i j = b.extract (i - a.size) (j - a.size)

Tactic:
apply ext

Result:
case h₁
α : Type u
a b : Array α
i j : Nat
h : a.size ≤ i
⊢ ((a ++ b).extract i j).size = (b.extract (i - a.size) (j - a.size)).size

case h₂
α : Type u
a b : Array α
i j : Nat
h : a.size ≤ i
⊢ ∀ (i_1 : Nat) (hi₁ : i_1 < ((a ++ b).extract i j).size) (hi₂ : i_1 < (b.extract (i - a.size) (j - a.size)).size),
    ((a ++ b).extract i j)[i_1] = (b.extract (i - a.size) (j - a.size))[i_1]

Proof state:
case h₁
α : Type u
a b : Array α
i j : Nat
h : a.size ≤ i
⊢ ((a ++ b).extract i j).size = (b.extract (i - a.size) (j - a.size)).size

Tactic:
rw [size_extract, size_extract, size_append]

Result:
case h₁
α : Type u
a b : Array α
i j : Nat
h : a.size ≤ i
⊢ min j (a.size + b.size) - i = min (j - a.size) b.size - (i - a.size)

Proof state:
case h₂
α : Type u
a b : Array α
i j : Nat
h : a.size ≤ i
k : Nat
hi : k < ((a ++ b).extract i j).size
h2 : k < (b.extract (i - a.size) (j - a.size)).size
⊢ ((a ++ b).extract i j)[k] = (b.extract (i - a.size) (j - a.size))[k]

Tactic:
rw [getElem_extract, getElem_extract,
  getElem_append_right (show size a ≤ i + k by omega)]

Result:
case h₂
α : Type u
a b : Array α
i j : Nat
h : a.size ≤ i
k : Nat
hi : k < ((a ++ b).extract i j).size
h2 : k < (b.extract (i - a.size) (j - a.size)).size
⊢ b[i + k - a.size] = b[i - a.size + k]

Proof state:
case h₂
α : Type u
a b : Array α
i j : Nat
h : a.size ≤ i
k : Nat
hi : k < ((a ++ b).extract i j).size
h2 : k < (b.extract (i - a.size) (j - a.size)).size
⊢ b[i + k - a.size] = b[i - a.size + k]

Tactic:
congr

Result:
case h₂.e_i
α : Type u
a b : Array α
i j : Nat
h : a.size ≤ i
k : Nat
hi : k < ((a ++ b).extract i j).size
h2 : k < (b.extract (i - a.size) (j - a.size)).size
⊢ i + k - a.size = i - a.size + k

Proof state:
case h₂.e_i
α : Type u
a b : Array α
i j : Nat
h : a.size ≤ i
k : Nat
hi : k < ((a ++ b).extract i j).size
h2 : k < (b.extract (i - a.size) (j - a.size)).size
⊢ i + k - a.size = i - a.size + k

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_eq_foldl (f : α → β) (l : Array α) :
    map f l = foldl (fun bs a => bs.push (f a)) #[] l

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ map f l = foldl (fun bs a => bs.push (f a)) #[] l

Tactic:
simpa using mapM_eq_foldlM (m := Id) f l

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Convex.lean
theorem isBounded_convexHull {s : Set E} :
    Bornology.IsBounded (convexHull ℝ s) ↔ Bornology.IsBounded s

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
⊢ Bornology.IsBounded ((convexHull ℝ) s) ↔ Bornology.IsBounded s

Tactic:
simp only [Metric.isBounded_iff_ediam_ne_top, convexHull_ediam]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Extend.lean
lemma mapX_none {i : Option ι} (hi : i = none) :
    mapX φ i = 0

Proof state:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
i : Option ι
hi : i = none
⊢ mapX φ i = 0

Tactic:
subst hi

Result:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
⊢ mapX φ none = 0

Proof state:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
⊢ mapX φ none = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem cast_eq_val [NeZero n] (a : ZMod n) : (cast a : R) = a.val

Proof state:
case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
inst✝ : NeZero 0
a : ZMod 0
⊢ a.cast = ↑a.val

Tactic:
cases NeZero.ne 0 rfl

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a : ZMod (n✝ + 1)
⊢ a.cast = ↑a.val

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
R : Type u_1
inst✝¹ : AddGroupWithOne R
inst✝ : NeZero n
a : ZMod n
⊢ a.cast = ↑a.val

Tactic:
cases n

Result:
case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
inst✝ : NeZero 0
a : ZMod 0
⊢ a.cast = ↑a.val

case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a : ZMod (n✝ + 1)
⊢ a.cast = ↑a.val
-- Mathlib/Control/Monad/Cont.lean
theorem ext {x y : ContT r m α} (h : ∀ f, x.run f = y.run f) : x = y

Proof state:
case h
r : Type u
m : Type u → Type v
α : Type w
x y : ContT r m α
h : ∀ (f : α → m r), x.run f = y.run f
x✝ : α → m r
⊢ x x✝ = y x✝

Tactic:
apply h

Result:
no goals

Proof state:
r : Type u
m : Type u → Type v
α : Type w
x y : ContT r m α
h : ∀ (f : α → m r), x.run f = y.run f
⊢ x = y

Tactic:
ext

Result:
case h
r : Type u
m : Type u → Type v
α : Type w
x y : ContT r m α
h : ∀ (f : α → m r), x.run f = y.run f
x✝ : α → m r
⊢ x x✝ = y x✝
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem degree_gcd_le_right (p) {q : R[X]} (hq : q ≠ 0) : (gcd p q).degree ≤ q.degree

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
⊢ (gcd q p).degree ≤ q.degree

Tactic:
exact degree_gcd_le_left hq p

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
⊢ (gcd p q).degree ≤ q.degree

Tactic:
rw [gcd_comm]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
⊢ (gcd q p).degree ≤ q.degree