harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem IsPrefix.findSome?_eq_some {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <+: l₂) :
    List.findSome? f l₁ = some b → List.findSome? f l₂ = some b

Proof state:
α : Type u_1
β : Type u_2
b : β
l₁ l₂ : List α
f : α → Option β
h : l₁ <+: l₂
⊢ findSome? f l₁ = some b → findSome? f l₂ = some b

Tactic:
rw [IsPrefix] at h

Result:
α : Type u_1
β : Type u_2
b : β
l₁ l₂ : List α
f : α → Option β
h : ∃ t, l₁ ++ t = l₂
⊢ findSome? f l₁ = some b → findSome? f l₂ = some b

Proof state:
α : Type u_1
β : Type u_2
b : β
l₁ l₂ : List α
f : α → Option β
h : ∃ t, l₁ ++ t = l₂
⊢ findSome? f l₁ = some b → findSome? f l₂ = some b

Tactic:
obtain ⟨t, rfl⟩ := h

Result:
case intro
α : Type u_1
β : Type u_2
b : β
l₁ : List α
f : α → Option β
t : List α
⊢ findSome? f l₁ = some b → findSome? f (l₁ ++ t) = some b

Proof state:
case intro
α : Type u_1
β : Type u_2
b : β
l₁ : List α
f : α → Option β
t : List α
⊢ findSome? f l₁ = some b → findSome? f (l₁ ++ t) = some b

Tactic:
simp +contextual [findSome?_append]

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem shortestPrefixDiff_pos {s : Set (∀ n, E n)} (hs : IsClosed s) (hne : s.Nonempty)
    {x : ∀ n, E n} (hx : x ∉ s) : 0 < shortestPrefixDiff x s

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : s.Nonempty
x : (n : ℕ) → E n
hx : x ∉ s
⊢ 0 < shortestPrefixDiff x s

Tactic:
rcases hne with ⟨y, hy⟩

Result:
case intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x : (n : ℕ) → E n
hx : x ∉ s
y : (n : ℕ) → E n
hy : y ∈ s
⊢ 0 < shortestPrefixDiff x s

Proof state:
case intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
x : (n : ℕ) → E n
hx : x ∉ s
y : (n : ℕ) → E n
hy : y ∈ s
⊢ 0 < shortestPrefixDiff x s

Tactic:
exact (zero_le _).trans_lt (firstDiff_lt_shortestPrefixDiff hs hx hy)

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
/--
If `colim` of shape `J` into an abelian category `C` preserves monomorphisms, then `C` has AB of
shape `J`.
-/
lemma hasExactColimitsOfShape_of_preservesMono [HasColimitsOfShape J C]
    [PreservesMonomorphisms (colim (J := J) (C := C))] : HasExactColimitsOfShape J C where
  preservesFiniteLimits

Proof state:
case inst
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasColimitsOfShape J C
inst✝ : colim.PreservesMonomorphisms
⊢ colim.PreservesHomology

Tactic:
exact preservesHomology_of_preservesMonos_and_cokernels _

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasColimitsOfShape J C
inst✝ : colim.PreservesMonomorphisms
⊢ PreservesFiniteLimits colim

Tactic:
apply (config := { allowSynthFailures := true }) preservesFiniteLimits_of_preservesHomology

Result:
case inst
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasColimitsOfShape J C
inst✝ : colim.PreservesMonomorphisms
⊢ colim.PreservesHomology

case inst
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasColimitsOfShape J C
inst✝ : colim.PreservesMonomorphisms
⊢ colim.Additive

Proof state:
case inst
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasColimitsOfShape J C
inst✝ : colim.PreservesMonomorphisms
⊢ colim.Additive

Tactic:
exact additive_of_preservesBinaryBiproducts _

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem orderTop_le_of_coeff_ne_zero {Γ} [LinearOrder Γ] {x : HahnSeries Γ R}
    {g : Γ} (h : x.coeff g ≠ 0) : x.orderTop ≤ g

