harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sshiftRight_eq_of_msb_false {x : BitVec w} {s : Nat} (h : x.msb = false) :
    (x.sshiftRight s) = x >>> s

Proof state:
case a
w : Nat
x : BitVec w
s : Nat
h : x.msb = false
⊢ (BitVec.ofInt w ((if 2 * x.toNat < 2 ^ w then ↑x.toNat else ↑x.toNat - ↑(2 ^ w)) >>> s)).toNat = (x >>> s).toNat

Tactic:
have hxbound : 2 * x.toNat < 2 ^ w := BitVec.msb_eq_false_iff_two_mul_lt.mp h

Result:
case a
w : Nat
x : BitVec w
s : Nat
h : x.msb = false
hxbound : 2 * x.toNat < 2 ^ w
⊢ (BitVec.ofInt w ((if 2 * x.toNat < 2 ^ w then ↑x.toNat else ↑x.toNat - ↑(2 ^ w)) >>> s)).toNat = (x >>> s).toNat

Proof state:
case a
w : Nat
x : BitVec w
s : Nat
h : x.msb = false
⊢ (x.sshiftRight s).toNat = (x >>> s).toNat

Tactic:
rw [BitVec.sshiftRight_eq, BitVec.toInt_eq_toNat_cond]

Result:
case a
w : Nat
x : BitVec w
s : Nat
h : x.msb = false
⊢ (BitVec.ofInt w ((if 2 * x.toNat < 2 ^ w then ↑x.toNat else ↑x.toNat - ↑(2 ^ w)) >>> s)).toNat = (x >>> s).toNat

Proof state:
w : Nat
x : BitVec w
s : Nat
h : x.msb = false
⊢ x.sshiftRight s = x >>> s

Tactic:
apply BitVec.eq_of_toNat_eq

Result:
case a
w : Nat
x : BitVec w
s : Nat
h : x.msb = false
⊢ (x.sshiftRight s).toNat = (x >>> s).toNat

Proof state:
case a
w : Nat
x : BitVec w
s : Nat
h : x.msb = false
hxbound : 2 * x.toNat < 2 ^ w
⊢ x.toNat >>> s % 2 ^ w = x.toNat >>> s

Tactic:
replace hxbound : x.toNat >>> s < 2 ^ w := by
  rw [Nat.shiftRight_eq_div_pow]
  exact Nat.lt_of_le_of_lt (Nat.div_le_self ..) x.isLt

Result:
case a
w : Nat
x : BitVec w
s : Nat
h : x.msb = false
hxbound : x.toNat >>> s < 2 ^ w
⊢ x.toNat >>> s % 2 ^ w = x.toNat >>> s

Proof state:
case a
w : Nat
x : BitVec w
s : Nat
h : x.msb = false
hxbound : 2 * x.toNat < 2 ^ w
⊢ (BitVec.ofInt w ((if 2 * x.toNat < 2 ^ w then ↑x.toNat else ↑x.toNat - ↑(2 ^ w)) >>> s)).toNat = (x >>> s).toNat

Tactic:
simp only [hxbound, ↓reduceIte, Int.natCast_shiftRight, Int.ofNat_eq_coe, ofInt_natCast,
  toNat_ofNat, toNat_ushiftRight]

Result:
case a
w : Nat
x : BitVec w
s : Nat
h : x.msb = false
hxbound : 2 * x.toNat < 2 ^ w
⊢ x.toNat >>> s % 2 ^ w = x.toNat >>> s

Proof state:
case a
w : Nat
x : BitVec w
s : Nat
h : x.msb = false
hxbound : x.toNat >>> s < 2 ^ w
⊢ x.toNat >>> s % 2 ^ w = x.toNat >>> s

Tactic:
apply Nat.mod_eq_of_lt hxbound

Result:
no goals

Proof state:
w : Nat
x : BitVec w
s : Nat
h : x.msb = false
hxbound : 2 * x.toNat < 2 ^ w
⊢ x.toNat / 2 ^ s < 2 ^ w

Tactic:
exact Nat.lt_of_le_of_lt (Nat.div_le_self ..) x.isLt

Result:
no goals

