harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/Between.lean
theorem wbtw_or_wbtw_smul_vadd_of_nonpos (x : P) (v : V) {r₁ r₂ : R} (hr₁ : r₁ ≤ 0) (hr₂ : r₂ ≤ 0) :
    Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ 0
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
rcases le_total r₁ r₂ with (h | h)

Result:
case inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ 0
h : r₁ ≤ r₂
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

case inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ 0
h : r₂ ≤ r₁
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Proof state:
case inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ 0
h : r₂ ≤ r₁
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
exact Or.inl (wbtw_smul_vadd_smul_vadd_of_nonpos_of_le x v hr₁ h)

Result:
no goals

Proof state:
case inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ 0
h : r₁ ≤ r₂
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
exact Or.inr (wbtw_smul_vadd_smul_vadd_of_nonpos_of_le x v hr₂ h)

Result:
no goals
-- Mathlib/Topology/UniformSpace/HeineCantor.lean
theorem Continuous.uniformContinuous_of_tendsto_cocompact {f : α → β} {x : β}
    (h_cont : Continuous f) (hx : Tendsto f (cocompact α) (𝓝 x)) : UniformContinuous f :=
  uniformContinuous_def.2 fun r hr => by
    obtain ⟨t, ht, htsymm, htr⟩ := comp_symm_mem_uniformity_sets hr
    obtain ⟨s, hs, hst⟩ := mem_cocompact.1 (hx <| mem_nhds_left _ ht)
    apply
      mem_of_superset
        (symmetrize_mem_uniformity <|
          (hs.uniformContinuousAt_of_continuousAt f fun _ _ => h_cont.continuousAt) <|
            symmetrize_mem_uniformity hr)
    rintro ⟨b₁, b₂⟩ h
    by_cases h₁ : b₁ ∈ s; · exact (h.1 h₁).1
    by_cases h₂ : b₂ ∈ s; · exact (h.2 h₂).2
    apply htr
    exact ⟨x, htsymm.mk_mem_comm.1 (hst h₁), hst h₂⟩

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
⊢ {x | (f x.1, f x.2) ∈ r} ∈ 𝓤 α

Tactic:
apply
  mem_of_superset
    (symmetrize_mem_uniformity <|
      (hs.uniformContinuousAt_of_continuousAt f fun _ _ => h_cont.continuousAt) <|
        symmetrize_mem_uniformity hr)

Result:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
⊢ symmetrizeRel {x | x.1 ∈ s → (f x.1, f x.2) ∈ symmetrizeRel r} ⊆ {x | (f x.1, f x.2) ∈ r}

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
⊢ symmetrizeRel {x | x.1 ∈ s → (f x.1, f x.2) ∈ symmetrizeRel r} ⊆ {x | (f x.1, f x.2) ∈ r}

Tactic:
rintro ⟨b₁, b₂⟩ h

Result:
case intro.intro.intro.intro.intro.mk
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
x : β
h_cont : Continuous f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y | (x, y) ∈ t}
b₁ b₂ : α
h : (b₁, b₂) ∈ symmetrizeRel {x | x.1 ∈ s → (f x.1, f x.2) ∈ symmetrizeRel r}
⊢ (b₁, b₂) ∈ {x | (f x.1, f x.2) ∈ r}
-- Mathlib/SetTheory/Nimber/Field.lean
theorem mul_ne_of_lt : ∀ a' < a, ∀ b' < b, a' * b + a * b' + a' * b' ≠ a * b

