harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Chain.lean
theorem Chain'.imp {S : α → α → Prop} (H : ∀ a b, R a b → S a b) {l : List α} (p : Chain' R l) :
    Chain' S l

Proof state:
α : Type u
R S : α → α → Prop
H : ∀ (a b : α), R a b → S a b
l : List α
p : Chain' R l
⊢ Chain' S l

Tactic:
cases l <;> [trivial; exact Chain.imp H p]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_setIfInBounds (v : Vector α n) (i : Nat) (x : α) (j : Nat) :
    (v.setIfInBounds i x)[j]? = if i = j then if i < n then some x else none else v[j]?

Proof state:
case mk
α : Type u_1
i : Nat
x : α
j : Nat
v : Array α
⊢ ({ toArray := v, size_toArray := ⋯ }.setIfInBounds i x)[j]? =
    if i = j then if i < v.size then some x else none else { toArray := v, size_toArray := ⋯ }[j]?

Tactic:
simp [Array.getElem?_setIfInBounds]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
x : α
j : Nat
⊢ (v.setIfInBounds i x)[j]? = if i = j then if i < n then some x else none else v[j]?

Tactic:
rcases v with ⟨v, rfl⟩

Result:
case mk
α : Type u_1
i : Nat
x : α
j : Nat
v : Array α
⊢ ({ toArray := v, size_toArray := ⋯ }.setIfInBounds i x)[j]? =
    if i = j then if i < v.size then some x else none else { toArray := v, size_toArray := ⋯ }[j]?
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalars_series_of_subsingleton [Subsingleton E] : ofScalars E c = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
c : ℕ → 𝕜
inst✝ : Subsingleton E
⊢ ∀ (n : ℕ) (x : Fin n → E), (c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) x = (0 n) x

Tactic:
exact fun _ _ ↦ Subsingleton.allEq _ _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
c : ℕ → 𝕜
inst✝ : Subsingleton E
⊢ ofScalars E c = 0

Tactic:
simp_rw [FormalMultilinearSeries.ext_iff, ofScalars, ContinuousMultilinearMap.ext_iff]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
c : ℕ → 𝕜
inst✝ : Subsingleton E
⊢ ∀ (n : ℕ) (x : Fin n → E), (c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) x = (0 n) x
-- Mathlib/Data/Real/EReal.lean
lemma toReal_nonneg {x : EReal} (hx : 0 ≤ x) : 0 ≤ x.toReal

Proof state:
x : EReal
hx : 0 ≤ x
⊢ 0 ≤ x.toReal

Tactic:
cases x

Result:
case h_bot
hx : 0 ≤ ⊥
⊢ 0 ≤ ⊥.toReal

case h_real
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ 0 ≤ (↑a✝).toReal

case h_top
hx : 0 ≤ ⊤
⊢ 0 ≤ ⊤.toReal

Proof state:
case h_real
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ 0 ≤ (↑a✝).toReal

Tactic:
exact toReal_coe _ ▸ EReal.coe_nonneg.mp hx

Result:
no goals

Proof state:
case h_top
hx : 0 ≤ ⊤
⊢ 0 ≤ ⊤.toReal

Tactic:
norm_num

Result:
no goals

Proof state:
case h_bot
hx : 0 ≤ ⊥
⊢ 0 ≤ ⊥.toReal

