harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem subgroupOf_range_eq_of_le {G₁ G₂ : Type*} [Group G₁] [Group G₂] {K : Subgroup G₂}
    (f : G₁ →* G₂) (h : f.range ≤ K) :
    f.range.subgroupOf K = (f.codRestrict K fun x => h ⟨x, rfl⟩).range

Proof state:
case h
G₁ : Type u_7
G₂ : Type u_8
inst✝¹ : Group G₁
inst✝ : Group G₂
K : Subgroup G₂
f : G₁ →* G₂
h : f.range ≤ K
k : ↥K
⊢ k ∈ f.range.subgroupOf K ↔ k ∈ (f.codRestrict K ⋯).range

Tactic:
refine exists_congr ?_

Result:
case h
G₁ : Type u_7
G₂ : Type u_8
inst✝¹ : Group G₁
inst✝ : Group G₂
K : Subgroup G₂
f : G₁ →* G₂
h : f.range ≤ K
k : ↥K
⊢ ∀ (a : G₁), f a = K.subtype k ↔ (f.codRestrict K ⋯) a = k

Proof state:
case h
G₁ : Type u_7
G₂ : Type u_8
inst✝¹ : Group G₁
inst✝ : Group G₂
K : Subgroup G₂
f : G₁ →* G₂
h : f.range ≤ K
k : ↥K
⊢ ∀ (a : G₁), f a = K.subtype k ↔ (f.codRestrict K ⋯) a = k

Tactic:
simp [Subtype.ext_iff]

Result:
no goals

Proof state:
G₁ : Type u_7
G₂ : Type u_8
inst✝¹ : Group G₁
inst✝ : Group G₂
K : Subgroup G₂
f : G₁ →* G₂
h : f.range ≤ K
⊢ f.range.subgroupOf K = (f.codRestrict K ⋯).range

Tactic:
ext k

Result:
case h
G₁ : Type u_7
G₂ : Type u_8
inst✝¹ : Group G₁
inst✝ : Group G₂
K : Subgroup G₂
f : G₁ →* G₂
h : f.range ≤ K
k : ↥K
⊢ k ∈ f.range.subgroupOf K ↔ k ∈ (f.codRestrict K ⋯).range
-- Mathlib/NumberTheory/Primorial.lean
theorem primorial_add (m n : ℕ) :
    (m + n)# = m# * ∏ p ∈ Ico (m + 1) (m + n + 1) with p.Prime, p

Proof state:
m n : ℕ
⊢ (m + n)# = m# * ∏ p ∈ filter (fun p => Nat.Prime p) (Ico (m + 1) (m + n + 1)), p

Tactic:
rw [primorial, primorial, ← Ico_zero_eq_range, ← prod_union, ← filter_union, Ico_union_Ico_eq_Ico]

Result:
case hab
m n : ℕ
⊢ 0 ≤ m + 1

case hbc
m n : ℕ
⊢ m + 1 ≤ m + n + 1

m n : ℕ
⊢ Disjoint (filter (fun p => Nat.Prime p) (Ico 0 (m + 1))) (filter (fun p => Nat.Prime p) (Ico (m + 1) (m + n + 1)))

Proof state:
case hab
m n : ℕ
⊢ 0 ≤ m + 1

case hbc
m n : ℕ
⊢ m + 1 ≤ m + n + 1

m n : ℕ
⊢ Disjoint (filter (fun p => Nat.Prime p) (Ico 0 (m + 1))) (filter (fun p => Nat.Prime p) (Ico (m + 1) (m + n + 1)))