Proof state:
a b : Nimber
H :
  sInf {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ ∈
    {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ
⊢ ∀ a' < a, ∀ b' < b, a' * b + a * b' + a' * b' ≠ a * b

Tactic:
rw [← mul_def] at H

Result:
a b : Nimber
H : a * b ∈ {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ
⊢ ∀ a' < a, ∀ b' < b, a' * b + a * b' + a' * b' ≠ a * b

Proof state:
a b : Nimber
⊢ ∀ a' < a, ∀ b' < b, a' * b + a * b' + a' * b' ≠ a * b

Tactic:
have H := csInf_mem (mul_nonempty a b)

Result:
a b : Nimber
H :
  sInf {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ ∈
    {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ
⊢ ∀ a' < a, ∀ b' < b, a' * b + a * b' + a' * b' ≠ a * b

Proof state:
a b : Nimber
H : a * b ∈ {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ
⊢ ∀ a' < a, ∀ b' < b, a' * b + a * b' + a' * b' ≠ a * b

Tactic:
simpa using H

Result:
no goals
-- Mathlib/Tactic/NormNum/GCD.lean
theorem isNat_ratDen : ∀ {q : ℚ} {n : ℤ} {n' : ℕ} {d : ℕ},
    IsRat q n d → n.natAbs = n' → n'.gcd d = 1 → IsNat q.den d
  | _, n, _, d, ⟨hi, rfl⟩, rfl, h => by
    constructor
    have : 0 < d := Nat.pos_iff_ne_zero.mpr <| by simpa using hi.ne_zero
    simp_rw [Rat.mul_den, Rat.intCast_den, invOf_eq_inv,
      Rat.inv_natCast_den_of_pos this, Rat.inv_natCast_num_of_pos this,
      Rat.intCast_num, one_mul, mul_one, Nat.cast_id, h, Nat.div_one]

Proof state:
n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
⊢ IsNat (↑n * ⅟↑d).den d

Tactic:
constructor

Result:
case out
n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
⊢ (↑n * ⅟↑d).den = ↑d

Proof state:
case out
n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
this : 0 < d
⊢ (↑n * ⅟↑d).den = ↑d

Tactic:
simp_rw [Rat.mul_den, Rat.intCast_den, invOf_eq_inv,
  Rat.inv_natCast_den_of_pos this, Rat.inv_natCast_num_of_pos this,
  Rat.intCast_num, one_mul, mul_one, Nat.cast_id, h, Nat.div_one]

Result:
no goals

Proof state:
n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
⊢ d ≠ 0

Tactic:
simpa using hi.ne_zero

Result:
no goals

Proof state:
case out
n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
⊢ (↑n * ⅟↑d).den = ↑d

Tactic:
have : 0 < d := Nat.pos_iff_ne_zero.mpr <| by simpa using hi.ne_zero

Result:
case out
n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
this : 0 < d
⊢ (↑n * ⅟↑d).den = ↑d
-- Mathlib/Data/Int/Init.lean
theorem le_induction_down {P : ℤ → Prop} {m : ℤ} (h0 : P m)
    (h1 : ∀ n : ℤ, n ≤ m → P n → P (n - 1)) (n : ℤ) : n ≤ m → P n :=
  Int.inductionOn' n m (fun _ ↦ h0) (fun k hle _ hle' ↦ by omega)
    fun k hle hi _ ↦ h1 k hle (hi hle)

Proof state:
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), n ≤ m → P n → P (n - 1)
n k : ℤ
hle : m ≤ k
x✝ : k ≤ m → P k
hle' : k + 1 ≤ m
⊢ P (k + 1)

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Basic.lean
theorem isZero_of_subsingleton (M : ModuleCat R) [Subsingleton M] : IsZero M where
  unique_to X := ⟨⟨⟨ofHom (0 : M →ₗ[R] X)⟩, fun f => by
    ext x
    rw [Subsingleton.elim x (0 : M)]
    dsimp
    simp⟩⟩
  unique_from X := ⟨⟨⟨ofHom (0 : X →ₗ[R] M)⟩, fun f => by
    ext x
    subsingleton⟩⟩

Proof state:
case hf.h
R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : X ⟶ M
x : ↑X
⊢ (Hom.hom f) x = (Hom.hom default) x

Tactic:
subsingleton

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : X ⟶ M
⊢ f = default

Tactic:
ext x

Result:
case hf.h
R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : X ⟶ M
x : ↑X
⊢ (Hom.hom f) x = (Hom.hom default) x

Proof state:
R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : M ⟶ X
⊢ f = default

Tactic:
ext x

Result:
case hf.h
R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : M ⟶ X
x : ↑M
⊢ (Hom.hom f) x = (Hom.hom default) x

Proof state:
case hf.h
R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : M ⟶ X
x : ↑M
⊢ (Hom.hom f) 0 = (Hom.hom default) 0

Tactic:
dsimp

Result:
case hf.h
R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : M ⟶ X
x : ↑M
⊢ (Hom.hom f) 0 = 0

Proof state:
case hf.h
R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : M ⟶ X
x : ↑M
⊢ (Hom.hom f) x = (Hom.hom default) x

Tactic:
rw [Subsingleton.elim x (0 : M)]

Result:
case hf.h
R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : M ⟶ X
x : ↑M
⊢ (Hom.hom f) 0 = (Hom.hom default) 0

Proof state:
case hf.h
R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : M ⟶ X
x : ↑M
⊢ (Hom.hom f) 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem firstDiffPos_eq (a b : String) :
    firstDiffPos a b = ⟨utf8Len (List.takeWhile₂ (· = ·) a.1 b.1).1⟩

Proof state:
a b : String
⊢ a.firstDiffPos b = { byteIdx := utf8Len (List.takeWhile₂ (fun x1 x2 => decide (x1 = x2)) a.data b.data).fst }

Tactic:
simpa [firstDiffPos] using
  firstDiffPos_loop_eq [] [] a.1 b.1 ((utf8Len a.1).min (utf8Len b.1)) 0 rfl rfl (by simp)

Result:
no goals

Proof state:
a b : String
⊢ (utf8Len a.data).min (utf8Len b.data) = min (utf8Len [] + utf8Len a.data) (utf8Len [] + utf8Len b.data)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Analytic/Composition.lean
theorem compAlongComposition_nnnorm {n : ℕ} (q : FormalMultilinearSeries 𝕜 F G)
    (p : FormalMultilinearSeries 𝕜 E F) (c : Composition n) :
    ‖q.compAlongComposition p c‖₊ ≤ ‖q c.length‖₊ * ∏ i, ‖p (c.blocksFun i)‖₊

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
⊢ ‖q.compAlongComposition p c‖ ≤ ‖q c.length‖ * ∏ x : Fin c.length, ‖p (c.blocksFun x)‖

Tactic:
exact q.compAlongComposition_norm p c

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
⊢ ‖q.compAlongComposition p c‖₊ ≤ ‖q c.length‖₊ * ∏ i : Fin c.length, ‖p (c.blocksFun i)‖₊

Tactic:
rw [← NNReal.coe_le_coe]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
⊢ ↑‖q.compAlongComposition p c‖₊ ≤ ↑(‖q c.length‖₊ * ∏ i : Fin c.length, ‖p (c.blocksFun i)‖₊)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
⊢ ↑‖q.compAlongComposition p c‖₊ ≤ ↑(‖q c.length‖₊ * ∏ i : Fin c.length, ‖p (c.blocksFun i)‖₊)

Tactic:
push_cast

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
⊢ ‖q.compAlongComposition p c‖ ≤ ‖q c.length‖ * ∏ x : Fin c.length, ‖p (c.blocksFun x)‖
-- Mathlib/Algebra/Ring/Int/Defs.lean
@[simp, norm_cast]
lemma cast_mul {α : Type*} [NonAssocRing α] : ∀ m n, ((m * n : ℤ) : α) = m * n := fun m => by
  obtain ⟨m, rfl | rfl⟩ := Int.eq_nat_or_neg m
  · induction m with
    | zero => simp
    | succ m ih => simp_all [add_mul]
  · induction m with
    | zero => simp
    | succ m ih => simp_all [add_mul]

Proof state:
case intro.inr.zero
α : Type u_1
inst✝ : NonAssocRing α
⊢ ∀ (n : ℤ), ↑(-↑0 * n) = ↑(-↑0) * ↑n

Tactic:
simp

Result:
no goals

Proof state:
case intro.inr.succ
α : Type u_1
inst✝ : NonAssocRing α
m : ℕ
ih : ∀ (n : ℤ), ↑(-↑m * n) = ↑(-↑m) * ↑n
⊢ ∀ (n : ℤ), ↑(-↑(m + 1) * n) = ↑(-↑(m + 1)) * ↑n

Tactic:
simp_all [add_mul]

Result:
no goals

Proof state:
case intro.inl.zero
α : Type u_1
inst✝ : NonAssocRing α
⊢ ∀ (n : ℤ), ↑(↑0 * n) = ↑↑0 * ↑n

Tactic:
simp

Result:
no goals

Proof state:
case intro.inr
α : Type u_1
inst✝ : NonAssocRing α
m : ℕ
⊢ ∀ (n : ℤ), ↑(-↑m * n) = ↑(-↑m) * ↑n

Tactic:
induction m with
| zero => simp
| succ m ih => simp_all [add_mul]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : NonAssocRing α
m : ℤ
⊢ ∀ (n : ℤ), ↑(m * n) = ↑m * ↑n

Tactic:
obtain ⟨m, rfl | rfl⟩ := Int.eq_nat_or_neg m

Result:
case intro.inl
α : Type u_1
inst✝ : NonAssocRing α
m : ℕ
⊢ ∀ (n : ℤ), ↑(↑m * n) = ↑↑m * ↑n

case intro.inr
α : Type u_1
inst✝ : NonAssocRing α
m : ℕ
⊢ ∀ (n : ℤ), ↑(-↑m * n) = ↑(-↑m) * ↑n

Proof state:
case intro.inl.succ
α : Type u_1
inst✝ : NonAssocRing α
m : ℕ
ih : ∀ (n : ℤ), ↑(↑m * n) = ↑↑m * ↑n
⊢ ∀ (n : ℤ), ↑(↑(m + 1) * n) = ↑↑(m + 1) * ↑n

Tactic:
simp_all [add_mul]

Result:
no goals

Proof state:
case intro.inl
α : Type u_1
inst✝ : NonAssocRing α
m : ℕ
⊢ ∀ (n : ℤ), ↑(↑m * n) = ↑↑m * ↑n

Tactic:
induction m with
| zero => simp
| succ m ih => simp_all [add_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
theorem length_Ioc (a b : ℝ) : f.length (Ioc a b) = ofReal (f b - f a)

Proof state:
f : StieltjesFunction
a b : ℝ
⊢ f.length (Ioc a b) = ofReal (↑f b - ↑f a)

Tactic:
refine
  le_antisymm (iInf_le_of_le a <| iInf₂_le b Subset.rfl)
    (le_iInf fun a' => le_iInf fun b' => le_iInf fun h => ENNReal.coe_le_coe.2 ?_)

Result:
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
⊢ (↑f b - ↑f a).toNNReal ≤ (↑f b' - ↑f a').toNNReal

Proof state:
case inr
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
ab : a < b
⊢ (↑f b - ↑f a).toNNReal ≤ (↑f b' - ↑f a').toNNReal

Tactic:
obtain ⟨h₁, h₂⟩ := (Ioc_subset_Ioc_iff ab).1 h

Result:
case inr.intro
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
ab : a < b
h₁ : b ≤ b'
h₂ : a' ≤ a
⊢ (↑f b - ↑f a).toNNReal ≤ (↑f b' - ↑f a').toNNReal

Proof state:
case inr.intro
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
ab : a < b
h₁ : b ≤ b'
h₂ : a' ≤ a
⊢ (↑f b - ↑f a).toNNReal ≤ (↑f b' - ↑f a').toNNReal

Tactic:
exact Real.toNNReal_le_toNNReal (sub_le_sub (f.mono h₁) (f.mono h₂))

Result:
no goals

Proof state:
case inl
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
ab : b ≤ a
⊢ (↑f b - ↑f a).toNNReal ≤ (↑f b' - ↑f a').toNNReal

Tactic:
rw [Real.toNNReal_of_nonpos (sub_nonpos.2 (f.mono ab))]

Result:
case inl
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
ab : b ≤ a
⊢ 0 ≤ (↑f b' - ↑f a').toNNReal

Proof state:
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
⊢ (↑f b - ↑f a).toNNReal ≤ (↑f b' - ↑f a').toNNReal

Tactic:
rcases le_or_lt b a with ab | ab

Result:
case inl
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
ab : b ≤ a
⊢ (↑f b - ↑f a).toNNReal ≤ (↑f b' - ↑f a').toNNReal

case inr
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
ab : a < b
⊢ (↑f b - ↑f a).toNNReal ≤ (↑f b' - ↑f a').toNNReal

Proof state:
case inl
f : StieltjesFunction
a b a' b' : ℝ
h : Ioc a b ⊆ Ioc a' b'
ab : b ≤ a
⊢ 0 ≤ (↑f b' - ↑f a').toNNReal

Tactic:
apply zero_le

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem oadd_lt_oadd_2 {e o₁ o₂ : ONote} {n₁ n₂ : ℕ+} (h₁ : NF (oadd e n₁ o₁)) (h : (n₁ : ℕ) < n₂) :
    oadd e n₁ o₁ < oadd e n₂ o₂

Proof state:
e o₁ o₂ : ONote
n₁ n₂ : ℕ+
h₁ : (e.oadd n₁ o₁).NF
h : ↑n₁ < ↑n₂
⊢ ω ^ e.repr * ↑↑n₁ + ω ^ e.repr ≤ ω ^ e.repr * ↑↑n₂

Tactic:
rwa [← mul_succ,Ordinal.mul_le_mul_iff_left (opow_pos _ omega0_pos), succ_le_iff, Nat.cast_lt]

Result:
no goals

Proof state:
e o₁ o₂ : ONote
n₁ n₂ : ℕ+
h₁ : (e.oadd n₁ o₁).NF
h : ↑n₁ < ↑n₂
⊢ ω ^ e.repr * ↑↑n₁ + o₁.repr < ω ^ e.repr * ↑↑n₂ + o₂.repr

Tactic:
refine lt_of_lt_of_le ((add_lt_add_iff_left _).2 h₁.snd'.repr_lt) (le_trans ?_ (le_add_right _ _))

Result:
e o₁ o₂ : ONote
n₁ n₂ : ℕ+
h₁ : (e.oadd n₁ o₁).NF
h : ↑n₁ < ↑n₂
⊢ ω ^ e.repr * ↑↑n₁ + ω ^ e.repr ≤ ω ^ e.repr * ↑↑n₂

Proof state:
e o₁ o₂ : ONote
n₁ n₂ : ℕ+
h₁ : (e.oadd n₁ o₁).NF
h : ↑n₁ < ↑n₂
⊢ e.oadd n₁ o₁ < e.oadd n₂ o₂

Tactic:
simp only [lt_def, repr]

Result:
e o₁ o₂ : ONote
n₁ n₂ : ℕ+
h₁ : (e.oadd n₁ o₁).NF
h : ↑n₁ < ↑n₂
⊢ ω ^ e.repr * ↑↑n₁ + o₁.repr < ω ^ e.repr * ↑↑n₂ + o₂.repr
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem degree_lt_degree (h : natDegree p < natDegree q) : degree p < degree q

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
⊢ p.degree < q.degree

Tactic:
by_cases hp : p = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : p = 0
⊢ p.degree < q.degree

case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : ¬p = 0
⊢ p.degree < q.degree

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : p = 0
hq : q.degree = ⊥
⊢ False

Tactic:
simp [hp, degree_eq_bot.mp hq, lt_irrefl] at h

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : p = 0
⊢ q.degree ≠ ⊥

Tactic:
intro hq

Result:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : p = 0
hq : q.degree = ⊥
⊢ False

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : p = 0
⊢ ⊥ < q.degree

Tactic:
rw [bot_lt_iff_ne_bot]

Result:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : p = 0
⊢ q.degree ≠ ⊥

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : p = 0
⊢ p.degree < q.degree

Tactic:
simp only [hp, degree_zero]

Result:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : p = 0
⊢ ⊥ < q.degree

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : ¬p = 0
⊢ p.degree < q.degree

Tactic:
rwa [degree_eq_natDegree hp, degree_eq_natDegree <| ne_zero_of_natDegree_gt h, Nat.cast_lt]

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
lemma toColex_lt_toColex_iff_exists_forall_lt :
    toColex s < toColex t ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ { ofColex := s } < { ofColex := t } ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a

Tactic:
rw [← not_le, toColex_le_toColex, not_forall]

Result:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ (∃ x, ¬(x ∈ t → x ∉ s → ∃ b ∈ s, b ∉ t ∧ x ≤ b)) ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ (∃ x, ¬(x ∈ t → x ∉ s → ∃ b ∈ s, b ∉ t ∧ x ≤ b)) ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a

Tactic:
simp only [not_forall, not_exists, not_and, not_le, exists_prop, exists_and_left]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Tower.lean
theorem lTensor_comp_cancelBaseChange (f : N →ₗ[R] Q) :
    lTensor _ _ f ∘ₗ cancelBaseChange R A B M N =
      (cancelBaseChange R A B M Q).toLinearMap ∘ₗ lTensor _ _ (lTensor _ _ f)

Proof state:
case a.h.a.h.h
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
Q : Type uQ
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring A
inst✝¹⁵ : Semiring B
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra R B
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
inst✝¹⁰ : Module A M
inst✝⁹ : Module B M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : IsScalarTower R B M
inst✝⁶ : SMulCommClass A B M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
f : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry ((curry ((lTensor B M) f ∘ₗ ↑(cancelBaseChange R A B M N))) x✝¹)) 1) x✝ =
    ((curry ((curry (↑(cancelBaseChange R A B M Q) ∘ₗ (lTensor B M) ((lTensor A A) f))) x✝¹)) 1) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
Q : Type uQ
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring A
inst✝¹⁵ : Semiring B
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra R B
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
inst✝¹⁰ : Module A M
inst✝⁹ : Module B M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : IsScalarTower R B M
inst✝⁶ : SMulCommClass A B M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
f : N →ₗ[R] Q
⊢ (lTensor B M) f ∘ₗ ↑(cancelBaseChange R A B M N) = ↑(cancelBaseChange R A B M Q) ∘ₗ (lTensor B M) ((lTensor A A) f)

Tactic:
ext

Result:
case a.h.a.h.h
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
Q : Type uQ
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring A
inst✝¹⁵ : Semiring B
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra R B
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
inst✝¹⁰ : Module A M
inst✝⁹ : Module B M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : IsScalarTower R B M
inst✝⁶ : SMulCommClass A B M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
f : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry ((curry ((lTensor B M) f ∘ₗ ↑(cancelBaseChange R A B M N))) x✝¹)) 1) x✝ =
    ((curry ((curry (↑(cancelBaseChange R A B M Q) ∘ₗ (lTensor B M) ((lTensor A A) f))) x✝¹)) 1) x✝
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_succ_mul_X (n : ℕ) (φ : R⟦X⟧) : coeff R (n + 1) (φ * X) = coeff R n φ

Proof state:
case h.e'_3
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (MvPowerSeries.coeff R (single () n)) φ = (MvPowerSeries.coeff R (single () n)) φ * 1

Tactic:
rw [mul_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (MvPowerSeries.coeff R (single () n + single () 1)) (φ * X) = (MvPowerSeries.coeff R (single () n)) φ

Tactic:
convert φ.coeff_add_mul_monomial (single () n) (single () 1) _

Result:
case h.e'_3
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (MvPowerSeries.coeff R (single () n)) φ = (MvPowerSeries.coeff R (single () n)) φ * 1

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (coeff R (n + 1)) (φ * X) = (coeff R n) φ

Tactic:
simp only [coeff, Finsupp.single_add]

Result:
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (MvPowerSeries.coeff R (single () n + single () 1)) (φ * X) = (MvPowerSeries.coeff R (single () n)) φ
-- Mathlib/CategoryTheory/Limits/Shapes/FunctorToTypes.lean
@[simp]
lemma inr_comp_binaryCoproductIso_hom :
    Limits.coprod.inr ≫ (binaryCoproductIso F G).hom = coprod.inr

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
⊢ Limits.coprod.inr ≫ (binaryCoproductIso F G).hom = coprod.inr

Tactic:
simp [binaryCoproductIso]

Result:
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
⊢ BinaryCofan.inr (binaryCoproductColimitCocone F G).cocone = coprod.inr

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
⊢ BinaryCofan.inr (binaryCoproductColimitCocone F G).cocone = coprod.inr

Tactic:
aesop

Result:
no goals