harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Round.lean
theorem round_intCast (n : ℤ) : round (n : α) = n

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
n : ℤ
⊢ round ↑n = n

Tactic:
simp [round]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α}
    {f : Option β → Option β} (h : m.WF) {hc : k ∈ Const.alter m k f} :
    (Const.alter m k f).getKey k hc = k

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k : α
f : Option β → Option β
h : m.WF
hc : k ∈ alter m k f
⊢ (alter m k f).getKey k hc = k

Tactic:
simp [getKey_alter h]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
lemma ext_to_X' (i : ι) (hi : ¬ c.Rel i (c.next i)) {A : C} {f g : A ⟶ X φ i}
    (h : f ≫ sndX φ i = g ≫ sndX φ i) : f = g

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
hi : ¬c.Rel i (c.next i)
A : C
f g : A ⟶ X φ i
h : f ≫ sndX φ i = g ≫ sndX φ i
⊢ f ≫ (XIso φ i hi).hom = g ≫ (XIso φ i hi).hom

Tactic:
simpa only [sndX, dif_neg hi] using h

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
hi : ¬c.Rel i (c.next i)
A : C
f g : A ⟶ X φ i
h : f ≫ sndX φ i = g ≫ sndX φ i
⊢ f = g

Tactic:
rw [← cancel_mono (XIso φ i hi).hom]

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
hi : ¬c.Rel i (c.next i)
A : C
f g : A ⟶ X φ i
h : f ≫ sndX φ i = g ≫ sndX φ i
⊢ f ≫ (XIso φ i hi).hom = g ≫ (XIso φ i hi).hom
-- Mathlib/Order/Filter/Basic.lean
theorem iInter_mem' {β : Sort v} {s : β → Set α} [Subsingleton β] :
    (⋂ i, s i) ∈ f ↔ ∀ i, s i ∈ f

Proof state:
α : Type u
f : Filter α
β : Sort v
s : β → Set α
inst✝ : Subsingleton β
⊢ ⋂ i, s i ∈ f ↔ ∀ (i : β), s i ∈ f

