harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem idxOf_lt_length [BEq α] [LawfulBEq α] {l : Array α} (h : a ∈ l) : l.idxOf a < l.size

Proof state:
case mk
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
h : a ∈ { toList := l }
⊢ idxOf a { toList := l } < { toList := l }.size

Tactic:
simp [List.idxOf_lt_length (by simpa using h)]

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
h : a ∈ { toList := l }
⊢ ?m.98135 ∈ ?m.98138

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : Array α
h : a ∈ l
⊢ idxOf a l < l.size

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
h : a ∈ { toList := l }
⊢ idxOf a { toList := l } < { toList := l }.size
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Mono.lean
lemma PushoutCocone.isIso_inl_of_epi_of_isColimit {t : PushoutCocone f f} (ht : IsColimit t) :
    IsIso t.inl

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ t.inl ≫ IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ = 𝟙 Y

Tactic:
simp

Result:
no goals

Proof state:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ t.inl ≫ IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ ≫ t.inl = t.inl ≫ 𝟙 t.pt

Tactic:
simp

Result:
no goals

Proof state:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ t.inr ≫ IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ ≫ t.inl = t.inr ≫ 𝟙 t.pt

Tactic:
simp [inl_eq_inr_of_epi_eq]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ IsIso t.inl

Tactic:
refine ⟨⟨PushoutCocone.IsColimit.desc ht (𝟙 _) (𝟙 _) (by simp), by simp, ?_⟩⟩

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ ≫ t.inl = 𝟙 t.pt

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ ≫ t.inl = 𝟙 t.pt

Tactic:
apply PushoutCocone.IsColimit.hom_ext ht

Result:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ t.inl ≫ IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ ≫ t.inl = t.inl ≫ 𝟙 t.pt

case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ t.inr ≫ IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ ≫ t.inl = t.inr ≫ 𝟙 t.pt

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ f ≫ 𝟙 Y = f ≫ 𝟙 Y

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Tower.lean
theorem map_add_right (f : M →ₗ[A] P) (g₁ g₂ : N →ₗ[R] Q) :
    map f (g₁ + g₂) = map f g₁ + map f g₂

Proof state:
case a.h.h
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[A] P
g₁ g₂ : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry (map f (g₁ + g₂))) x✝¹) x✝ = ((curry (map f g₁ + map f g₂)) x✝¹) x✝

Tactic:
simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, add_apply, map_tmul,
  add_apply, tmul_add]

Result:
no goals

Proof state:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[A] P
g₁ g₂ : N →ₗ[R] Q
⊢ map f (g₁ + g₂) = map f g₁ + map f g₂

Tactic:
ext

