harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/PNat/Basic.lean
theorem mod_le (m k : ℕ+) : mod m k ≤ m ∧ mod m k ≤ k

Proof state:
case neg
m k : ℕ+
h : ¬↑m % ↑k = 0
⊢ ↑m % ↑k ≤ ↑m ∧ ↑m % ↑k ≤ ↑k

Tactic:
exact ⟨Nat.mod_le (m : ℕ) (k : ℕ), (Nat.mod_lt (m : ℕ) k.pos).le⟩

Result:
no goals

Proof state:
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k

Tactic:
by_cases h₁ : (m : ℕ) / (k : ℕ) = 0

Result:
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
h₁ : ↑m / ↑k = 0
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k

case neg
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
h₁ : ¬↑m / ↑k = 0
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k

Proof state:
case neg
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
h₁ : ¬↑m / ↑k = 0
h₂ : ↑k * 1 ≤ ↑k * (↑m / ↑k) := Nat.mul_le_mul_left (↑k) (succ_le_of_lt (Nat.pos_of_ne_zero h₁))
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k

Tactic:
rw [mul_one] at h₂

Result:
case neg
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
h₁ : ¬↑m / ↑k = 0
h₂ : ↑k ≤ ↑k * (↑m / ↑k)
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k

Proof state:
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
h₁ : ↑m / ↑k = 0
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k

Tactic:
rw [h₁, mul_zero] at hm

Result:
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : 0 > 0
h₁ : ↑m / ↑k = 0
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k

Proof state:
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑m > 0
⊢ ↑k ≤ ↑m ∧ ↑k ≤ ↑k

Tactic:
rw [← Nat.mod_add_div (m : ℕ) (k : ℕ), h, zero_add] at hm ⊢

Result:
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k

Proof state:
m k : ℕ+
⊢ m.mod k ≤ m ∧ m.mod k ≤ k

Tactic:
change (mod m k : ℕ) ≤ (m : ℕ) ∧ (mod m k : ℕ) ≤ (k : ℕ)

Result:
m k : ℕ+
⊢ ↑(m.mod k) ≤ ↑m ∧ ↑(m.mod k) ≤ ↑k

Proof state:
case neg
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
h₁ : ¬↑m / ↑k = 0
h₂ : ↑k ≤ ↑k * (↑m / ↑k)
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k

Tactic:
exact ⟨h₂, le_refl (k : ℕ)⟩

Result:
no goals

Proof state:
case neg
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
h₁ : ¬↑m / ↑k = 0
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k

Tactic:
let h₂ : (k : ℕ) * 1 ≤ k * (m / k) :=
  Nat.mul_le_mul_left (k : ℕ) (Nat.succ_le_of_lt (Nat.pos_of_ne_zero h₁))

Result:
case neg
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
h₁ : ¬↑m / ↑k = 0
h₂ : ↑k * 1 ≤ ↑k * (↑m / ↑k) := Nat.mul_le_mul_left (↑k) (succ_le_of_lt (Nat.pos_of_ne_zero h₁))
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k

Proof state:
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : 0 > 0
h₁ : ↑m / ↑k = 0
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k

Tactic:
exact (lt_irrefl _ hm).elim

Result:
no goals

Proof state:
m k : ℕ+
⊢ ↑(m.mod k) ≤ ↑m ∧ ↑(m.mod k) ≤ ↑k

Tactic:
rw [mod_coe]

Result:
m k : ℕ+
⊢ (if ↑m % ↑k = 0 then ↑k else ↑m % ↑k) ≤ ↑m ∧ (if ↑m % ↑k = 0 then ↑k else ↑m % ↑k) ≤ ↑k

Proof state:
case pos
m k : ℕ+
h : ↑m % ↑k = 0
⊢ ↑k ≤ ↑m ∧ ↑k ≤ ↑k

Tactic:
have hm : (m : ℕ) > 0 := m.pos

Result:
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑m > 0
⊢ ↑k ≤ ↑m ∧ ↑k ≤ ↑k

Proof state:
m k : ℕ+
⊢ (if ↑m % ↑k = 0 then ↑k else ↑m % ↑k) ≤ ↑m ∧ (if ↑m % ↑k = 0 then ↑k else ↑m % ↑k) ≤ ↑k

