harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem append_left_nil (u : Fin m → α) (v : Fin n → α) (hu : m = 0) :
    append u v = v ∘ Fin.cast (by rw [hu, Nat.zero_add])

Proof state:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
⊢ append u v = v ∘ Fin.cast ⋯

Tactic:
refine funext (Fin.addCases (fun l => ?_) fun r => ?_)

Result:
case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
l : Fin m
⊢ append u v (castAdd n l) = (v ∘ Fin.cast ⋯) (castAdd n l)

case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ append u v (natAdd m r) = (v ∘ Fin.cast ⋯) (natAdd m r)

Proof state:
case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ append u v (natAdd m r) = (v ∘ Fin.cast ⋯) (natAdd m r)

Tactic:
rw [append_right, Function.comp_apply]

Result:
case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ v r = v (Fin.cast ⋯ (natAdd m r))

Proof state:
m n : ℕ
α✝ : Fin (n + 1) → Sort u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ i.succ
i : Fin n
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
⊢ m + n = n

Tactic:
rw [hu, Nat.zero_add]

Result:
no goals

Proof state:
case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ ↑r = ↑(Fin.cast ⋯ (natAdd m r))

Tactic:
simp [hu]

Result:
no goals

Proof state:
case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ v r = v (Fin.cast ⋯ (natAdd m r))

Tactic:
refine congr_arg v (Fin.ext ?_)

Result:
case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ ↑r = ↑(Fin.cast ⋯ (natAdd m r))

Proof state:
case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
l : Fin m
⊢ append u v (castAdd n l) = (v ∘ Fin.cast ⋯) (castAdd n l)

Tactic:
exact (Fin.cast hu l).elim0

Result:
no goals
-- Mathlib/Algebra/Group/Action/Defs.lean
theorem smul_iterate (a : M) : ∀ n : ℕ, (a • · : α → α)^[n] = (a ^ n • ·)
  | 0 => by simp [funext_iff]
  | n + 1 => by ext; simp [smul_iterate, pow_succ, smul_smul]

Proof state:
M : Type u_1
α : Type u_5
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : M
n : ℕ
⊢ (fun x => a • x)^[n + 1] = fun x => a ^ (n + 1) • x

Tactic:
ext

Result:
case h
M : Type u_1
α : Type u_5
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : M
n : ℕ
x✝ : α
⊢ (fun x => a • x)^[n + 1] x✝ = a ^ (n + 1) • x✝

Proof state:
M : Type u_1
α : Type u_5
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : M
⊢ (fun x => a • x)^[0] = fun x => a ^ 0 • x

Tactic:
simp [funext_iff]

Result:
no goals

Proof state:
case h
M : Type u_1
α : Type u_5
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : M
n : ℕ
x✝ : α
⊢ (fun x => a • x)^[n + 1] x✝ = a ^ (n + 1) • x✝

Tactic:
simp [smul_iterate, pow_succ, smul_smul]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
/-- The left and right shift of cochains commute only up to a sign. -/
lemma leftShift_rightShift_eq_negOnePow_rightShift_leftShift
    (a n' n'' : ℤ) (hn' : n' + a = n) (hn'' : n + a = n'') :
    (γ.rightShift a n' hn').leftShift a n hn' =
      a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' n'' : ℤ
hn' : n' + a = n
hn'' : n + a = n''
⊢ (γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''

Tactic:
rw [leftShift_rightShift, rightShift_leftShift, smul_smul, ← hn'', add_comm n a, mul_add,
  Int.negOnePow_add, Int.negOnePow_add, Int.negOnePow_add, Int.negOnePow_mul_self,
  ← mul_assoc, ← mul_assoc, Int.units_mul_self, one_mul]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
theorem mul_le_mul_of_nonpos_right [ExistsAddOfLE α] [MulPosMono α]
    [AddRightMono α] [AddRightReflectLE α]
    (h : b ≤ a) (hc : c ≤ 0) : a * c ≤ b * c

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : Preorder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosMono α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
h : b ≤ a
hc : c ≤ 0
⊢ a * c ≤ b * c

Tactic:
obtain ⟨d, hcd⟩ := exists_add_of_le hc

Result:
case intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : Preorder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosMono α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
h : b ≤ a
hc : c ≤ 0
d : α
hcd : 0 = c + d
⊢ a * c ≤ b * c

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : Preorder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosMono α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
h : b ≤ a
hc : c ≤ 0
d : α
hcd : 0 = c + d
⊢ a * c + (b * d + a * d) = b * d

Tactic:
rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]

Result:
no goals

Proof state:
case intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : Preorder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosMono α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
h : b ≤ a
hc : c ≤ 0
d : α
hcd : 0 = c + d
⊢ a * c ≤ b * c

Tactic:
refine le_of_add_le_add_right (a := b * d + a * d) ?_

Result:
case intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : Preorder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosMono α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
h : b ≤ a
hc : c ≤ 0
d : α
hcd : 0 = c + d
⊢ a * c + (b * d + a * d) ≤ b * c + (b * d + a * d)

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : Preorder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosMono α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
h : b ≤ a
hc : c ≤ 0
d : α
hcd : 0 = c + d
⊢ a * d = b * c + (b * d + a * d)

Tactic:
rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]