Result:
case a.h.h
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[A] P
g₁ g₂ : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry (map f (g₁ + g₂))) x✝¹) x✝ = ((curry (map f g₁ + map f g₂)) x✝¹) x✝
-- Mathlib/Data/Matrix/Mul.lean
theorem single_vecMul_diagonal [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (v : n → R)
    (j : n) (x : R) : (Pi.single j x) ᵥ* (diagonal v) = Pi.single j (x * v j)

Proof state:
case h
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ Pi.single j x i * v i = Pi.single j (x * v j) i

Tactic:
exact Pi.apply_single (fun i x => x * v i) (fun i => zero_mul _) j x i

Result:
no goals

Proof state:
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
⊢ Pi.single j x ᵥ* diagonal v = Pi.single j (x * v j)

Tactic:
ext i

Result:
case h
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ (Pi.single j x ᵥ* diagonal v) i = Pi.single j (x * v j) i

Proof state:
case h
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ (Pi.single j x ᵥ* diagonal v) i = Pi.single j (x * v j) i

Tactic:
rw [vecMul_diagonal]

Result:
case h
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ Pi.single j x i * v i = Pi.single j (x * v j) i
-- Mathlib/Analysis/RCLike/Basic.lean
lemma exists_norm_eq_mul_self (x : K) : ∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c * x

Proof state:
case inr
K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c * x

Tactic:
exact ⟨‖x‖ / x, by simp [norm_ne_zero_iff.2, hx]⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ‖↑‖x‖ / x‖ = 1 ∧ ↑‖x‖ = ↑‖x‖ / x * x

Tactic:
simp [norm_ne_zero_iff.2, hx]

Result:
no goals

Proof state:
case inl
K : Type u_1
inst✝ : RCLike K
⊢ ∃ c, ‖c‖ = 1 ∧ ↑‖0‖ = c * 0

Tactic:
exact ⟨1, by simp⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
⊢ ‖1‖ = 1 ∧ ↑‖0‖ = 1 * 0

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ ∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c * x

Tactic:
obtain rfl | hx := eq_or_ne x 0

Result:
case inl
K : Type u_1
inst✝ : RCLike K
⊢ ∃ c, ‖c‖ = 1 ∧ ↑‖0‖ = c * 0

case inr
K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c * x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Basic.lean
theorem length_push (c : Char) : (String.push s c).length = s.length + 1

Proof state:
s : String
c : Char
⊢ (s.push c).length = s.length + 1

Tactic:
rw [push, length_mk, List.length_append, List.length_singleton, Nat.succ.injEq]

Result:
s : String
c : Char
⊢ s.data.length = s.length

Proof state:
s : String
c : Char
⊢ s.data.length = s.length

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finsupp/Fin.lean
theorem cons_tail : cons (t 0) (tail t) = t

Proof state:
case h
n : ℕ
M : Type u_1
inst✝ : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
⊢ (cons (t 0) t.tail) a = t a

Tactic:
by_cases c_a : a = 0

Result:
case pos
n : ℕ
M : Type u_1
inst✝ : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
c_a : a = 0
⊢ (cons (t 0) t.tail) a = t a

case neg
n : ℕ
M : Type u_1
inst✝ : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
c_a : ¬a = 0
⊢ (cons (t 0) t.tail) a = t a

Proof state:
case neg
n : ℕ
M : Type u_1
inst✝ : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
c_a : ¬a = 0
⊢ (cons (t 0) t.tail) a = t a

Tactic:
rw [← Fin.succ_pred a c_a, cons_succ, ← tail_apply]

Result:
no goals

Proof state:
case pos
n : ℕ
M : Type u_1
inst✝ : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
c_a : a = 0
⊢ (cons (t 0) t.tail) a = t a

Tactic:
rw [c_a, cons_zero]

Result:
no goals

Proof state:
n : ℕ
M : Type u_1
inst✝ : Zero M
t : Fin (n + 1) →₀ M
⊢ cons (t 0) t.tail = t

Tactic:
ext a

Result:
case h
n : ℕ
M : Type u_1
inst✝ : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
⊢ (cons (t 0) t.tail) a = t a
-- Mathlib/RingTheory/Ideal/GoingUp.lean
lemma map_eq_top_iff {R S} [CommRing R] [CommRing S]
    (f : R →+* S) {I : Ideal R} (hf₁ : Function.Injective f) (hf₂ : f.IsIntegral) :
    I.map f = ⊤ ↔ I = ⊤ :=
  map_eq_top_iff_of_ker_le f (by simp [f.injective_iff_ker_eq_bot.mp hf₁]) hf₂

Proof state:
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : Function.Injective ⇑f
hf₂ : f.IsIntegral
⊢ RingHom.ker f ≤ I

Tactic:
simp [f.injective_iff_ker_eq_bot.mp hf₁]

Result:
no goals
-- Mathlib/Topology/Instances/NNReal/Lemmas.lean
theorem tendsto_cofinite_zero_of_summable {α} {f : α → ℝ≥0} (hf : Summable f) :
    Tendsto f cofinite (𝓝 0)

Proof state:
α : Type u_2
f : α → ℝ≥0
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
simp only [← summable_coe, ← tendsto_coe] at hf ⊢

Result:
α : Type u_2
f : α → ℝ≥0
hf : Summable fun a => ↑(f a)
⊢ Tendsto (fun a => ↑(f a)) cofinite (𝓝 ↑0)

Proof state:
α : Type u_2
f : α → ℝ≥0
hf : Summable fun a => ↑(f a)
⊢ Tendsto (fun a => ↑(f a)) cofinite (𝓝 ↑0)

Tactic:
exact hf.tendsto_cofinite_zero

Result:
no goals
-- Mathlib/Topology/Algebra/Support.lean
theorem _root_.isCompact_range_of_mulSupport_subset_isCompact [TopologicalSpace β]
    (hf : Continuous f) {k : Set α} (hk : IsCompact k) (h'f : mulSupport f ⊆ k) :
    IsCompact (range f)

Proof state:
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : TopologicalSpace β
hf : Continuous f
k : Set α
hk : IsCompact k
h'f : mulSupport f ⊆ k
⊢ IsCompact (range f)

Tactic:
rcases range_eq_image_or_of_mulSupport_subset h'f with h2 | h2 <;> rw [h2]

Result:
case inl
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : TopologicalSpace β
hf : Continuous f
k : Set α
hk : IsCompact k
h'f : mulSupport f ⊆ k
h2 : range f = f '' k
⊢ IsCompact (f '' k)

case inr
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : TopologicalSpace β
hf : Continuous f
k : Set α
hk : IsCompact k
h'f : mulSupport f ⊆ k
h2 : range f = insert 1 (f '' k)
⊢ IsCompact (insert 1 (f '' k))

Proof state:
case inl
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : TopologicalSpace β
hf : Continuous f
k : Set α
hk : IsCompact k
h'f : mulSupport f ⊆ k
h2 : range f = f '' k
⊢ IsCompact (f '' k)

case inr
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : TopologicalSpace β
hf : Continuous f
k : Set α
hk : IsCompact k
h'f : mulSupport f ⊆ k
h2 : range f = insert 1 (f '' k)
⊢ IsCompact (insert 1 (f '' k))

Tactic:
exacts [hk.image hf, (hk.image hf).insert 1]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iInf_singleton {f : β → α} {b : β} : ⨅ x ∈ (singleton b : Set β), f x = f b

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
b : β
⊢ ⨅ x ∈ {b}, f x = f b

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem xn_ge_a_pow : ∀ n : ℕ, a ^ n ≤ xn a1 n
  | 0 => le_refl 1
  | n + 1 => by
    simp only [_root_.pow_succ, xn_succ]
    exact le_trans (Nat.mul_le_mul_right _ (xn_ge_a_pow n)) (Nat.le_add_right _ _)

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ a ^ (n + 1) ≤ xn a1 (n + 1)

Tactic:
simp only [_root_.pow_succ, xn_succ]

Result:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ a ^ n * a ≤ xn a1 n * a + Pell.d a1 * yn a1 n

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ a ^ n * a ≤ xn a1 n * a + Pell.d a1 * yn a1 n

Tactic:
exact le_trans (Nat.mul_le_mul_right _ (xn_ge_a_pow n)) (Nat.le_add_right _ _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem insert_append_of_mem_left {l₁ l₂ : List α} (h : a ∈ l₂) :
    (l₁ ++ l₂).insert a = l₁ ++ l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ l₂ : List α
h : a ∈ l₂
⊢ List.insert a (l₁ ++ l₂) = l₁ ++ l₂

Tactic:
simp [insert_append, h]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_re_zero_left (x : E) : re ⟪0, x⟫ = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ re ⟪0, x⟫_𝕜 = 0

Tactic:
simp only [inner_zero_left, AddMonoidHom.map_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
lemma meas_le_of_le_of_forall_le_meas_thickening_add {ε₁ ε₂ : ℝ≥0∞} (μ ν : Measure Ω)
    (h_le : ε₁ ≤ ε₂) {B : Set Ω} (hε₁ : μ B ≤ ν (thickening ε₁.toReal B) + ε₁) :
    μ B ≤ ν (thickening ε₂.toReal B) + ε₂

Proof state:
case neg
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
ε₁ ε₂ : ℝ≥0∞
μ ν : Measure Ω
h_le : ε₁ ≤ ε₂
B : Set Ω
hε₁ : μ B ≤ ν (thickening ε₁.toReal B) + ε₁
ε_top : ¬ε₂ = ⊤
⊢ μ B ≤ ν (thickening ε₂.toReal B) + ε₂

Tactic:
apply hε₁.trans (add_le_add ?_ h_le)

Result:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
ε₁ ε₂ : ℝ≥0∞
μ ν : Measure Ω
h_le : ε₁ ≤ ε₂
B : Set Ω
hε₁ : μ B ≤ ν (thickening ε₁.toReal B) + ε₁
ε_top : ¬ε₂ = ⊤
⊢ ν (thickening ε₁.toReal B) ≤ ν (thickening ε₂.toReal B)

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
ε₁ ε₂ : ℝ≥0∞
μ ν : Measure Ω
h_le : ε₁ ≤ ε₂
B : Set Ω
hε₁ : μ B ≤ ν (thickening ε₁.toReal B) + ε₁
⊢ μ B ≤ ν (thickening ε₂.toReal B) + ε₂

Tactic:
by_cases ε_top : ε₂ = ∞

Result:
case pos
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
ε₁ ε₂ : ℝ≥0∞
μ ν : Measure Ω
h_le : ε₁ ≤ ε₂
B : Set Ω
hε₁ : μ B ≤ ν (thickening ε₁.toReal B) + ε₁
ε_top : ε₂ = ⊤
⊢ μ B ≤ ν (thickening ε₂.toReal B) + ε₂

case neg
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
ε₁ ε₂ : ℝ≥0∞
μ ν : Measure Ω
h_le : ε₁ ≤ ε₂
B : Set Ω
hε₁ : μ B ≤ ν (thickening ε₁.toReal B) + ε₁
ε_top : ¬ε₂ = ⊤
⊢ μ B ≤ ν (thickening ε₂.toReal B) + ε₂

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
ε₁ ε₂ : ℝ≥0∞
μ ν : Measure Ω
h_le : ε₁ ≤ ε₂
B : Set Ω
hε₁ : μ B ≤ ν (thickening ε₁.toReal B) + ε₁
ε_top : ¬ε₂ = ⊤
⊢ ν (thickening ε₁.toReal B) ≤ ν (thickening ε₂.toReal B)

Tactic:
exact measure_mono (μ := ν) (thickening_mono (toReal_mono ε_top h_le) B)

Result:
no goals

Proof state:
case pos
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
ε₁ ε₂ : ℝ≥0∞
μ ν : Measure Ω
h_le : ε₁ ≤ ε₂
B : Set Ω
hε₁ : μ B ≤ ν (thickening ε₁.toReal B) + ε₁
ε_top : ε₂ = ⊤
⊢ μ B ≤ ν (thickening ε₂.toReal B) + ε₂

Tactic:
simp only [ne_eq, FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure, ε_top, top_toReal,
            add_top, le_top]

Result:
no goals
-- Mathlib/SetTheory/Game/State.lean
theorem turnBound_ne_zero_of_left_move {s t : S} (m : t ∈ l s) : turnBound s ≠ 0

Proof state:
S : Type u
inst✝ : State S
s t✝ : S
m : t✝ ∈ l s
h : turnBound s = 0
t : turnBound t✝ < turnBound s
⊢ False

Tactic:
rw [h] at t

Result:
S : Type u
inst✝ : State S
s t✝ : S
m : t✝ ∈ l s
h : turnBound s = 0
t : turnBound t✝ < 0
⊢ False

Proof state:
S : Type u
inst✝ : State S
s t : S
m : t ∈ l s
h : turnBound s = 0
⊢ False

Tactic:
have t := left_bound m

Result:
S : Type u
inst✝ : State S
s t✝ : S
m : t✝ ∈ l s
h : turnBound s = 0
t : turnBound t✝ < turnBound s
⊢ False

Proof state:
S : Type u
inst✝ : State S
s t✝ : S
m : t✝ ∈ l s
h : turnBound s = 0
t : turnBound t✝ < 0
⊢ False

Tactic:
exact Nat.not_succ_le_zero _ t

Result:
no goals

Proof state:
S : Type u
inst✝ : State S
s t : S
m : t ∈ l s
⊢ turnBound s ≠ 0

Tactic:
intro h

Result:
S : Type u
inst✝ : State S
s t : S
m : t ∈ l s
h : turnBound s = 0
⊢ False
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_σ_succ {n} {i : Fin (n + 1)} : X.σ i ≫ X.δ i.succ = 𝟙 _

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ i.succ).op = 𝟙 (X _⦋n⦌)

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_succ, op_id, X.map_id]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ X.δ i.succ = 𝟙 (X _⦋n⦌)

Tactic:
dsimp [δ, σ]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ i.succ).op = 𝟙 (X _⦋n⦌)
-- Mathlib/Data/Complex/Cardinality.lean
theorem mk_complex : #ℂ = 𝔠

Proof state:
⊢ #ℂ = 𝔠

Tactic:
rw [mk_congr Complex.equivRealProd, mk_prod, lift_id, mk_real, continuum_mul_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem mk_succ_pos (i : Nat) (h : i < n) :
    (0 : Fin (n + 1)) < ⟨i.succ, Nat.add_lt_add_right h 1⟩

Proof state:
n i : Nat
h : i < n
⊢ 0 < ↑⟨i.succ, ⋯⟩

Tactic:
exact Nat.succ_pos i

Result:
no goals

Proof state:
n i : Nat
h : i < n
⊢ 0 < ⟨i.succ, ⋯⟩

Tactic:
rw [lt_def, val_zero]

Result:
n i : Nat
h : i < n
⊢ 0 < ↑⟨i.succ, ⋯⟩
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem truncate_truncate {n₁ n₂ n₃ : ℕ} (h1 : n₁ ≤ n₂) (h2 : n₂ ≤ n₃)
    (x : TruncatedWittVector p n₃ R) :
    (truncate h1) (truncate h2 x) = truncate (h1.trans h2) x

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n₁ n₂ n₃ : ℕ
h1 : n₁ ≤ n₂
h2 : n₂ ≤ n₃
x : TruncatedWittVector p n₃ R
⊢ (truncate h1) ((truncate h2) x) = (truncate ⋯) x

Tactic:
obtain ⟨x, rfl⟩ := WittVector.truncate_surjective (p := p) n₃ R x

Result:
case intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n₁ n₂ n₃ : ℕ
h1 : n₁ ≤ n₂
h2 : n₂ ≤ n₃
x : 𝕎 R
⊢ (truncate h1) ((truncate h2) ((WittVector.truncate n₃) x)) = (truncate ⋯) ((WittVector.truncate n₃) x)

Proof state:
case intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n₁ n₂ n₃ : ℕ
h1 : n₁ ≤ n₂
h2 : n₂ ≤ n₃
x : 𝕎 R
⊢ (truncate h1) ((truncate h2) ((WittVector.truncate n₃) x)) = (truncate ⋯) ((WittVector.truncate n₃) x)

Tactic:
simp only [truncate_wittVector_truncate]

Result:
no goals
-- Mathlib/Data/W/Basic.lean
theorem elim_injective (γ : Type*) (fγ : (Σa : α, β a → γ) → γ)
    (fγ_injective : Function.Injective fγ) : Function.Injective (elim γ fγ)
  | ⟨a₁, f₁⟩, ⟨a₂, f₂⟩, h => by
    obtain ⟨rfl, h⟩ := Sigma.mk.inj_iff.mp (fγ_injective h)
    congr with x
    exact elim_injective γ fγ fγ_injective (congr_fun (eq_of_heq h) x :)

Proof state:
α : Type u_1
β : α → Type u_2
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ : β a₁ → WType β
a₂ : α
f₂ : β a₂ → WType β
h : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₂ f₂)
⊢ mk a₁ f₁ = mk a₂ f₂

Tactic:
obtain ⟨rfl, h⟩ := Sigma.mk.inj_iff.mp (fγ_injective h)

Result:
case intro
α : Type u_1
β : α → Type u_2
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ f₂ : β a₁ → WType β
h✝ : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₁ f₂)
h : HEq (fun b => elim γ fγ (f₁ b)) fun b => elim γ fγ (f₂ b)
⊢ mk a₁ f₁ = mk a₁ f₂

