harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/Basic.lean
theorem dense_of_exists_between [OrderTopology α] [Nontrivial α] {s : Set α}
    (h : ∀ ⦃a b⦄, a < b → ∃ c ∈ s, a < c ∧ c < b) : Dense s

Proof state:
case intro.intro.intro.intro.intro
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, a < c ∧ c < b
U : Set α
U_open : IsOpen U
U_nonempty : U.Nonempty
a b : α
hab : a < b
H : Ioo a b ⊆ U
x : α
xs : x ∈ s
hx : a < x ∧ x < b
⊢ (U ∩ s).Nonempty

Tactic:
exact ⟨x, ⟨H hx, xs⟩⟩

Result:
no goals

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, a < c ∧ c < b
⊢ Dense s

Tactic:
refine dense_iff_inter_open.2 fun U U_open U_nonempty => ?_

Result:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, a < c ∧ c < b
U : Set α
U_open : IsOpen U
U_nonempty : U.Nonempty
⊢ (U ∩ s).Nonempty

Proof state:
case intro.intro.intro
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, a < c ∧ c < b
U : Set α
U_open : IsOpen U
U_nonempty : U.Nonempty
a b : α
hab : a < b
H : Ioo a b ⊆ U
⊢ (U ∩ s).Nonempty

Tactic:
obtain ⟨x, xs, hx⟩ : ∃ x ∈ s, a < x ∧ x < b := h hab

Result:
case intro.intro.intro.intro.intro
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, a < c ∧ c < b
U : Set α
U_open : IsOpen U
U_nonempty : U.Nonempty
a b : α
hab : a < b
H : Ioo a b ⊆ U
x : α
xs : x ∈ s
hx : a < x ∧ x < b
⊢ (U ∩ s).Nonempty

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, a < c ∧ c < b
U : Set α
U_open : IsOpen U
U_nonempty : U.Nonempty
⊢ (U ∩ s).Nonempty

Tactic:
obtain ⟨a, b, hab, H⟩ : ∃ a b : α, a < b ∧ Ioo a b ⊆ U := U_open.exists_Ioo_subset U_nonempty

Result:
case intro.intro.intro
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, a < c ∧ c < b
U : Set α
U_open : IsOpen U
U_nonempty : U.Nonempty
a b : α
hab : a < b
H : Ioo a b ⊆ U
⊢ (U ∩ s).Nonempty
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_insertListIfNewUnit_of_contains_eq_false_of_mem [BEq α] [EquivBEq α]
    {l : List ((_ : α) × Unit)} {toInsert : List α}
    {k k' : α} (k_beq : k == k')
    {h} (contains_eq_false : containsKey k l = false)
    (distinct : toInsert.Pairwise (fun a b => (a == b) = false))
    (mem : k ∈ toInsert) :
    getKey k' (insertListIfNewUnit l toInsert) h = k

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
h : containsKey k' (insertListIfNewUnit l toInsert) = true
contains_eq_false : containsKey k l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ getKey k' (insertListIfNewUnit l toInsert) h = k

Tactic:
rw [← Option.some_inj, ← getKey?_eq_some_getKey,
  getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem k_beq contains_eq_false distinct mem]

Result:
no goals
-- Mathlib/Algebra/Ring/Hom/Defs.lean
theorem domain_nontrivial [Nontrivial β] : Nontrivial α :=
  ⟨⟨1, 0, mt (fun h => show f 1 = 0 by rw [h, map_zero]) f.map_one_ne_zero⟩⟩

Proof state:
α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
inst✝ : Nontrivial β
h : 1 = 0
⊢ f 1 = 0

Tactic:
rw [h, map_zero]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_self_eq_norm_sq (x : E) : re ⟪x, x⟫ = ‖x‖ ^ 2

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ re ⟪x, x⟫_𝕜 = ‖x‖ ^ 2