Proof state:
w : Nat
x : BitVec w
s : Nat
h : x.msb = false
hxbound : 2 * x.toNat < 2 ^ w
⊢ x.toNat >>> s < 2 ^ w

Tactic:
rw [Nat.shiftRight_eq_div_pow]

Result:
w : Nat
x : BitVec w
s : Nat
h : x.msb = false
hxbound : 2 * x.toNat < 2 ^ w
⊢ x.toNat / 2 ^ s < 2 ^ w
-- Mathlib/Topology/Category/Profinite/EffectiveEpi.lean
theorem effectiveEpi_tfae
    {B X : Profinite.{u}} (π : X ⟶ B) :
    TFAE
    [ EffectiveEpi π
    , Epi π
    , Function.Surjective π
    ]

Proof state:
B X : Profinite
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
tfae_2_iff_3 : Epi π ↔ Function.Surjective ⇑(ConcreteCategory.hom π)
tfae_3_to_1 : Function.Surjective ⇑(ConcreteCategory.hom π) → EffectiveEpi π
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
B X : Profinite
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
tfae_2_iff_3 : Epi π ↔ Function.Surjective ⇑(ConcreteCategory.hom π)
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Tactic:
tfae_have 3 → 1 := fun hπ ↦ ⟨⟨CompHausLike.effectiveEpiStruct π hπ⟩⟩

Result:
B X : Profinite
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
tfae_2_iff_3 : Epi π ↔ Function.Surjective ⇑(ConcreteCategory.hom π)
tfae_3_to_1 : Function.Surjective ⇑(ConcreteCategory.hom π) → EffectiveEpi π
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Proof state:
B X : Profinite
π : X ⟶ B
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Tactic:
tfae_have 1 → 2 := fun _ ↦ inferInstance

Result:
B X : Profinite
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Proof state:
B X : Profinite
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Tactic:
tfae_have 2 ↔ 3 := epi_iff_surjective π

Result:
B X : Profinite
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
tfae_2_iff_3 : Epi π ↔ Function.Surjective ⇑(ConcreteCategory.hom π)
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE
-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem BlockTriangular.sub [SubNegZeroMonoid R]
    (hM : BlockTriangular M b) (hN : BlockTriangular N b) :
    BlockTriangular (M - N) b := fun i j h => by simp_rw [Matrix.sub_apply, hM h, hN h, sub_zero]

Proof state:
α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : SubNegZeroMonoid R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
h : b j < b i
⊢ (M - N) i j = 0

Tactic:
simp_rw [Matrix.sub_apply, hM h, hN h, sub_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Periodic.lean
theorem lintegral_preimage (t : ℝ) (f : AddCircle T → ℝ≥0∞) :
    (∫⁻ a in Ioc t (t + T), f a) = ∫⁻ b : AddCircle T, f b

Proof state:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this : ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x => ↑↑x) volume = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a
⊢ (fun x => ↑↑x) = QuotientAddGroup.mk ∘ Subtype.val

Tactic:
ext1 x

Result:
case h
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this : ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x => ↑↑x) volume = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a
x : ↑(Ioc t (t + T))
⊢ ↑↑x = (QuotientAddGroup.mk ∘ Subtype.val) x

Proof state:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this : ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x => ↑↑x) volume = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a
⊢ ∫⁻ (a : ℝ) in Ioc t (t + T), f ↑a = ∫⁻ (b : AddCircle T), f b

Tactic:
rw [← (AddCircle.measurePreserving_mk T t).map_eq]

Result:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this : ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x => ↑↑x) volume = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a
⊢ ∫⁻ (a : ℝ) in Ioc t (t + T), f ↑a =
    ∫⁻ (b : AddCircle T), f b ∂Measure.map QuotientAddGroup.mk (volume.restrict (Ioc t (t + T)))

Proof state:
case h.e'_2
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this : ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x => ↑↑x) volume = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a
⊢ ∫⁻ (a : ℝ), f ↑a ∂Measure.map Subtype.val (Measure.comap Subtype.val volume) = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a

Tactic:
exact MeasurableEmbedding.lintegral_map (MeasurableEmbedding.subtype_coe m) _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem _root_.List.filterMap_toArray' (f : α → Option β) (l : List α) (h : stop = l.length) :
    l.toArray.filterMap f 0 stop = (l.filterMap f).toArray