Tactic:
split_ifs with h

Result:
case pos
m k : ℕ+
h : ↑m % ↑k = 0
⊢ ↑k ≤ ↑m ∧ ↑k ≤ ↑k

case neg
m k : ℕ+
h : ¬↑m % ↑k = 0
⊢ ↑m % ↑k ≤ ↑m ∧ ↑m % ↑k ≤ ↑k
-- Mathlib/Algebra/Group/Nat/Range.lean
theorem disjoint_range_addLeftEmbedding (a : ℕ) (s : Finset ℕ) :
    Disjoint (range a) (map (addLeftEmbedding a) s)

Proof state:
a : ℕ
s : Finset ℕ
⊢ Disjoint (range a) (map (addLeftEmbedding a) s)

Tactic:
simp_rw [disjoint_left, mem_map, mem_range, addLeftEmbedding_apply]

Result:
a : ℕ
s : Finset ℕ
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 < a → ¬∃ a_3 ∈ s, a + a_3 = a_1

Proof state:
a : ℕ
s : Finset ℕ
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 < a → ¬∃ a_3 ∈ s, a + a_3 = a_1

Tactic:
rintro _ h ⟨l, -, rfl⟩

Result:
case intro.intro
a : ℕ
s : Finset ℕ
l : ℕ
h : a + l < a
⊢ False

Proof state:
case intro.intro
a : ℕ
s : Finset ℕ
l : ℕ
h : a + l < a
⊢ False

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Normed/Field/InfiniteSum.lean
theorem summable_sum_mul_range_of_summable_norm' {f g : ℕ → R}
    (hf : Summable fun x => ‖f x‖) (h'f : Summable f)
    (hg : Summable fun x => ‖g x‖) (h'g : Summable g) :
    Summable fun n => ∑ k ∈ range (n + 1), f k * g (n - k)

Proof state:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
h'f : Summable f
hg : Summable fun x => ‖g x‖
h'g : Summable g
⊢ Summable fun n => ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2

Tactic:
exact summable_sum_mul_antidiagonal_of_summable_norm' hf h'f hg h'g

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
h'f : Summable f
hg : Summable fun x => ‖g x‖
h'g : Summable g
⊢ Summable fun n => ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]

Result:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
h'f : Summable f
hg : Summable fun x => ‖g x‖
h'g : Summable g
⊢ Summable fun n => ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2
-- Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean
lemma llp_isStableUnderCoproductsOfShape (J : Type*) :
    T.llp.IsStableUnderCoproductsOfShape J

Proof state:
case hW
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
⊢ ∀ (X₁ X₂ : J → C) [inst : Limits.HasCoproduct X₁] [inst_1 : Limits.HasCoproduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), T.llp (f j)) → T.llp (Limits.Sigma.map f)

Tactic:
intro A B _ _ f hf X Y p hp

Result:
case hW
C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasCoproduct A
inst✝ : Limits.HasCoproduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.llp (f j)
X Y : C
p : X ⟶ Y
hp : T p
⊢ HasLiftingProperty (Limits.Sigma.map f) p

Proof state:
case hW
C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasCoproduct A
inst✝ : Limits.HasCoproduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.llp (f j)
X Y : C
p : X ⟶ Y
hp : T p
⊢ HasLiftingProperty (Limits.Sigma.map f) p

Tactic:
have := fun j ↦ hf j _ hp

Result:
case hW
C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasCoproduct A
inst✝ : Limits.HasCoproduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.llp (f j)
X Y : C
p : X ⟶ Y
hp : T p
this : ∀ (j : J), HasLiftingProperty (f j) p
⊢ HasLiftingProperty (Limits.Sigma.map f) p

Proof state:
case hW
C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasCoproduct A
inst✝ : Limits.HasCoproduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.llp (f j)
X Y : C
p : X ⟶ Y
hp : T p
this : ∀ (j : J), HasLiftingProperty (f j) p
⊢ HasLiftingProperty (Limits.Sigma.map f) p

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
⊢ T.llp.IsStableUnderCoproductsOfShape J