Tactic:
rw [pow_two, inner_self_eq_norm_mul_norm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean
lemma indicator_le_apprSeq (n : ℕ) :
    indicator F (fun _ ↦ 1) ≤ hF.apprSeq n

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
n : ℕ
x : X
⊢ F.indicator (fun x => 1) x ≤ (hF.apprSeq n) x

Tactic:
by_cases hxF : x ∈ F

Result:
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
n : ℕ
x : X
hxF : x ∈ F
⊢ F.indicator (fun x => 1) x ≤ (hF.apprSeq n) x

case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
n : ℕ
x : X
hxF : x ∉ F
⊢ F.indicator (fun x => 1) x ≤ (hF.apprSeq n) x

Proof state:
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
n : ℕ
x : X
hxF : x ∈ F
⊢ F.indicator (fun x => 1) x ≤ (hF.apprSeq n) x

Tactic:
simp only [hxF, indicator_of_mem, apprSeq_apply_eq_one hF n, le_refl]

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
n : ℕ
⊢ (F.indicator fun x => 1) ≤ ⇑(hF.apprSeq n)

Tactic:
intro x

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
n : ℕ
x : X
⊢ F.indicator (fun x => 1) x ≤ (hF.apprSeq n) x

Proof state:
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
n : ℕ
x : X
hxF : x ∉ F
⊢ F.indicator (fun x => 1) x ≤ (hF.apprSeq n) x

Tactic:
simp only [hxF, not_false_eq_true, indicator_of_not_mem, zero_le]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
lemma le_sin (hx : x ≤ 0) : x ≤ sin x

Proof state:
x : ℝ
hx : x ≤ 0
⊢ x ≤ sin x

Tactic:
simpa using sin_le <| neg_nonneg.2 hx

Result:
no goals
-- Mathlib/Analysis/Normed/Order/Lattice.lean
theorem norm_inf_sub_inf_le_add_norm (a b c d : α) : ‖a ⊓ b - c ⊓ d‖ ≤ ‖a - c‖ + ‖b - d‖

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| ≤ ||a - c| + |b - d||

Tactic:
rw [abs_of_nonneg (add_nonneg (abs_nonneg (a - c)) (abs_nonneg (b - d)))]

Result:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| ≤ |a - c| + |b - d|

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ ‖a ⊓ b - c ⊓ d‖ ≤ ‖a - c‖ + ‖b - d‖

Tactic:
rw [← norm_abs_eq_norm (a - c), ← norm_abs_eq_norm (b - d)]

Result:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ ‖a ⊓ b - c ⊓ d‖ ≤ ‖|a - c|‖ + ‖|b - d|‖

Proof state:
case h₂
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |b ⊓ c - d ⊓ c| ≤ |b - d|

Tactic:
exact abs_inf_sub_inf_le_abs _ _ _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| = |a ⊓ b - c ⊓ b + (c ⊓ b - c ⊓ d)|

Tactic:
rw [sub_add_sub_cancel]

Result:
no goals

Proof state:
case h₁
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊓ b - c ⊓ b| ≤ |a - c|

Tactic:
exact abs_inf_sub_inf_le_abs _ _ _

Result:
no goals

Proof state:
case h₂
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |c ⊓ b - c ⊓ d| ≤ |b - d|

Tactic:
rw [inf_comm c, inf_comm c]

Result:
case h₂
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |b ⊓ c - d ⊓ c| ≤ |b - d|

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊓ b - c ⊓ b| + |c ⊓ b - c ⊓ d| ≤ |a - c| + |b - d|

Tactic:
apply add_le_add

Result:
case h₁
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊓ b - c ⊓ b| ≤ |a - c|

case h₂
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |c ⊓ b - c ⊓ d| ≤ |b - d|

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ ‖a ⊓ b - c ⊓ d‖ ≤ ‖|a - c|‖ + ‖|b - d|‖

Tactic:
refine le_trans (solid ?_) (norm_add_le |a - c| |b - d|)

Result:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| ≤ ||a - c| + |b - d||
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem contDiff_nat_iff_iteratedDeriv {n : ℕ} : ContDiff 𝕜 n f ↔
    (∀ m : ℕ, m ≤ n → Continuous (iteratedDeriv m f)) ∧
      ∀ m : ℕ, m < n → Differentiable 𝕜 (iteratedDeriv m f)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
n : ℕ
⊢ ((∀ (m : ℕ), ↑m ≤ ↑n → Continuous (iteratedDeriv m f)) ∧ ∀ (m : ℕ), ↑m < ↑n → Differentiable 𝕜 (iteratedDeriv m f)) ↔
    (∀ m ≤ n, Continuous (iteratedDeriv m f)) ∧ ∀ m < n, Differentiable 𝕜 (iteratedDeriv m f)

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
n : ℕ
⊢ ContDiff 𝕜 (↑n) f ↔ (∀ m ≤ n, Continuous (iteratedDeriv m f)) ∧ ∀ m < n, Differentiable 𝕜 (iteratedDeriv m f)

Tactic:
rw [show n = ((n : ℕ∞) : WithTop ℕ∞) from rfl, contDiff_iff_iteratedDeriv]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
n : ℕ
⊢ ((∀ (m : ℕ), ↑m ≤ ↑n → Continuous (iteratedDeriv m f)) ∧ ∀ (m : ℕ), ↑m < ↑n → Differentiable 𝕜 (iteratedDeriv m f)) ↔
    (∀ m ≤ n, Continuous (iteratedDeriv m f)) ∧ ∀ m < n, Differentiable 𝕜 (iteratedDeriv m f)
-- Mathlib/Algebra/Module/Presentation/Differentials.lean
/-- Same as `comm₂₃` below, but here we have not yet constructed `differentialsSolution`. -/
lemma comm₂₃' : pres.toExtension.toKaehler.comp pres.cotangentSpaceBasis.repr.symm.toLinearMap =
    Finsupp.linearCombination S (fun g ↦ D _ _ (pres.val g))

Proof state:
case h.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
g : pres.vars
⊢ pres.toExtension.toKaehler (pres.cotangentSpaceBasis.repr.symm (Finsupp.single g 1)) =
    (Finsupp.linearCombination S fun g => (D R S) (pres.val g)) (Finsupp.single g 1)

Tactic:
rw [Basis.repr_symm_apply, Finsupp.linearCombination_single,
  Finsupp.linearCombination_single, one_smul, one_smul,
  Generators.cotangentSpaceBasis_apply]

Result:
case h.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
g : pres.vars
⊢ pres.toExtension.toKaehler (1 ⊗ₜ[pres.Ring] (D R pres.Ring) (MvPolynomial.X g)) = (D R S) (pres.val g)

Proof state:
case h.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
g : pres.vars
⊢ pres.toExtension.toKaehler (1 ⊗ₜ[pres.Ring] (D R pres.Ring) (MvPolynomial.X g)) = (D R S) (pres.val g)

Tactic:
simp [Generators.toExtension]

Result:
no goals

Proof state:
case h.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
g : pres.vars
⊢ ((pres.toExtension.toKaehler ∘ₗ ↑pres.cotangentSpaceBasis.repr.symm) ∘ₗ Finsupp.lsingle g) 1 =
    ((Finsupp.linearCombination S fun g => (D R S) (pres.val g)) ∘ₗ Finsupp.lsingle g) 1

Tactic:
dsimp

Result:
case h.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
g : pres.vars
⊢ pres.toExtension.toKaehler (pres.cotangentSpaceBasis.repr.symm (Finsupp.single g 1)) =
    (Finsupp.linearCombination S fun g => (D R S) (pres.val g)) (Finsupp.single g 1)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
⊢ pres.toExtension.toKaehler ∘ₗ ↑pres.cotangentSpaceBasis.repr.symm =
    Finsupp.linearCombination S fun g => (D R S) (pres.val g)

Tactic:
ext g

Result:
case h.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
g : pres.vars
⊢ ((pres.toExtension.toKaehler ∘ₗ ↑pres.cotangentSpaceBasis.repr.symm) ∘ₗ Finsupp.lsingle g) 1 =
    ((Finsupp.linearCombination S fun g => (D R S) (pres.val g)) ∘ₗ Finsupp.lsingle g) 1
-- Mathlib/Algebra/Category/Grp/Images.lean
theorem image.lift_fac (F' : MonoFactorisation f) : image.lift F' ≫ F'.m = image.ι f

Proof state:
case hf.h
G H : AddCommGrp
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ (Hom.hom (lift F' ≫ F'.m)) x = (Hom.hom (ι f)) x

Tactic:
change (F'.e ≫ F'.m) _ = _

Result:
case hf.h
G H : AddCommGrp
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 => (Hom.hom f) x_1 = ↑x) ⋯) =
    (Hom.hom (ι f)) x

