harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Polynomial/Basic.lean
theorem isEquivalent_atTop_lead :
    (fun x => eval x P) ~[atTop] fun x => P.leadingCoeff * x ^ P.natDegree

Proof state:
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : ¬P = 0
⊢ (fun x => ∑ i ∈ range P.natDegree, P.coeff i * x ^ i + P.coeff P.natDegree * x ^ P.natDegree) ~[atTop] fun x =>
    P.leadingCoeff * x ^ P.natDegree

Tactic:
exact
  IsLittleO.add_isEquivalent
    (IsLittleO.sum fun i hi =>
      IsLittleO.const_mul_left
        ((IsLittleO.const_mul_right fun hz => h <| leadingCoeff_eq_zero.mp hz) <|
          isLittleO_pow_pow_atTop_of_lt (mem_range.mp hi))
        _)
    IsEquivalent.refl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ (fun x => eval x P) ~[atTop] fun x => P.leadingCoeff * x ^ P.natDegree

Tactic:
by_cases h : P = 0

Result:
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P = 0
⊢ (fun x => eval x P) ~[atTop] fun x => P.leadingCoeff * x ^ P.natDegree

case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : ¬P = 0
⊢ (fun x => eval x P) ~[atTop] fun x => P.leadingCoeff * x ^ P.natDegree

Proof state:
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : ¬P = 0
⊢ (fun x => eval x P) ~[atTop] fun x => P.leadingCoeff * x ^ P.natDegree

Tactic:
simp only [Polynomial.eval_eq_sum_range, sum_range_succ]

Result:
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : ¬P = 0
⊢ (fun x => ∑ i ∈ range P.natDegree, P.coeff i * x ^ i + P.coeff P.natDegree * x ^ P.natDegree) ~[atTop] fun x =>
    P.leadingCoeff * x ^ P.natDegree

Proof state:
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P = 0
⊢ (fun x => eval x P) ~[atTop] fun x => P.leadingCoeff * x ^ P.natDegree

Tactic:
simp [h, IsEquivalent.refl]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@[to_additive] lemma inv_mabs_le (a : α) : |a|ₘ⁻¹ ≤ a

Proof state:
case inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
h : a ≤ 1
⊢ (mabs a)⁻¹ ≤ a

Tactic:
simp [mabs_of_le_one h]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
h : 1 ≤ a
⊢ (mabs a)⁻¹ ≤ a

