harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
lemma map_opcyclesMap' : F.map (ShortComplex.opcyclesMap' φ hr₁ hr₂) =
    ShortComplex.opcyclesMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)

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✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hr₁.IsPreservedBy F
inst✝ : hr₂.IsPreservedBy F
γ : RightHomologyMapData φ hr₁ hr₂
⊢ F.map (opcyclesMap' φ hr₁ hr₂) = opcyclesMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)

Tactic:
rw [γ.opcyclesMap'_eq, (γ.map F).opcyclesMap'_eq,  ShortComplex.RightHomologyMapData.map_φQ]

Result:
no goals

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✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hr₁.IsPreservedBy F
inst✝ : hr₂.IsPreservedBy F
⊢ F.map (opcyclesMap' φ hr₁ hr₂) = opcyclesMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)

Tactic:
have γ : ShortComplex.RightHomologyMapData φ hr₁ hr₂ := default

Result:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hr₁.IsPreservedBy F
inst✝ : hr₂.IsPreservedBy F
γ : RightHomologyMapData φ hr₁ hr₂
⊢ F.map (opcyclesMap' φ hr₁ hr₂) = opcyclesMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)
-- Mathlib/Probability/StrongLaw.lean
theorem strong_law_aux6 {c : ℝ} (c_one : 1 < c) :
    ∀ᵐ ω, Tendsto (fun n : ℕ => (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) / ⌊c ^ n⌋₊) atTop (𝓝 𝔼[X 0])

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g => IndepFun f g ℙ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
⊢ ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) / ↑⌊c ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))

Tactic:
have H : ∀ n : ℕ, (0 : ℝ) < ⌊c ^ n⌋₊ := by
  intro n
  refine zero_lt_one.trans_le ?_
  simp only [Nat.one_le_cast, Nat.one_le_floor_iff, one_le_pow₀ c_one.le]

Result:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g => IndepFun f g ℙ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
⊢ ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) / ↑⌊c ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
-- Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean
theorem Right.pow_lt_one_of_lt {n : ℕ} {x : M} (hn : 0 < n) (h : x < 1) : x ^ n < 1

Proof state:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
n : ℕ
x : M
hn : 0 < n
h : x < 1
⊢ x ^ n < 1

Tactic:
rcases Nat.exists_eq_succ_of_ne_zero hn.ne' with ⟨k, rfl⟩

Result:
case intro
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
x : M
h : x < 1
k : ℕ
hn : 0 < k.succ
⊢ x ^ k.succ < 1

Proof state:
case intro
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
x : M
h : x < 1
k : ℕ
hn : 0 < k.succ
⊢ x ^ k * x < 1

Tactic:
exact mul_lt_one_of_le_of_lt (pow_le_one_of_le h.le) h

Result:
no goals

Proof state:
case intro
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
x : M
h : x < 1
k : ℕ
hn : 0 < k.succ
⊢ x ^ k.succ < 1

Tactic:
rw [pow_succ]