Proof state:
case intro.e_f.h
α : Type u_1
β : α → Type u_2
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ f₂ : β a₁ → WType β
h✝ : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₁ f₂)
h : HEq (fun b => elim γ fγ (f₁ b)) fun b => elim γ fγ (f₂ b)
x : β a₁
⊢ f₁ x = f₂ x

Tactic:
exact elim_injective γ fγ fγ_injective (congr_fun (eq_of_heq h) x :)

Result:
no goals

Proof state:
case intro
α : Type u_1
β : α → Type u_2
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ f₂ : β a₁ → WType β
h✝ : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₁ f₂)
h : HEq (fun b => elim γ fγ (f₁ b)) fun b => elim γ fγ (f₂ b)
⊢ mk a₁ f₁ = mk a₁ f₂

Tactic:
congr with x

Result:
case intro.e_f.h
α : Type u_1
β : α → Type u_2
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ f₂ : β a₁ → WType β
h✝ : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₁ f₂)
h : HEq (fun b => elim γ fγ (f₁ b)) fun b => elim γ fγ (f₂ b)
x : β a₁
⊢ f₁ x = f₂ x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem containsThenInsertIfNew_snd_val [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} {b : β a} :
    (m.val.containsThenInsertIfNew a b).2 = (m.containsThenInsertIfNew a b).2.1

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β a
⊢ (m.val.containsThenInsertIfNew a b).snd = (m.containsThenInsertIfNew a b).snd.val