Tactic:
simpa [mabs_of_one_le h] using (inv_le_one'.2 h).trans h

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ (mabs a)⁻¹ ≤ a

Tactic:
obtain h | h := le_total 1 a

Result:
case inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
h : 1 ≤ a
⊢ (mabs a)⁻¹ ≤ a

case inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
h : a ≤ 1
⊢ (mabs a)⁻¹ ≤ a
-- Mathlib/CategoryTheory/Sites/Grothendieck.lean
theorem isGLB_sInf (s : Set (GrothendieckTopology C)) : IsGLB s (sInf s)

Proof state:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
s : Set (GrothendieckTopology C)
⊢ ∀ {x y : GrothendieckTopology C}, x.sieves ≤ y.sieves ↔ x ≤ y

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
s : Set (GrothendieckTopology C)
⊢ IsGLB s (sInf s)

Tactic:
refine @IsGLB.of_image _ _ _ _ sieves ?_ _ _ ?_

Result:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
s : Set (GrothendieckTopology C)
⊢ ∀ {x y : GrothendieckTopology C}, x.sieves ≤ y.sieves ↔ x ≤ y

case refine_2
C : Type u
inst✝ : Category.{v, u} C
s : Set (GrothendieckTopology C)
⊢ IsGLB (sieves '' s) (sInf s).sieves

Proof state:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
s : Set (GrothendieckTopology C)
⊢ IsGLB (sieves '' s) (sInf s).sieves

Tactic:
exact _root_.isGLB_sInf _

Result:
no goals
-- Mathlib/Logic/Basic.lean
lemma imp_forall_iff_forall (A : Prop) (B : A → Prop) :
  (A → ∀ h : A, B h) ↔ ∀ h : A, B h

Proof state:
A : Prop
B : A → Prop
⊢ (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h

Tactic:
by_cases h : A <;> simp [h]

Result:
no goals
-- Mathlib/CategoryTheory/Category/Basic.lean
theorem epi_of_epi {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Epi (f ≫ g)] : Epi g :=
  ⟨fun _ _ w => (cancel_epi (f ≫ g)).1 <| by simp only [Category.assoc, w]⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi (f ≫ g)
Z✝ : C
x✝¹ x✝ : Z ⟶ Z✝
w : g ≫ x✝¹ = g ≫ x✝
⊢ (f ≫ g) ≫ x✝¹ = (f ≫ g) ≫ x✝

Tactic:
simp only [Category.assoc, w]

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem iteratedDeriv_eq_iterate : iteratedDeriv n f = deriv^[n] f

Proof state:
case h.e'_3.h.e'_1.h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
x✝ : 𝕜 → F
⊢ deriv x✝ = derivWithin x✝ univ

Tactic:
simp [derivWithin_univ]

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ iteratedDeriv n f x = deriv^[n] f x

Tactic:
rw [← iteratedDerivWithin_univ]

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ iteratedDerivWithin n f univ x = deriv^[n] f x

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ iteratedDerivWithin n f univ x = deriv^[n] f x

Tactic:
convert iteratedDerivWithin_eq_iterate (F := F)

Result:
case h.e'_3.h.e'_1.h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
x✝ : 𝕜 → F
⊢ deriv x✝ = derivWithin x✝ univ

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ iteratedDeriv n f = deriv^[n] f

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ iteratedDeriv n f x = deriv^[n] f x
-- Mathlib/Topology/ContinuousOn.lean
theorem continuous_if_const (p : Prop) [Decidable p] (hf : p → Continuous f)
    (hg : ¬p → Continuous g) : Continuous fun a => if p then f a else g a

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : Prop
inst✝ : Decidable p
hf : p → Continuous f
hg : ¬p → Continuous g
h : p
⊢ Continuous fun a => f a

case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : Prop
inst✝ : Decidable p
hf : p → Continuous f
hg : ¬p → Continuous g
h : ¬p
⊢ Continuous fun a => g a

Tactic:
exacts [hf h, hg h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : Prop
inst✝ : Decidable p
hf : p → Continuous f
hg : ¬p → Continuous g
⊢ Continuous fun a => if p then f a else g a

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : Prop
inst✝ : Decidable p
hf : p → Continuous f
hg : ¬p → Continuous g
h : p
⊢ Continuous fun a => f a

case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : Prop
inst✝ : Decidable p
hf : p → Continuous f
hg : ¬p → Continuous g
h : ¬p
⊢ Continuous fun a => g a
-- Mathlib/Algebra/Ring/Submonoid.lean
/-- The product of two elements of the additive closure of a submonoid `M` is an element of the
additive closure of `M`. -/
lemma mul_mem_add_closure (ha : a ∈ closure (S : Set R))
    (hb : b ∈ closure (S : Set R)) : a * b ∈ closure (S : Set R)

Proof state:
case one
M : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
ha : a ∈ closure ↑S
⊢ a * 0 ∈ closure ↑S

Tactic:
simp only [mul_zero, zero_mem _]

Result:
no goals

Proof state:
case mul
M : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
ha : a ∈ closure ↑S
r s : R
hx✝ : r ∈ closure ↑S
hy✝ : s ∈ closure ↑S
hr : a * r ∈ closure ↑S
hs : a * s ∈ closure ↑S
⊢ a * (r + s) ∈ closure ↑S

Tactic:
simpa only [mul_add] using add_mem hr hs

Result:
no goals

Proof state:
case mem
M : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
ha : a ∈ closure ↑S
r : R
hr : r ∈ ↑S
⊢ a * r ∈ closure ↑S

Tactic:
exact MulMemClass.mul_right_mem_add_closure ha hr

Result:
no goals

Proof state:
M : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
ha : a ∈ closure ↑S
hb : b ∈ closure ↑S
⊢ a * b ∈ closure ↑S

Tactic:
induction hb using closure_induction with
| mem r hr => exact MulMemClass.mul_right_mem_add_closure ha hr
| one => simp only [mul_zero, zero_mem _]
| mul r s _ _ hr hs => simpa only [mul_add] using add_mem hr hs

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem get : ∀ {s}, Valid s → s.toString.1 = m₁ ++ c :: m₂ → s.get ⟨utf8Len m₁⟩ = c
  | _, h, e => by
    let ⟨l, m, r, h⟩ := h.validFor
    simp only [h.toString] at e; subst e; simp [h.get]

Proof state:
m₁ : List Char
c : Char
m₂ : List Char
x✝ : Substring
h✝ : x✝.Valid
l m r : List Char
h : ValidFor l m r x✝
e : m = m₁ ++ c :: m₂
⊢ x✝.get { byteIdx := utf8Len m₁ } = c

Tactic:
subst e

Result:
m₁ : List Char
c : Char
m₂ : List Char
x✝ : Substring
h✝ : x✝.Valid
l r : List Char
h : ValidFor l (m₁ ++ c :: m₂) r x✝
⊢ x✝.get { byteIdx := utf8Len m₁ } = c

Proof state:
m₁ : List Char
c : Char
m₂ : List Char
x✝ : Substring
h✝ : x✝.Valid
l r : List Char
h : ValidFor l (m₁ ++ c :: m₂) r x✝
⊢ x✝.get { byteIdx := utf8Len m₁ } = c

Tactic:
simp [h.get]

Result:
no goals

Proof state:
m₁ : List Char
c : Char
m₂ : List Char
x✝ : Substring
h✝ : x✝.Valid
e : x✝.toString.data = m₁ ++ c :: m₂
l m r : List Char
h : ValidFor l m r x✝
⊢ x✝.get { byteIdx := utf8Len m₁ } = c

Tactic:
simp only [h.toString] at e

Result:
m₁ : List Char
c : Char
m₂ : List Char
x✝ : Substring
h✝ : x✝.Valid
l m r : List Char
h : ValidFor l m r x✝
e : m = m₁ ++ c :: m₂
⊢ x✝.get { byteIdx := utf8Len m₁ } = c

Proof state:
m₁ : List Char
c : Char
m₂ : List Char
x✝ : Substring
h : x✝.Valid
e : x✝.toString.data = m₁ ++ c :: m₂
⊢ x✝.get { byteIdx := utf8Len m₁ } = c

Tactic:
let ⟨l, m, r, h⟩ := h.validFor

Result:
m₁ : List Char
c : Char
m₂ : List Char
x✝ : Substring
h✝ : x✝.Valid
e : x✝.toString.data = m₁ ++ c :: m₂
l m r : List Char
h : ValidFor l m r x✝
⊢ x✝.get { byteIdx := utf8Len m₁ } = c
-- Mathlib/FieldTheory/Finite/Polynomial.lean
theorem ker_evalₗ [Finite σ] : ker (evalᵢ σ K) = ⊥

Proof state:
case intro
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ Module.finrank K (R σ K) = Module.finrank K ((σ → K) → K)

Tactic:
rw [Module.finrank_fintype_fun_eq_card, finrank_R]

Result:
no goals

Proof state:
case intro
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ Module.finrank K (R σ K) = Module.finrank K ((σ → K) → K)

Tactic:
classical
rw [Module.finrank_fintype_fun_eq_card, finrank_R]

Result:
no goals

Proof state:
case intro
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ ker (evalᵢ σ K) = ⊥

Tactic:
refine (ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank ?_).mpr (range_evalᵢ σ K)

Result:
case intro
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ Module.finrank K (R σ K) = Module.finrank K ((σ → K) → K)

Proof state:
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
⊢ ker (evalᵢ σ K) = ⊥

Tactic:
cases nonempty_fintype σ

Result:
case intro
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ ker (evalᵢ σ K) = ⊥
-- Mathlib/Data/Nat/PartENat.lean
theorem coe_lt_iff (n : ℕ) (x : PartENat) : (n : PartENat) < x ↔ ∀ h : x.Dom, n < x.get h

Proof state:
n : ℕ
x : PartENat
⊢ (∀ (hy : x.Dom), (↑n).get ⋯ < x.get hy) ↔ ∀ (h : x.Dom), n < x.get h

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
x : PartENat
⊢ ↑n < x ↔ ∀ (h : x.Dom), n < x.get h

Tactic:
simp only [lt_def, exists_prop_of_true, dom_some, forall_true_iff]

Result:
n : ℕ
x : PartENat
⊢ (∀ (hy : x.Dom), (↑n).get ⋯ < x.get hy) ↔ ∀ (h : x.Dom), n < x.get h
-- Mathlib/Algebra/Group/Pi/Units.lean
@[to_additive]
lemma Pi.isUnit_iff :
    IsUnit x ↔ ∀ i, IsUnit (x i)

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
⊢ (∃ b, ∀ (x_1 : ι), (x * b) x_1 = 1 x_1 ∧ (b * x) x_1 = 1 x_1) ↔ ∀ (i : ι), ∃ b, x i * b = 1 ∧ b * x i = 1

Tactic:
exact Classical.skolem (p := fun i y ↦ x i * y = 1 ∧ y * x i = 1).symm

Result:
no goals

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
⊢ IsUnit x ↔ ∀ (i : ι), IsUnit (x i)

Tactic:
simp_rw [isUnit_iff_exists, funext_iff, ← forall_and]

Result:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
⊢ (∃ b, ∀ (x_1 : ι), (x * b) x_1 = 1 x_1 ∧ (b * x) x_1 = 1 x_1) ↔ ∀ (i : ι), ∃ b, x i * b = 1 ∧ b * x i = 1
-- Mathlib/Topology/PartialHomeomorph.lean
theorem ofSet_trans' {s : Set X} (hs : IsOpen s) :
    (ofSet s hs).trans e = e.restr (e.source ∩ s)

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Set X
hs : IsOpen s
⊢ (ofSet s hs).trans e = e.restr (e.source ∩ s)

Tactic:
rw [ofSet_trans, restr_source_inter]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
lemma qaryEntropy_nonneg (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) : 0 ≤ qaryEntropy q p

Proof state:
case inr
q : ℕ
p : ℝ
hp₀✝ : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ 0 ≤ qaryEntropy q p

Tactic:
obtain rfl | hp₁ := hp₁.eq_or_lt

Result:
case inr.inl
q : ℕ
hp₀✝ : 0 ≤ 1
hp₁ : 1 ≤ 1
hp₀ : 0 < 1
⊢ 0 ≤ qaryEntropy q 1

case inr.inr
q : ℕ
p : ℝ
hp₀✝ : 0 ≤ p
hp₁✝ : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 ≤ qaryEntropy q p

Proof state:
case inr.inr
q : ℕ
p : ℝ
hp₀✝ : 0 ≤ p
hp₁✝ : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 ≤ qaryEntropy q p

Tactic:
exact (qaryEntropy_pos hp₀ hp₁).le

Result:
no goals

Proof state:
q : ℕ
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
⊢ 0 ≤ qaryEntropy q p

Tactic:
obtain rfl | hp₀ := hp₀.eq_or_lt

Result:
case inl
q : ℕ
hp₀ : 0 ≤ 0
hp₁ : 0 ≤ 1
⊢ 0 ≤ qaryEntropy q 0

case inr
q : ℕ
p : ℝ
hp₀✝ : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ 0 ≤ qaryEntropy q p

Proof state:
case inr.inl
q : ℕ
hp₀✝ : 0 ≤ 1
hp₁ : 1 ≤ 1
hp₀ : 0 < 1
⊢ 0 ≤ qaryEntropy q 1

Tactic:
simpa [qaryEntropy, -Int.cast_sub] using log_intCast_nonneg _

Result:
no goals

Proof state:
case inl
q : ℕ
hp₀ : 0 ≤ 0
hp₁ : 0 ≤ 1
⊢ 0 ≤ qaryEntropy q 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem smul_set_compl : a • sᶜ = (a • s)ᶜ

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
a : α
⊢ a • sᶜ = (a • s)ᶜ

Tactic:
simp_rw [Set.compl_eq_univ_diff, smul_set_sdiff, smul_set_univ]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_bit0 [AddGroupWithOne α] : ∀ n : ZNum, (n.bit0 : α) = (n : α) + n
  | 0 => (add_zero _).symm
  | pos p => by rw [ZNum.bit0, cast_pos, cast_pos]; rfl
  | neg p => by
    rw [ZNum.bit0, cast_neg, cast_neg, PosNum.cast_bit0, neg_add_rev]

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑p.bit0 = ↑p + ↑p

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(neg p).bit0 = ↑(neg p) + ↑(neg p)

Tactic:
rw [ZNum.bit0, cast_neg, cast_neg, PosNum.cast_bit0, neg_add_rev]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(pos p).bit0 = ↑(pos p) + ↑(pos p)

Tactic:
rw [ZNum.bit0, cast_pos, cast_pos]

Result:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑p.bit0 = ↑p + ↑p
-- Mathlib/Probability/Process/Stopping.lean
theorem add_const [AddGroup ι] [Preorder ι] [AddRightMono ι]
    [AddLeftMono ι] {f : Filtration ι m} {τ : Ω → ι} (hτ : IsStoppingTime f τ)
    {i : ι} (hi : 0 ≤ i) : IsStoppingTime f fun ω => τ ω + i

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : AddGroup ι
inst✝² : Preorder ι
inst✝¹ : AddRightMono ι
inst✝ : AddLeftMono ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
⊢ IsStoppingTime f fun ω => τ ω + i

Tactic:
intro j

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : AddGroup ι
inst✝² : Preorder ι
inst✝¹ : AddRightMono ι
inst✝ : AddLeftMono ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
⊢ MeasurableSet {ω | (fun ω => τ ω + i) ω ≤ j}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : AddGroup ι
inst✝² : Preorder ι
inst✝¹ : AddRightMono ι
inst✝ : AddLeftMono ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
⊢ MeasurableSet {ω | τ ω ≤ j - i}

Tactic:
exact f.mono (sub_le_self j hi) _ (hτ (j - i))

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : AddGroup ι
inst✝² : Preorder ι
inst✝¹ : AddRightMono ι
inst✝ : AddLeftMono ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
⊢ MeasurableSet {ω | (fun ω => τ ω + i) ω ≤ j}

Tactic:
simp_rw [← le_sub_iff_add_le]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : AddGroup ι
inst✝² : Preorder ι
inst✝¹ : AddRightMono ι
inst✝ : AddLeftMono ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
⊢ MeasurableSet {ω | τ ω ≤ j - i}
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem comp {Kf Kg : ℝ≥0} {f : β → γ} {g : α → β} (hf : LipschitzWith Kf f)
    (hg : LipschitzWith Kg g) : LipschitzWith (Kf * Kg) (f ∘ g) := fun x y =>
  calc
    edist (f (g x)) (f (g y)) ≤ Kf * edist (g x) (g y) := hf _ _
    _ ≤ Kf * (Kg * edist x y) := mul_left_mono (hg _ _)
    _ = (Kf * Kg : ℝ≥0) * edist x y

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
Kf Kg : ℝ≥0
f : β → γ
g : α → β
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
x y : α
⊢ ↑Kf * (↑Kg * edist x y) = ↑(Kf * Kg) * edist x y

Tactic:
rw [← mul_assoc, ENNReal.coe_mul]

Result:
no goals
-- Mathlib/Algebra/Order/UpperLower.lean
theorem IsUpperSet.div_right (hs : IsUpperSet s) : IsUpperSet (s / t)

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
hs : IsUpperSet s
⊢ IsUpperSet (s * t⁻¹)

Tactic:
exact hs.mul_right

Result:
no goals

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
hs : IsUpperSet s
⊢ IsUpperSet (s / t)

Tactic:
rw [div_eq_mul_inv]

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
hs : IsUpperSet s
⊢ IsUpperSet (s * t⁻¹)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem le_findIdx_of_not {p : α → Bool} {xs : Array α} {i : Nat} (h : i < xs.size)
    (h2 : ∀ j (hji : j < i), p (xs[j]'(Nat.lt_trans hji h)) = false) : i ≤ xs.findIdx p

Proof state:
case h
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
f : findIdx p xs < i
⊢ False

Tactic:
exact absurd (@findIdx_getElem _ p xs (Nat.lt_trans f h)) (by simpa using h2 (xs.findIdx p) f)

Result:
no goals

Proof state:
case h
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
⊢ ¬i ≤ findIdx p xs → False

Tactic:
intro f

Result:
case h
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
f : ¬i ≤ findIdx p xs
⊢ False

Proof state:
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
⊢ i ≤ findIdx p xs

Tactic:
apply Decidable.byContradiction

Result:
case h
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
⊢ ¬i ≤ findIdx p xs → False

Proof state:
case h
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
f : ¬i ≤ findIdx p xs
⊢ False

Tactic:
simp only [Nat.not_le] at f

Result:
case h
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
f : findIdx p xs < i
⊢ False

Proof state:
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
f : findIdx p xs < i
⊢ ¬p xs[findIdx p xs] = true

Tactic:
simpa using h2 (xs.findIdx p) f

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean
theorem contMDiffAt_prod_iff (f : M → M' × N') :
    ContMDiffAt I (I'.prod J') n f x ↔
      ContMDiffAt I I' n (Prod.fst ∘ f) x ∧ ContMDiffAt I J' n (Prod.snd ∘ f) x

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
F' : Type u_11
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_12
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
x : M
n : WithTop ℕ∞
f : M → M' × N'
⊢ ContMDiffAt I (I'.prod J') n f x ↔ ContMDiffAt I I' n (Prod.fst ∘ f) x ∧ ContMDiffAt I J' n (Prod.snd ∘ f) x

Tactic:
simp_rw [← contMDiffWithinAt_univ]

Result:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
F' : Type u_11
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_12
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
x : M
n : WithTop ℕ∞
f : M → M' × N'
⊢ ContMDiffWithinAt I (I'.prod J') n f univ x ↔
    ContMDiffWithinAt I I' n (Prod.fst ∘ f) univ x ∧ ContMDiffWithinAt I J' n (Prod.snd ∘ f) univ x

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
F' : Type u_11
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_12
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_13
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
x : M
n : WithTop ℕ∞
f : M → M' × N'
⊢ ContMDiffWithinAt I (I'.prod J') n f univ x ↔
    ContMDiffWithinAt I I' n (Prod.fst ∘ f) univ x ∧ ContMDiffWithinAt I J' n (Prod.snd ∘ f) univ x

Tactic:
exact contMDiffWithinAt_prod_iff f

Result:
no goals