Result:
no goals

Proof state:
case intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : Preorder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosMono α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
h : b ≤ a
hc : c ≤ 0
d : α
hcd : 0 = c + d
⊢ a * c + (b * d + a * d) ≤ b * c + (b * d + a * d)

Tactic:
calc
  _ = b * d := by rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
  _ ≤ a * d := mul_le_mul_of_nonneg_right h <| hcd.trans_le <| add_le_of_nonpos_left hc
  _ = _ := by rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem comp_sup_eq_sup_comp [SemilatticeSup γ] [OrderBot γ] {s : Finset β} {f : β → α} (g : α → γ)
    (g_sup : ∀ x y, g (x ⊔ y) = g x ⊔ g y) (bot : g ⊥ = ⊥) : g (s.sup f) = s.sup (g ∘ f) :=
  Finset.cons_induction_on s bot fun c t hc ih => by
    rw [sup_cons, sup_cons, g_sup, ih, Function.comp_apply]

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup γ
inst✝ : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : c ∉ t
ih : g (t.sup f) = t.sup (g ∘ f)
⊢ g ((cons c t hc).sup f) = (cons c t hc).sup (g ∘ f)

Tactic:
rw [sup_cons, sup_cons, g_sup, ih, Function.comp_apply]

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem openSegment_eq_image' (x y : E) :
    openSegment 𝕜 x y = (fun θ : 𝕜 => x + θ • (y - x)) '' Ioo (0 : 𝕜) 1

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
⊢ openSegment 𝕜 x y = (fun θ => x + θ • (y - x)) '' Ioo 0 1

Tactic:
convert openSegment_eq_image 𝕜 x y using 2

Result:
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Ioo 0 1
⊢ x + a✝¹ • (y - x) = (1 - a✝¹) • x + a✝¹ • y

Proof state:
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Ioo 0 1
⊢ x + (a✝¹ • y - a✝¹ • x) = x - a✝¹ • x + a✝¹ • y

Tactic:
abel

Result:
no goals

Proof state:
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Ioo 0 1
⊢ x + a✝¹ • (y - x) = (1 - a✝¹) • x + a✝¹ • y

Tactic:
simp only [smul_sub, sub_smul, one_smul]

Result:
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Ioo 0 1
⊢ x + (a✝¹ • y - a✝¹ • x) = x - a✝¹ • x + a✝¹ • y
-- Mathlib/Data/Finsupp/Defs.lean
theorem support_nonempty_iff {f : α →₀ M} : f.support.Nonempty ↔ f ≠ 0

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
⊢ f.support.Nonempty ↔ f ≠ 0

Tactic:
simp only [Finsupp.support_eq_empty, Finset.nonempty_iff_ne_empty, Ne]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
lemma reps_one_id (A : FixedDetMatrix (Fin 2) ℤ 1) (a1 : A.1 1 0 = 0) (a4 : 0 < A.1 0 0)
    (a6 : |A.1 0 1| < |(A.1 1 1)|) : A = (1 : SL(2, ℤ))

Proof state:
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : ↑A 1 0 = 0
a4 : 0 < ↑A 0 0
a6 : |↑A 0 1| < |↑A 1 1|
this : ↑A 0 0 = 1 ∧ ↑A 1 1 = 1 ∨ ↑A 0 0 = -1 ∧ ↑A 1 1 = -1
⊢ A = 1

Tactic:
ext i j