Proof state:
case h
α : Type u_1
β : Type u_2
stop : Nat
f : α → Option β
l : List α
h : stop = l.length
⊢ (filterMap f l.toArray 0 stop).toList = (List.filterMap f l).toArray.toList

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
stop : Nat
f : α → Option β
l : List α
h : stop = l.length
⊢ filterMap f l.toArray 0 stop = (List.filterMap f l).toArray

Tactic:
apply ext'

Result:
case h
α : Type u_1
β : Type u_2
stop : Nat
f : α → Option β
l : List α
h : stop = l.length
⊢ (filterMap f l.toArray 0 stop).toList = (List.filterMap f l).toArray.toList
-- Mathlib/Data/Set/Lattice.lean
theorem biUnion_insert (a : α) (s : Set α) (t : α → Set β) :
    ⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x

Proof state:
α : Type u_1
β : Type u_2
a : α
s : Set α
t : α → Set β
⊢ ⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem add_factorial_le_factorial_add (i : ℕ) {n : ℕ} (n1 : 1 ≤ n) : i + n ! ≤ (i + n)!

Proof state:
case step
i h : ℕ
a✝ : Nat.le 1 h
⊢ i + h.succ ! ≤ (i + h.succ)!

Tactic:
exact add_factorial_succ_le_factorial_add_succ i h

Result:
no goals

Proof state:
case refl
i : ℕ
⊢ i + 1! ≤ (i + 1)!

Tactic:
exact self_le_factorial _

Result:
no goals

Proof state:
i n : ℕ
n1 : 1 ≤ n
⊢ i + n ! ≤ (i + n)!

Tactic:
rcases n1 with - | @h

Result:
case refl
i : ℕ
⊢ i + 1! ≤ (i + 1)!

case step
i h : ℕ
a✝ : Nat.le 1 h
⊢ i + h.succ ! ≤ (i + h.succ)!
-- Mathlib/GroupTheory/Coset/Basic.lean
theorem mem_own_leftCoset (a : α) : a ∈ a • (s : Set α) :=
  suffices a * 1 ∈ a • (s : Set α) by simpa
  mem_leftCoset a (one_mem s : 1 ∈ s)

Proof state:
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
this : a * 1 ∈ a • ↑s
⊢ a ∈ a • ↑s

Tactic:
simpa

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Theta.lean
theorem IsTheta.tendsto_zero_iff (h : f'' =Θ[l] g'') :
    Tendsto f'' l (𝓝 0) ↔ Tendsto g'' l (𝓝 0)

Proof state:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
g'' : α → F''
l : Filter α
h : f'' =Θ[l] g''
⊢ Tendsto f'' l (𝓝 0) ↔ Tendsto g'' l (𝓝 0)

Tactic:
simp only [← isLittleO_one_iff ℝ, h.isLittleO_congr_left]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem existsUnique (h : π.IsPartition) (hx : x ∈ I) :
    ∃! J ∈ π, x ∈ J

Proof state:
case intro.intro
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
h✝ : π.IsPartition
hx✝ : x ∈ I
J : Box ι
h : J ∈ π
hx : x ∈ J
⊢ ∃! J, J ∈ π ∧ x ∈ J

Tactic:
exact ExistsUnique.intro J ⟨h, hx⟩ fun J' ⟨h', hx'⟩ => π.eq_of_mem_of_mem h' h hx' hx

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
h : π.IsPartition
hx : x ∈ I
⊢ ∃! J, J ∈ π ∧ x ∈ J

Tactic:
rcases h x hx with ⟨J, h, hx⟩

Result:
case intro.intro
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
h✝ : π.IsPartition
hx✝ : x ∈ I
J : Box ι
h : J ∈ π
hx : x ∈ J
⊢ ∃! J, J ∈ π ∧ x ∈ J
-- Mathlib/CategoryTheory/Preadditive/Yoneda/Injective.lean
theorem injective_iff_preservesEpimorphisms_preadditiveYoneda_obj (J : C) :
    Injective J ↔ (preadditiveYoneda.obj J).PreservesEpimorphisms