Tactic:
rw [← sInter_range, sInter_eq_biInter, biInter_mem' (subsingleton_range s), forall_mem_range]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) :
    Const.get? (Const.modify m k f) k = (Const.get? m k).map f

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : β → β
h : m.WF
⊢ get? (modify m k f) k = Option.map f (get? m k)

Tactic:
simp_to_raw using Raw₀.Const.get?_modify_self

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean
@[reassoc]
lemma δ₂_two_comp_σ₂_zero : δ₂ (2 : Fin 3) ≫ σ₂ 0 = σ₂ 0 ≫ δ₂ 1 :=
  SimplexCategory.δ_comp_σ_of_gt' (by decide)

Proof state:
⊢ Fin.succ 0 < 2

Tactic:
decide

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/--
The even Hurwitz completed zeta is differentiable away from `s = 0` and `s = 1` (and also at
`s = 0` if `a ≠ 0`)
-/
lemma differentiableAt_completedHurwitzZetaEven
    (a : UnitAddCircle) {s : ℂ} (hs : s ≠ 0 ∨ a ≠ 0) (hs' : s ≠ 1) :
    DifferentiableAt ℂ (completedHurwitzZetaEven a) s

Proof state:
case refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ s / 2 ≠ ↑(1 / 2)

Tactic:
rw [ofReal_div, ofReal_one, ofReal_ofNat]

Result:
case refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ s / 2 ≠ 1 / 2

Proof state:
case refine_1
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ s / 2 ≠ 0 ∨ (hurwitzEvenFEPair a).f₀ = 0

Tactic:
rcases hs with h | h <;>
simp [hurwitzEvenFEPair, h]

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (completedHurwitzZetaEven a) s

Tactic:
refine (((hurwitzEvenFEPair a).differentiableAt_Λ ?_ (Or.inl ?_)).comp s
    (differentiableAt_id.div_const _)).div_const _

Result:
case refine_1
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ s / 2 ≠ 0 ∨ (hurwitzEvenFEPair a).f₀ = 0

case refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ s / 2 ≠ ↑(hurwitzEvenFEPair a).k

Proof state:
case refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ s / 2 ≠ ↑(hurwitzEvenFEPair a).k

Tactic:
change s / 2 ≠ ↑(1 / 2 : ℝ)

Result:
case refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ s / 2 ≠ ↑(1 / 2)

Proof state:
case refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ s / 2 ≠ 1 / 2

Tactic:
exact hs' ∘ (div_left_inj' two_ne_zero).mp

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Map.lean
theorem equivMapOfInjective_coe_mulEquiv (H : Subgroup G) (e : G ≃* G') :
    H.equivMapOfInjective (e : G →* G') (EquivLike.injective e) = e.subgroupMap H

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
e : G ≃* G'
⊢ H.equivMapOfInjective ↑e ⋯ = e.subgroupMap H

Tactic:
ext

Result:
case h.a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
e : G ≃* G'
x✝ : ↥H
⊢ ↑((H.equivMapOfInjective ↑e ⋯) x✝) = ↑((e.subgroupMap H) x✝)

Proof state:
case h.a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
e : G ≃* G'
x✝ : ↥H
⊢ ↑((H.equivMapOfInjective ↑e ⋯) x✝) = ↑((e.subgroupMap H) x✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[ext]
lemma opcycles_ext {A : C} (f₁ f₂ : S.opcycles ⟶ A)
    (h : S.pOpcycles ≫ f₁ = S.pOpcycles ≫ f₂) : f₁ = f₂

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasRightHomology
A : C
f₁ f₂ : S.opcycles ⟶ A
h : S.pOpcycles ≫ f₁ = S.pOpcycles ≫ f₂
⊢ f₁ = f₂

Tactic:
simpa only [opcycles_ext_iff]

Result:
no goals
-- Mathlib/Algebra/Lie/Solvable.lean
lemma isSolvable_iff : IsSolvable L ↔ ∃ k, derivedSeries R L k = ⊥

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ IsSolvable L ↔ ∃ k, derivedSeries R L k = ⊥

Tactic:
simp [isSolvable_iff_int, SetLike.ext'_iff, LieIdeal.coe_derivedSeries_eq_int]

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/MazurUlam.lean
theorem coe_toRealAffineIsometryEquiv (f : PE ≃ᵢ PF) :
    f.toRealAffineIsometryEquiv.toIsometryEquiv = f

Proof state:
case H
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x✝ : PE
⊢ f.toRealAffineIsometryEquiv.toIsometryEquiv x✝ = f x✝

Tactic:
rfl

Result:
no goals

Proof state:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
⊢ f.toRealAffineIsometryEquiv.toIsometryEquiv = f

Tactic:
ext

Result:
case H
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x✝ : PE
⊢ f.toRealAffineIsometryEquiv.toIsometryEquiv x✝ = f x✝
-- Mathlib/Algebra/Ring/Commute.lean
theorem mul_self_sub_mul_self_eq' [NonUnitalNonAssocRing R] {a b : R} (h : Commute a b) :
    a * a - b * b = (a - b) * (a + b)

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = (a - b) * (a + b)

Tactic:
rw [mul_add, sub_mul, sub_mul, h.eq, sub_add_sub_cancel]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem norm_intervalIntegral_eq (f : ℝ → E) (a b : ℝ) (μ : Measure ℝ) :
    ‖∫ x in a..b, f x ∂μ‖ = ‖∫ x in Ι a b, f x ∂μ‖

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
⊢ ‖∫ (x : ℝ) in a..b, f x ∂μ‖ = ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖

Tactic:
simp_rw [intervalIntegral_eq_integral_uIoc, norm_smul]

Result:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
⊢ ‖if a ≤ b then 1 else -1‖ * ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖ = ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
⊢ ‖if a ≤ b then 1 else -1‖ * ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖ = ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖

Tactic:
split_ifs <;> simp only [norm_neg, norm_one, one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem fmod_def (a b : Int) : a.fmod b = a - b * a.fdiv b

Proof state:
a b : Int
⊢ a.fmod b = a - b * a.fdiv b

Tactic:
rw [← Int.add_sub_cancel (a.fmod b), fmod_add_fdiv]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/FunctorCategory.lean
theorem app_units_zsmul (X : C) (α : F ⟶ G) (n : ℤˣ) : (n • α).app X = n • α.app X

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 D
F G : C ⥤ D
X : C
α : F ⟶ G
n : ℤˣ
⊢ (n • α).app X = n • α.app X

Tactic:
apply app_zsmul

Result:
no goals
-- Mathlib/Data/Nat/PrimeFin.lean
@[simp] lemma primeFactors_one : primeFactors 1 = ∅

Proof state:
case h
a✝ : ℕ
⊢ a✝ ∈ primeFactors 1 ↔ a✝ ∈ ∅

Tactic:
simpa using Prime.ne_one

Result:
no goals

Proof state:
⊢ primeFactors 1 = ∅

Tactic:
ext

Result:
case h
a✝ : ℕ
⊢ a✝ ∈ primeFactors 1 ↔ a✝ ∈ ∅
-- Mathlib/Data/Finset/Sym.lean
theorem eq_empty_of_sym_eq_empty (h : s.sym n = ∅) : s = ∅

Proof state:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
h : s.sym n = ∅
⊢ s = ∅

Tactic:
rw [← not_nonempty_iff_eq_empty] at h ⊢

Result:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
h : ¬(s.sym n).Nonempty
⊢ ¬s.Nonempty

Proof state:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
h : ¬(s.sym n).Nonempty
⊢ ¬s.Nonempty

Tactic:
exact fun hs ↦ h (hs.sym _)

Result:
no goals
-- Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
@[simp]
lemma dualCoannihilator_map_linearEquiv_flip (p : Submodule R M) :
    (p.map e.flip).dualCoannihilator = p.dualAnnihilator.map e.symm

Proof state:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R M
x✝ : N
⊢ x✝ ∈ (map e.flip p).dualCoannihilator ↔ x✝ ∈ map e.symm p.dualAnnihilator

Tactic:
simp [LinearEquiv.symm_apply_eq, Submodule.mem_dualCoannihilator]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R M
⊢ (map e.flip p).dualCoannihilator = map e.symm p.dualAnnihilator

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R M
x✝ : N
⊢ x✝ ∈ (map e.flip p).dualCoannihilator ↔ x✝ ∈ map e.symm p.dualAnnihilator
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem mem_closedBall_comm : x ∈ closedBall y ε ↔ y ∈ closedBall x ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
⊢ x ∈ closedBall y ε ↔ y ∈ closedBall x ε

Tactic:
rw [mem_closedBall', mem_closedBall]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/ByteArray.lean
theorem get_ofFn (f : Fin n → UInt8) (i : Fin (ofFn f).size) :
    (ofFn f).get i = f (i.cast (size_ofFn f))

Proof state:
n : Nat
f : Fin n → UInt8
i : Fin (ofFn f).size
⊢ (ofFn f).get ↑i ⋯ = f (Fin.cast ⋯ i)

Tactic:
simp [get, Fin.cast]

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

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

Tactic:
simp_rw [sub_eq_add_neg, ← neg_smul, toIcoMod_add_zsmul']

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/Basic.lean
@[simp] lemma map_add_left_Ioc (a b c : α) :
    (Ioc a b).map (addLeftEmbedding c) = Ioc (c + a) (c + b)

Proof state:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addLeftEmbedding c) (Ioc a b) = Ioc (c + a) (c + b)

Tactic:
rw [← coe_inj, coe_map, coe_Ioc, coe_Ioc]

Result:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addLeftEmbedding c) '' Set.Ioc a b = Set.Ioc (c + a) (c + b)

Proof state:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addLeftEmbedding c) '' Set.Ioc a b = Set.Ioc (c + a) (c + b)

Tactic:
exact Set.image_const_add_Ioc _ _ _

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma baseChange_ψ (n : ℤ) : (W.baseChange B).ψ n = ((W.baseChange A).ψ n).map (mapRingHom f)

Proof state:
R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
⊢ (W.baseChange B).ψ n = Polynomial.map (mapRingHom ↑f) ((W.baseChange A).ψ n)

Tactic:
rw [← map_ψ, map_baseChange]

Result:
no goals
-- Mathlib/Order/Bounded.lean
theorem bounded_le_iff_bounded_lt [Preorder α] [NoMaxOrder α] :
    Bounded (· ≤ ·) s ↔ Bounded (· < ·) s

Proof state:
case intro.intro
α : Type u_1
s : Set α
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
ha : ∀ b ∈ s, (fun x1 x2 => x1 ≤ x2) b a
b : α
hb : a < b
⊢ Bounded (fun x1 x2 => x1 < x2) s

Tactic:
exact ⟨b, fun c hc => lt_of_le_of_lt (ha c hc) hb⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
s : Set α
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
ha : ∀ b ∈ s, (fun x1 x2 => x1 ≤ x2) b a
⊢ Bounded (fun x1 x2 => x1 < x2) s

Tactic:
obtain ⟨b, hb⟩ := exists_gt a

Result:
case intro.intro
α : Type u_1
s : Set α
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
ha : ∀ b ∈ s, (fun x1 x2 => x1 ≤ x2) b a
b : α
hb : a < b
⊢ Bounded (fun x1 x2 => x1 < x2) s

Proof state:
α : Type u_1
s : Set α
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
⊢ Bounded (fun x1 x2 => x1 ≤ x2) s ↔ Bounded (fun x1 x2 => x1 < x2) s

Tactic:
refine ⟨fun h => ?_, bounded_le_of_bounded_lt⟩

Result:
α : Type u_1
s : Set α
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
h : Bounded (fun x1 x2 => x1 ≤ x2) s
⊢ Bounded (fun x1 x2 => x1 < x2) s

Proof state:
α : Type u_1
s : Set α
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
h : Bounded (fun x1 x2 => x1 ≤ x2) s
⊢ Bounded (fun x1 x2 => x1 < x2) s

Tactic:
obtain ⟨a, ha⟩ := h

Result:
case intro
α : Type u_1
s : Set α
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
ha : ∀ b ∈ s, (fun x1 x2 => x1 ≤ x2) b a
⊢ Bounded (fun x1 x2 => x1 < x2) s
-- Mathlib/Order/Max.lean
theorem NoBotOrder.to_noMinOrder (α : Type*) [LinearOrder α] [NoBotOrder α] : NoMinOrder α :=
  { exists_lt := fun a => by simpa [not_le] using exists_not_ge a }

Proof state:
α : Type u_3
inst✝¹ : LinearOrder α
inst✝ : NoBotOrder α
a : α
⊢ ∃ b, b < a

Tactic:
simpa [not_le] using exists_not_ge a

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/IterateMapComap.lean
theorem ker_le_of_iterateMapComap_eq_succ (K : Submodule R N)
    (m : ℕ) (heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K)
    (hf : Surjective f) (hi : Injective i) : LinearMap.ker f ≤ K

Proof state:
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective ⇑f
hi : Injective ⇑i
⊢ ker f ≤ K

Tactic:
rw [show K = _ from f.iterateMapComap_eq_succ i K m heq hf hi 0]

Result:
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective ⇑f
hi : Injective ⇑i
⊢ ker f ≤ f.iterateMapComap i (0 + 1) K

Proof state:
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective ⇑f
hi : Injective ⇑i
⊢ ker f ≤ f.iterateMapComap i (0 + 1) K

Tactic:
exact f.ker_le_comap

Result:
no goals
-- Mathlib/Analysis/Complex/Schwarz.lean
theorem norm_deriv_le_div_of_mapsTo_ball (hd : DifferentiableOn ℂ f (ball c R₁))
    (h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)) (h₀ : 0 < R₁) : ‖deriv f c‖ ≤ R₂ / R₁

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
h₀ : 0 < R₁
⊢ ‖deriv f c‖ ≤ R₂ / R₁

Tactic:
simpa only [dslope_same] using norm_dslope_le_div_of_mapsTo_ball hd h_maps (mem_ball_self h₀)

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem IsCoseparating.isCodetecting [Balanced C] {𝒢 : Set C} :
    IsCoseparating 𝒢 → IsCodetecting 𝒢

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Balanced C
𝒢 : Set C
⊢ IsCoseparating 𝒢 → IsCodetecting 𝒢

Tactic:
simpa only [← isDetecting_op_iff, ← isSeparating_op_iff] using IsSeparating.isDetecting

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Swap.lean
/-- Multiplying with `swap R i j` on the right swaps the `j`-th column with the `i`-th column. -/
@[simp]
lemma mul_swap_apply_right (i j : n) (a : m) (g : Matrix m n R) :
    (g * swap R i j) a j = g a i

Proof state:
R : Type u_1
n : Type u_2
m : Type u_3
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
a : m
g : Matrix m n R
⊢ (g * swap R i j) a j = g a i

Tactic:
rw [swap_comm, mul_swap_apply_left]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem frequently_const {f : Filter α} [NeBot f] {p : Prop} : (∃ᶠ _ in f, p) ↔ p

Proof state:
α : Type u
f : Filter α
inst✝ : f.NeBot
p : Prop
⊢ (∃ᶠ (x : α) in f, p) ↔ p

Tactic:
by_cases p <;> simp [*]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem not_eq_false_eq_eq_true (a : Bool) : (not a = false) = (a = true)

Proof state:
a : Bool
⊢ ((!a) = false) = (a = true)

Tactic:
cases a <;> simp

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem tanh_conj : tanh (conj x) = conj (tanh x)

Proof state:
x : ℂ
⊢ tanh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (tanh x)

Tactic:
rw [tanh, sinh_conj, cosh_conj, ← map_div₀, tanh]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem midpoint_sub_add (x y : V) : midpoint R (x - y) (x + y) = x

Proof state:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R (x - y) (x + y) = x

Tactic:
rw [sub_eq_add_neg, ← vadd_eq_add, ← vadd_eq_add, ← midpoint_vadd_midpoint]

Result:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R x x +ᵥ midpoint R (-y) y = x

Proof state:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R x x +ᵥ midpoint R (-y) y = x

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Strong.lean
lemma UniformConvexOn.convexOn (hf : UniformConvexOn s φ f) (hφ : 0 ≤ φ) : ConvexOn ℝ s f

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
hφ : 0 ≤ φ
⊢ ConvexOn ℝ s f

Tactic:
simpa using hf.mono hφ

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
lemma neg_hom (α : Ext X Y n) : (-α).hom = -α.hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α : Ext X Y n
⊢ (-α).hom = -α.hom

Tactic:
rw [← add_right_inj α.hom, ← add_hom, add_neg_cancel, add_neg_cancel, zero_hom]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem sdiff_le_sdiff_of_sup_le_sup_left (h : c ⊔ a ≤ c ⊔ b) : a \ c ≤ b \ c

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
h : c ⊔ a ≤ c ⊔ b
⊢ (c ⊔ a) \ c ≤ (c ⊔ b) \ c

Tactic:
exact sdiff_le_sdiff_right h

Result:
no goals

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
h : c ⊔ a ≤ c ⊔ b
⊢ a \ c ≤ b \ c

Tactic:
rw [← sup_sdiff_left_self, ← @sup_sdiff_left_self _ _ _ b]

Result:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
h : c ⊔ a ≤ c ⊔ b
⊢ (c ⊔ a) \ c ≤ (c ⊔ b) \ c
-- Mathlib/Algebra/Ring/Pointwise/Finset.lean
@[simp]
lemma neg_smul_finset : -a • t = -(a • t)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Ring α
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : DecidableEq β
t : Finset β
a : α
⊢ -a • t = -(a • t)

Tactic:
simp only [← image_smul, ← image_neg_eq_neg, image_image, neg_smul, Function.comp_def]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
theorem iff_of_isAffine [IsAffine X] [IsAffine Y] :
    P f ↔ Q (f.appTop).hom

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ P f ↔ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
rw [iff_of_source_openCover (P := P) (Scheme.coverOfIsIso.{u} (𝟙 _))]

Result:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ (∀ (i : (Scheme.coverOfIsIso (𝟙 X)).J),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appTop ((Scheme.coverOfIsIso (𝟙 X)).map i ≫ f)))) ↔
    Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ (∀ (i : (Scheme.coverOfIsIso (𝟙 X)).J),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appTop ((Scheme.coverOfIsIso (𝟙 X)).map i ≫ f)))) ↔
    Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
simp

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem fin_succ {n} : Primrec (@Fin.succ n) :=
  fin_val_iff.1 <| by simp [succ.comp fin_val]

Proof state:
n : ℕ
⊢ Primrec fun a => ↑a.succ

Tactic:
simp [succ.comp fin_val]

Result:
no goals
-- Mathlib/Data/Matrix/Invertible.lean
theorem mul_invOf_cancel_left (A : Matrix n n α) (B : Matrix n m α) [Invertible A] :
    A * (⅟ A * B) = B

Proof state:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix n n α
B : Matrix n m α
inst✝ : Invertible A
⊢ A * (⅟A * B) = B

Tactic:
rw [← Matrix.mul_assoc, mul_invOf_self, Matrix.one_mul]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
protected lemma Topology.IsClosedEmbedding.inclusion (hst : s ⊆ t) (hs : IsClosed (t ↓∩ s)) :
    IsClosedEmbedding (inclusion hst) where
  toIsEmbedding := .inclusion _
  isClosed_range

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hst : s ⊆ t
hs : IsClosed (t ↓∩ s)
⊢ IsClosed (range (inclusion hst))

Tactic:
rwa [range_inclusion]

Result:
no goals