Tactic:
simp [Raw.containsThenInsertIfNew, m.2]

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem repr_floor_apply (m : E) (i : ι) : b.repr (floor b m) i = ⌊b.repr m i⌋

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
i : ι
⊢ (b.repr ↑(floor b m)) i = ↑⌊(b.repr m) i⌋

Tactic:
simp only [floor, ← Int.cast_smul_eq_zsmul K, b.repr.map_smul, Finsupp.single_apply,
Finset.sum_apply', Basis.repr_self, Finsupp.smul_single', mul_one, Finset.sum_ite_eq', coe_sum,
Finset.mem_univ, if_true, coe_smul_of_tower, Basis.restrictScalars_apply, map_sum]

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
i : ι
⊢ (b.repr ↑(floor b m)) i = ↑⌊(b.repr m) i⌋

Tactic:
classical simp only [floor, ← Int.cast_smul_eq_zsmul K, b.repr.map_smul, Finsupp.single_apply,
  Finset.sum_apply', Basis.repr_self, Finsupp.smul_single', mul_one, Finset.sum_ite_eq', coe_sum,
  Finset.mem_univ, if_true, coe_smul_of_tower, Basis.restrictScalars_apply, map_sum]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Instances.lean
theorem one_minus_lt_one (x : Ioo (0 : β) 1) : 1 - (x : β) < 1

