harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem generate_of_contains_isSplitEpi {R : Presieve X} (f : Y ⟶ X) [IsSplitEpi f] (hf : R f) :
    generate R = ⊤

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
R : Presieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
hf : R f
⊢ generate R = ⊤

Tactic:
rw [← id_mem_iff_eq_top]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
R : Presieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
hf : R f
⊢ (generate R).arrows (𝟙 X)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
R : Presieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
hf : R f
⊢ section_ f ≫ f = 𝟙 X

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
R : Presieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
hf : R f
⊢ (generate R).arrows (𝟙 X)

Tactic:
exact ⟨_, section_ f, f, hf, by simp⟩

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem isVonNBounded_add :
    IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs

Result:
case inl
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
t : Set E
⊢ IsVonNBounded 𝕜 (∅ + t) ↔ ∅ = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 ∅ ∧ IsVonNBounded 𝕜 t

case inr
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : s.Nonempty
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Proof state:
case inr
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : s.Nonempty
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
rcases t.eq_empty_or_nonempty with rfl | ht

Result:
case inr.inl
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
hs : s.Nonempty
⊢ IsVonNBounded 𝕜 (s + ∅) ↔ s = ∅ ∨ ∅ = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 ∅

case inr.inr
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : s.Nonempty
ht : t.Nonempty
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Proof state:
case inl
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
t : Set E
⊢ IsVonNBounded 𝕜 (∅ + t) ↔ ∅ = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 ∅ ∧ IsVonNBounded 𝕜 t

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : s.Nonempty
ht : t.Nonempty
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
simp [hs.ne_empty, ht.ne_empty, isVonNBounded_add_of_nonempty hs ht]

Result:
no goals

Proof state:
case inr.inl
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
hs : s.Nonempty
⊢ IsVonNBounded 𝕜 (s + ∅) ↔ s = ∅ ∨ ∅ = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 ∅

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Pi.lean
theorem iSup_range_single_eq_iInf_ker_proj {I J : Set ι} (hd : Disjoint I J)
    (hu : Set.univ ⊆ I ∪ J) (hI : Set.Finite I) :
    ⨆ i ∈ I, range (single R φ i) = ⨅ i ∈ J, ker (proj i : (∀ i, φ i) →ₗ[R] φ i)

Proof state:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : I.Finite
⊢ Set.univ ⊆ ↑hI.toFinset ∪ J

Tactic:
rwa [hI.coe_toFinset]

Result:
no goals

Proof state:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : I.Finite
⊢ ⨅ i ∈ J, ker (proj i) ≤ ⨆ i ∈ I, range (single R φ i)

Tactic:
have : Set.univ ⊆ ↑hI.toFinset ∪ J := by rwa [hI.coe_toFinset]

Result:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : I.Finite
this : Set.univ ⊆ ↑hI.toFinset ∪ J
⊢ ⨅ i ∈ J, ker (proj i) ≤ ⨆ i ∈ I, range (single R φ i)

Proof state:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : I.Finite
this : Set.univ ⊆ ↑hI.toFinset ∪ J
i : ι
⊢ ⨆ (_ : i ∈ hI.toFinset), range (single R φ i) ≤ ⨆ (_ : i ∈ I), range (single R φ i)

Tactic:
rw [Set.Finite.mem_toFinset]

Result:
no goals

Proof state:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : I.Finite
this : Set.univ ⊆ ↑hI.toFinset ∪ J
⊢ ⨅ i ∈ J, ker (proj i) ≤ ⨆ i ∈ I, range (single R φ i)

Tactic:
refine le_trans (iInf_ker_proj_le_iSup_range_single R φ this) (iSup_mono fun i => ?_)

Result:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : I.Finite
this : Set.univ ⊆ ↑hI.toFinset ∪ J
i : ι
⊢ ⨆ (_ : i ∈ hI.toFinset), range (single R φ i) ≤ ⨆ (_ : i ∈ I), range (single R φ i)

Proof state:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : I.Finite
⊢ ⨆ i ∈ I, range (single R φ i) = ⨅ i ∈ J, ker (proj i)