Tactic:
norm_num

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem HasIntegral.add (h : HasIntegral I l f vol y) (h' : HasIntegral I l g vol y') :
    HasIntegral I l (f + g) vol (y + y')

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
h : HasIntegral I l f vol y
h' : HasIntegral I l g vol y'
⊢ HasIntegral I l (f + g) vol (y + y')

Tactic:
simpa only [HasIntegral, ← integralSum_add] using h.add h'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem lt_of_add_lt_add_right {a b c : Int} (h : a + b < c + b) : a < c :=
  Int.lt_of_add_lt_add_left (a := b) <| by rwa [Int.add_comm b a, Int.add_comm b c]

Proof state:
a b c : Int
h : a + b < c + b
⊢ b + a < b + c

Tactic:
rwa [Int.add_comm b a, Int.add_comm b c]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/RationalRoot.lean
theorem scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero {p : A[X]} {r : A} {s : M}
    (hr : aeval (mk' S r s) p = 0) : aeval (algebraMap A S r) (scaleRoots p s) = 0

Proof state:
A : Type u_1
S : Type u_4
inst✝³ : CommRing A
inst✝² : CommRing S
M : Submonoid A
inst✝¹ : Algebra A S
inst✝ : IsLocalization M S
p : A[X]
r : A
s : ↥M
hr : (aeval (mk' S r s)) p = 0
⊢ (aeval ((algebraMap A S) r)) (p.scaleRoots ↑s) = 0

Tactic:
convert scaleRoots_eval₂_eq_zero (algebraMap A S) hr

Result:
case h.e'_2.h.e
A : Type u_1
S : Type u_4
inst✝³ : CommRing A
inst✝² : CommRing S
M : Submonoid A
inst✝¹ : Algebra A S
inst✝ : IsLocalization M S
p : A[X]
r : A
s : ↥M
hr : (aeval (mk' S r s)) p = 0
⊢ ⇑(aeval ((algebraMap A S) r)) = eval₂ (algebraMap A S) ((algebraMap A S) ↑s * mk' S r s)

Proof state:
case h.e'_2.h.e.h
A : Type u_1
S : Type u_4
inst✝³ : CommRing A
inst✝² : CommRing S
M : Submonoid A
inst✝¹ : Algebra A S
inst✝ : IsLocalization M S
p : A[X]
r : A
s : ↥M
hr : (aeval (mk' S r s)) p = 0
x✝ : A[X]
⊢ (aeval ((algebraMap A S) r)) x✝ = eval₂ (algebraMap A S) ((algebraMap A S) ↑s * mk' S r s) x✝

Tactic:
rw [aeval_def, mk'_spec' _ r s]

Result:
no goals

Proof state:
case h.e'_2.h.e
A : Type u_1
S : Type u_4
inst✝³ : CommRing A
inst✝² : CommRing S
M : Submonoid A
inst✝¹ : Algebra A S
inst✝ : IsLocalization M S
p : A[X]
r : A
s : ↥M
hr : (aeval (mk' S r s)) p = 0
⊢ ⇑(aeval ((algebraMap A S) r)) = eval₂ (algebraMap A S) ((algebraMap A S) ↑s * mk' S r s)

Tactic:
funext

Result:
case h.e'_2.h.e.h
A : Type u_1
S : Type u_4
inst✝³ : CommRing A
inst✝² : CommRing S
M : Submonoid A
inst✝¹ : Algebra A S
inst✝ : IsLocalization M S
p : A[X]
r : A
s : ↥M
hr : (aeval (mk' S r s)) p = 0
x✝ : A[X]
⊢ (aeval ((algebraMap A S) r)) x✝ = eval₂ (algebraMap A S) ((algebraMap A S) ↑s * mk' S r s) x✝
-- Mathlib/Combinatorics/SimpleGraph/Partition.lean
theorem partOfVertex_ne_of_adj {v w : V} (h : G.Adj v w) : P.partOfVertex v ≠ P.partOfVertex w

Proof state:
V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
h : G.Adj v w
hn : P.partOfVertex v = P.partOfVertex w
hw : w ∈ P.partOfVertex w
⊢ False

Tactic:
rw [← hn] at hw

Result:
V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
h : G.Adj v w
hn : P.partOfVertex v = P.partOfVertex w
hw : w ∈ P.partOfVertex v
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
h : G.Adj v w
hn : P.partOfVertex v = P.partOfVertex w
hw : w ∈ P.partOfVertex v
⊢ False

Tactic:
exact P.independent _ (P.partOfVertex_mem v) (P.mem_partOfVertex v) hw (G.ne_of_adj h) h

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
h : G.Adj v w
hn : P.partOfVertex v = P.partOfVertex w
⊢ False

Tactic:
have hw := P.mem_partOfVertex w

Result:
V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
h : G.Adj v w
hn : P.partOfVertex v = P.partOfVertex w
hw : w ∈ P.partOfVertex w
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
h : G.Adj v w
⊢ P.partOfVertex v ≠ P.partOfVertex w

Tactic:
intro hn

Result:
V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
h : G.Adj v w
hn : P.partOfVertex v = P.partOfVertex w
⊢ False
-- Mathlib/Analysis/NormedSpace/RCLike.lean
theorem RCLike.norm_coe_norm {z : E} : ‖(‖z‖ : 𝕜)‖ = ‖z‖

Proof state:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
E : Type u_2
inst✝ : NormedAddCommGroup E
z : E
⊢ ‖↑‖z‖‖ = ‖z‖

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Category/AlgebraCat/Basic.lean
lemma inv_hom_apply {A B : AlgebraCat.{v} R} (e : A ≅ B) (x : A) : e.inv (e.hom x) = x

Proof state:
R : Type u
inst✝ : CommRing R
A B : AlgebraCat R
e : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom (e.hom ≫ e.inv)) x = x

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
A B : AlgebraCat R
e : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
rw [← comp_apply]

Result:
R : Type u
inst✝ : CommRing R
A B : AlgebraCat R
e : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom (e.hom ≫ e.inv)) x = x
-- Mathlib/Topology/LocallyConstant/Basic.lean
theorem comp_continuous [TopologicalSpace Y] {g : Y → Z} {f : X → Y} (hg : IsLocallyConstant g)
    (hf : Continuous f) : IsLocallyConstant (g ∘ f) := fun s => by
  rw [Set.preimage_comp]
  exact hf.isOpen_preimage _ (hg _)

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : Y → Z
f : X → Y
hg : IsLocallyConstant g
hf : Continuous f
s : Set Z
⊢ IsOpen (g ∘ f ⁻¹' s)

Tactic:
rw [Set.preimage_comp]

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : Y → Z
f : X → Y
hg : IsLocallyConstant g
hf : Continuous f
s : Set Z
⊢ IsOpen (f ⁻¹' (g ⁻¹' s))

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : Y → Z
f : X → Y
hg : IsLocallyConstant g
hf : Continuous f
s : Set Z
⊢ IsOpen (f ⁻¹' (g ⁻¹' s))

Tactic:
exact hf.isOpen_preimage _ (hg _)

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
lemma restrictSubtype_isBasis_iff {Y : Set α} {I X : Set Y} :
    (M.restrictSubtype Y).IsBasis I X ↔ M.IsBasis' I X

Proof state:
α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ (M.restrictSubtype Y).IsBasis I X ↔ M.IsBasis' (Subtype.val '' I) (Subtype.val '' X)

Tactic:
rw [restrictSubtype, comap_isBasis_iff, and_iff_right Subtype.val_injective.injOn,
  and_iff_left_of_imp, isBasis_restrict_iff', isBasis'_iff_isBasis_inter_ground]

Result:
α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ M.IsBasis (↑I) (↑X ∩ M.E) ∧ ↑X ⊆ Y ↔ M.IsBasis (Subtype.val '' I) (Subtype.val '' X ∩ M.E)

α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ (M ↾ Y).IsBasis ↑I ↑X → I ⊆ X

Proof state:
α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ (M ↾ Y).IsBasis ↑I ↑X → I ⊆ X

Tactic:
exact fun h ↦ (image_subset_image_iff Subtype.val_injective).1 h.subset

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ M.IsBasis (↑I) (↑X ∩ M.E) ∧ ↑X ⊆ Y ↔ M.IsBasis (Subtype.val '' I) (Subtype.val '' X ∩ M.E)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_X_mul : eval₂ f x (X * p) = eval₂ f x p * x

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x (X * p) = eval₂ f x p * x

Tactic:
rw [X_mul, eval₂_mul_X]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_congr {f g : α → ℝ≥0∞} (h : ∀ a, f a = g a) : ∫⁻ a, f a ∂μ = ∫⁻ a, g a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ (a : α), f a = g a
⊢ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

Tactic:
simp only [h]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem Ioc_subset_Ioo_succ_right_of_not_isMax (hb : ¬IsMax b) : Ioc a b ⊆ Ioo a (succ b)

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ioi a ∩ Iic b ⊆ Ioi a ∩ Iio (succ b)

Tactic:
gcongr

Result:
case H
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Iic b ⊆ Iio (succ b)

Proof state:
case H
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
a✝ : α
h : a✝ ∈ Iic b
⊢ a✝ ∈ Iio (succ b)

Tactic:
apply Iic_subset_Iio_succ_of_not_isMax hb h

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ioc a b ⊆ Ioo a (succ b)

Tactic:
rw [← Ioi_inter_Iio, ← Ioi_inter_Iic]

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ioi a ∩ Iic b ⊆ Ioi a ∩ Iio (succ b)

Proof state:
case H
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Iic b ⊆ Iio (succ b)

Tactic:
intro _ h

Result:
case H
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
a✝ : α
h : a✝ ∈ Iic b
⊢ a✝ ∈ Iio (succ b)
-- Mathlib/NumberTheory/DiophantineApproximation/Basic.lean
theorem exists_nat_abs_mul_sub_round_le (ξ : ℝ) {n : ℕ} (n_pos : 0 < n) :
    ∃ k : ℕ, 0 < k ∧ k ≤ n ∧ |↑k * ξ - round (↑k * ξ)| ≤ 1 / (n + 1)

Proof state:
case intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < ↑k.toNat
hk₁ : ↑k.toNat ≤ ↑n
h : |↑↑k.toNat * ξ - ↑j| ≤ 1 / (↑n + 1)
hk : ↑k.toNat = k
⊢ ∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)

Tactic:
exact ⟨k.toNat, natCast_pos.mp hk₀, Nat.cast_le.mp hk₁, (round_le (↑k.toNat * ξ) j).trans h⟩

Result:
no goals

Proof state:
ξ : ℝ
n : ℕ
n_pos : 0 < n
⊢ ∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)

Tactic:
obtain ⟨j, k, hk₀, hk₁, h⟩ := exists_int_int_abs_mul_sub_le ξ n_pos

Result:
case intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
⊢ ∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)

Proof state:
case intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
⊢ ∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)

Tactic:
have hk := toNat_of_nonneg hk₀.le

Result:
case intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk : ↑k.toNat = k
⊢ ∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)

Proof state:
case intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk : ↑k.toNat = k
⊢ ∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)

Tactic:
rw [← hk] at hk₀ hk₁ h

Result:
case intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < ↑k.toNat
hk₁ : ↑k.toNat ≤ ↑n
h : |↑↑k.toNat * ξ - ↑j| ≤ 1 / (↑n + 1)
hk : ↑k.toNat = k
⊢ ∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)
-- Mathlib/NumberTheory/LSeries/ZMod.lean
/-- The L-function of a function on `ZMod 1` is a scalar multiple of the Riemann zeta function. -/
lemma LFunction_modOne_eq (Φ : ZMod 1 → ℂ) (s : ℂ) :
    LFunction Φ s = Φ 0 * riemannZeta s

Proof state:
Φ : ZMod 1 → ℂ
s : ℂ
⊢ LFunction Φ s = Φ 0 * riemannZeta s

Tactic:
simp only [LFunction, Nat.cast_one, one_cpow, ← singleton_eq_univ (0 : ZMod 1), sum_singleton,
  map_zero, hurwitzZeta_zero, one_mul]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_nonneg_iff_neg_imp_nonpos : 0 ≤ a • b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ 0 ≤ a • b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

Tactic:
rw [← neg_smul_neg, smul_nonneg_iff_pos_imp_nonneg]

Result:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < -a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ -a) ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < -a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ -a) ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

Tactic:
simp only [neg_pos, neg_nonneg]

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem sZMod_eq_s (p' : ℕ) (i : ℕ) : sZMod (p' + 2) i = (s i : ZMod (2 ^ (p' + 2) - 1))

Proof state:
p' i : ℕ
⊢ sZMod (p' + 2) i = ↑(s i)

Tactic:
induction i with
| zero => dsimp [s, sZMod]; norm_num
| succ i ih => push_cast [s, sZMod, ih]; rfl

Result:
no goals

Proof state:
case zero
p' : ℕ
⊢ 4 = ↑4

Tactic:
norm_num

Result:
no goals

Proof state:
case succ
p' i : ℕ
ih : sZMod (p' + 2) i = ↑(s i)
⊢ sZMod (p' + 2) (i + 1) = ↑(s (i + 1))

Tactic:
push_cast [s, sZMod, ih]

Result:
case succ
p' i : ℕ
ih : sZMod (p' + 2) i = ↑(s i)
⊢ ↑(s i) ^ 2 - 2 = ↑(s i) ^ 2 - 2

Proof state:
case zero
p' : ℕ
⊢ sZMod (p' + 2) 0 = ↑(s 0)

Tactic:
dsimp [s, sZMod]

Result:
case zero
p' : ℕ
⊢ 4 = ↑4

Proof state:
case succ
p' i : ℕ
ih : sZMod (p' + 2) i = ↑(s i)
⊢ ↑(s i) ^ 2 - 2 = ↑(s i) ^ 2 - 2

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem restrict_eq_zero_iff (μ : FiniteMeasure Ω) (A : Set Ω) : μ.restrict A = 0 ↔ μ A = 0

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
A : Set Ω
⊢ μ.restrict A = 0 ↔ μ A = 0

Tactic:
rw [← mass_zero_iff, restrict_mass]

Result:
no goals
-- Mathlib/Data/Multiset/Count.lean
theorem count_singleton (a b : α) : count a ({b} : Multiset α) = if a = b then 1 else 0

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
⊢ count a {b} = if a = b then 1 else 0

Tactic:
simp only [count_cons, ← cons_zero, count_zero, Nat.zero_add]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma infSum_union_add_infSum_sups (𝒜 ℬ : Finset (Finset α)) :
    infSum (𝒜 ∪ ℬ) + infSum (𝒜 ⊻ ℬ) = infSum 𝒜 + infSum ℬ

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ,
    ↑(#((𝒜 ∪ ℬ).truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) +
        ↑(#((𝒜 ⊻ ℬ).truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) =
      ↑(#(𝒜.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) +
        ↑(#(ℬ.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s))

Tactic:
simp_rw [div_add_div_same, ← Nat.cast_add, card_truncatedInf_union_add_card_truncatedInf_sups]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ, True

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∑ s : Finset α, ↑(#((𝒜 ∪ ℬ).truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) +
      ∑ s : Finset α, ↑(#((𝒜 ⊻ ℬ).truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) =
    ∑ s : Finset α, ↑(#(𝒜.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) +
      ∑ s : Finset α, ↑(#(ℬ.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s))

Tactic:
rw [← sum_add_distrib, ← sum_add_distrib, sum_congr rfl fun s _ ↦ _]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ,
    ↑(#((𝒜 ∪ ℬ).truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) +
        ↑(#((𝒜 ⊻ ℬ).truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) =
      ↑(#(𝒜.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) +
        ↑(#(ℬ.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s))

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ infSum (𝒜 ∪ ℬ) + infSum (𝒜 ⊻ ℬ) = infSum 𝒜 + infSum ℬ

Tactic:
unfold infSum

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∑ s : Finset α, ↑(#((𝒜 ∪ ℬ).truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) +
      ∑ s : Finset α, ↑(#((𝒜 ⊻ ℬ).truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) =
    ∑ s : Finset α, ↑(#(𝒜.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) +
      ∑ s : Finset α, ↑(#(ℬ.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s))

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ s ∈ univ, True

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem identical_iff' : ∀ {x y : PGame}, x ≡ y ↔
    ((∀ i, x.moveLeft i ∈ₗ y) ∧ (∀ j, y.moveLeft j ∈ₗ x)) ∧
      ((∀ i, x.moveRight i ∈ᵣ y) ∧ (∀ j, y.moveRight j ∈ᵣ x))
  | mk xl xr xL xR, mk yl yr yL yR => by
    convert identical_iff <;>
    dsimp [Relator.BiTotal, Relator.LeftTotal, Relator.RightTotal] <;>
    congr! <;>
    exact exists_congr <| fun _ ↦ identical_comm

Proof state:
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
⊢ mk xl xr xL xR ≡ mk yl yr yL yR ↔
    ((∀ (i : (mk xl xr xL xR).LeftMoves), (mk xl xr xL xR).moveLeft i ∈ₗ mk yl yr yL yR) ∧
        ∀ (j : (mk yl yr yL yR).LeftMoves), (mk yl yr yL yR).moveLeft j ∈ₗ mk xl xr xL xR) ∧
      (∀ (i : (mk xl xr xL xR).RightMoves), (mk xl xr xL xR).moveRight i ∈ᵣ mk yl yr yL yR) ∧
        ∀ (j : (mk yl yr yL yR).RightMoves), (mk yl yr yL yR).moveRight j ∈ᵣ mk xl xr xL xR

Tactic:
convert identical_iff <;>
dsimp [Relator.BiTotal, Relator.LeftTotal, Relator.RightTotal] <;>
congr! <;>
exact exists_congr <| fun _ ↦ identical_comm

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
theorem pow_pred_clog_lt_self {b : ℕ} (hb : 1 < b) {x : ℕ} (hx : 1 < x) :
    b ^ (clog b x).pred < x

Proof state:
b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ (clog b x).pred < clog b x

Tactic:
exact pred_lt (clog_pos hb hx).ne'

Result:
no goals

Proof state:
b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ b ^ (clog b x).pred < x

Tactic:
rw [← not_le, le_pow_iff_clog_le hb, not_le]

Result:
b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ (clog b x).pred < clog b x
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem fac_lift {F : MonoFactorisation f} (hF : IsImage F) (F' : MonoFactorisation f) :
    F.e ≫ hF.lift F' = F'.e :=
  (cancel_mono F'.m).1 <| by simp

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : MonoFactorisation f
hF : IsImage F
F' : MonoFactorisation f
⊢ (F.e ≫ hF.lift F') ≫ F'.m = F'.e ≫ F'.m

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Erase.lean
theorem getElem_eraseIdx_of_lt (l : Vector α n) (i : Nat) (w : i < n) (j : Nat) (h : j < n - 1) (h' : j < i) :
    (l.eraseIdx i)[j] = l[j]

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
w : i < n
j : Nat
h : j < n - 1
h' : j < i
⊢ (l.eraseIdx i w)[j] = l[j]

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
i j : Nat
h' : j < i
l : Array α
w : i < l.size
h : j < l.size - 1
⊢ ({ toArray := l, size_toArray := ⋯ }.eraseIdx i w)[j] = { toArray := l, size_toArray := ⋯ }[j]

Proof state:
case mk
α : Type u_1
i j : Nat
h' : j < i
l : Array α
w : i < l.size
h : j < l.size - 1
⊢ ({ toArray := l, size_toArray := ⋯ }.eraseIdx i w)[j] = { toArray := l, size_toArray := ⋯ }[j]

Tactic:
simp [Array.getElem_eraseIdx_of_lt, *]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/DecidableEq.lean
theorem isEqv_eq_decide (a b : Vector α n) (r) :
    Vector.isEqv a b r = decide (∀ (i : Nat) (h' : i < n), r a[i] b[i])

Proof state:
case mk.mk
α : Type u_1
r : α → α → Bool
a b : Array α
h : b.size = a.size
⊢ { toArray := a, size_toArray := ⋯ }.isEqv { toArray := b, size_toArray := h } r =
    decide
      (∀ (i : Nat) (h' : i < a.size),
        r { toArray := a, size_toArray := ⋯ }[i] { toArray := b, size_toArray := h }[i] = true)

Tactic:
simp [Array.isEqv_eq_decide, h]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a b : Vector α n
r : α → α → Bool
⊢ a.isEqv b r = decide (∀ (i : Nat) (h' : i < n), r a[i] b[i] = true)

Tactic:
rcases a with ⟨a, rfl⟩

Result:
case mk
α : Type u_1
r : α → α → Bool
a : Array α
b : Vector α a.size
⊢ { toArray := a, size_toArray := ⋯ }.isEqv b r =
    decide (∀ (i : Nat) (h' : i < a.size), r { toArray := a, size_toArray := ⋯ }[i] b[i] = true)

Proof state:
case mk
α : Type u_1
r : α → α → Bool
a : Array α
b : Vector α a.size
⊢ { toArray := a, size_toArray := ⋯ }.isEqv b r =
    decide (∀ (i : Nat) (h' : i < a.size), r { toArray := a, size_toArray := ⋯ }[i] b[i] = true)

Tactic:
rcases b with ⟨b, h⟩

Result:
case mk.mk
α : Type u_1
r : α → α → Bool
a b : Array α
h : b.size = a.size
⊢ { toArray := a, size_toArray := ⋯ }.isEqv { toArray := b, size_toArray := h } r =
    decide
      (∀ (i : Nat) (h' : i < a.size),
        r { toArray := a, size_toArray := ⋯ }[i] { toArray := b, size_toArray := h }[i] = true)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_set_ne (v : Vector α n) (i : Nat) (x : α) (hi : i < n) (j : Nat)
    (hj : j < n) (h : i ≠ j) : (v.set i x hi)[j] = v[j]

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
x : α
hi : i < n
j : Nat
hj : j < n
h : i ≠ j
⊢ (v.set i x hi)[j] = v[j]

Tactic:
simp [getElem_set, h]

Result:
no goals