Proof state:
R : Type u_3
inst✝¹ : Zero R
Γ : Type u_5
inst✝ : LinearOrder Γ
x : HahnSeries Γ R
g : Γ
h : x.coeff g ≠ 0
⊢ ⋯.min ⋯ ≤ g

Tactic:
exact Set.IsWF.min_le _ _ ((mem_support _ _).2 h)

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : Zero R
Γ : Type u_5
inst✝ : LinearOrder Γ
x : HahnSeries Γ R
g : Γ
h : x.coeff g ≠ 0
⊢ x.orderTop ≤ ↑g

Tactic:
rw [orderTop_of_ne (ne_zero_of_coeff_ne_zero h), WithTop.coe_le_coe]

Result:
R : Type u_3
inst✝¹ : Zero R
Γ : Type u_5
inst✝ : LinearOrder Γ
x : HahnSeries Γ R
g : Γ
h : x.coeff g ≠ 0
⊢ ⋯.min ⋯ ≤ g
-- Mathlib/Analysis/Complex/UpperHalfPlane/Exp.lean
theorem UpperHalfPlane.norm_qParam_lt_one (n : ℕ) [NeZero n] (τ : ℍ) : ‖𝕢 n τ‖ < 1

Proof state:
n : ℕ
inst✝ : NeZero n
τ : ℍ
⊢ 0 < 2 * π * τ.im

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
τ : ℍ
⊢ ‖𝕢 ↑n ↑τ‖ < 1

Tactic:
rw [Periodic.norm_qParam, Real.exp_lt_one_iff, neg_mul, coe_im, neg_mul, neg_div, neg_lt_zero,
  div_pos_iff_of_pos_right (mod_cast Nat.pos_of_ne_zero <| NeZero.ne _)]

Result:
n : ℕ
inst✝ : NeZero n
τ : ℍ
⊢ 0 < 2 * π * τ.im
-- Mathlib/Data/Multiset/AddSub.lean
theorem erase_cons_tail_of_mem (h : a ∈ s) :
    (b ::ₘ s).erase a = b ::ₘ s.erase a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a b : α
h : a ∈ s
⊢ (b ::ₘ s).erase a = b ::ₘ s.erase a

Tactic:
rcases eq_or_ne a b with rfl | hab

Result:
case inl
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ (a ::ₘ s).erase a = a ::ₘ s.erase a

case inr
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a b : α
h : a ∈ s
hab : a ≠ b
⊢ (b ::ₘ s).erase a = b ::ₘ s.erase a

Proof state:
case inl
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ (a ::ₘ s).erase a = a ::ₘ s.erase a

Tactic:
simp [cons_erase h]

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a b : α
h : a ∈ s
hab : a ≠ b
⊢ (b ::ₘ s).erase a = b ::ₘ s.erase a

Tactic:
exact s.erase_cons_tail hab.symm

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
/-- This is a version of `Finset.mem_convexHull` stated without `Finset.centerMass`. -/
lemma Finset.mem_convexHull' {s : Finset E} {x : E} :
    x ∈ convexHull R (s : Set E) ↔
      ∃ w : E → R, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ ∑ y ∈ s, w y • y = x

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
x : E
⊢ x ∈ (convexHull R) ↑s ↔ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ ∑ y ∈ s, w y • y = x

Tactic:
rw [mem_convexHull]

Result:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
x : E
⊢ (∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x) ↔
    ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ ∑ y ∈ s, w y • y = x

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
x : E
w : E → R
hw : ∑ y ∈ s, w y = 1
⊢ s.centerMass w id = x ↔ ∑ y ∈ s, w y • y = x

Tactic:
simp_rw [centerMass_eq_of_sum_1 _ _ hw, id_eq]

Result:
no goals

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
x : E
⊢ (∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x) ↔
    ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ ∑ y ∈ s, w y • y = x

Tactic:
refine exists_congr fun w ↦ and_congr_right' <| and_congr_right fun hw ↦ ?_