Proof state:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
a✝ : (preadditiveYoneda.obj J).PreservesEpimorphisms
⊢ (yoneda.obj J).PreservesEpimorphisms

Tactic:
exact (inferInstance : (preadditiveYoneda.obj J ⋙ forget _).PreservesEpimorphisms)

Result:
no goals

Proof state:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
h : (preadditiveYoneda.obj J ⋙ forget AddCommGrp).PreservesEpimorphisms
⊢ (preadditiveYoneda.obj J).PreservesEpimorphisms

Tactic:
exact
  Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveYoneda.obj J) (forget _)

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ (yoneda.obj J).PreservesEpimorphisms ↔ (preadditiveYoneda.obj J).PreservesEpimorphisms

Tactic:
refine
  ⟨fun h : (preadditiveYoneda.obj J ⋙ (forget AddCommGrp)).PreservesEpimorphisms => ?_, ?_⟩

Result:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
h : (preadditiveYoneda.obj J ⋙ forget AddCommGrp).PreservesEpimorphisms
⊢ (preadditiveYoneda.obj J).PreservesEpimorphisms

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ (preadditiveYoneda.obj J).PreservesEpimorphisms → (yoneda.obj J).PreservesEpimorphisms

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ Injective J ↔ (preadditiveYoneda.obj J).PreservesEpimorphisms

Tactic:
rw [injective_iff_preservesEpimorphisms_yoneda_obj]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ (yoneda.obj J).PreservesEpimorphisms ↔ (preadditiveYoneda.obj J).PreservesEpimorphisms

Proof state:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ (preadditiveYoneda.obj J).PreservesEpimorphisms → (yoneda.obj J).PreservesEpimorphisms

Tactic:
intro