Tactic:
refine le_antisymm (iSup_range_single_le_iInf_ker_proj _ _ _ _ hd) ?_

Result:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : I.Finite
⊢ ⨅ i ∈ J, ker (proj i) ≤ ⨆ i ∈ I, range (single R φ i)
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem toNonUnitalSubalgebra_bot :
    (⊥ : NonUnitalStarSubalgebra R A).toNonUnitalSubalgebra = ⊥

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
⊢ ⊥.toNonUnitalSubalgebra = ⊥

Tactic:
ext x

Result:
case h
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
x : A
⊢ x ∈ ⊥.toNonUnitalSubalgebra ↔ x ∈ ⊥

Proof state:
case h
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
x : A
⊢ x ∈ ⊥.toNonUnitalSubalgebra ↔ x ∈ ⊥

Tactic:
simp only [mem_bot, NonUnitalStarSubalgebra.mem_toNonUnitalSubalgebra, NonUnitalAlgebra.mem_bot]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean
theorem go_get_aux (aig : AIG α) (n : Nat) (curr : Nat) (hcurr : curr ≤ n)
    (input : AIG.RefVec aig w) (s : AIG.RefVec aig (w * curr)) :
    ∀ (idx : Nat) (hidx : idx < w * curr),
        (go n input curr hcurr s).get idx (aux4 hidx hcurr)
          =
        s.get idx hidx

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx : idx < w * curr
h✝ : ¬curr < n
this : curr = n
⊢ (⋯ ▸ s).refs[idx] = s.refs[idx]

Tactic:
subst this

Result:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx : idx < w * curr
hcurr : curr ≤ curr
h✝ : ¬curr < curr
⊢ (⋯ ▸ s).refs[idx] = s.refs[idx]

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
⊢ ∀ (idx : Nat) (hidx : idx < w * curr), (go n input curr hcurr s).get idx ⋯ = s.get idx hidx

Tactic:
intro idx hidx

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx : idx < w * curr
⊢ (go n input curr hcurr s).get idx ⋯ = s.get idx hidx

Proof state:
case isTrue.hidx
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
n curr : Nat
hcurr : curr ≤ n
input : aig.RefVec w
s : aig.RefVec (w * curr)
idx : Nat
hidx : idx < w * curr
h✝ : curr < n
⊢ idx < w * curr + w

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
/-- Note this lemma can only be written about non-dependent tuples as `insertNth (last n) = snoc` is
not a definitional equality. -/
@[simp] lemma insertNthEquiv_last (n : ℕ) (α : Type*) :
    insertNthEquiv (fun _ ↦ α) (last n) = snocEquiv (fun _ ↦ α)

Proof state:
n : ℕ
α : Type u_3
⊢ insertNthEquiv (fun x => α) (last n) = snocEquiv fun x => α

Tactic:
ext

Result:
case H.h
n : ℕ
α : Type u_3
x✝¹ : α × (Fin n → α)
x✝ : Fin (n + 1)
⊢ (insertNthEquiv (fun x => α) (last n)) x✝¹ x✝ = (snocEquiv fun x => α) x✝¹ x✝

Proof state:
case H.h
n : ℕ
α : Type u_3
x✝¹ : α × (Fin n → α)
x✝ : Fin (n + 1)
⊢ (insertNthEquiv (fun x => α) (last n)) x✝¹ x✝ = (snocEquiv fun x => α) x✝¹ x✝

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
lemma jacobiTheta₂'_neg_left (z τ : ℂ) : jacobiTheta₂' (-z) τ = -jacobiTheta₂' z τ

Proof state:
z τ : ℂ
⊢ ∑' (c : ℤ), jacobiTheta₂'_term ((Equiv.neg ℤ) c) (-z) τ = ∑' (b : ℤ), -jacobiTheta₂'_term b z τ

Tactic:
congr 1 with n

Result:
case e_f.h
z τ : ℂ
n : ℤ
⊢ jacobiTheta₂'_term ((Equiv.neg ℤ) n) (-z) τ = -jacobiTheta₂'_term n z τ