Result:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
x : E
w : E → R
hw : ∑ y ∈ s, w y = 1
⊢ s.centerMass w id = x ↔ ∑ y ∈ s, w y • y = x
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem not_continuous_cofiniteTopology_of_symm [Infinite X] [DiscreteTopology X] :
    ¬Continuous (@CofiniteTopology.of (OnePoint X)).symm

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
⊢ ¬Continuous ⇑CofiniteTopology.of.symm

Tactic:
inhabit X

Result:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ¬Continuous ⇑CofiniteTopology.of.symm

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ∃ x, ¬Tendsto (⇑CofiniteTopology.of.symm) (𝓝 x) (𝓝 (CofiniteTopology.of.symm x))

Tactic:
use CofiniteTopology.of ↑(default : X)

Result:
case h
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ¬Tendsto (⇑CofiniteTopology.of.symm) (𝓝 (CofiniteTopology.of ↑default))
      (𝓝 (CofiniteTopology.of.symm (CofiniteTopology.of ↑default)))

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ¬Continuous ⇑CofiniteTopology.of.symm

Tactic:
simp only [continuous_iff_continuousAt, ContinuousAt, not_forall]

Result:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ∃ x, ¬Tendsto (⇑CofiniteTopology.of.symm) (𝓝 x) (𝓝 (CofiniteTopology.of.symm x))

Proof state:
case h
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ¬Tendsto (⇑CofiniteTopology.of.symm) (𝓝 (CofiniteTopology.of ↑default))
      (𝓝 (CofiniteTopology.of.symm (CofiniteTopology.of ↑default)))

Tactic:
simpa [nhds_coe_eq, nhds_discrete, CofiniteTopology.nhds_eq] using
  (finite_singleton ((default : X) : OnePoint X)).infinite_compl

Result:
no goals
-- Mathlib/Probability/ConditionalProbability.lean
lemma cond_pos_of_inter_ne_zero [IsFiniteMeasure μ] (hms : MeasurableSet s) (hci : μ (s ∩ t) ≠ 0) :
    0 < μ[t | s]

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hci : μ (s ∩ t) ≠ 0
⊢ 0 < μ[t | s]

Tactic:
rw [cond_apply hms]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hci : μ (s ∩ t) ≠ 0
⊢ 0 < (μ s)⁻¹ * μ (s ∩ t)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hci : μ (s ∩ t) ≠ 0
⊢ (μ s)⁻¹ ≠ 0

Tactic:
exact ENNReal.inv_ne_zero.mpr (measure_ne_top _ _)

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hci : μ (s ∩ t) ≠ 0
⊢ 0 < (μ s)⁻¹ * μ (s ∩ t)

Tactic:
refine ENNReal.mul_pos ?_ hci

Result:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hci : μ (s ∩ t) ≠ 0
⊢ (μ s)⁻¹ ≠ 0
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem hom_congr_vars {f₁ f₂ : MvPolynomial σ R →+* S} {p₁ p₂ : MvPolynomial σ R}
    (hC : f₁.comp C = f₂.comp C) (hv : ∀ i, i ∈ p₁.vars → i ∈ p₂.vars → f₁ (X i) = f₂ (X i))
    (hp : p₁ = p₂) : f₁ p₁ = f₂ p₂ :=
  calc
    f₁ p₁ = eval₂Hom (f₁.comp C) (f₁ ∘ X) p₁ := RingHom.congr_fun (by ext <;> simp) _
    _ = eval₂Hom (f₂.comp C) (f₂ ∘ X) p₂ := eval₂Hom_congr' hC hv hp
    _ = f₂ p₂ := RingHom.congr_fun (by ext <;> simp) _

Proof state:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (X i) = f₂ (X i)
hp : p₁ = p₂
⊢ eval₂Hom (f₂.comp C) (⇑f₂ ∘ X) = f₂

Tactic:
ext <;> simp

Result:
no goals