Proof state:
β : Type u_2
inst✝ : OrderedRing β
x : ↑(Ioo 0 1)
⊢ 1 - ↑x < 1

Tactic:
simpa using x.2.1

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem ord_nat (n : ℕ) : ord n = n :=
  (ord_le.2 (card_nat n).ge).antisymm
    (by
      induction' n with n IH
      · apply Ordinal.zero_le
      · exact succ_le_of_lt (IH.trans_lt <| ord_lt_ord.2 <| Nat.cast_lt.2 (Nat.lt_succ_self n)))

Proof state:
n : ℕ
⊢ ↑n ≤ (↑n).ord

Tactic:
induction' n with n IH

Result:
case zero

⊢ ↑0 ≤ (↑0).ord

case succ
n : ℕ
IH : ↑n ≤ (↑n).ord
⊢ ↑(n + 1) ≤ (↑(n + 1)).ord

Proof state:
case zero

⊢ ↑0 ≤ (↑0).ord

Tactic:
apply Ordinal.zero_le

Result:
no goals

Proof state:
case succ
n : ℕ
IH : ↑n ≤ (↑n).ord
⊢ ↑(n + 1) ≤ (↑(n + 1)).ord

Tactic:
exact succ_le_of_lt (IH.trans_lt <| ord_lt_ord.2 <| Nat.cast_lt.2 (Nat.lt_succ_self n))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/SOM.lean
theorem Poly.denote_insertSorted (ctx : Context) (k : Nat) (m : Mon) (p : Poly) : (p.insertSorted k m).denote ctx = p.denote ctx + k * m.denote ctx

Proof state:
ctx : Context
k : Nat
m : Mon
p : Poly
⊢ denote ctx (insertSorted k m []) = denote ctx [] + k * Mon.denote ctx m

Tactic:
simp!

Result:
no goals

Proof state:
ctx : Context
k : Nat
m : Mon
p : Poly
⊢ denote ctx (insertSorted k m p) = denote ctx p + k * Mon.denote ctx m

Tactic:
match p with
| [] => simp!
| (k', m') :: p =>
  by_cases h : m < m' <;> simp! [h, denote_insertSorted ctx k m p, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]

Result:
no goals

Proof state:
ctx : Context
k : Nat
m : Mon
p✝ : Poly
k' : Nat
m' : Mon
p : List (Nat × Mon)
⊢ denote ctx (insertSorted k m ((k', m') :: p)) = denote ctx ((k', m') :: p) + k * Mon.denote ctx m

Tactic:
by_cases h : m < m' <;> simp! [h, denote_insertSorted ctx k m p, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]

Result:
no goals