Result:
case h
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : ↑A 1 0 = 0
a4 : 0 < ↑A 0 0
a6 : |↑A 0 1| < |↑A 1 1|
this : ↑A 0 0 = 1 ∧ ↑A 1 1 = 1 ∨ ↑A 0 0 = -1 ∧ ↑A 1 1 = -1
i j : Fin 2
⊢ ↑A i j = ↑1 i j

Proof state:
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : ↑A 1 0 = 0
a4 : 0 < ↑A 0 0
a6 : |↑A 0 1| < |↑A 1 1|
⊢ A = 1

Tactic:
have := Int.mul_eq_one_iff_eq_one_or_neg_one.mp (A_c_eq_zero a1)

Result:
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : ↑A 1 0 = 0
a4 : 0 < ↑A 0 0
a6 : |↑A 0 1| < |↑A 1 1|
this : ↑A 0 0 = 1 ∧ ↑A 1 1 = 1 ∨ ↑A 0 0 = -1 ∧ ↑A 1 1 = -1
⊢ A = 1

Proof state:
case h
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : ↑A 1 0 = 0
a4 : 0 < ↑A 0 0
a6 : |↑A 0 1| < |↑A 1 1|
this : ↑A 0 0 = 1 ∧ ↑A 1 1 = 1 ∨ ↑A 0 0 = -1 ∧ ↑A 1 1 = -1
i j : Fin 2
⊢ ↑A i j = ↑1 i j

Tactic:
fin_cases i <;> fin_cases j <;> aesop

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem A_mono (L : F) (r : ℝ) {ε δ : ℝ} (h : ε ≤ δ) : A f L r ε ⊆ A f L r δ