Proof state:
case e_f.h
z τ : ℂ
n : ℤ
⊢ 2 * ↑π * I * ↑(-n) * cexp (2 * ↑π * I * ↑(-n) * -z + ↑π * I * ↑(-n) ^ 2 * τ) =
    -(2 * ↑π * I * ↑n) * cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)

Tactic:
push_cast

Result:
case e_f.h
z τ : ℂ
n : ℤ
⊢ 2 * ↑π * I * -↑n * cexp (2 * ↑π * I * -↑n * -z + ↑π * I * (-↑n) ^ 2 * τ) =
    -(2 * ↑π * I * ↑n) * cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)

Proof state:
case e_f.h
z τ : ℂ
n : ℤ
⊢ 2 * ↑π * I * ↑((Equiv.neg ℤ) n) * cexp (2 * ↑π * I * ↑((Equiv.neg ℤ) n) * -z + ↑π * I * ↑((Equiv.neg ℤ) n) ^ 2 * τ) =
    -(2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ))

Tactic:
rw [Equiv.neg_apply, ← neg_mul]

Result:
case e_f.h
z τ : ℂ
n : ℤ
⊢ 2 * ↑π * I * ↑(-n) * cexp (2 * ↑π * I * ↑(-n) * -z + ↑π * I * ↑(-n) ^ 2 * τ) =
    -(2 * ↑π * I * ↑n) * cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)

Proof state:
z τ : ℂ
⊢ jacobiTheta₂' (-z) τ = -jacobiTheta₂' z τ

Tactic:
rw [jacobiTheta₂', jacobiTheta₂', ← tsum_neg, ← (Equiv.neg ℤ).tsum_eq]

Result:
z τ : ℂ
⊢ ∑' (c : ℤ), jacobiTheta₂'_term ((Equiv.neg ℤ) c) (-z) τ = ∑' (b : ℤ), -jacobiTheta₂'_term b z τ

Proof state:
case e_f.h
z τ : ℂ
n : ℤ
⊢ 2 * ↑π * I * -↑n * cexp (2 * ↑π * I * -↑n * -z + ↑π * I * (-↑n) ^ 2 * τ) =
    -(2 * ↑π * I * ↑n) * cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)

Tactic:
ring_nf

Result:
no goals

Proof state:
case e_f.h
z τ : ℂ
n : ℤ
⊢ jacobiTheta₂'_term ((Equiv.neg ℤ) n) (-z) τ = -jacobiTheta₂'_term n z τ

Tactic:
simp only [jacobiTheta₂'_term, jacobiTheta₂_term]

Result:
case e_f.h
z τ : ℂ
n : ℤ
⊢ 2 * ↑π * I * ↑((Equiv.neg ℤ) n) * cexp (2 * ↑π * I * ↑((Equiv.neg ℤ) n) * -z + ↑π * I * ↑((Equiv.neg ℤ) n) ^ 2 * τ) =
    -(2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ))
-- Mathlib/Analysis/Convex/Mul.lean
lemma ConvexOn.smul_concaveOn' [OrderedSMul 𝕜 E] (hf : ConvexOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g)
    (hf₀ : ∀ ⦃x⦄, x ∈ s → f x ≤ 0) (hg₀ : ∀ ⦃x⦄, x ∈ s → 0 ≤ g x) (hfg : MonovaryOn f g s) :
    ConvexOn 𝕜 s (f • g)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : LinearOrderedCommRing 𝕜
inst✝⁹ : LinearOrderedCommRing E
inst✝⁸ : LinearOrderedAddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : OrderedSMul 𝕜 F
inst✝¹ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
inst✝ : OrderedSMul 𝕜 E
hf : ConvexOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
⊢ ConcaveOn 𝕜 s (f • -g)