Tactic:
apply IsStableUnderCoproductsOfShape.mk

Result:
case hW
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
⊢ ∀ (X₁ X₂ : J → C) [inst : Limits.HasCoproduct X₁] [inst_1 : Limits.HasCoproduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), T.llp (f j)) → T.llp (Limits.Sigma.map f)
-- Mathlib/Control/Traversable/Instances.lean
theorem mem_traverse {f : α' → Set β'} :
    ∀ (l : List α') (n : List β'), n ∈ traverse f l ↔ Forall₂ (fun b a => b ∈ f a) n l
  | [], [] => by simp
  | a :: as, [] => by simp
  | [], b :: bs => by simp
  | a :: as, b :: bs => by simp [mem_traverse as bs]

Proof state:
α' β' : Type u
f : α' → Set β'
b : β'
bs : List β'
⊢ b :: bs ∈ traverse f [] ↔ Forall₂ (fun b a => b ∈ f a) (b :: bs) []

Tactic:
simp

Result:
no goals

Proof state:
α' β' : Type u
f : α' → Set β'
a : α'
as : List α'
⊢ [] ∈ traverse f (a :: as) ↔ Forall₂ (fun b a => b ∈ f a) [] (a :: as)

Tactic:
simp

Result:
no goals

Proof state:
α' β' : Type u
f : α' → Set β'
⊢ [] ∈ traverse f [] ↔ Forall₂ (fun b a => b ∈ f a) [] []

Tactic:
simp

Result:
no goals

Proof state:
α' β' : Type u
f : α' → Set β'
a : α'
as : List α'
b : β'
bs : List β'
⊢ b :: bs ∈ traverse f (a :: as) ↔ Forall₂ (fun b a => b ∈ f a) (b :: bs) (a :: as)

Tactic:
simp [mem_traverse as bs]

Result:
no goals
-- Mathlib/LinearAlgebra/FreeProduct/Basic.lean
theorem induction_lon {R : Type*} [Semiring R] {ι: Type*} [DecidableEq ι]
    {M : ι → Type*} [(i: ι) → AddCommMonoid <| M i] [(i : ι) → Module R (M i)]
    {C: (⨁ i, M i) → Prop} (x : ⨁ i, M i)
    (H_zero : C 0)
    (H_basic : ∀ i (x : M i), C (lof R ι M i x))
    (H_plus : ∀ (x y : ⨁ i, M i), C x → C y → C (x + y)) : C x

Proof state:
case H_plus
R : Type u_1
inst✝³ : Semiring R
ι : Type u_2
inst✝² : DecidableEq ι
M : ι → Type u_3
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
C : (⨁ (i : ι), M i) → Prop
H_zero : C 0
H_basic : ∀ (i : ι) (x : M i), C ((lof R ι M i) x)
H_plus : ∀ (x y : ⨁ (i : ι), M i), C x → C y → C (x + y)
x y : ⨁ (i : ι), M i
hx : C x
hy : C y
⊢ C (x + y)

Tactic:
exact H_plus x y hx hy

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Semiring R
ι : Type u_2
inst✝² : DecidableEq ι
M : ι → Type u_3
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
C : (⨁ (i : ι), M i) → Prop
x : ⨁ (i : ι), M i
H_zero : C 0
H_basic : ∀ (i : ι) (x : M i), C ((lof R ι M i) x)
H_plus : ∀ (x y : ⨁ (i : ι), M i), C x → C y → C (x + y)
⊢ C x

Tactic:
induction x using DirectSum.induction_on with
| H_zero => exact H_zero
| H_basic => exact H_basic _ _
| H_plus x y hx hy => exact H_plus x y hx hy

Result:
no goals

Proof state:
case H_basic
R : Type u_1
inst✝³ : Semiring R
ι : Type u_2
inst✝² : DecidableEq ι
M : ι → Type u_3
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
C : (⨁ (i : ι), M i) → Prop
H_zero : C 0
H_basic : ∀ (i : ι) (x : M i), C ((lof R ι M i) x)
H_plus : ∀ (x y : ⨁ (i : ι), M i), C x → C y → C (x + y)
i✝ : ι
x✝ : M i✝
⊢ C ((of M i✝) x✝)

