harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/MvPolynomial/PDeriv.lean
theorem pderiv_mul {i : σ} {f g : MvPolynomial σ R} :
    pderiv i (f * g) = pderiv i f * g + f * pderiv i g

Proof state:
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ (pderiv i) (f * g) = (pderiv i) f * g + f * (pderiv i) g

Tactic:
simp only [(pderiv i).leibniz f g, smul_eq_mul, mul_comm, add_comm]

Result:
no goals
-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem affineSpan_orthocenter_point_le_altitude (t : Triangle ℝ P) (i : Fin 3) :
    line[ℝ, t.orthocenter, t.points i] ≤ t.altitude i

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i : Fin 3
⊢ {t.orthocenter, t.points i} ⊆ ↑(altitude t i)

Tactic:
rw [Set.insert_subset_iff, Set.singleton_subset_iff]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i : Fin 3
⊢ t.orthocenter ∈ ↑(altitude t i) ∧ t.points i ∈ ↑(altitude t i)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i : Fin 3
⊢ t.orthocenter ∈ ↑(altitude t i) ∧ t.points i ∈ ↑(altitude t i)

Tactic:
exact ⟨t.orthocenter_mem_altitude, t.mem_altitude i⟩

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
t : Triangle ℝ P
i : Fin 3
⊢ affineSpan ℝ {t.orthocenter, t.points i} ≤ altitude t i

Tactic:
refine spanPoints_subset_coe_of_subset_coe ?_

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i : Fin 3
⊢ {t.orthocenter, t.points i} ⊆ ↑(altitude t i)
-- Mathlib/LinearAlgebra/Matrix/Trace.lean
lemma trace_blockDiagonal [DecidableEq p] (M : p → Matrix n n R) :
    trace (blockDiagonal M) = ∑ i, trace (M i)

Proof state:
n : Type u_3
p : Type u_4
R : Type u_6
inst✝³ : Fintype n
inst✝² : Fintype p
inst✝¹ : AddCommMonoid R
inst✝ : DecidableEq p
M : p → Matrix n n R
⊢ (blockDiagonal M).trace = ∑ i : p, (M i).trace

Tactic:
simp [blockDiagonal, trace, Finset.sum_comm (γ := n), Fintype.sum_prod_type]

Result:
no goals
-- Mathlib/Data/List/Infix.lean
theorem getElem_inits (l : List α) (n : Nat) (h : n < length (inits l)) :
    (inits l)[n] = l.take n

Proof state:
α : Type u_1
l : List α
n : ℕ
h : n < l.inits.length
⊢ l.inits[n] = take n l

Tactic:
induction l generalizing n with
| nil => simp
| cons a l ihl =>
  cases n with
  | zero => simp
  | succ n => simp [ihl]

Result:
no goals

Proof state:
case cons.zero
α : Type u_1
a : α
l : List α
ihl : ∀ (n : ℕ) (h : n < l.inits.length), l.inits[n] = take n l
h : 0 < (a :: l).inits.length
⊢ (a :: l).inits[0] = take 0 (a :: l)

Tactic:
simp

Result:
no goals

Proof state:
case nil
α : Type u_1
n : ℕ
h : n < [].inits.length
⊢ [].inits[n] = take n []

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
a : α
l : List α
ihl : ∀ (n : ℕ) (h : n < l.inits.length), l.inits[n] = take n l
n : ℕ
h : n < (a :: l).inits.length
⊢ (a :: l).inits[n] = take n (a :: l)

Tactic:
cases n with
| zero => simp
| succ n => simp [ihl]

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
a : α
l : List α
ihl : ∀ (n : ℕ) (h : n < l.inits.length), l.inits[n] = take n l
n : ℕ
h : n + 1 < (a :: l).inits.length
⊢ (a :: l).inits[n + 1] = take (n + 1) (a :: l)

Tactic:
simp [ihl]