Tactic:
exacts [Nat.zero_le _, add_le_add_right (Nat.le_add_right _ _) _,
  disjoint_filter_filter <| Ico_disjoint_Ico_consecutive _ _ _]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem map_attach {l : Vector α n} (f : { x // x ∈ l } → β) :
    l.attach.map f = l.pmap (fun a h => f ⟨a, h⟩) (fun _ => id)

Proof state:
case mk
α : Type u_1
n : Nat
β : Type u_2
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
f : { x // x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } } → β
⊢ map f { toArray := toArray✝, size_toArray := size_toArray✝ }.attach =
    pmap (fun a h => f ⟨a, h⟩) { toArray := toArray✝, size_toArray := size_toArray✝ } ⋯

Tactic:
ext <;> simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : { x // x ∈ l } → β
⊢ map f l.attach = pmap (fun a h => f ⟨a, h⟩) l ⋯

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
β : Type u_2
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
f : { x // x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } } → β
⊢ map f { toArray := toArray✝, size_toArray := size_toArray✝ }.attach =
    pmap (fun a h => f ⟨a, h⟩) { toArray := toArray✝, size_toArray := size_toArray✝ } ⋯
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tsum_add_one_eq_top {f : ℕ → ℝ≥0∞} (hf : ∑' n, f n = ∞) (hf0 : f 0 ≠ ∞) :
    ∑' n, f (n + 1) = ∞

Proof state:
f : ℕ → ℝ≥0∞
hf : f 0 = ⊤ ∨ ∑' (b : ℕ), f (b + 1) = ⊤
hf0 : f 0 ≠ ⊤
⊢ ∑' (n : ℕ), f (n + 1) = ⊤

Tactic:
exact hf.resolve_left hf0

Result:
no goals

Proof state:
f : ℕ → ℝ≥0∞
hf : ∑' (n : ℕ), f n = ⊤
hf0 : f 0 ≠ ⊤
⊢ ∑' (n : ℕ), f (n + 1) = ⊤

Tactic:
rw [tsum_eq_zero_add' ENNReal.summable, add_eq_top] at hf

Result:
f : ℕ → ℝ≥0∞
hf : f 0 = ⊤ ∨ ∑' (b : ℕ), f (b + 1) = ⊤
hf0 : f 0 ≠ ⊤
⊢ ∑' (n : ℕ), f (n + 1) = ⊤
-- Mathlib/Algebra/Star/Subalgebra.lean
theorem comap_comap (S : StarSubalgebra R C) (g : B →⋆ₐ[R] C) (f : A →⋆ₐ[R] B) :
    (S.comap g).comap f = S.comap (g.comp f) :=
  SetLike.coe_injective <| by exact Set.preimage_preimage

Proof state:
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : Semiring B
inst✝⁶ : StarRing B
inst✝⁵ : Algebra R B
inst✝⁴ : StarModule R B
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
S : StarSubalgebra R C
g : B →⋆ₐ[R] C
f : A →⋆ₐ[R] B
⊢ ↑(comap f (comap g S)) = ↑(comap (g.comp f) S)

Tactic:
exact Set.preimage_preimage

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg (hab : 0 ≤ a • b) :
    0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
simp only [Decidable.or_iff_not_and_not, not_and, not_le]

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

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : 0 < a
⊢ a • b < 0

case inr.inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
b : β
hab : 0 ≤ 0 • b
ab : 0 ≤ 0 → b < 0
nab : 0 ≤ 0 → 0 < b
⊢ 0 • b < 0

case inr.inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : a < 0
⊢ a • b < 0

Tactic:
exacts [smul_neg_of_pos_of_neg ha (ab ha.le), ((ab le_rfl).asymm (nab le_rfl)).elim,
  smul_neg_of_neg_of_pos ha (nab ha.le)]

Result:
no goals

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

Tactic:
refine fun ab nab ↦ hab.not_lt ?_

Result:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
⊢ a • b < 0

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
⊢ a • b < 0

Tactic:
obtain ha | rfl | ha := lt_trichotomy 0 a

Result:
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : 0 < a
⊢ a • b < 0

case inr.inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
b : β
hab : 0 ≤ 0 • b
ab : 0 ≤ 0 → b < 0
nab : 0 ≤ 0 → 0 < b
⊢ 0 • b < 0

case inr.inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : a < 0
⊢ a • b < 0
-- Mathlib/Data/Set/Image.lean
theorem preimage_subtype_coe_eq_compl {s u v : Set α} (hsuv : s ⊆ u ∪ v)
    (H : s ∩ (u ∩ v) = ∅) : ((↑) : s → α) ⁻¹' u = ((↑) ⁻¹' v)ᶜ

Proof state:
case h.mk.mp
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
x_in_u : ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u
x_in_v : ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' v
⊢ False

Tactic:
exact eq_empty_iff_forall_not_mem.mp H x ⟨x_in_s, ⟨x_in_u, x_in_v⟩⟩

Result:
no goals

Proof state:
case h.mk
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u ↔ ⟨x, x_in_s⟩ ∈ (Subtype.val ⁻¹' v)ᶜ

Tactic:
constructor

Result:
case h.mk.mp
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u → ⟨x, x_in_s⟩ ∈ (Subtype.val ⁻¹' v)ᶜ

case h.mk.mpr
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ ⟨x, x_in_s⟩ ∈ (Subtype.val ⁻¹' v)ᶜ → ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u

Proof state:
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
⊢ Subtype.val ⁻¹' u = (Subtype.val ⁻¹' v)ᶜ

Tactic:
ext ⟨x, x_in_s⟩

Result:
case h.mk
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u ↔ ⟨x, x_in_s⟩ ∈ (Subtype.val ⁻¹' v)ᶜ

Proof state:
case h.mk.mpr
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ ⟨x, x_in_s⟩ ∈ (Subtype.val ⁻¹' v)ᶜ → ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u

Tactic:
intro hx

Result:
case h.mk.mpr
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
hx : ⟨x, x_in_s⟩ ∈ (Subtype.val ⁻¹' v)ᶜ
⊢ ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u

Proof state:
case h.mk.mpr
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
hx : ⟨x, x_in_s⟩ ∈ (Subtype.val ⁻¹' v)ᶜ
⊢ ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u

Tactic:
exact Or.elim (hsuv x_in_s) id fun hx' => hx.elim hx'

Result:
no goals

Proof state:
case h.mk.mp
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u → ⟨x, x_in_s⟩ ∈ (Subtype.val ⁻¹' v)ᶜ

Tactic:
intro x_in_u x_in_v

Result:
case h.mk.mp
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
x_in_u : ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u
x_in_v : ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' v
⊢ False
-- Mathlib/Geometry/Manifold/IsManifold/Basic.lean
theorem uniqueDiffOn_preimage {s : Set H} (hs : IsOpen s) :
    UniqueDiffOn 𝕜 (I.symm ⁻¹' s ∩ range I)

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
s : Set H
hs : IsOpen s
⊢ UniqueDiffOn 𝕜 (range ↑I ∩ ↑I.symm ⁻¹' s)

Tactic:
exact I.uniqueDiffOn.inter (hs.preimage I.continuous_invFun)

Result:
no goals

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
s : Set H
hs : IsOpen s
⊢ UniqueDiffOn 𝕜 (↑I.symm ⁻¹' s ∩ range ↑I)

Tactic:
rw [inter_comm]

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
s : Set H
hs : IsOpen s
⊢ UniqueDiffOn 𝕜 (range ↑I ∩ ↑I.symm ⁻¹' s)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_alter [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option (β k) → Option (β k)} :
    (m.alter k f).1.size =
      if m.contains k && (f (m.get? k)).isNone then
        m.1.size - 1
      else if !m.contains k && (f (m.get? k)).isSome then
        m.1.size + 1
      else
        m.1.size

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option (β k) → Option (β k)
⊢ (m.alter k f).val.size =
    if (m.contains k && (f (m.get? k)).isNone) = true then m.val.size - 1
    else if (!m.contains k && (f (m.get? k)).isSome) = true then m.val.size + 1 else m.val.size

Tactic:
simp_to_model [alter] using List.length_alterKey'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_or {x y : BitVec w} : (x ||| y).msb = (x.msb || y.msb)

Proof state:
w : Nat
x y : BitVec w
⊢ (x ||| y).msb = (x.msb || y.msb)

Tactic:
simp [BitVec.msb]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem parentD_findAux_lt {self : UnionFind} {x : Fin self.size} (h : i < self.size) :
    parentD (findAux self x).s i < self.size

Proof state:
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h' : ¬self.arr[↑x].parent = ↑x
⊢ (if i = ↑x then self.rootD ↑x else parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i) < self.size

Tactic:
split

Result:
case isTrue
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h' : ¬self.arr[↑x].parent = ↑x
h✝ : i = ↑x
⊢ self.rootD ↑x < self.size

case isFalse
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h' : ¬self.arr[↑x].parent = ↑x
h✝ : ¬i = ↑x
⊢ parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i < self.size

Proof state:
case isFalse
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h' : ¬self.arr[↑x].parent = ↑x
h✝ : ¬i = ↑x
this : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
⊢ parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i < self.size

Tactic:
apply parentD_findAux_lt h

Result:
no goals

Proof state:
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h' : self.arr[↑x].parent = ↑x
⊢ parentD self.arr i < self.size

Tactic:
apply self.parentD_lt h

Result:
no goals

Proof state:
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h' : self.arr[↑x].parent = ↑x
⊢ parentD (self.findAux x).s i < self.size

Tactic:
rw [findAux_s, if_pos h']

Result:
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h' : self.arr[↑x].parent = ↑x
⊢ parentD self.arr i < self.size

Proof state:
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h' : ¬self.arr[↑x].parent = ↑x
⊢ parentD (self.findAux x).s i < self.size

Tactic:
rw [parentD_findAux]

Result:
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h' : ¬self.arr[↑x].parent = ↑x
⊢ (if i = ↑x then self.rootD ↑x else parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i) < self.size

Proof state:
case isTrue
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h' : ¬self.arr[↑x].parent = ↑x
h✝ : i = ↑x
⊢ self.rootD ↑x < self.size

Tactic:
simp [rootD_lt]

Result:
no goals

Proof state:
case isFalse
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h' : ¬self.arr[↑x].parent = ↑x
h✝ : ¬i = ↑x
⊢ parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i < self.size

Tactic:
have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)

Result:
case isFalse
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h' : ¬self.arr[↑x].parent = ↑x
h✝ : ¬i = ↑x
this : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
⊢ parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i < self.size
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} :
    (m.erase k).contains a → m.contains a

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a : α
⊢ (m.erase k).contains a = true → m.contains a = true

Tactic:
simp_to_model [erase] using List.containsKey_of_containsKey_eraseKey

Result:
no goals
-- Mathlib/Order/Filter/Ultrafilter/Defs.lean
theorem iSup_ultrafilter_le_eq (f : Filter α) :
    ⨆ (g : Ultrafilter α) (_ : g ≤ f), (g : Filter α) = f :=
  eq_of_forall_ge_iff fun f' => by simp only [iSup_le_iff, ← le_iff_ultrafilter]

Proof state:
α : Type u
f f' : Filter α
⊢ ⨆ g, ⨆ (_ : ↑g ≤ f), ↑g ≤ f' ↔ f ≤ f'

Tactic:
simp only [iSup_le_iff, ← le_iff_ultrafilter]

Result:
no goals
-- Mathlib/Topology/ApproximateUnit.lean
/-- In a topological unital magma, `𝓝 1` is an approximate unit. -/
lemma nhds_one [ContinuousMul α] : IsApproximateUnit (𝓝 (1 : α)) where
  tendsto_mul_left m

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MulOneClass α
inst✝ : ContinuousMul α
m : α
⊢ Tendsto (fun x => m * x) (𝓝 1) (𝓝 m)

Tactic:
simpa using tendsto_id (x := 𝓝 1) |>.const_mul m

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MulOneClass α
inst✝ : ContinuousMul α
m : α
⊢ Tendsto (fun x => x * m) (𝓝 1) (𝓝 m)

Tactic:
simpa using tendsto_id (x := 𝓝 1) |>.mul_const m

Result:
no goals
-- Mathlib/Analysis/Complex/Periodic.lean
theorem invQParam_tendsto (hh : 0 < h) : Tendsto (invQParam h) (𝓝[≠] 0) I∞

Proof state:
h : ℝ
hh : 0 < h
⊢ 0 < 2 * π

Tactic:
positivity

Result:
no goals

Proof state:
h : ℝ
hh : 0 < h
⊢ Tendsto (invQParam h) (𝓝[≠] 0) I∞

Tactic:
simp only [tendsto_comap_iff, comp_def, im_invQParam]

Result:
h : ℝ
hh : 0 < h
⊢ Tendsto (fun x => -h / (2 * π) * Real.log ‖x‖) (𝓝[≠] 0) atTop

Proof state:
h : ℝ
hh : 0 < h
⊢ Tendsto (fun x => Real.log ‖x‖) (𝓝[≠] 0) atBot

Tactic:
exact Real.tendsto_log_nhdsWithin_zero_right.comp tendsto_norm_nhdsNE_zero

Result:
no goals

Proof state:
h : ℝ
hh : 0 < h
⊢ Tendsto (fun x => -h / (2 * π) * Real.log ‖x‖) (𝓝[≠] 0) atTop

Tactic:
apply Tendsto.const_mul_atBot_of_neg (div_neg_of_neg_of_pos (neg_lt_zero.mpr hh) (by positivity))

Result:
h : ℝ
hh : 0 < h
⊢ Tendsto (fun x => Real.log ‖x‖) (𝓝[≠] 0) atBot
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem cycleType_le_of_mem_cycleFactorsFinset {f g : Perm α} (hf : f ∈ g.cycleFactorsFinset) :
    f.cycleType ≤ g.cycleType

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
⊢ f.cycleType ≤ g.cycleType

Tactic:
have hf' := mem_cycleFactorsFinset_iff.1 hf

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
hf' : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
⊢ f.cycleType ≤ g.cycleType

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
hf' : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
⊢ f.cycleType ≤ g.cycleType

Tactic:
rw [cycleType_def, cycleType_def, hf'.left.cycleFactorsFinset_eq_singleton]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
hf' : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
⊢ Multiset.map (Finset.card ∘ support) {f}.val ≤ Multiset.map (Finset.card ∘ support) g.cycleFactorsFinset.val

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
hf' : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
⊢ {f}.val ≤ g.cycleFactorsFinset.val

Tactic:
simpa only [Finset.singleton_val, singleton_le, Finset.mem_val] using hf

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
hf' : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
⊢ Multiset.map (Finset.card ∘ support) {f}.val ≤ Multiset.map (Finset.card ∘ support) g.cycleFactorsFinset.val

Tactic:
refine map_le_map ?_

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
hf' : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
⊢ {f}.val ≤ g.cycleFactorsFinset.val
-- Mathlib/Topology/Algebra/UniformGroup/Basic.lean
theorem totallyBounded_inv {s : Set α} (hs : TotallyBounded s) : TotallyBounded (s⁻¹)

Proof state:
case h.e'_3.h.e
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set α
hs : TotallyBounded s
⊢ Inv.inv = image fun x => x⁻¹

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set α
hs : TotallyBounded s
⊢ TotallyBounded s⁻¹

Tactic:
convert TotallyBounded.image hs uniformContinuous_inv

Result:
case h.e'_3.h.e
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set α
hs : TotallyBounded s
⊢ Inv.inv = image fun x => x⁻¹
-- Mathlib/LinearAlgebra/Determinant.lean
theorem det_eq_one_of_subsingleton [Subsingleton M] (f : M →ₗ[R] M) :
    LinearMap.det (f : M →ₗ[R] M) = 1

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton M
f : M →ₗ[R] M
⊢ LinearMap.det f = 1

Tactic:
have b : Basis (Fin 0) R M := Basis.empty M

Result:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton M
f : M →ₗ[R] M
b : Basis (Fin 0) R M
⊢ LinearMap.det f = 1

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton M
f : M →ₗ[R] M
b : Basis (Fin 0) R M
⊢ ((toMatrix b b) f).det = 1

Tactic:
exact Matrix.det_isEmpty

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton M
f : M →ₗ[R] M
b : Basis (Fin 0) R M
⊢ LinearMap.det f = 1

Tactic:
rw [← f.det_toMatrix b]

Result:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton M
f : M →ₗ[R] M
b : Basis (Fin 0) R M
⊢ ((toMatrix b b) f).det = 1
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_nonneg {f : R → R} {a : A} (h : ∀ x ∈ σₙ R a, 0 ≤ f x) :
    0 ≤ cfcₙ f a

Proof state:
case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁵ : OrderedCommSemiring R
inst✝¹⁴ : Nontrivial R
inst✝¹³ : StarRing R
inst✝¹² : MetricSpace R
inst✝¹¹ : IsTopologicalSemiring R
inst✝¹⁰ : ContinuousStar R
inst✝⁹ : ∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ 0 ≤ cfcₙ f a

Tactic:
simp only [not_and_or] at hf

Result:
case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁵ : OrderedCommSemiring R
inst✝¹⁴ : Nontrivial R
inst✝¹³ : StarRing R
inst✝¹² : MetricSpace R
inst✝¹¹ : IsTopologicalSemiring R
inst✝¹⁰ : ContinuousStar R
inst✝⁹ : ∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬ContinuousOn f (σₙ R a) ∨ ¬f 0 = 0
⊢ 0 ≤ cfcₙ f a

Proof state:
case neg.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁵ : OrderedCommSemiring R
inst✝¹⁴ : Nontrivial R
inst✝¹³ : StarRing R
inst✝¹² : MetricSpace R
inst✝¹¹ : IsTopologicalSemiring R
inst✝¹⁰ : ContinuousStar R
inst✝⁹ : ∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, 0 ≤ f x
hf : ¬f 0 = 0
⊢ 0 ≤ cfcₙ f a

Tactic:
simp only [cfcₙ_apply_of_not_map_zero _ hf, le_rfl]

Result:
no goals