Result:
case intro
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
x : M
h : x < 1
k : ℕ
hn : 0 < k.succ
⊢ x ^ k * x < 1
-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
/--
Pull back a `HasExactLimitsOfShape J` along a functor which preserves and reflects finite colimits
and preserves limits of shape `J`
-/
lemma HasExactLimitsOfShape.domain_of_functor {D : Type*} (J : Type*) [Category D] [Category J]
    [HasLimitsOfShape J C] [HasLimitsOfShape J D] [HasExactLimitsOfShape J D]
    (F : C ⥤ D) [PreservesFiniteColimits F] [ReflectsFiniteColimits F] [HasFiniteColimits C]
    [PreservesLimitsOfShape J F] : HasExactLimitsOfShape J C where
  preservesFiniteColimits := { preservesFiniteColimits I := { preservesColimit {G} := {
    preserves {c} hc

Proof state:
case val.t
C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} D
inst✝⁹ : Category.{u_4, u_2} J
inst✝⁸ : HasLimitsOfShape J C
inst✝⁷ : HasLimitsOfShape J D
inst✝⁶ : HasExactLimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteColimits F
inst✝⁴ : ReflectsFiniteColimits F
inst✝³ : HasFiniteColimits C
inst✝² : PreservesLimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cocone G
hc : IsColimit c
⊢ (Cocones.precompose (isoWhiskerLeft G (preservesLimitNatIso F).symm).inv).obj
      (((whiskeringRight J C D).obj F ⋙ lim).mapCocone c) ≅
    F.mapCocone (lim.mapCocone c)

Tactic:
refine Cocones.ext ((preservesLimitNatIso F).symm.app _) fun i ↦ ?_

Result:
case val.t
C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} D
inst✝⁹ : Category.{u_4, u_2} J
inst✝⁸ : HasLimitsOfShape J C
inst✝⁷ : HasLimitsOfShape J D
inst✝⁶ : HasExactLimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteColimits F
inst✝⁴ : ReflectsFiniteColimits F
inst✝³ : HasFiniteColimits C
inst✝² : PreservesLimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cocone G
hc : IsColimit c
i : I
⊢ ((Cocones.precompose (isoWhiskerLeft G (preservesLimitNatIso F).symm).inv).obj
              (((whiskeringRight J C D).obj F ⋙ lim).mapCocone c)).ι.app
        i ≫
      ((preservesLimitNatIso F).symm.app c.pt).hom =
    (F.mapCocone (lim.mapCocone c)).ι.app i
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem ContDiffOn.differentiableOn_iteratedDerivWithin {n : WithTop ℕ∞} {m : ℕ}
    (h : ContDiffOn 𝕜 n f s) (hmn : m < n) (hs : UniqueDiffOn 𝕜 s) :
    DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s := fun x hx =>
  (h x hx).differentiableWithinAt_iteratedDerivWithin hmn <| by rwa [insert_eq_of_mem hx]

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : WithTop ℕ∞
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 s
x : 𝕜
hx : x ∈ s
⊢ UniqueDiffOn 𝕜 (insert x s)

Tactic:
rwa [insert_eq_of_mem hx]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem lintegral_eq_of_measure_preimage [MeasurableSpace β] {f : α →ₛ ℝ≥0∞} {g : β →ₛ ℝ≥0∞}
    {ν : Measure β} (H : ∀ y, μ (f ⁻¹' {y}) = ν (g ⁻¹' {y})) : f.lintegral μ = g.lintegral ν

Proof state:
case hs
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
ν : Measure β
H : ∀ (y : ℝ≥0∞), μ (⇑f ⁻¹' {y}) = ν (⇑g ⁻¹' {y})
⊢ ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ g.range

Tactic:
simp only [H]

Result:
case hs
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
ν : Measure β
H : ∀ (y : ℝ≥0∞), μ (⇑f ⁻¹' {y}) = ν (⇑g ⁻¹' {y})
⊢ ∀ (x : α), f x ≠ 0 → ν (⇑g ⁻¹' {f x}) ≠ 0 → f x ∈ g.range

Proof state:
case hs
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
ν : Measure β
H : ∀ (y : ℝ≥0∞), μ (⇑f ⁻¹' {y}) = ν (⇑g ⁻¹' {y})
⊢ ∀ (x : α), f x ≠ 0 → ν (⇑g ⁻¹' {f x}) ≠ 0 → f x ∈ g.range

Tactic:
intros

Result:
case hs
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
ν : Measure β
H : ∀ (y : ℝ≥0∞), μ (⇑f ⁻¹' {y}) = ν (⇑g ⁻¹' {y})
x✝ : α
a✝¹ : f x✝ ≠ 0
a✝ : ν (⇑g ⁻¹' {f x✝}) ≠ 0
⊢ f x✝ ∈ g.range

Proof state:
case hs
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
ν : Measure β
H : ∀ (y : ℝ≥0∞), μ (⇑f ⁻¹' {y}) = ν (⇑g ⁻¹' {y})
x✝ : α
a✝¹ : f x✝ ≠ 0
a✝ : ν (⇑g ⁻¹' {f x✝}) ≠ 0
⊢ f x✝ ∈ g.range

Tactic:
exact mem_range_of_measure_ne_zero ‹_›

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
ν : Measure β
H : ∀ (y : ℝ≥0∞), μ (⇑f ⁻¹' {y}) = ν (⇑g ⁻¹' {y})
⊢ f.lintegral μ = g.lintegral ν

Tactic:
simp only [lintegral, ← H]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
ν : Measure β
H : ∀ (y : ℝ≥0∞), μ (⇑f ⁻¹' {y}) = ν (⇑g ⁻¹' {y})
⊢ ∑ x ∈ f.range, x * μ (⇑f ⁻¹' {x}) = ∑ x ∈ g.range, x * μ (⇑f ⁻¹' {x})

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
ν : Measure β
H : ∀ (y : ℝ≥0∞), μ (⇑f ⁻¹' {y}) = ν (⇑g ⁻¹' {y})
⊢ ∑ x ∈ f.range, x * μ (⇑f ⁻¹' {x}) = ∑ x ∈ g.range, x * μ (⇑f ⁻¹' {x})

Tactic:
apply lintegral_eq_of_subset

Result:
case hs
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
ν : Measure β
H : ∀ (y : ℝ≥0∞), μ (⇑f ⁻¹' {y}) = ν (⇑g ⁻¹' {y})
⊢ ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ g.range
-- Mathlib/Geometry/Euclidean/Inversion/ImageHyperplane.lean
theorem inversion_mem_perpBisector_inversion_iff (hR : R ≠ 0) (hx : x ≠ c) (hy : y ≠ c) :
    inversion c R x ∈ perpBisector c (inversion c R y) ↔ dist x y = dist y c

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hx : x ≠ c
hy : y ≠ c
⊢ R ^ 2 / dist x c = R ^ 2 / (dist x c * dist y c) * dist x y ↔ dist x y = dist y c

Tactic:
have hx' := dist_ne_zero.2 hx

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hx : x ≠ c
hy : y ≠ c
hx' : dist x c ≠ 0
⊢ R ^ 2 / dist x c = R ^ 2 / (dist x c * dist y c) * dist x y ↔ dist x y = dist y c

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hx : x ≠ c
hy : y ≠ c
hx' : dist x c ≠ 0
⊢ R ^ 2 / dist x c = R ^ 2 / (dist x c * dist y c) * dist x y ↔ dist x y = dist y c

Tactic:
have hy' := dist_ne_zero.2 hy

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hx : x ≠ c
hy : y ≠ c
hx' : dist x c ≠ 0
hy' : dist y c ≠ 0
⊢ R ^ 2 / dist x c = R ^ 2 / (dist x c * dist y c) * dist x y ↔ dist x y = dist y c

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hx : x ≠ c
hy : y ≠ c
hx' : dist x c ≠ 0
hy' : dist y c ≠ 0
⊢ R ^ 2 / dist x c = R ^ 2 / (dist x c * dist y c) * dist x y ↔ dist x y = dist y c

Tactic:
field_simp [mul_assoc, mul_comm, hx, hx.symm, eq_comm]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hx : x ≠ c
hy : y ≠ c
⊢ inversion c R x ∈ perpBisector c (inversion c R y) ↔ dist x y = dist y c

Tactic:
rw [mem_perpBisector_iff_dist_eq, dist_inversion_inversion hx hy, dist_inversion_center]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hx : x ≠ c
hy : y ≠ c
⊢ R ^ 2 / dist x c = R ^ 2 / (dist x c * dist y c) * dist x y ↔ dist x y = dist y c
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem eq_zero_iff {p : MvPolynomial σ R} : p = 0 ↔ ∀ d, coeff d p = 0

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (∀ (m : σ →₀ ℕ), coeff m p = coeff m 0) ↔ ∀ (d : σ →₀ ℕ), coeff d p = 0

Tactic:
simp only [coeff_zero]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p = 0 ↔ ∀ (d : σ →₀ ℕ), coeff d p = 0

Tactic:
rw [MvPolynomial.ext_iff]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (∀ (m : σ →₀ ℕ), coeff m p = coeff m 0) ↔ ∀ (d : σ →₀ ℕ), coeff d p = 0
-- Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean
theorem norm_id [Nontrivial E] : ‖id 𝕜 E‖ = 1

Proof state:
𝕜 : Type u_1
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
⊢ ∃ x, ‖x‖ ≠ 0

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : E)

Result:
case intro
𝕜 : Type u_1
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
⊢ ∃ x, ‖x‖ ≠ 0

Proof state:
𝕜 : Type u_1
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
⊢ ‖id 𝕜 E‖ = 1

Tactic:
refine norm_id_of_nontrivial_seminorm ?_

Result:
𝕜 : Type u_1
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
⊢ ∃ x, ‖x‖ ≠ 0

Proof state:
case intro
𝕜 : Type u_1
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
⊢ ∃ x, ‖x‖ ≠ 0

Tactic:
exact ⟨x, ne_of_gt (norm_pos_iff.2 hx)⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem smul_eval_comm (lc : LinearCombo) (i : Int) (v : Coeffs) :
    (i * lc).eval v = lc.eval v * i

Proof state:
lc : LinearCombo
i : Int
v : Coeffs
⊢ (i * lc).eval v = lc.eval v * i

Tactic:
simp [Int.mul_comm]

Result:
no goals
-- Mathlib/Tactic/Lift.lean
theorem Subtype.exists_pi_extension {ι : Sort*} {α : ι → Sort*} [ne : ∀ i, Nonempty (α i)]
    {p : ι → Prop} (f : ∀ i : Subtype p, α i) :
    ∃ g : ∀ i : ι, α i, (fun i : Subtype p => g i) = f

Proof state:
ι : Sort u_1
α : ι → Sort u_2
ne : ∀ (i : ι), Nonempty (α i)
p : ι → Prop
f : (i : Subtype p) → α i.val
⊢ ∃ g, (fun i => g i.val) = f

Tactic:
haveI : DecidablePred p := fun i ↦ Classical.propDecidable (p i)

Result:
ι : Sort u_1
α : ι → Sort u_2
ne : ∀ (i : ι), Nonempty (α i)
p : ι → Prop
f : (i : Subtype p) → α i.val
this : DecidablePred p
⊢ ∃ g, (fun i => g i.val) = f

Proof state:
ι : Sort u_1
α : ι → Sort u_2
ne : ∀ (i : ι), Nonempty (α i)
p : ι → Prop
f : (i : Subtype p) → α i.val
this : DecidablePred p
⊢ ∃ g, (fun i => g i.val) = f

Tactic:
exact ⟨fun i => if hi : p i then f ⟨i, hi⟩ else Classical.choice (ne i),
  funext fun i ↦ dif_pos i.2⟩

Result:
no goals
-- Mathlib/Algebra/AddTorsor/Basic.lean
theorem vsub_left_cancel {p₁ p₂ p : P} (h : p₁ -ᵥ p = p₂ -ᵥ p) : p₁ = p₂

Proof state:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p₁ p₂ p : P
h : p₁ -ᵥ p = p₂ -ᵥ p
⊢ p₁ = p₂

Tactic:
rwa [← sub_eq_zero, vsub_sub_vsub_cancel_right, vsub_eq_zero_iff_eq] at h

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem cauchy_zero : (0 : ℝ).cauchy = 0 :=
  show zero.cauchy = 0 by rw [zero_def]

Proof state:
⊢ Real.zero.cauchy = 0

Tactic:
rw [zero_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem?_zero_ofBool (b : Bool) : (ofBool b)[0]? = some b

Proof state:
b : Bool
⊢ (if b = true then 1#1 else 0#1)[0]? = some b

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
b : Bool
⊢ (ofBool b)[0]? = some b

Tactic:
simp only [ofBool, ofNat_eq_ofNat, cond_eq_if]

Result:
b : Bool
⊢ (if b = true then 1#1 else 0#1)[0]? = some b
-- Mathlib/Topology/Constructions.lean
theorem isOpen_sigma_fst_preimage (s : Set ι) : IsOpen (Sigma.fst ⁻¹' s : Set (Σ a, σ a))

Proof state:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
s : Set ι
⊢ IsOpen (⋃ i ∈ s, range (Sigma.mk i))

Tactic:
exact isOpen_biUnion fun _ _ => isOpen_range_sigmaMk

Result:
no goals

Proof state:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
s : Set ι
⊢ IsOpen (Sigma.fst ⁻¹' s)

Tactic:
rw [← biUnion_of_singleton s, preimage_iUnion₂]

Result:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
s : Set ι
⊢ IsOpen (⋃ i ∈ s, Sigma.fst ⁻¹' {i})

Proof state:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
s : Set ι
⊢ IsOpen (⋃ i ∈ s, Sigma.fst ⁻¹' {i})

Tactic:
simp only [← range_sigmaMk]

Result:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
s : Set ι
⊢ IsOpen (⋃ i ∈ s, range (Sigma.mk i))
-- Mathlib/Data/List/Lattice.lean
theorem bagInter_nil_iff_inter_nil : ∀ l₁ l₂ : List α, l₁.bagInter l₂ = [] ↔ l₁ ∩ l₂ = []
  | [], l₂ => by simp
  | b :: l₁, l₂ => by
    by_cases h : b ∈ l₂
    · simp [h]
    · simpa [h] using bagInter_nil_iff_inter_nil l₁ l₂

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []

Tactic:
simpa [h] using bagInter_nil_iff_inter_nil l₁ l₂

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
⊢ [].bagInter l₂ = [] ↔ [] ∩ l₂ = []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
⊢ (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []

Tactic:
by_cases h : b ∈ l₂

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : b ∈ l₂
⊢ (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []

case neg
α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : b ∈ l₂
⊢ (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem aroots_map (p : T[X]) [CommRing S] [Algebra T S] [Algebra S R] [Algebra T R]
    [IsScalarTower T S R] :
    (p.map (algebraMap T S)).aroots R = p.aroots R

Proof state:
R : Type u
S : Type v
T : Type w
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing T
p : T[X]
inst✝⁴ : CommRing S
inst✝³ : Algebra T S
inst✝² : Algebra S R
inst✝¹ : Algebra T R
inst✝ : IsScalarTower T S R
⊢ (map (algebraMap T S) p).aroots R = p.aroots R

Tactic:
rw [aroots_def, aroots_def, map_map, IsScalarTower.algebraMap_eq T S R]

Result:
no goals
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem HasLineDerivAt.le_of_lipschitzOn
    {f : E → F} {f' : F} {x₀ : E} (hf : HasLineDerivAt 𝕜 f f' x₀ v)
    {s : Set E} (hs : s ∈ 𝓝 x₀) {C : ℝ≥0} (hlip : LipschitzOnWith C f s) :
    ‖f'‖ ≤ C * ‖v‖

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ‖f'‖ ≤ ↑C * ‖v‖

Tactic:
refine hf.le_of_lip' C.coe_nonneg ?_

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ ↑C * ‖x - x₀‖

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ ↑C * ‖x - x₀‖

Tactic:
filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tsum_iSup_eq {α : Type*} (a : α) {f : α → ℝ≥0∞} : (∑' b : α, ⨆ _ : a = b, f b) = f a :=
  (tsum_eq_single a fun _ h => by simp [h.symm]).trans <| by simp

Proof state:
α : Type u_4
a : α
f : α → ℝ≥0∞
x✝ : α
h : x✝ ≠ a
⊢ ⨆ (_ : a = x✝), f x✝ = 0

Tactic:
simp [h.symm]

Result:
no goals

Proof state:
α : Type u_4
a : α
f : α → ℝ≥0∞
⊢ ⨆ (_ : a = a), f a = f a

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
@[norm_cast] lemma coe_stepBound {α : Type*} [Semiring α] (n : ℕ) :
    (stepBound n : α) = n * 4 ^ n

Proof state:
α : Type u_1
inst✝ : Semiring α
n : ℕ
⊢ ↑(stepBound n) = ↑n * 4 ^ n

Tactic:
unfold stepBound

Result:
α : Type u_1
inst✝ : Semiring α
n : ℕ
⊢ ↑(n * 4 ^ n) = ↑n * 4 ^ n

Proof state:
α : Type u_1
inst✝ : Semiring α
n : ℕ
⊢ ↑(n * 4 ^ n) = ↑n * 4 ^ n

Tactic:
norm_cast

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem umod_def {x y : BitVec n} :
    x % y = BitVec.ofNat n (x.toNat % y.toNat)

Proof state:
n : Nat
x y : BitVec n
h : x.toNat % y.toNat < 2 ^ n
⊢ x.umod y = BitVec.ofNat n (x.toNat % y.toNat)

Tactic:
simp [umod, bv_toNat, Nat.mod_eq_of_lt h]

Result:
no goals

Proof state:
n : Nat
x y : BitVec n
⊢ x % y = BitVec.ofNat n (x.toNat % y.toNat)

Tactic:
rw [← umod_eq]

Result:
n : Nat
x y : BitVec n
⊢ x.umod y = BitVec.ofNat n (x.toNat % y.toNat)

Proof state:
n : Nat
x y : BitVec n
⊢ x.umod y = BitVec.ofNat n (x.toNat % y.toNat)

Tactic:
have h : x.toNat % y.toNat < 2 ^ n := Nat.lt_of_le_of_lt (Nat.mod_le _ _) x.isLt

Result:
n : Nat
x y : BitVec n
h : x.toNat % y.toNat < 2 ^ n
⊢ x.umod y = BitVec.ofNat n (x.toNat % y.toNat)
-- Mathlib/GroupTheory/Complement.lean
@[to_additive]
lemma exists_isComplement_left (H : Subgroup G) (g : G) : ∃ S, IsComplement S H ∧ g ∈ S

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
⊢ ∃ S, IsComplement S ↑H ∧ g ∈ S

Tactic:
refine ⟨Set.range (Function.update Quotient.out _ g), isComplement_range_left fun q ↦ ?_,
  QuotientGroup.mk g, Function.update_self (Quotient.mk'' g) g Quotient.out⟩

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ ↑(update Quotient.out (Quotient.mk'' g) g q) = q

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ ↑(update Quotient.out (Quotient.mk'' g) g q) = q

Tactic:
by_cases hq : q = Quotient.mk'' g

Result:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
hq : q = Quotient.mk'' g
⊢ ↑(update Quotient.out (Quotient.mk'' g) g q) = q

case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
hq : ¬q = Quotient.mk'' g
⊢ ↑(update Quotient.out (Quotient.mk'' g) g q) = q

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
hq : ¬q = Quotient.mk'' g
⊢ ↑(update Quotient.out (Quotient.mk'' g) g q) = q

Tactic:
refine Function.update_of_ne ?_ g Quotient.out ▸ q.out_eq'

Result:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
hq : ¬q = Quotient.mk'' g
⊢ q ≠ Quotient.mk'' g

Proof state:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
hq : q = Quotient.mk'' g
⊢ ↑(update Quotient.out (Quotient.mk'' g) g q) = q

Tactic:
exact hq.symm ▸ congr_arg _ (Function.update_self (Quotient.mk'' g) g Quotient.out)

Result:
no goals

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
hq : ¬q = Quotient.mk'' g
⊢ q ≠ Quotient.mk'' g

Tactic:
exact hq

Result:
no goals