Proof state:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (X i) = f₂ (X i)
hp : p₁ = p₂
⊢ f₁ = eval₂Hom (f₁.comp C) (⇑f₁ ∘ X)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem tan_arg (x : ℂ) : Real.tan (arg x) = x.im / x.re

Proof state:
case neg
x : ℂ
h : ¬x = 0
⊢ Real.tan x.arg = x.im / x.re

Tactic:
rw [Real.tan_eq_sin_div_cos, sin_arg, cos_arg h,
  div_div_div_cancel_right₀ (norm_ne_zero_iff.mpr h)]

Result:
no goals

Proof state:
case pos
x : ℂ
h : x = 0
⊢ Real.tan x.arg = x.im / x.re

Tactic:
simp only [h, zero_div, Complex.zero_im, Complex.arg_zero, Real.tan_zero, Complex.zero_re]

Result:
no goals

Proof state:
x : ℂ
⊢ Real.tan x.arg = x.im / x.re

Tactic:
by_cases h : x = 0

Result:
case pos
x : ℂ
h : x = 0
⊢ Real.tan x.arg = x.im / x.re

case neg
x : ℂ
h : ¬x = 0
⊢ Real.tan x.arg = x.im / x.re
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {h} :
    getKey a (⟨k, v⟩ :: l) h = if h' : k == a then k
      else getKey a l (containsKey_of_containsKey_cons (k := k) h (Bool.eq_false_iff.2 h'))

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (⟨k, v⟩ :: l) = true
h✝ : (k == a) = true
⊢ some k = some k

Tactic:
rfl

Result:
no goals

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (⟨k, v⟩ :: l) = true
h✝ : ¬(k == a) = true
⊢ getKey? a l = some (getKey a l ⋯)

Tactic:
exact getKey?_eq_some_getKey _

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (⟨k, v⟩ :: l) = true
⊢ (if (k == a) = true then some k else getKey? a l) = if h : (k == a) = true then some k else some (getKey a l ⋯)

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (⟨k, v⟩ :: l) = true
h✝ : (k == a) = true
⊢ some k = some k

case isFalse
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (⟨k, v⟩ :: l) = true
h✝ : ¬(k == a) = true
⊢ getKey? a l = some (getKey a l ⋯)

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (⟨k, v⟩ :: l) = true
⊢ getKey a (⟨k, v⟩ :: l) h = if h' : (k == a) = true then k else getKey a l ⋯

Tactic:
rw [← Option.some_inj, ← getKey?_eq_some_getKey, getKey?_cons, apply_dite Option.some,
  cond_eq_if]

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (⟨k, v⟩ :: l) = true
⊢ (if (k == a) = true then some k else getKey? a l) = if h : (k == a) = true then some k else some (getKey a l ⋯)
-- Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean
theorem ext [G.IsCoverDense K] (ℱ : Sheaf K (Type _)) (X : D) {s t : ℱ.val.obj (op X)}
    (h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op s = ℱ.val.map f.op t) : s = t

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
D : Type u_2
inst✝¹ : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsCoverDense K
ℱ : Sheaf K (Type u_7)
X : D
s t : ℱ.val.obj (op X)
h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op s = ℱ.val.map f.op t
⊢ ∀ ⦃Y : D⦄ ⦃f : Y ⟶ X⦄, (Sieve.coverByImage G X).arrows f → ℱ.val.map f.op s = ℱ.val.map f.op t

Tactic:
rintro Y _ ⟨Z, f₁, f₂, ⟨rfl⟩⟩

Result:
case intro.mk.refl
C : Type u_1
inst✝² : Category.{u_5, u_1} C
D : Type u_2
inst✝¹ : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsCoverDense K
ℱ : Sheaf K (Type u_7)
X : D
s t : ℱ.val.obj (op X)
h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op s = ℱ.val.map f.op t
Y : D
Z : C
f₁ : Y ⟶ G.obj Z
f₂ : G.obj Z ⟶ X
⊢ ℱ.val.map (f₁ ≫ f₂).op s = ℱ.val.map (f₁ ≫ f₂).op t

Proof state:
case intro.mk.refl
C : Type u_1
inst✝² : Category.{u_5, u_1} C
D : Type u_2
inst✝¹ : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsCoverDense K
ℱ : Sheaf K (Type u_7)
X : D
s t : ℱ.val.obj (op X)
h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op s = ℱ.val.map f.op t
Y : D
Z : C
f₁ : Y ⟶ G.obj Z
f₂ : G.obj Z ⟶ X
⊢ ℱ.val.map (f₁ ≫ f₂).op s = ℱ.val.map (f₁ ≫ f₂).op t

Tactic:
simp [h f₂]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
D : Type u_2
inst✝¹ : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsCoverDense K
ℱ : Sheaf K (Type u_7)
X : D
s t : ℱ.val.obj (op X)
h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op s = ℱ.val.map f.op t
⊢ s = t

Tactic:
apply ((isSheaf_iff_isSheaf_of_type _ _ ).1 ℱ.cond
  (Sieve.coverByImage G X) (G.is_cover_of_isCoverDense K X)).isSeparatedFor.ext

Result:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
D : Type u_2
inst✝¹ : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsCoverDense K
ℱ : Sheaf K (Type u_7)
X : D
s t : ℱ.val.obj (op X)
h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op s = ℱ.val.map f.op t
⊢ ∀ ⦃Y : D⦄ ⦃f : Y ⟶ X⦄, (Sieve.coverByImage G X).arrows f → ℱ.val.map f.op s = ℱ.val.map f.op t
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem ediv_eq_of_eq_mul_right {a b c : Int}
    (H1 : b ≠ 0) (H2 : a = b * c) : a / b = c

Proof state:
a b c : Int
H1 : b ≠ 0
H2 : a = b * c
⊢ a / b = c

Tactic:
rw [H2, Int.mul_ediv_cancel_left _ H1]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Polish.lean
theorem complete_polishSpaceMetric (α : Type*) [ht : TopologicalSpace α] [h : PolishSpace α] :
    @CompleteSpace α (polishSpaceMetric α).toUniformSpace

Proof state:
α : Type u_3
ht : TopologicalSpace α
h : PolishSpace α
⊢ CompleteSpace α

Tactic:
convert h.complete.choose_spec.2

Result:
case h.e'_2.h.e'_2.h.e'_2
α : Type u_3
ht : TopologicalSpace α
h : PolishSpace α
⊢ polishSpaceMetric α = ⋯.choose

Proof state:
case h.e'_2.h.e'_2.h.e'_2
α : Type u_3
ht : TopologicalSpace α
h : PolishSpace α
⊢ polishSpaceMetric α = ⋯.choose

Tactic:
exact MetricSpace.replaceTopology_eq _ _

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Finset.lean
theorem tendsto_finset_image_atTop_atTop [DecidableEq β] {i : β → γ} {j : γ → β}
    (h : Function.LeftInverse j i) : Tendsto (Finset.image j) atTop atTop :=
  (Finset.image_mono j).tendsto_atTop_finset fun a =>
    ⟨{i a}, by simp only [Finset.image_singleton, h a, Finset.mem_singleton]⟩

Proof state:
β : Type u_4
γ : Type u_5
inst✝ : DecidableEq β
i : β → γ
j : γ → β
h : Function.LeftInverse j i
a : β
⊢ a ∈ Finset.image j {i a}

Tactic:
simp only [Finset.image_singleton, h a, Finset.mem_singleton]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma CFC.conjugate_rpow_neg_one_half {a : A} (h₀ : IsUnit a) (ha : 0 ≤ a

Proof state:
case intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : autoParam (0 ≤ ↑a) _auto✝
⊢ ↑a ^ (-(1 / 2)) * ↑a * ↑a ^ (-(1 / 2)) = 1

Tactic:
nth_rw 2 [← rpow_one (a : A)]

Result:
case intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : autoParam (0 ≤ ↑a) _auto✝
⊢ ↑a ^ (-(1 / 2)) * ↑a ^ 1 * ↑a ^ (-(1 / 2)) = 1

Proof state:
case intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : autoParam (0 ≤ ↑a) _auto✝
⊢ ↑a ^ (-(1 / 2)) * ↑a ^ 1 * ↑a ^ (-(1 / 2)) = 1

Tactic:
simp only [← rpow_add (a.zero_not_mem_spectrum ℝ≥0)]

Result:
case intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : autoParam (0 ≤ ↑a) _auto✝
⊢ ↑a ^ (-(1 / 2) + 1 + -(1 / 2)) = 1

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
h₀ : IsUnit a
ha : autoParam (0 ≤ a) _auto✝
⊢ a ^ (-(1 / 2)) * a * a ^ (-(1 / 2)) = 1

Tactic:
lift a to Aˣ using h₀

Result:
case intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : autoParam (0 ≤ ↑a) _auto✝
⊢ ↑a ^ (-(1 / 2)) * ↑a * ↑a ^ (-(1 / 2)) = 1

Proof state:
case intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : autoParam (0 ≤ ↑a) _auto✝
⊢ ↑a ^ (-(1 / 2) + 1 + -(1 / 2)) = 1

Tactic:
norm_num

Result:
case intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : autoParam (0 ≤ ↑a) _auto✝
⊢ ↑a ^ 0 = 1

Proof state:
case intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : autoParam (0 ≤ ↑a) _auto✝
⊢ ↑a ^ 0 = 1

Tactic:
exact rpow_zero _

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean
theorem exists_pos_lt_subset_ball {R : ℝ} {s : Set E} {x : E} (hR : 0 < R) (hs : IsClosed s)
    (h : s ⊆ ball x R) : ∃ r ∈ Ioo 0 R, s ⊆ ball x r

Proof state:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
R : ℝ
s : Set E
x : E
hR : 0 < R
hs : IsClosed s
h : ⇑toEuclidean '' s ⊆ Metric.ball (toEuclidean x) R
⊢ ∃ r ∈ Ioo 0 R, s ⊆ ball x r

Tactic:
rcases exists_pos_lt_subset_ball hR (toEuclidean.isClosed_image.2 hs) h with ⟨r, hr, hsr⟩

Result:
case intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
R : ℝ
s : Set E
x : E
hR : 0 < R
hs : IsClosed s
h : ⇑toEuclidean '' s ⊆ Metric.ball (toEuclidean x) R
r : ℝ
hr : r ∈ Ioo 0 R
hsr : ⇑toEuclidean '' s ⊆ Metric.ball (toEuclidean x) r
⊢ ∃ r ∈ Ioo 0 R, s ⊆ ball x r

Proof state:
case intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
R : ℝ
s : Set E
x : E
hR : 0 < R
hs : IsClosed s
h : ⇑toEuclidean '' s ⊆ Metric.ball (toEuclidean x) R
r : ℝ
hr : r ∈ Ioo 0 R
hsr : ⇑toEuclidean '' s ⊆ Metric.ball (toEuclidean x) r
⊢ ∃ r ∈ Ioo 0 R, s ⊆ ball x r

Tactic:
exact ⟨r, hr, image_subset_iff.1 hsr⟩

Result:
no goals

Proof state:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
R : ℝ
s : Set E
x : E
hR : 0 < R
hs : IsClosed s
h : s ⊆ ball x R
⊢ ∃ r ∈ Ioo 0 R, s ⊆ ball x r

Tactic:
rw [ball_eq_preimage, ← image_subset_iff] at h

Result:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
R : ℝ
s : Set E
x : E
hR : 0 < R
hs : IsClosed s
h : ⇑toEuclidean '' s ⊆ Metric.ball (toEuclidean x) R
⊢ ∃ r ∈ Ioo 0 R, s ⊆ ball x r