Tactic:
exact H_basic _ _

Result:
no goals

Proof state:
case H_zero
R : Type u_1
inst✝³ : Semiring R
ι : Type u_2
inst✝² : DecidableEq ι
M : ι → Type u_3
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
C : (⨁ (i : ι), M i) → Prop
H_zero : C 0
H_basic : ∀ (i : ι) (x : M i), C ((lof R ι M i) x)
H_plus : ∀ (x y : ⨁ (i : ι), M i), C x → C y → C (x + y)
⊢ C 0

Tactic:
exact H_zero

Result:
no goals
-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
lemma levyProkhorovEDist_self (μ : Measure Ω) :
    levyProkhorovEDist μ μ = 0

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ : Measure Ω
ε : ℝ≥0∞
x✝¹ : ε ∈ Ioo 0 ⊤
B : Set Ω
x✝ : MeasurableSet B
hε₀ : 0 < ε
hε_top : ε < ⊤
⊢ μ B ≤ μ (thickening ε.toReal B) + ε

Tactic:
refine le_add_right <| measure_mono <| self_subset_thickening ?_ _

Result:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ : Measure Ω
ε : ℝ≥0∞
x✝¹ : ε ∈ Ioo 0 ⊤
B : Set Ω
x✝ : MeasurableSet B
hε₀ : 0 < ε
hε_top : ε < ⊤
⊢ 0 < ε.toReal

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ : Measure Ω
⊢ levyProkhorovEDist μ μ ≤ sInf (Ioo 0 ⊤)

Tactic:
refine sInf_le_sInf fun ε ⟨hε₀, hε_top⟩ B _ ↦ and_self_iff.2 ?_

Result:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ : Measure Ω
ε : ℝ≥0∞
x✝¹ : ε ∈ Ioo 0 ⊤
B : Set Ω
x✝ : MeasurableSet B
hε₀ : 0 < ε
hε_top : ε < ⊤
⊢ μ B ≤ μ (thickening ε.toReal B) + ε

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ : Measure Ω
⊢ levyProkhorovEDist μ μ = 0

Tactic:
rw [← nonpos_iff_eq_zero, ← csInf_Ioo zero_lt_top]

Result:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ : Measure Ω
⊢ levyProkhorovEDist μ μ ≤ sInf (Ioo 0 ⊤)

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ : Measure Ω
ε : ℝ≥0∞
x✝¹ : ε ∈ Ioo 0 ⊤
B : Set Ω
x✝ : MeasurableSet B
hε₀ : 0 < ε
hε_top : ε < ⊤
⊢ 0 < ε.toReal

Tactic:
exact ENNReal.toReal_pos hε₀.ne' hε_top.ne

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContDiffAt.iteratedFDeriv_right {i : ℕ} (hf : ContDiffAt 𝕜 n f x₀)
    (hmn : m + i ≤ n) : ContDiffAt 𝕜 m (iteratedFDeriv 𝕜 i f) x₀

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
m n : WithTop ℕ∞
i : ℕ
hf : ContDiffAt 𝕜 n f x₀
hmn : m + ↑i ≤ n
⊢ ContDiffAt 𝕜 m (iteratedFDeriv 𝕜 i f) x₀

Tactic:
rw [← iteratedFDerivWithin_univ, ← contDiffWithinAt_univ] at *

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
m n : WithTop ℕ∞
i : ℕ
hf : ContDiffWithinAt 𝕜 n f univ x₀
hmn : m + ↑i ≤ n
⊢ ContDiffWithinAt 𝕜 m (iteratedFDerivWithin 𝕜 i f univ) univ x₀

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
m n : WithTop ℕ∞
i : ℕ
hf : ContDiffWithinAt 𝕜 n f univ x₀
hmn : m + ↑i ≤ n
⊢ ContDiffWithinAt 𝕜 m (iteratedFDerivWithin 𝕜 i f univ) univ x₀