Tactic:
exact hf.smul'' hg.neg hf₀ (fun x hx ↦ neg_nonpos.2 <| hg₀ hx) hfg.neg_right

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : LinearOrderedCommRing 𝕜
inst✝⁹ : LinearOrderedCommRing E
inst✝⁸ : LinearOrderedAddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : OrderedSMul 𝕜 F
inst✝¹ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
inst✝ : OrderedSMul 𝕜 E
hf : ConvexOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
⊢ ConvexOn 𝕜 s (f • g)

Tactic:
rw [← neg_concaveOn_iff, ← smul_neg]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : LinearOrderedCommRing 𝕜
inst✝⁹ : LinearOrderedCommRing E
inst✝⁸ : LinearOrderedAddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : OrderedSMul 𝕜 F
inst✝¹ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
inst✝ : OrderedSMul 𝕜 E
hf : ConvexOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
⊢ ConcaveOn 𝕜 s (f • -g)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_fill {w i : Nat} {v : Bool} :
    (fill w v).getMsbD i = (v && decide (i < w))

Proof state:
w i : Nat
v : Bool
⊢ (fill w v).getMsbD i = (v && decide (i < w))

Tactic:
by_cases h : v
<;> simp [h, BitVec.fill, BitVec.negOne_eq_allOnes]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Core.lean
theorem ind₂
    {motive : Quotient s₁ → Quotient s₂ → Prop}
    (h : (a : α) → (b : β) → motive (Quotient.mk s₁ a) (Quotient.mk s₂ b))
    (q₁ : Quotient s₁)
    (q₂ : Quotient s₂)
    : motive q₁ q₂

Proof state:
case a
α : Sort uA
β : Sort uB
s₁ : Setoid α
s₂ : Setoid β
motive : Quotient s₁ → Quotient s₂ → Prop
h : ∀ (a : α) (b : β), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)
q₂ : Quotient s₂
a✝ : α
⊢ motive (Quotient.mk s₁ a✝) q₂

Tactic:
induction q₂ using Quotient.ind

Result:
case a.a
α : Sort uA
β : Sort uB
s₁ : Setoid α
s₂ : Setoid β
motive : Quotient s₁ → Quotient s₂ → Prop
h : ∀ (a : α) (b : β), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)
a✝¹ : α
a✝ : β
⊢ motive (Quotient.mk s₁ a✝¹) (Quotient.mk s₂ a✝)

Proof state:
case a.a
α : Sort uA
β : Sort uB
s₁ : Setoid α
s₂ : Setoid β
motive : Quotient s₁ → Quotient s₂ → Prop
h : ∀ (a : α) (b : β), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)
a✝¹ : α
a✝ : β
⊢ motive (Quotient.mk s₁ a✝¹) (Quotient.mk s₂ a✝)

Tactic:
apply h

Result:
no goals

Proof state:
α : Sort uA
β : Sort uB
s₁ : Setoid α
s₂ : Setoid β
motive : Quotient s₁ → Quotient s₂ → Prop
h : ∀ (a : α) (b : β), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)
q₁ : Quotient s₁
q₂ : Quotient s₂
⊢ motive q₁ q₂

Tactic:
induction q₁ using Quotient.ind

Result:
case a
α : Sort uA
β : Sort uB
s₁ : Setoid α
s₂ : Setoid β
motive : Quotient s₁ → Quotient s₂ → Prop
h : ∀ (a : α) (b : β), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)
q₂ : Quotient s₂
a✝ : α
⊢ motive (Quotient.mk s₁ a✝) q₂
-- Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean
/-- Given two commutative squares
```
a --φ--> b --ψ--> c
|        |        |
v        v        v
R --f--> S --g--> T
```
such that `φ ≫ ψ` and `ψ` are strongly cartesian, then so is `φ`. -/
protected lemma of_comp [IsStronglyCartesian p g ψ] [IsStronglyCartesian p (f ≫ g) (φ ≫ ψ)]
    [IsHomLift p f φ] : IsStronglyCartesian p f φ where
  universal_property'