Result:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
a✝ : (preadditiveYoneda.obj J).PreservesEpimorphisms
⊢ (yoneda.obj J).PreservesEpimorphisms
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem map_extend_symm_nhdsWithin {y : M} (hy : y ∈ f.source) :
    map (f.extend I).symm (𝓝[(f.extend I).symm ⁻¹' s ∩ range I] f.extend I y) = 𝓝[s] y

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
⊢ ↑(f.extend I).symm ∘ ↑(f.extend I) =ᶠ[𝓝[s] y] id

Tactic:
exact (f.extend I).leftInvOn.eqOn.eventuallyEq_of_mem (extend_source_mem_nhdsWithin _ hy)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
⊢ map (↑(f.extend I).symm) (𝓝[↑(f.extend I).symm ⁻¹' s ∩ range ↑I] ↑(f.extend I) y) = 𝓝[s] y

Tactic:
rw [← map_extend_nhdsWithin f hy, map_map, Filter.map_congr, map_id]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
⊢ ↑(f.extend I).symm ∘ ↑(f.extend I) =ᶠ[𝓝[s] y] id
-- Mathlib/CategoryTheory/Category/Basic.lean
theorem id_of_comp_left_id (f : X ⟶ X) (w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g) : f = 𝟙 X

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

Tactic:
convert w (𝟙 X)

Result:
case h.e'_2
C : Type u
inst✝ : Category.{v, u} C
X : C
f : X ⟶ X
w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g
⊢ f = f ≫ 𝟙 X

Proof state:
case h.e'_2
C : Type u
inst✝ : Category.{v, u} C
X : C
f : X ⟶ X
w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g
⊢ f = f ≫ 𝟙 X

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Basic.lean
lemma add_mem {x y} (hx : x ∈ I) (hy : y ∈ I) : x + y ∈ I

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
hx : x ∈ I
hy : y ∈ I
⊢ x + y ∈ I

Tactic:
simpa using I.ringCon.add hx hy

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem infinite_of_injective_forall_mem [Infinite α] {s : Set β} {f : α → β} (hi : Injective f)
    (hf : ∀ x : α, f x ∈ s) : s.Infinite

Proof state:
α : Type u
β : Type v
inst✝ : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : range f ⊆ s
⊢ s.Infinite

Tactic:
exact (infinite_range_of_injective hi).mono hf

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : ∀ (x : α), f x ∈ s
⊢ s.Infinite

Tactic:
rw [← range_subset_iff] at hf

Result:
α : Type u
β : Type v
inst✝ : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : range f ⊆ s
⊢ s.Infinite
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem lt_rank_root {self : UnionFind} {x : Nat} :
    self.rank x < self.rank (self.rootD x) ↔ self.parent x ≠ x

Proof state:
self : UnionFind
x : Nat
h : self.parent x ≠ x
⊢ self.rank x < self.rank (self.rootD (self.parent x))

Tactic:
exact Nat.lt_of_lt_of_le (self.rank_lt h) le_rank_root

Result:
no goals

Proof state:
self : UnionFind
x : Nat
h : self.parent x ≠ x
⊢ self.rank x < self.rank (self.rootD x)

Tactic:
rw [← rootD_parent]

Result:
self : UnionFind
x : Nat
h : self.parent x ≠ x
⊢ self.rank x < self.rank (self.rootD (self.parent x))

Proof state:
self : UnionFind
x : Nat
⊢ self.rank x < self.rank (self.rootD x) ↔ self.parent x ≠ x

Tactic:
refine ⟨fun h h' => Nat.ne_of_lt h (by rw [rootD_eq_self.2 h']), fun h => ?_⟩

Result:
self : UnionFind
x : Nat
h : self.parent x ≠ x
⊢ self.rank x < self.rank (self.rootD x)

Proof state:
self : UnionFind
x : Nat
h : self.rank x < self.rank (self.rootD x)
h' : self.parent x = x
⊢ self.rank x = self.rank (self.rootD x)

Tactic:
rw [rootD_eq_self.2 h']

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurableSet_pi_of_nonempty {s : Set δ} {t : ∀ i, Set (π i)} (hs : s.Countable)
    (h : (pi s t).Nonempty) : MeasurableSet (pi s t) ↔ ∀ i ∈ s, MeasurableSet (t i)

Proof state:
case intro
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
s : Set δ
t : (i : δ) → Set (π i)
hs : s.Countable
f : (i : δ) → π i
hf : f ∈ s.pi t
hst : MeasurableSet (s.pi t)
i : δ
hi : i ∈ s
⊢ MeasurableSet (t i)

Tactic:
convert measurable_update f (a := i) hst

Result:
case h.e'_3
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
s : Set δ
t : (i : δ) → Set (π i)
hs : s.Countable
f : (i : δ) → π i
hf : f ∈ s.pi t
hst : MeasurableSet (s.pi t)
i : δ
hi : i ∈ s
⊢ t i = update f i ⁻¹' s.pi t

Proof state:
case h.e'_3
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
s : Set δ
t : (i : δ) → Set (π i)
hs : s.Countable
f : (i : δ) → π i
hf : f ∈ s.pi t
hst : MeasurableSet (s.pi t)
i : δ
hi : i ∈ s
⊢ ∀ j ∈ s, j ≠ i → f j ∈ t j

Tactic:
exact fun j hj _ => hf j hj

Result:
no goals

Proof state:
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
s : Set δ
t : (i : δ) → Set (π i)
hs : s.Countable
h : (s.pi t).Nonempty
⊢ MeasurableSet (s.pi t) ↔ ∀ i ∈ s, MeasurableSet (t i)

Tactic:
rcases h with ⟨f, hf⟩

Result:
case intro
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
s : Set δ
t : (i : δ) → Set (π i)
hs : s.Countable
f : (i : δ) → π i
hf : f ∈ s.pi t
⊢ MeasurableSet (s.pi t) ↔ ∀ i ∈ s, MeasurableSet (t i)

Proof state:
case h.e'_3
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
s : Set δ
t : (i : δ) → Set (π i)
hs : s.Countable
f : (i : δ) → π i
hf : f ∈ s.pi t
hst : MeasurableSet (s.pi t)
i : δ
hi : i ∈ s
⊢ t i = update f i ⁻¹' s.pi t

Tactic:
rw [update_preimage_pi hi]

Result:
case h.e'_3
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
s : Set δ
t : (i : δ) → Set (π i)
hs : s.Countable
f : (i : δ) → π i
hf : f ∈ s.pi t
hst : MeasurableSet (s.pi t)
i : δ
hi : i ∈ s
⊢ ∀ j ∈ s, j ≠ i → f j ∈ t j

Proof state:
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
s : Set δ
t : (i : δ) → Set (π i)
hs : s.Countable
h : (s.pi t).Nonempty
⊢ MeasurableSet (s.pi t) ↔ ∀ i ∈ s, MeasurableSet (t i)

Tactic:
classical
  rcases h with ⟨f, hf⟩
  refine ⟨fun hst i hi => ?_, MeasurableSet.pi hs⟩
  convert measurable_update f (a := i) hst
  rw [update_preimage_pi hi]
  exact fun j hj _ => hf j hj

Result:
no goals

Proof state:
case intro
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
s : Set δ
t : (i : δ) → Set (π i)
hs : s.Countable
f : (i : δ) → π i
hf : f ∈ s.pi t
⊢ MeasurableSet (s.pi t) ↔ ∀ i ∈ s, MeasurableSet (t i)

Tactic:
refine ⟨fun hst i hi => ?_, MeasurableSet.pi hs⟩

Result:
case intro
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
s : Set δ
t : (i : δ) → Set (π i)
hs : s.Countable
f : (i : δ) → π i
hf : f ∈ s.pi t
hst : MeasurableSet (s.pi t)
i : δ
hi : i ∈ s
⊢ MeasurableSet (t i)
-- Mathlib/Order/RelSeries.lean
theorem length_ne_zero (irrefl : Irreflexive r) : s.length ≠ 0 ↔ {x | x ∈ s}.Nontrivial

Proof state:
α : Type u_1
r : Rel α α
s : RelSeries r
irrefl : Irreflexive r
⊢ s.length ≠ 0 ↔ {x | x ∈ s}.Nontrivial

Tactic:
refine ⟨fun h ↦ ⟨s 0, by simp [mem_def], s 1, by simp [mem_def], fun rid ↦ irrefl (s 0) ?_⟩,
  length_ne_zero_of_nontrivial⟩

Result:
α : Type u_1
r : Rel α α
s : RelSeries r
irrefl : Irreflexive r
h : s.length ≠ 0
rid : s.toFun 0 = s.toFun 1
⊢ r (s.toFun 0) (s.toFun 0)

Proof state:
α : Type u_1
r : Rel α α
s : RelSeries r
irrefl : Irreflexive r
h : s.length ≠ 0
rid : s.toFun 0 = s.toFun 1
⊢ r (s.toFun 0) (s.toFun 0)

Tactic:
nth_rw 2 [rid]

Result:
α : Type u_1
r : Rel α α
s : RelSeries r
irrefl : Irreflexive r
h : s.length ≠ 0
rid : s.toFun 0 = s.toFun 1
⊢ r (s.toFun 0) (s.toFun 1)

Proof state:
α : Type u_1
r : Rel α α
s : RelSeries r
irrefl : Irreflexive r
h : s.length ≠ 0
⊢ s.toFun 1 ∈ {x | x ∈ s}

Tactic:
simp [mem_def]

Result:
no goals

Proof state:
case h.e'_2.h.e'_4.h
α : Type u_1
r : Rel α α
s : RelSeries r
irrefl : Irreflexive r
h : s.length ≠ 0
rid : s.toFun 0 = s.toFun 1
⊢ ↑1 = ↑⟨0, ⋯⟩.succ

Tactic:
simpa [Nat.pos_iff_ne_zero]

Result:
no goals

Proof state:
α : Type u_1
r : Rel α α
s : RelSeries r
irrefl : Irreflexive r
h : s.length ≠ 0
rid : s.toFun 0 = s.toFun 1
⊢ 0 < s.length

Tactic:
omega

Result:
no goals

Proof state:
case h.e'_2.h.e'_4
α : Type u_1
r : Rel α α
s : RelSeries r
irrefl : Irreflexive r
h : s.length ≠ 0
rid : s.toFun 0 = s.toFun 1
⊢ 1 = ⟨0, ⋯⟩.succ

Tactic:
ext

Result:
case h.e'_2.h.e'_4.h
α : Type u_1
r : Rel α α
s : RelSeries r
irrefl : Irreflexive r
h : s.length ≠ 0
rid : s.toFun 0 = s.toFun 1
⊢ ↑1 = ↑⟨0, ⋯⟩.succ

Proof state:
α : Type u_1
r : Rel α α
s : RelSeries r
irrefl : Irreflexive r
h : s.length ≠ 0
rid : s.toFun 0 = s.toFun 1
⊢ r (s.toFun 0) (s.toFun 1)

Tactic:
convert s.step ⟨0, by omega⟩

Result:
case h.e'_2.h.e'_4
α : Type u_1
r : Rel α α
s : RelSeries r
irrefl : Irreflexive r
h : s.length ≠ 0
rid : s.toFun 0 = s.toFun 1
⊢ 1 = ⟨0, ⋯⟩.succ

Proof state:
α : Type u_1
r : Rel α α
s : RelSeries r
irrefl : Irreflexive r
h : s.length ≠ 0
⊢ s.toFun 0 ∈ {x | x ∈ s}

Tactic:
simp [mem_def]

Result:
no goals
-- Mathlib/Data/ZMod/QuotientGroup.lean
theorem Nat.card_zpowers : Nat.card (zpowers a) = orderOf a

Proof state:
α : Type u_3
inst✝ : Group α
a : α
⊢ Nat.card ↥(zpowers a) = orderOf a

Tactic:
have := Nat.card_congr (MulAction.orbitZPowersEquiv a (1 : α))

Result:
α : Type u_3
inst✝ : Group α
a : α
this : Nat.card ↑(MulAction.orbit (↥(zpowers a)) 1) = Nat.card (ZMod (Function.minimalPeriod (fun x => a • x) 1))
⊢ Nat.card ↥(zpowers a) = orderOf a

Proof state:
α : Type u_3
inst✝ : Group α
a : α
this : Nat.card ↑(MulAction.orbit (↥(zpowers a)) 1) = Nat.card (ZMod (Function.minimalPeriod (fun x => a • x) 1))
⊢ Nat.card ↥(zpowers a) = orderOf a

Tactic:
rwa [Nat.card_zmod, orbit_subgroup_one_eq_self] at this

Result:
no goals
-- Mathlib/Data/Matrix/Diagonal.lean
theorem diagonal_sub [SubNegZeroMonoid α] (d₁ d₂ : n → α) :
    diagonal d₁ - diagonal d₂ = diagonal fun i => d₁ i - d₂ i

Proof state:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : SubNegZeroMonoid α
d₁ d₂ : n → α
⊢ diagonal d₁ - diagonal d₂ = diagonal fun i => d₁ i - d₂ i

Tactic:
ext i j

Result:
case a
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : SubNegZeroMonoid α
d₁ d₂ : n → α
i j : n
⊢ (diagonal d₁ - diagonal d₂) i j = diagonal (fun i => d₁ i - d₂ i) i j

Proof state:
case a
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : SubNegZeroMonoid α
d₁ d₂ : n → α
i j : n
⊢ (diagonal d₁ - diagonal d₂) i j = diagonal (fun i => d₁ i - d₂ i) i j

Tactic:
by_cases h : i = j <;>
simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem shiftLeft_eq_shiftLeftRec (x : BitVec w₁) (y : BitVec w₂) :
    x <<< y = shiftLeftRec x y (w₂ - 1)

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
⊢ x <<< y = x.shiftLeftRec y (w₂ - 1)

Tactic:
rcases w₂ with rfl | w₂

Result:
case zero
w₁ : Nat
x : BitVec w₁
y : BitVec 0
⊢ x <<< y = x.shiftLeftRec y (0 - 1)

case succ
w₁ : Nat
x : BitVec w₁
w₂ : Nat
y : BitVec (w₂ + 1)
⊢ x <<< y = x.shiftLeftRec y (w₂ + 1 - 1)

Proof state:
case succ
w₁ : Nat
x : BitVec w₁
w₂ : Nat
y : BitVec (w₂ + 1)
⊢ x <<< y = x.shiftLeftRec y (w₂ + 1 - 1)

Tactic:
simp [shiftLeftRec_eq]

Result:
no goals

Proof state:
case zero
w₁ : Nat
x : BitVec w₁
y : BitVec 0
⊢ x <<< y = x.shiftLeftRec y (0 - 1)

Tactic:
simp [of_length_zero]

Result:
no goals