Tactic:
exact hf.iteratedFDerivWithin_right uniqueDiffOn_univ hmn trivial

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem setLIntegral_map [MeasurableSpace β] {f : β → ℝ≥0∞} {g : α → β} {s : Set β}
    (hs : MeasurableSet s) (hf : Measurable f) (hg : Measurable g) :
    ∫⁻ y in s, f y ∂map g μ = ∫⁻ x in g ⁻¹' s, f (g x) ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
s : Set β
hs : MeasurableSet s
hf : Measurable f
hg : Measurable g
⊢ ∫⁻ (y : β) in s, f y ∂Measure.map g μ = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ

Tactic:
rw [restrict_map hg hs, lintegral_map hf hg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.udiv_ofNat_eq_of_lt (w : Nat) (x : BitVec w) (n : Nat) (k : Nat) (hk : 2 ^ k = n) (hlt : k < w) :
    x / (BitVec.ofNat w n) = x >>> k

Proof state:
w : Nat
x : BitVec w
n k : Nat
hk : 2 ^ k = n
hlt : k < w
⊢ x / BitVec.ofNat w n = x >>> k

Tactic:
have : BitVec.ofNat w n = BitVec.twoPow w k := by simp [bv_toNat, hk]

Result:
w : Nat
x : BitVec w
n k : Nat
hk : 2 ^ k = n
hlt : k < w
this : BitVec.ofNat w n = BitVec.twoPow w k
⊢ x / BitVec.ofNat w n = x >>> k

Proof state:
w : Nat
x : BitVec w
n k : Nat
hk : 2 ^ k = n
hlt : k < w
this : BitVec.ofNat w n = BitVec.twoPow w k
⊢ k < w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
n k : Nat
hk : 2 ^ k = n
hlt : k < w
⊢ BitVec.ofNat w n = BitVec.twoPow w k

Tactic:
simp [bv_toNat, hk]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
n k : Nat
hk : 2 ^ k = n
hlt : k < w
this : BitVec.ofNat w n = BitVec.twoPow w k
⊢ x / BitVec.ofNat w n = x >>> k

Tactic:
rw [this, BitVec.udiv_twoPow_eq_of_lt (hk := by omega)]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
lemma locallyLinear [ExplicitDisjoint t] [NoAccidental t] : (graph t).LocallyLinear

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝¹ : ExplicitDisjoint t
inst✝ : NoAccidental t
⊢ (graph t).LocallyLinear

Tactic:
refine ⟨?_, fun x y hxy ↦ ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝¹ : ExplicitDisjoint t
inst✝ : NoAccidental t
⊢ (graph t).EdgeDisjointTriangles

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝¹ : ExplicitDisjoint t
inst✝ : NoAccidental t
x y : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
⊢ ∃ s, (graph t).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝¹ : ExplicitDisjoint t
inst✝ : NoAccidental t
⊢ ((graph t).cliqueSet 3).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton

Tactic:
convert map_toTriangle_disjoint t

Result:
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝¹ : ExplicitDisjoint t
inst✝ : NoAccidental t
⊢ (graph t).cliqueSet 3 = ↑(map toTriangle t)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝¹ : ExplicitDisjoint t
inst✝ : NoAccidental t
x y : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
⊢ ∃ s, (graph t).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s

Tactic:
obtain ⟨z, hz, hxy⟩ := exists_mem_toTriangle hxy

Result:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝¹ : ExplicitDisjoint t
inst✝ : NoAccidental t
x y : α ⊕ β ⊕ γ
hxy✝ : (graph t).Adj x y
z : α × β × γ
hz : z ∈ t
hxy : x ∈ toTriangle z ∧ y ∈ toTriangle z
⊢ ∃ s, (graph t).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s

Proof state:
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝¹ : ExplicitDisjoint t
inst✝ : NoAccidental t
⊢ (graph t).cliqueSet 3 = ↑(map toTriangle t)

Tactic:
rw [cliqueSet_eq_image, coe_map]

Result:
no goals

Proof state:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝¹ : ExplicitDisjoint t
inst✝ : NoAccidental t
x y : α ⊕ β ⊕ γ
hxy✝ : (graph t).Adj x y
z : α × β × γ
hz : z ∈ t
hxy : x ∈ toTriangle z ∧ y ∈ toTriangle z
⊢ ∃ s, (graph t).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s

Tactic:
exact ⟨_, toTriangle_is3Clique hz, hxy⟩

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝¹ : ExplicitDisjoint t
inst✝ : NoAccidental t
⊢ (graph t).EdgeDisjointTriangles

Tactic:
unfold EdgeDisjointTriangles

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝¹ : ExplicitDisjoint t
inst✝ : NoAccidental t
⊢ ((graph t).cliqueSet 3).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton
-- Mathlib/FieldTheory/SplittingField/IsSplittingField.lean
theorem IsIntegral.mem_intermediateField_of_minpoly_splits {x : L} (int : IsIntegral K x)
    {F : IntermediateField K L} (h : Splits (algebraMap K F) (minpoly K x)) : x ∈ F

Proof state:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
int : IsIntegral K x
F : IntermediateField K L
h : Splits (algebraMap K ↥F) (minpoly K x)
⊢ x ∈ F

Tactic:
rw [← F.fieldRange_val]

Result:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
int : IsIntegral K x
F : IntermediateField K L
h : Splits (algebraMap K ↥F) (minpoly K x)
⊢ x ∈ F.val.fieldRange

Proof state:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
int : IsIntegral K x
F : IntermediateField K L
h : Splits (algebraMap K ↥F) (minpoly K x)
⊢ x ∈ F.val.fieldRange

Tactic:
exact int.mem_range_algebraMap_of_minpoly_splits h

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem le_sInf {A : C} (s : Set (Subobject A)) (f : Subobject A) (k : ∀ g ∈ s, f ≤ g) :
    f ≤ sInf s

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, f ≤ g
⊢ f ≤ sInf s

Tactic:
fapply le_of_comm

Result:
case f
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, f ≤ g
⊢ underlying.obj f ⟶ underlying.obj (sInf s)

case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, f ≤ g
⊢ ?f ≫ (sInf s).arrow = f.arrow

Proof state:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, f ≤ g
⊢ (limit.lift (wideCospan s) (leInfCone s f k) ≫ (underlyingIso (widePullbackι s)).inv) ≫ (sInf s).arrow = f.arrow

Tactic:
dsimp [sInf]

Result:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, f ≤ g
⊢ (limit.lift (wideCospan s) (leInfCone s f k) ≫ (underlyingIso (widePullbackι s)).inv) ≫ (mk (widePullbackι s)).arrow =
    f.arrow

Proof state:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, f ≤ g
⊢ (limit.lift (wideCospan s) (leInfCone s f k) ≫ (underlyingIso (widePullbackι s)).inv) ≫ (mk (widePullbackι s)).arrow =
    f.arrow

Tactic:
rw [assoc, underlyingIso_arrow, widePullbackι, limit.lift_π, leInfCone_π_app_none]

Result:
no goals

Proof state:
case f
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, f ≤ g
⊢ underlying.obj f ⟶ underlying.obj (sInf s)

Tactic:
exact Limits.limit.lift _ (leInfCone s f k) ≫ (underlyingIso _).inv

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_div_le_neg_one (h1 : a < 0) (h2 : -1 ≤ a) : 1 / a ≤ -1 :=
  suffices 1 / a ≤ 1 / -1 by rwa [one_div_neg_one_eq_neg_one] at this
  one_div_le_one_div_of_neg_of_le h1 h2

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a : α
h1 : a < 0
h2 : -1 ≤ a
this : 1 / a ≤ 1 / -1
⊢ 1 / a ≤ -1

Tactic:
rwa [one_div_neg_one_eq_neg_one] at this

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/EraseIdx.lean
theorem mem_eraseIdx_iff_get {x : α} {l} {k} :
    x ∈ eraseIdx l k ↔ ∃ i : Fin l.length, ↑i ≠ k ∧ l.get i = x

Proof state:
α : Type u
x : α
l : List α
k : Nat
⊢ (∃ i, ¬i = k ∧ ∃ x_1, l[i] = x) ↔ ∃ i, ¬↑i = k ∧ l[↑i] = x

Tactic:
constructor

Result:
case mp
α : Type u
x : α
l : List α
k : Nat
⊢ (∃ i, ¬i = k ∧ ∃ x_1, l[i] = x) → ∃ i, ¬↑i = k ∧ l[↑i] = x

case mpr
α : Type u
x : α
l : List α
k : Nat
⊢ (∃ i, ¬↑i = k ∧ l[↑i] = x) → ∃ i, ¬i = k ∧ ∃ x_1, l[i] = x

Proof state:
case mpr
α : Type u
x : α
l : List α
k : Nat
⊢ (∃ i, ¬↑i = k ∧ l[↑i] = x) → ∃ i, ¬i = k ∧ ∃ x_1, l[i] = x

Tactic:
rintro ⟨i, h, rfl⟩

Result:
case mpr.intro.intro
α : Type u
l : List α
k : Nat
i : Fin l.length
h : ¬↑i = k
⊢ ∃ i_1, ¬i_1 = k ∧ ∃ x, l[i_1] = l[↑i]

Proof state:
case mpr.intro.intro
α : Type u
l : List α
k : Nat
i : Fin l.length
h : ¬↑i = k
⊢ ∃ i_1, ¬i_1 = k ∧ ∃ x, l[i_1] = l[↑i]

Tactic:
exact ⟨i.1, h, i.2, rfl⟩

Result:
no goals

Proof state:
α : Type u
x : α
l : List α
k : Nat
⊢ x ∈ l.eraseIdx k ↔ ∃ i, ↑i ≠ k ∧ l.get i = x

Tactic:
simp only [mem_eraseIdx_iff_getElem, ne_eq, exists_and_left, get_eq_getElem]

Result:
α : Type u
x : α
l : List α
k : Nat
⊢ (∃ i, ¬i = k ∧ ∃ x_1, l[i] = x) ↔ ∃ i, ¬↑i = k ∧ l[↑i] = x

Proof state:
case mp
α : Type u
x : α
l : List α
k : Nat
⊢ (∃ i, ¬i = k ∧ ∃ x_1, l[i] = x) → ∃ i, ¬↑i = k ∧ l[↑i] = x

Tactic:
rintro ⟨i, h, w, rfl⟩

Result:
case mp.intro.intro.intro
α : Type u
l : List α
k i : Nat
h : ¬i = k
w : i < l.length
⊢ ∃ i_1, ¬↑i_1 = k ∧ l[↑i_1] = l[i]

Proof state:
case mp.intro.intro.intro
α : Type u
l : List α
k i : Nat
h : ¬i = k
w : i < l.length
⊢ ∃ i_1, ¬↑i_1 = k ∧ l[↑i_1] = l[i]

Tactic:
exact ⟨⟨i, w⟩, h, rfl⟩

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem IsLimit.sSup_Iio {o : Ordinal} (h : IsLimit o) : sSup (Iio o) = o

Proof state:
case H
o : Ordinal.{u_4}
h : o.IsLimit
a : Ordinal.{u_4}
ha : a < o
⊢ a < sSup fun a => Preorder.toLT.1 a o

Tactic:
exact (lt_succ a).trans_le (le_csSup bddAbove_Iio (h.succ_lt ha))

Result:
no goals

Proof state:
o : Ordinal.{u_4}
h : o.IsLimit
⊢ sSup (Iio o) = o

Tactic:
apply (csSup_le' (fun a ha ↦ le_of_lt ha)).antisymm

Result:
o : Ordinal.{u_4}
h : o.IsLimit
⊢ o ≤ sSup fun a => Preorder.toLT.1 a o

Proof state:
o : Ordinal.{u_4}
h : o.IsLimit
⊢ o ≤ sSup fun a => Preorder.toLT.1 a o

Tactic:
apply le_of_forall_lt

Result:
case H
o : Ordinal.{u_4}
h : o.IsLimit
⊢ ∀ c < o, c < sSup fun a => Preorder.toLT.1 a o

Proof state:
case H
o : Ordinal.{u_4}
h : o.IsLimit
⊢ ∀ c < o, c < sSup fun a => Preorder.toLT.1 a o

Tactic:
intro a ha

Result:
case H
o : Ordinal.{u_4}
h : o.IsLimit
a : Ordinal.{u_4}
ha : a < o
⊢ a < sSup fun a => Preorder.toLT.1 a o