Proof state:
case hf.h
G H : AddCommGrp
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 => (Hom.hom f) x_1 = ↑x) ⋯) =
    (Hom.hom (ι f)) x

Tactic:
rw [F'.fac, (Classical.indefiniteDescription _ x.2).2]

Result:
case hf.h
G H : AddCommGrp
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ ↑x = (Hom.hom (ι f)) x

Proof state:
case hf.h
G H : AddCommGrp
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ ↑x = (Hom.hom (ι f)) x

Tactic:
rfl

Result:
no goals

Proof state:
G H : AddCommGrp
f : G ⟶ H
F' : MonoFactorisation f
⊢ lift F' ≫ F'.m = ι f

Tactic:
ext x

Result:
case hf.h
G H : AddCommGrp
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ (Hom.hom (lift F' ≫ F'.m)) x = (Hom.hom (ι f)) x
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
@[simp]
protected lemma map_neg (P : Fin 3 → R) : (W'.map f).toProjective.neg (f ∘ P) = f ∘ W'.neg P

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ ![(⇑f ∘ P) x, f (W'.negY P), (⇑f ∘ P) z] = ![f (P x), f (W'.negY P), f (P z)]

Tactic:
map_simp

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ (map W' f).toProjective.neg (⇑f ∘ P) = ⇑f ∘ W'.neg P

Tactic:
simp only [neg, map_negY, comp_fin3]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ ![(⇑f ∘ P) x, f (W'.negY P), (⇑f ∘ P) z] = ![f (P x), f (W'.negY P), f (P z)]
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem Ico_image_const_sub_eq_Ico (hac : a ≤ c) :
    ((Ico a b).image fun x => c - x) = Ico (c + 1 - b) (c + 1 - a)

Proof state:
a b c : ℕ
hac : a ≤ c
x : ℕ
h : c + 1 - b ≤ x ∧ x < c + 1 - a
⊢ (a ≤ c - x ∧ c - x < b) ∧ c - (c - x) = x

Tactic:
omega

Result:
no goals

Proof state:
a b c : ℕ
hac : a ≤ c
⊢ image (fun x => c - x) (Ico a b) = Ico (c + 1 - b) (c + 1 - a)

Tactic:
ext x

Result:
case h
a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ x ∈ image (fun x => c - x) (Ico a b) ↔ x ∈ Ico (c + 1 - b) (c + 1 - a)

Proof state:
case h
a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ (∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ c - a_1 = x) → c + 1 - b ≤ x ∧ x < c + 1 - a

Tactic:
rintro ⟨x, hx, rfl⟩

Result:
case h.intro.intro
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
⊢ c + 1 - b ≤ c - x ∧ c - x < c + 1 - a

Proof state:
case h
a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ x ∈ image (fun x => c - x) (Ico a b) ↔ x ∈ Ico (c + 1 - b) (c + 1 - a)

Tactic:
simp_rw [mem_image, mem_Ico]

Result:
case h
a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ (∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ c - a_1 = x) ↔ c + 1 - b ≤ x ∧ x < c + 1 - a

Proof state:
case h.intro.intro
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
⊢ c + 1 - b ≤ c - x ∧ c - x < c + 1 - a

Tactic:
omega

Result:
no goals

Proof state:
case h
a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ (∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ c - a_1 = x) ↔ c + 1 - b ≤ x ∧ x < c + 1 - a

Tactic:
refine ⟨?_, fun h ↦ ⟨c - x, by omega⟩⟩

Result:
case h
a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ (∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ c - a_1 = x) → c + 1 - b ≤ x ∧ x < c + 1 - a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem mem_eraseIdx_iff_getElem? {x : α} {l} {k} {h} : x ∈ eraseIdx l k h ↔ ∃ i ≠ k, l[i]? = some x

Proof state:
α : Type u_1
x : α
l : Array α
k : Nat
h : k < l.size
⊢ x ∈ l.eraseIdx k h ↔ ∃ i, i ≠ k ∧ l[i]? = some x

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
x : α
k : Nat
l : List α
h : k < { toList := l }.size
⊢ x ∈ { toList := l }.eraseIdx k h ↔ ∃ i, i ≠ k ∧ { toList := l }[i]? = some x

Proof state:
case mk
α : Type u_1
x : α
k : Nat
l : List α
h : k < { toList := l }.size
⊢ x ∈ { toList := l }.eraseIdx k h ↔ ∃ i, i ≠ k ∧ { toList := l }[i]? = some x

Tactic:
simp [List.mem_eraseIdx_iff_getElem?, *]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_abs {i : Nat} {x : BitVec w} (h : i < w) :
    x.abs[i] = if x.msb then (-x)[i] else x[i]

Proof state:
w i : Nat
x : BitVec w
h : i < w
⊢ x.abs[i] = if x.msb = true then (-x)[i] else x[i]

Tactic:
by_cases h : x.msb <;> simp [BitVec.abs, h]

Result:
no goals
-- Mathlib/Order/Heyting/Boundary.lean
theorem hnot_hnot_sup_boundary (a : α) : ￢￢a ⊔ ∂ a = a

Proof state:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢￢a ⊔ ∂ a = a

Tactic:
rw [boundary, sup_inf_left, hnot_sup_self, inf_top_eq, sup_eq_right]

Result:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢￢a ≤ a

Proof state:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢￢a ≤ a

Tactic:
exact hnot_hnot_le

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_sub_zsmul (a b : α) (m : ℤ) : toIocMod hp a (b - m • p) = toIocMod hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp a (b - m • p) = toIocMod hp a b

Tactic:
rw [sub_eq_add_neg, ← neg_smul, toIocMod_add_zsmul]

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem image_connectedComponentIn {s : Set X} (h : X ≃ₜ Y) {x : X} (hx : x ∈ s) :
    h '' connectedComponentIn s x = connectedComponentIn (h '' s) (h x)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
⊢ ⇑h '' connectedComponentIn s x = connectedComponentIn (⇑h '' s) (h x)

Tactic:
refine (h.continuous.image_connectedComponentIn_subset hx).antisymm ?_

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
⊢ connectedComponentIn (⇑h '' s) (h x) ⊆ ⇑h '' connectedComponentIn s x

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
this : ⇑h.symm '' connectedComponentIn (⇑h '' s) (h x) ⊆ connectedComponentIn (⇑h.symm '' (⇑h '' s)) (h.symm (h x))
⊢ connectedComponentIn (⇑h '' s) (h x) ⊆ ⇑h '' connectedComponentIn s x

Tactic:
rwa [image_subset_iff, h.preimage_symm, h.image_symm, h.preimage_image, h.symm_apply_apply]
  at this

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
⊢ connectedComponentIn (⇑h '' s) (h x) ⊆ ⇑h '' connectedComponentIn s x

Tactic:
have := h.symm.continuous.image_connectedComponentIn_subset (mem_image_of_mem h hx)

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
this : ⇑h.symm '' connectedComponentIn (⇑h '' s) (h x) ⊆ connectedComponentIn (⇑h.symm '' (⇑h '' s)) (h.symm (h x))
⊢ connectedComponentIn (⇑h '' s) (h x) ⊆ ⇑h '' connectedComponentIn s x
-- Mathlib/Analysis/Seminorm.lean
theorem isLUB_sSup (s : Set (Seminorm 𝕜 E)) (hs₁ : BddAbove s) (hs₂ : s.Nonempty) :
    IsLUB s (sSup s)

Proof state:
case refine_1
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
this : Nonempty ↑s
⊢ p x ≤ ⨆ i, ↑i x

Tactic:
rcases hs₁ with ⟨q, hq⟩

Result:
case refine_1.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
this : Nonempty ↑s
q : Seminorm 𝕜 E
hq : q ∈ upperBounds s
⊢ p x ≤ ⨆ i, ↑i x

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
refine ⟨fun p hp x => ?_, fun p hp x => ?_⟩ <;> haveI : Nonempty ↑s := hs₂.coe_sort <;>
  dsimp <;> rw [Seminorm.coe_sSup_eq hs₁, iSup_apply]

Result:
case refine_1
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
this : Nonempty ↑s
⊢ p x ≤ ⨆ i, ↑i x

case refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ upperBounds s
x : E
this : Nonempty ↑s
⊢ ⨆ i, ↑i x ≤ p x

Proof state:
case refine_1.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
this : Nonempty ↑s
q : Seminorm 𝕜 E
hq : q ∈ upperBounds s
⊢ p x ≤ ⨆ i, ↑i x

Tactic:
exact le_ciSup ⟨q x, forall_mem_range.mpr fun i : s => hq i.2 x⟩ ⟨p, hp⟩

Result:
no goals

Proof state:
case refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ upperBounds s
x : E
this : Nonempty ↑s
⊢ ⨆ i, ↑i x ≤ p x

Tactic:
exact ciSup_le fun q => hp q.2 x

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem zipIdx_eq_map_add (l : List α) (n : Nat) :
    l.zipIdx n = l.zipIdx.map (fun ⟨a, i⟩ => (a, n + i))

Proof state:
α : Type u_1
l : List α
n : Nat
⊢ l.zipIdx n =
    map
      (fun x =>
        match x with
        | (a, i) => (a, n + i))
      l.zipIdx

Tactic:
induction l generalizing n with
| nil => rfl
| cons _ _ ih => simp [ih (n+1), zipIdx_succ, Nat.add_assoc, Nat.add_comm 1]

Result:
no goals

Proof state:
case nil
α : Type u_1
n : Nat
⊢ [].zipIdx n =
    map
      (fun x =>
        match x with
        | (a, i) => (a, n + i))
      [].zipIdx

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
ih :
  ∀ (n : Nat),
    tail✝.zipIdx n =
      map
        (fun x =>
          match x with
          | (a, i) => (a, n + i))
        tail✝.zipIdx
n : Nat
⊢ (head✝ :: tail✝).zipIdx n =
    map
      (fun x =>
        match x with
        | (a, i) => (a, n + i))
      (head✝ :: tail✝).zipIdx

Tactic:
simp [ih (n+1), zipIdx_succ, Nat.add_assoc, Nat.add_comm 1]

Result:
no goals
-- Mathlib/Order/Cover.lean
theorem OrderEmbedding.wcovBy_of_apply {α β : Type*} [Preorder α] [Preorder β]
    (f : α ↪o β) {x y : α} (h : f x ⩿ f y) : x ⩿ y

Proof state:
case right
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
x y : α
h : f x ⩿ f y
a : α
⊢ f x < f a → ¬f a < f y

Tactic:
apply h.2

Result:
no goals

Proof state:
case right
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
x y : α
h : f x ⩿ f y
⊢ ∀ ⦃c : α⦄, x < c → ¬c < y

Tactic:
intro a

Result:
case right
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
x y : α
h : f x ⩿ f y
a : α
⊢ x < a → ¬a < y

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
x y : α
h : f x ⩿ f y
⊢ x ⩿ y

Tactic:
use f.le_iff_le.1 h.1

Result:
case right
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
x y : α
h : f x ⩿ f y
⊢ ∀ ⦃c : α⦄, x < c → ¬c < y

Proof state:
case right
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
x y : α
h : f x ⩿ f y
a : α
⊢ x < a → ¬a < y

Tactic:
rw [← f.lt_iff_lt, ← f.lt_iff_lt]

Result:
case right
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
x y : α
h : f x ⩿ f y
a : α
⊢ f x < f a → ¬f a < f y