Proof state:
case intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
L : F
r ε δ : ℝ
h : ε ≤ δ
x r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
y : ℝ
hy : y ∈ Icc x (x + r')
z : ℝ
hz : z ∈ Icc x (x + r')
⊢ 0 ≤ r

Tactic:
linarith [hy.1, hy.2, r'r.2]

Result:
no goals

Proof state:
case intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
L : F
r ε δ : ℝ
h : ε ≤ δ
x r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
⊢ x ∈ A f L r δ

Tactic:
refine ⟨r', r'r, fun y hy z hz => (hr' y hy z hz).trans (mul_le_mul_of_nonneg_right h ?_)⟩

Result:
case intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
L : F
r ε δ : ℝ
h : ε ≤ δ
x r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
y : ℝ
hy : y ∈ Icc x (x + r')
z : ℝ
hz : z ∈ Icc x (x + r')
⊢ 0 ≤ r

Proof state:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
L : F
r ε δ : ℝ
h : ε ≤ δ
⊢ A f L r ε ⊆ A f L r δ

Tactic:
rintro x ⟨r', r'r, hr'⟩

Result:
case intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
L : F
r ε δ : ℝ
h : ε ≤ δ
x r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
⊢ x ∈ A f L r δ
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
/-- The exponent of a generalized eigenvalue is never 0. -/
lemma HasUnifEigenvalue.exp_ne_zero {f : End R M} {μ : R} {k : ℕ}
    (h : f.HasUnifEigenvalue μ k) : k ≠ 0

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : f.HasUnifEigenvalue μ ↑k
⊢ k ≠ 0

Tactic:
rintro rfl

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
h : f.HasUnifEigenvalue μ ↑0
⊢ False

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
h : f.HasUnifEigenvalue μ ↑0
⊢ False

Tactic:
simp [HasUnifEigenvalue, Nat.cast_zero, genEigenspace_zero] at h

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Prod.lean
theorem prod_atTop_atTop_eq [Preorder α] [Preorder β] :
    (atTop : Filter α) ×ˢ (atTop : Filter β) = (atTop : Filter (α × β))

Proof state:
case inr.inr
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ atTop ×ˢ atTop = atTop

Tactic:
simpa [atTop, prod_iInf_left, prod_iInf_right, iInf_prod] using iInf_comm

Result:
no goals

Proof state:
case inr
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝ : Nonempty α
⊢ atTop ×ˢ atTop = atTop

Tactic:
cases isEmpty_or_nonempty β

Result:
case inr.inl
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ atTop ×ˢ atTop = atTop

case inr.inr
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ atTop ×ˢ atTop = atTop

Proof state:
case inl
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝ : IsEmpty α
⊢ atTop ×ˢ atTop = atTop

Tactic:
subsingleton

Result:
no goals

Proof state:
case inr.inl
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ atTop ×ˢ atTop = atTop

Tactic:
subsingleton

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ atTop ×ˢ atTop = atTop

Tactic:
cases isEmpty_or_nonempty α

Result:
case inl
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝ : IsEmpty α
⊢ atTop ×ˢ atTop = atTop

case inr
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝ : Nonempty α
⊢ atTop ×ˢ atTop = atTop
-- Mathlib/Computability/TMToPartrec.lean
theorem codeSupp'_self (c k) : trStmts₁ (trNormal c k) ⊆ codeSupp' c k

Proof state:
case tail
k : Cont'
⊢ trStmts₁ (trNormal Code.tail k) ⊆ codeSupp' Code.tail k

Tactic:
rfl

Result:
no goals

Proof state:
c : Code
k : Cont'
⊢ trStmts₁ (trNormal c k) ⊆ codeSupp' c k

Tactic:
cases c <;> first | rfl | exact Finset.union_subset_left (fun _ a ↦ a)

Result:
no goals

Proof state:
case fix
k : Cont'
a✝ : Code
⊢ trStmts₁ (trNormal a✝.fix k) ⊆ codeSupp' a✝.fix k

Tactic:
exact Finset.union_subset_left (fun _ a ↦ a)

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasDerivWithinAt.comp (hh₂ : HasDerivWithinAt h₂ h₂' s' (h x))
    (hh : HasDerivWithinAt h h' s x) (hst : MapsTo h s s') :
    HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
hh₂ : HasDerivWithinAt h₂ h₂' s' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s s'
⊢ HasDerivWithinAt (h₂ ∘ h) (h' * h₂') s x

Tactic:
exact hh₂.scomp x hh hst

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
hh₂ : HasDerivWithinAt h₂ h₂' s' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s s'
⊢ HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Tactic:
rw [mul_comm]

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
hh₂ : HasDerivWithinAt h₂ h₂' s' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s s'
⊢ HasDerivWithinAt (h₂ ∘ h) (h' * h₂') s x
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
lemma negPart_eq_neg (a : A) : a⁻ = -a ↔ a ≤ 0

Proof state:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : a ≤ 0
⊢ a = -a⁻

Tactic:
rw [← neg_nonneg] at ha

Result:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ -a
⊢ a = -a⁻

Proof state:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ -a
⊢ a = -a⁻

Tactic:
rw [negPart_def, ← cfcₙ_neg]

Result:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ -a
⊢ a = cfcₙ (fun x => -x⁻) a
-- Mathlib/Analysis/Convex/Jensen.lean
/-- A form of the **equality case of Jensen's equality**.

For a strictly convex function `f` and positive weights `w`, if
`f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)`, then the points `p` are all equal.

See also `StrictConvexOn.map_sum_eq_iff`. -/
lemma StrictConvexOn.eq_of_le_map_sum (hf : StrictConvexOn 𝕜 s f) (h₀ : ∀ i ∈ t, 0 < w i)
    (h₁ : ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s)
    (h_eq : ∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, w i • p i)) :
    ∀ ⦃j⦄, j ∈ t → ∀ ⦃k⦄, k ∈ t → p j = p k

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
h_eq : ∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, w i • p i)
this : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k
⊢ False

Tactic:
exact h_eq.not_lt <| hf.map_sum_lt h₀ h₁ hmem this

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
h_eq : ∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, w i • p i)
⊢ ∀ ⦃j : ι⦄, j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k

Tactic:
by_contra!

Result:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
h_eq : ∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, w i • p i)
this : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k
⊢ False
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem eval_tensorHom {f g h i : C}
    {η η' : f ⟶ g} {θ θ' : h ⟶ i} {ι : f ⊗ h ⟶ g ⊗ i}
    (e_η : η = η') (e_θ : θ = θ') (e_ι : η' ⊗ θ' = ι) :
    η ⊗ θ = ι

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i : C
η η' : f ⟶ g
θ θ' : h ⟶ i
ι : f ⊗ h ⟶ g ⊗ i
e_η : η = η'
e_θ : θ = θ'
e_ι : η' ⊗ θ' = ι
⊢ η ⊗ θ = ι

Tactic:
simp [e_η, e_θ, e_ι]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigO.mul_isLittleO {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜} (h₁ : f₁ =O[l] g₁) (h₂ : f₂ =o[l] g₂) :
    (fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x

Proof state:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → 𝕜
h₁ : f₁ =O[l] g₁
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂
c : ℝ
cpos : 0 < c
⊢ IsBigOWith c l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x

Tactic:
rcases h₁.exists_pos with ⟨c', c'pos, hc'⟩

Result:
case intro.intro
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → 𝕜
h₁ : f₁ =O[l] g₁
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂
c : ℝ
cpos : 0 < c
c' : ℝ
c'pos : c' > 0
hc' : IsBigOWith c' l f₁ g₁
⊢ IsBigOWith c l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x

Proof state:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → 𝕜
h₁ : f₁ =O[l] g₁
h₂ : f₂ =o[l] g₂
⊢ (fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x

Tactic:
simp only [IsLittleO_def] at *

Result:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → 𝕜
h₁ : f₁ =O[l] g₁
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂
⊢ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x

Proof state:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → 𝕜
h₁ : f₁ =O[l] g₁
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂
⊢ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x

Tactic:
intro c cpos

Result:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → 𝕜
h₁ : f₁ =O[l] g₁
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂
c : ℝ
cpos : 0 < c
⊢ IsBigOWith c l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x

Proof state:
case intro.intro
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → 𝕜
h₁ : f₁ =O[l] g₁
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂
c : ℝ
cpos : 0 < c
c' : ℝ
c'pos : c' > 0
hc' : IsBigOWith c' l f₁ g₁
⊢ IsBigOWith c l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x

Tactic:
exact (hc'.mul (h₂ (div_pos cpos c'pos))).congr_const (mul_div_cancel₀ _ (ne_of_gt c'pos))

Result:
no goals
-- Mathlib/GroupTheory/Exponent.lean
theorem exponent_eq_iSup_orderOf' :
    exponent G = if ∃ g : G, orderOf g = 0 then 0 else ⨆ g : G, orderOf g

Proof state:
G : Type u
inst✝ : CommMonoid G
⊢ exponent G = if ∃ g, orderOf g = 0 then 0 else ⨆ g, orderOf g

Tactic:
split_ifs with h

Result:
case pos
G : Type u
inst✝ : CommMonoid G
h : ∃ g, orderOf g = 0
⊢ exponent G = 0

case neg
G : Type u
inst✝ : CommMonoid G
h : ¬∃ g, orderOf g = 0
⊢ exponent G = ⨆ g, orderOf g

Proof state:
case neg
G : Type u
inst✝ : CommMonoid G
h : ¬∃ g, orderOf g = 0
⊢ exponent G = ⨆ g, orderOf g

Tactic:
have := not_exists.mp h

Result:
case neg
G : Type u
inst✝ : CommMonoid G
h : ¬∃ g, orderOf g = 0
this : ∀ (x : G), ¬orderOf x = 0
⊢ exponent G = ⨆ g, orderOf g

Proof state:
case neg
G : Type u
inst✝ : CommMonoid G
h : ¬∃ g, orderOf g = 0
this : ∀ (x : G), ¬orderOf x = 0
⊢ exponent G = ⨆ g, orderOf g

Tactic:
exact exponent_eq_iSup_orderOf fun g => Ne.bot_lt <| this g

Result:
no goals

Proof state:
case pos
G : Type u
inst✝ : CommMonoid G
h : ∃ g, orderOf g = 0
⊢ exponent G = 0

Tactic:
obtain ⟨g, hg⟩ := h

Result:
case pos.intro
G : Type u
inst✝ : CommMonoid G
g : G
hg : orderOf g = 0
⊢ exponent G = 0

Proof state:
case pos.intro
G : Type u
inst✝ : CommMonoid G
g : G
hg : orderOf g = 0
⊢ exponent G = 0

Tactic:
exact exponent_eq_zero_of_order_zero hg

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Currying.lean
lemma flip_injective {F₁ F₂ : B ⥤ C ⥤ D} (h : F₁.flip = F₂.flip) :
    F₁ = F₂

Proof state:
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F₁ F₂ : B ⥤ C ⥤ D
h : F₁.flip = F₂.flip
⊢ F₁ = F₂

Tactic:
rw [← flip_flip F₁, ← flip_flip F₂, h]

Result:
no goals