Result:
no goals
-- Mathlib/NumberTheory/Rayleigh.lean
theorem hit_or_miss' (h : r > 0) :
    j ∈ {beattySeq' r k | k} ∨ ∃ k : ℤ, k ≤ j / r ∧ (j + 1) / r < k + 1

Proof state:
case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑⌊(↑j + 1) / r⌋ * r > ↑j
⊢ ↑j + 1 - 1 < ↑⌊(↑j + 1) / r⌋ * r ∧ ↑⌊(↑j + 1) / r⌋ * r ≤ ↑j + 1

Tactic:
constructor

Result:
case inr.left
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑⌊(↑j + 1) / r⌋ * r > ↑j
⊢ ↑j + 1 - 1 < ↑⌊(↑j + 1) / r⌋ * r

case inr.right
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑⌊(↑j + 1) / r⌋ * r > ↑j
⊢ ↑⌊(↑j + 1) / r⌋ * r ≤ ↑j + 1

Proof state:
case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑⌊(↑j + 1) / r⌋ * r > ↑j
⊢ j ∈ {x | ∃ k, beattySeq' r k = x} ∨ ∃ k, ↑k ≤ ↑j / r ∧ (↑j + 1) / r < ↑k + 1

Tactic:
refine Or.inl ⟨⌊(j + 1) / r⌋, ?_⟩

Result:
case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑⌊(↑j + 1) / r⌋ * r > ↑j
⊢ beattySeq' r ⌊(↑j + 1) / r⌋ = j

Proof state:
case inl
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑⌊(↑j + 1) / r⌋ * r ≤ ↑j
⊢ j ∈ {x | ∃ k, beattySeq' r k = x} ∨ ∃ k, ↑k ≤ ↑j / r ∧ (↑j + 1) / r < ↑k + 1

Tactic:
exact Or.inr ⟨⌊(j + 1) / r⌋, (le_div_iff₀ h).2 ‹_›, Int.lt_floor_add_one _⟩

Result:
no goals

Proof state:
case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑⌊(↑j + 1) / r⌋ * r > ↑j
⊢ beattySeq' r ⌊(↑j + 1) / r⌋ = j

Tactic:
rw [beattySeq', sub_eq_iff_eq_add, Int.ceil_eq_iff, Int.cast_add, Int.cast_one]

Result:
case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑⌊(↑j + 1) / r⌋ * r > ↑j
⊢ ↑j + 1 - 1 < ↑⌊(↑j + 1) / r⌋ * r ∧ ↑⌊(↑j + 1) / r⌋ * r ≤ ↑j + 1

Proof state:
case inr.right
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑⌊(↑j + 1) / r⌋ * r > ↑j
⊢ ↑⌊(↑j + 1) / r⌋ * r ≤ ↑j + 1

Tactic:
exact sub_nonneg.1 (Int.sub_floor_div_mul_nonneg (j + 1 : ℝ) h)

Result:
no goals

Proof state:
r : ℝ
j : ℤ
h : r > 0
⊢ j ∈ {x | ∃ k, beattySeq' r k = x} ∨ ∃ k, ↑k ≤ ↑j / r ∧ (↑j + 1) / r < ↑k + 1

Tactic:
cases le_or_gt (⌊(j + 1) / r⌋ * r) j

Result:
case inl
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑⌊(↑j + 1) / r⌋ * r ≤ ↑j
⊢ j ∈ {x | ∃ k, beattySeq' r k = x} ∨ ∃ k, ↑k ≤ ↑j / r ∧ (↑j + 1) / r < ↑k + 1

case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑⌊(↑j + 1) / r⌋ * r > ↑j
⊢ j ∈ {x | ∃ k, beattySeq' r k = x} ∨ ∃ k, ↑k ≤ ↑j / r ∧ (↑j + 1) / r < ↑k + 1

Proof state:
case inr.left
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑⌊(↑j + 1) / r⌋ * r > ↑j
⊢ ↑j + 1 - 1 < ↑⌊(↑j + 1) / r⌋ * r

Tactic:
rwa [add_sub_cancel_right]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/Datatypes.lean
theorem structuralIsoOfExpr_whiskerRight {f g : a ⟶ b} (h : b ⟶ c)
    (η : f ⟶ g) (η' : f ≅ g) (ih_η : η'.hom = η)  :
    (whiskerRightIso η' h).hom = η ▷ h

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f g : a ⟶ b
h : b ⟶ c
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
⊢ (whiskerRightIso η' h).hom = η ▷ h

Tactic:
simp [ih_η]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem isCycle_swap (hxy : x ≠ y) : IsCycle (swap x y) :=
  ⟨y, by rwa [swap_apply_right], fun a (ha : ite (a = x) y (ite (a = y) x a) ≠ a) =>
    if hya : y = a then ⟨0, hya⟩
    else
      ⟨1, by
        rw [zpow_one, swap_apply_def]
        split_ifs at * <;> tauto⟩⟩

Proof state:
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
⊢ (swap x y) y ≠ y

Tactic:
rwa [swap_apply_right]

Result:
no goals

Proof state:
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
⊢ (if y = x then y else if y = y then x else y) = a

Tactic:
split_ifs at * <;> tauto

Result:
no goals

Proof state:
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
⊢ (swap x y ^ 1) y = a

Tactic:
rw [zpow_one, swap_apply_def]

Result:
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
⊢ (if y = x then y else if y = y then x else y) = a
-- Mathlib/Topology/Order/Lattice.lean
lemma finset_sup_nhds [SemilatticeSup L] [OrderBot L] [ContinuousSup L]
    (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) : Tendsto (s.sup f) l (𝓝 (s.sup g))

Proof state:
case inl
L : Type u_1
inst✝³ : TopologicalSpace L
ι : Type u_3
α : Type u_4
f : ι → α → L
l : Filter α
g : ι → L
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
hs : ∀ i ∈ ∅, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (∅.sup f) l (𝓝 (∅.sup g))

Tactic:
simpa using tendsto_const_nhds

Result:
no goals

Proof state:
case inr
L : Type u_1
inst✝³ : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
hne : s.Nonempty
⊢ Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))

Tactic:
exact finset_sup'_nhds hne hs

Result:
no goals

Proof state:
case inr
L : Type u_1
inst✝³ : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
hne : s.Nonempty
⊢ Tendsto (s.sup f) l (𝓝 (s.sup g))

Tactic:
simp only [← sup'_eq_sup hne]

Result:
case inr
L : Type u_1
inst✝³ : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
hne : s.Nonempty
⊢ Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))

Proof state:
L : Type u_1
inst✝³ : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (s.sup f) l (𝓝 (s.sup g))

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hne

Result:
case inl
L : Type u_1
inst✝³ : TopologicalSpace L
ι : Type u_3
α : Type u_4
f : ι → α → L
l : Filter α
g : ι → L
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
hs : ∀ i ∈ ∅, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (∅.sup f) l (𝓝 (∅.sup g))

case inr
L : Type u_1
inst✝³ : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
hne : s.Nonempty
⊢ Tendsto (s.sup f) l (𝓝 (s.sup g))
-- Mathlib/LinearAlgebra/Goursat.lean
lemma goursatFst_toAddSubgroup :
    (goursatFst L).toAddSubgroup = L.toAddSubgroup.goursatFst

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
⊢ L.goursatFst.toAddSubgroup = L.toAddSubgroup.goursatFst

Tactic:
ext x

Result:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
x : M
⊢ x ∈ L.goursatFst.toAddSubgroup ↔ x ∈ L.toAddSubgroup.goursatFst

Proof state:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
x : M
⊢ x ∈ L.goursatFst.toAddSubgroup ↔ x ∈ L.toAddSubgroup.goursatFst

Tactic:
simp [mem_toAddSubgroup, goursatFst, AddSubgroup.mem_goursatFst]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray

Proof state:
case h
α : Type u_1
l : List α
a : α
⊢ (l.toArray.push a).toList = (l ++ [a]).toArray.toList

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
a : α
⊢ l.toArray.push a = (l ++ [a]).toArray

Tactic:
apply ext'

Result:
case h
α : Type u_1
l : List α
a : α
⊢ (l.toArray.push a).toList = (l ++ [a]).toArray.toList
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
theorem eval_det (M : Matrix n n R[X]) (r : R) :
    Polynomial.eval r M.det = (Polynomial.eval (scalar n r) (matPolyEquiv M)).det

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R[X]
r : R
⊢ (eval₂RingHom (RingHom.id R) r).mapMatrix M = eval ((scalar n) r) (matPolyEquiv M)

Tactic:
ext

Result:
case a
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R[X]
r : R
i✝ j✝ : n
⊢ (eval₂RingHom (RingHom.id R) r).mapMatrix M i✝ j✝ = eval ((scalar n) r) (matPolyEquiv M) i✝ j✝

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R[X]
r : R
⊢ ((eval₂RingHom (RingHom.id R) r).mapMatrix M).det = (eval ((scalar n) r) (matPolyEquiv M)).det

Tactic:
apply congr_arg det

Result:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R[X]
r : R
⊢ (eval₂RingHom (RingHom.id R) r).mapMatrix M = eval ((scalar n) r) (matPolyEquiv M)

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R[X]
r : R
⊢ eval r M.det = (eval ((scalar n) r) (matPolyEquiv M)).det

Tactic:
rw [Polynomial.eval, ← coe_eval₂RingHom, RingHom.map_det]

Result:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R[X]
r : R
⊢ ((eval₂RingHom (RingHom.id R) r).mapMatrix M).det = (eval ((scalar n) r) (matPolyEquiv M)).det

Proof state:
case a
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R[X]
r : R
i✝ j✝ : n
⊢ (eval₂RingHom (RingHom.id R) r).mapMatrix M i✝ j✝ = eval ((scalar n) r) (matPolyEquiv M) i✝ j✝

Tactic:
symm

Result:
case a
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R[X]
r : R
i✝ j✝ : n
⊢ eval ((scalar n) r) (matPolyEquiv M) i✝ j✝ = (eval₂RingHom (RingHom.id R) r).mapMatrix M i✝ j✝

Proof state:
case a
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R[X]
r : R
i✝ j✝ : n
⊢ eval ((scalar n) r) (matPolyEquiv M) i✝ j✝ = (eval₂RingHom (RingHom.id R) r).mapMatrix M i✝ j✝

Tactic:
exact matPolyEquiv_eval _ _ _ _

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem lcm_mul_left {m n k : ℕ} : (m * n).lcm (m * k) = m * n.lcm k

Proof state:
case a
m n k : ℕ
h : m ∣ (m * n).lcm (m * k)
⊢ m * n.lcm k ∣ (m * n).lcm (m * k)

Tactic:
rw [← dvd_div_iff_mul_dvd h, lcm_dvd_iff, dvd_div_iff_mul_dvd h, dvd_div_iff_mul_dvd h,
  ← lcm_dvd_iff]

Result:
no goals

Proof state:
case a
m n k : ℕ
⊢ m * n.lcm k ∣ (m * n).lcm (m * k)

Tactic:
have h : m ∣ lcm (m * n) (m * k) := (dvd_mul_right m n).trans (dvd_lcm_left (m * n) (m * k))

Result:
case a
m n k : ℕ
h : m ∣ (m * n).lcm (m * k)
⊢ m * n.lcm k ∣ (m * n).lcm (m * k)

Proof state:
case a
m n k : ℕ
⊢ (m * n).lcm (m * k) ∣ m * n.lcm k

Tactic:
exact lcm_dvd (mul_dvd_mul_left m (dvd_lcm_left n k)) (mul_dvd_mul_left m (dvd_lcm_right n k))

Result:
no goals

Proof state:
m n k : ℕ
⊢ (m * n).lcm (m * k) = m * n.lcm k

Tactic:
apply dvd_antisymm

Result:
case a
m n k : ℕ
⊢ (m * n).lcm (m * k) ∣ m * n.lcm k

case a
m n k : ℕ
⊢ m * n.lcm k ∣ (m * n).lcm (m * k)
-- Mathlib/Analysis/Convex/Function.lean
theorem convexOn_id {s : Set β} (hs : Convex 𝕜 s) : ConvexOn 𝕜 s _root_.id :=
  ⟨hs, by
    intros
    rfl⟩

Proof state:
𝕜 : Type u_1
β : Type u_5
inst✝² : OrderedSemiring 𝕜
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
s : Set β
hs : Convex 𝕜 s
x✝ : β
a✝⁵ : x✝ ∈ s
y✝ : β
a✝⁴ : y✝ ∈ s
a✝³ b✝ : 𝕜
a✝² : 0 ≤ a✝³
a✝¹ : 0 ≤ b✝
a✝ : a✝³ + b✝ = 1
⊢ _root_.id (a✝³ • x✝ + b✝ • y✝) ≤ a✝³ • _root_.id x✝ + b✝ • _root_.id y✝

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
β : Type u_5
inst✝² : OrderedSemiring 𝕜
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
s : Set β
hs : Convex 𝕜 s
⊢ ∀ ⦃x : β⦄,
    x ∈ s →
      ∀ ⦃y : β⦄,
        y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → _root_.id (a • x + b • y) ≤ a • _root_.id x + b • _root_.id y

Tactic:
intros

Result:
𝕜 : Type u_1
β : Type u_5
inst✝² : OrderedSemiring 𝕜
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
s : Set β
hs : Convex 𝕜 s
x✝ : β
a✝⁵ : x✝ ∈ s
y✝ : β
a✝⁴ : y✝ ∈ s
a✝³ b✝ : 𝕜
a✝² : 0 ≤ a✝³
a✝¹ : 0 ≤ b✝
a✝ : a✝³ + b✝ = 1
⊢ _root_.id (a✝³ • x✝ + b✝ • y✝) ≤ a✝³ • _root_.id x✝ + b✝ • _root_.id y✝
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_one : (1 : F[X]).natSepDegree = 0

Proof state:
F : Type u
inst✝ : Field F
⊢ natSepDegree 1 = 0

Tactic:
rw [← C_1, natSepDegree_C]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Lemmas.lean
theorem getElem_insertIdx_gt (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α)
    (k) (h' : k < (as.insertIdx i v).size) (h : i < k) :
    (as.insertIdx i v)[k] = as[k-1]'(by simp at h'; omega)

Proof state:
α : Type ?u.131818
as : Array α
i : Nat
h✝ : i ≤ as.size
v : α
k : Nat
h' : k < (as.insertIdx i v h✝).size
h : i < k
⊢ k - 1 < as.size

Tactic:
simp at h'

Result:
α : Type ?u.131818
as : Array α
i : Nat
h✝ : i ≤ as.size
v : α
k : Nat
h : i < k
h' : k < as.size + 1
⊢ k - 1 < as.size

Proof state:
α : Type u_1
as : Array α
i : Nat
h✝ : i ≤ as.size
v : α
k : Nat
h' : k < (as.insertIdx i v h✝).size
h : i < k
⊢ (as.insertIdx i v h✝)[k] = as[k - 1]

Tactic:
rw [getElem_insertIdx]

Result:
α : Type u_1
as : Array α
i : Nat
h✝ : i ≤ as.size
v : α
k : Nat
h' : k < (as.insertIdx i v h✝).size
h : i < k
⊢ (if h₁ : k < i then as[k] else if h₂ : k = i then v else as[k - 1]) = as[k - 1]

Proof state:
α : Type u_1
as : Array α
i : Nat
h✝ : i ≤ as.size
v : α
k : Nat
h' : k < (as.insertIdx i v h✝).size
h : i < k
⊢ ¬k = i

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.131818
as : Array α
i : Nat
h✝ : i ≤ as.size
v : α
k : Nat
h : i < k
h' : k < as.size + 1
⊢ k - 1 < as.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
as : Array α
i : Nat
h✝ : i ≤ as.size
v : α
k : Nat
h' : k < (as.insertIdx i v h✝).size
h : i < k
⊢ (if h₁ : k < i then as[k] else if h₂ : k = i then v else as[k - 1]) = as[k - 1]

Tactic:
rw [dif_neg (by omega), dif_neg (by omega)]

Result:
no goals

Proof state:
α : Type u_1
as : Array α
i : Nat
h✝ : i ≤ as.size
v : α
k : Nat
h' : k < (as.insertIdx i v h✝).size
h : i < k
⊢ ¬k < i

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem _root_.Array.mk_mkArray (a : α) (n : Nat) (h : (mkArray n a).size = m) :
    mk (Array.mkArray n a) h = (mkVector n a).cast (by simpa using h) := rfl

Proof state:
α : Type ?u.74792
m : Nat
a : α
n : Nat
h : (mkArray n a).size = m
⊢ n = m

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
theorem doublingGamma_eq_Gamma {s : ℝ} (hs : 0 < s) : doublingGamma s = Gamma s

Proof state:
s : ℝ
hs : 0 < s
y : ℝ
hy : 0 < y
⊢ 0 < y.doublingGamma

Tactic:
apply_rules [mul_pos, Gamma_pos_of_pos, add_pos, inv_pos_of_pos, rpow_pos_of_pos, two_pos,
  one_pos, sqrt_pos_of_pos pi_pos]

Result:
no goals

Proof state:
s : ℝ
hs : 0 < s
⊢ s.doublingGamma = Gamma s

Tactic:
refine
  eq_Gamma_of_log_convex doublingGamma_log_convex_Ioi
    (fun {y} hy => doublingGamma_add_one y hy.ne') (fun {y} hy => ?_) doublingGamma_one hs

Result:
s : ℝ
hs : 0 < s
y : ℝ
hy : 0 < y
⊢ 0 < y.doublingGamma
-- Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean
lemma transfiniteCompositions_le_llp_rlp :
    transfiniteCompositions.{w} W ≤ W.rlp.llp

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ transfiniteCompositions.{w, v, u} W ≤ W.rlp.llp

Tactic:
intro _ _ f hf

Result:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : transfiniteCompositions.{w, v, u} W f
⊢ W.rlp.llp f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : ∃ J x x_1 x_2, ∃ (x_3 : WellFoundedLT J), W.transfiniteCompositionsOfShape J f
⊢ W.rlp.llp f

Tactic:
obtain ⟨_, _, _, _, _, hf⟩ := hf

Result:
case intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
w✝⁴ : Type w
w✝³ : LinearOrder w✝⁴
w✝² : SuccOrder w✝⁴
w✝¹ : OrderBot w✝⁴
w✝ : WellFoundedLT w✝⁴
hf : W.transfiniteCompositionsOfShape w✝⁴ f
⊢ W.rlp.llp f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : transfiniteCompositions.{w, v, u} W f
⊢ W.rlp.llp f

Tactic:
rw [transfiniteCompositions_iff] at hf

Result:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : ∃ J x x_1 x_2, ∃ (x_3 : WellFoundedLT J), W.transfiniteCompositionsOfShape J f
⊢ W.rlp.llp f

Proof state:
case intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
w✝⁴ : Type w
w✝³ : LinearOrder w✝⁴
w✝² : SuccOrder w✝⁴
w✝¹ : OrderBot w✝⁴
w✝ : WellFoundedLT w✝⁴
hf : W.transfiniteCompositionsOfShape w✝⁴ f
⊢ W.rlp.llp f

Tactic:
exact W.transfiniteCompositionsOfShape_le_llp_rlp _ _ hf

Result:
no goals
-- Mathlib/RepresentationTheory/Basic.lean
theorem ofMulAction_apply {H : Type*} [MulAction G H] (g : G) (f : H →₀ k) (h : H) :
    ofMulAction k G H g f h = f (g⁻¹ • h)

Proof state:
k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
H : Type u_4
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
⊢ (((ofMulAction k G H) g) f) h = f (g⁻¹ • h)

Tactic:
conv_lhs => rw [← smul_inv_smul g h]

Result:
k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
H : Type u_4
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
⊢ (((ofMulAction k G H) g) f) (g • g⁻¹ • h) = f (g⁻¹ • h)

Proof state:
k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
H : Type u_4
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
⊢ (((ofMulAction k G H) g) f) (g • g⁻¹ • h) = f (g⁻¹ • h)

Tactic:
let h' := g⁻¹ • h

Result:
k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
H : Type u_4
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
⊢ (((ofMulAction k G H) g) f) (g • g⁻¹ • h) = f (g⁻¹ • h)

Proof state:
k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
H : Type u_4
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
⊢ (((ofMulAction k G H) g) f) (g • g⁻¹ • h) = f (g⁻¹ • h)

Tactic:
change ofMulAction k G H g f (g • h') = f h'

Result:
k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
H : Type u_4
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
⊢ (((ofMulAction k G H) g) f) (g • h') = f h'

Proof state:
k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
H : Type u_4
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
h₁ h₂ : H
⊢ (fun x => g • x) h₁ = (fun x => g • x) h₂ → h₁ = h₂

Tactic:
simp

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
H : Type u_4
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
⊢ Function.Injective fun x => g • x

Tactic:
intro h₁ h₂

Result:
k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
H : Type u_4
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
h₁ h₂ : H
⊢ (fun x => g • x) h₁ = (fun x => g • x) h₂ → h₁ = h₂

Proof state:
k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
H : Type u_4
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
hg : Function.Injective fun x => g • x
⊢ (((ofMulAction k G H) g) f) (g • h') = f h'

Tactic:
simp only [ofMulAction_def, Finsupp.lmapDomain_apply, Finsupp.mapDomain_apply, hg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Erase.lean
theorem eraseIdx_eq_dropLast (l : List α) (i : Nat) (h : i + 1 = l.length) :
    l.eraseIdx i = l.dropLast

Proof state:
α : Type u_1
l : List α
i : Nat
h : i + 1 = l.length
⊢ l.eraseIdx i = l.dropLast

Tactic:
simp [eraseIdx_eq_take_drop_succ, h]

Result:
α : Type u_1
l : List α
i : Nat
h : i + 1 = l.length
⊢ take i l = l.dropLast

Proof state:
α : Type u_1
l : List α
i : Nat
h : i + 1 = l.length
⊢ take i l = l.dropLast

Tactic:
rw [take_eq_dropLast h]

Result:
no goals