Proof state:
case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCartesian g ψ
inst✝¹ : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
⊢ ∀ (y : a' ⟶ a), (fun χ => p.IsHomLift h χ ∧ χ ≫ φ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (τ ≫ ψ)

Tactic:
intro π' ⟨hπ'₁, hπ'₂⟩

Result:
case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCartesian g ψ
inst✝¹ : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
π' : a' ⟶ a
hπ'₁ : p.IsHomLift h π'
hπ'₂ : π' ≫ φ = τ
⊢ π' = map p (f ≫ g) (φ ≫ ψ) ⋯ (τ ≫ ψ)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem exists_lt_succ_left' {p : (m : Nat) → (m < n + 1) → Prop} :
    (∃ m, ∃ (h : m < n + 1), p m h) ↔ p 0 (by omega) ∨ (∃ m, ∃ (h : m < n), p (m + 1) (by omega))

Proof state:
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ 0 < n + 1

Tactic:
omega

Result:
no goals

Proof state:
case mp
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ (∃ m h, p m h) → p 0 ⋯ ∨ ∃ m h, p (m + 1) ⋯

Tactic:
rintro ⟨_|m, h, w⟩

Result:
case mp.intro.zero.intro
n : Nat
p : (m : Nat) → m < n + 1 → Prop
h : 0 < n + 1
w : p 0 h
⊢ p 0 ⋯ ∨ ∃ m h, p (m + 1) ⋯

case mp.intro.succ.intro
n : Nat
p : (m : Nat) → m < n + 1 → Prop
m : Nat
h : m + 1 < n + 1
w : p (m + 1) h
⊢ p 0 ⋯ ∨ ∃ m h, p (m + 1) ⋯

Proof state:
n : Nat
p : (m : Nat) → m < n + 1 → Prop
m : Nat
h : m < n
⊢ m + 1 < n + 1

Tactic:
omega

Result:
no goals

Proof state:
n : Nat
p : (m : Nat) → m < n + 1 → Prop
w : p 0 ⋯
⊢ 0 < n + 1

Tactic:
omega

Result:
no goals

Proof state:
case mpr.inr.intro.intro
n : Nat
p : (m : Nat) → m < n + 1 → Prop
m : Nat
h : m < n
w : p (m + 1) ⋯
⊢ ∃ m h, p m h

Tactic:
exact ⟨m + 1, by omega, w⟩

Result:
no goals

Proof state:
n : Nat
p : (m : Nat) → m < n + 1 → Prop
m : Nat
h : m + 1 < n + 1
w : p (m + 1) h
⊢ m < n

Tactic:
omega

Result:
no goals

Proof state:
case mp.intro.succ.intro
n : Nat
p : (m : Nat) → m < n + 1 → Prop
m : Nat
h : m + 1 < n + 1
w : p (m + 1) h
⊢ p 0 ⋯ ∨ ∃ m h, p (m + 1) ⋯

Tactic:
exact .inr ⟨m, by omega, w⟩

Result:
no goals

Proof state:
n : Nat
p : (m : Nat) → m < n + 1 → Prop
m : Nat
h : m < n
w : p (m + 1) ⋯
⊢ m + 1 < n + 1

Tactic:
omega

Result:
no goals

Proof state:
case mpr.inl
n : Nat
p : (m : Nat) → m < n + 1 → Prop
w : p 0 ⋯
⊢ ∃ m h, p m h

Tactic:
exact ⟨0, by omega, w⟩

Result:
no goals

Proof state:
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ (∃ m h, p m h) ↔ p 0 ⋯ ∨ ∃ m h, p (m + 1) ⋯

Tactic:
constructor

Result:
case mp
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ (∃ m h, p m h) → p 0 ⋯ ∨ ∃ m h, p (m + 1) ⋯

case mpr
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ (p 0 ⋯ ∨ ∃ m h, p (m + 1) ⋯) → ∃ m h, p m h

Proof state:
case mpr
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ (p 0 ⋯ ∨ ∃ m h, p (m + 1) ⋯) → ∃ m h, p m h

Tactic:
rintro (w|⟨m, h, w⟩)

Result:
case mpr.inl
n : Nat
p : (m : Nat) → m < n + 1 → Prop
w : p 0 ⋯
⊢ ∃ m h, p m h

case mpr.inr.intro.intro
n : Nat
p : (m : Nat) → m < n + 1 → Prop
m : Nat
h : m < n
w : p (m + 1) ⋯
⊢ ∃ m h, p m h

Proof state:
case mp.intro.zero.intro
n : Nat
p : (m : Nat) → m < n + 1 → Prop
h : 0 < n + 1
w : p 0 h
⊢ p 0 ⋯ ∨ ∃ m h, p (m + 1) ⋯

Tactic:
exact .inl w

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem map_sub_range' (a s n : Nat) (h : a ≤ s) :
    map (· - a) (range' s n step) = range' (s - a) n step

Proof state:
case h
step a s n : Nat
h : a ≤ s
x : Nat
⊢ ((fun x => x - a) ∘ fun x => a + x) x = id x

Tactic:
apply Nat.add_sub_cancel_left

Result:
no goals

Proof state:
step a s n : Nat
h : a ≤ s
⊢ map (fun x => x - a) (range' s n step) = range' (s - a) n step

Tactic:
conv => lhs; rw [← Nat.add_sub_cancel' h]

Result:
step a s n : Nat
h : a ≤ s
⊢ map (fun x => x - a) (range' (a + (s - a)) n step) = range' (s - a) n step

Proof state:
step a s n : Nat
h : a ≤ s
⊢ map (fun x => x - a) (range' (a + (s - a)) n step) = range' (s - a) n step

Tactic:
rw [← map_add_range', map_map, (?_ : _∘_ = _), map_id]

Result:
step a s n : Nat
h : a ≤ s
⊢ ((fun x => x - a) ∘ fun x => a + x) = id

Proof state:
step a s n : Nat
h : a ≤ s
⊢ ((fun x => x - a) ∘ fun x => a + x) = id

Tactic:
funext x

Result:
case h
step a s n : Nat
h : a ≤ s
x : Nat
⊢ ((fun x => x - a) ∘ fun x => a + x) x = id x
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
lemma mul_eq_mul_of_div_eq_div (a c : G₀) (hb : b ≠ 0) (hd : d ≠ 0)
    (h : a / b = c / d) : a * d = c * b

Proof state:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
b d a c : G₀
hb : b ≠ 0
hd : d ≠ 0
h : a / b = c / d
⊢ a * d = c * b

Tactic:
rw [← mul_one a, ← div_self hb, ← mul_comm_div, h, div_mul_eq_mul_div, div_mul_cancel₀ _ hd]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem head_iota (n : Nat) (h) : (iota n).head h = n

Proof state:
case zero
h : iota 0 ≠ []
⊢ (iota 0).head h = 0

Tactic:
simp at h

Result:
no goals

Proof state:
n : Nat
h : iota n ≠ []
⊢ (iota n).head h = n

Tactic:
cases n with
| zero => simp at h
| succ n => simp

Result:
no goals

Proof state:
case succ
n : Nat
h : iota (n + 1) ≠ []
⊢ (iota (n + 1)).head h = n + 1

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Primorial.lean
theorem primorial_succ {n : ℕ} (hn1 : n ≠ 1) (hn : Odd n) : (n + 1)# = n#

Proof state:
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ (n + 1)# = n#

Tactic:
refine prod_congr ?_ fun _ _ ↦ rfl

Result:
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ filter (fun p => Nat.Prime p) (range (n + 1 + 1)) = filter (fun p => Nat.Prime p) (range (n + 1))

Proof state:
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ filter (fun p => Nat.Prime p) (range (n + 1 + 1)) = filter (fun p => Nat.Prime p) (range (n + 1))

Tactic:
rw [range_succ, filter_insert, if_neg fun h ↦ not_even_iff_odd.2 hn _]

Result:
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ Nat.Prime (n + 1) → Even n

Proof state:
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ Nat.Prime (n + 1) → Even n

Tactic:
exact fun h ↦ h.even_sub_one <| mt succ.inj hn1

Result:
no goals