harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- A number that divides an `s`-factored number is itself `s`-factored. -/
lemma mem_factoredNumbers_of_dvd {s : Finset ℕ} {m k : ℕ} (h : m ∈ factoredNumbers s)
    (h' : k ∣ m) :
    k ∈ factoredNumbers s

Proof state:
case intro
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
⊢ k ∈ factoredNumbers s

Tactic:
have hk := ne_zero_of_dvd_ne_zero h₁ h'

Result:
case intro
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
hk : k ≠ 0
⊢ k ∈ factoredNumbers s

Proof state:
case intro
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
hk : k ≠ 0
p : ℕ
hp : Prime p ∧ p ∣ k
⊢ Prime p ∧ p ∣ m

Tactic:
exact ⟨hp.1, hp.2.trans h'⟩

Result:
no goals

Proof state:
case intro
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
hk : k ≠ 0
⊢ k ∈ factoredNumbers s

Tactic:
refine ⟨hk, fun p hp ↦ h₂ p ?_⟩

Result:
case intro
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
hk : k ≠ 0
p : ℕ
hp : p ∈ k.primeFactorsList
⊢ p ∈ m.primeFactorsList

Proof state:
case intro
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
hk : k ≠ 0
p : ℕ
hp : p ∈ k.primeFactorsList
⊢ p ∈ m.primeFactorsList

Tactic:
rw [mem_primeFactorsList <| by assumption] at hp ⊢

Result:
case intro
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
hk : k ≠ 0
p : ℕ
hp : Prime p ∧ p ∣ k
⊢ Prime p ∧ p ∣ m

Proof state:
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
hk : k ≠ 0
p : ℕ
hp : Prime p ∧ p ∣ k
⊢ m ≠ 0

Tactic:
assumption

Result:
no goals

Proof state:
s : Finset ℕ
m k : ℕ
h : m ∈ factoredNumbers s
h' : k ∣ m
⊢ k ∈ factoredNumbers s

Tactic:
obtain ⟨h₁, h₂⟩ := h

Result:
case intro
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
⊢ k ∈ factoredNumbers s
-- Mathlib/Topology/ContinuousMap/BoundedCompactlySupported.lean
theorem norm_lt_iff_of_compactlySupported {f : α →ᵇ γ} (h : f ∈ C_cb(α, γ)) {M : ℝ}
    (M0 : 0 < M) : ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

Proof state:
case inr.intro
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
he : Nonempty α
x : α
hx : ‖f x‖ = ‖f‖
⊢ (∀ (x : α), ‖f x‖ < M) → ‖f‖ < M

Tactic:
exact fun h ↦ hx ▸ h x

Result:
no goals

Proof state:
case inl
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
he : IsEmpty α
⊢ (∀ (x : α), ‖f x‖ < M) → ‖f‖ < M

Tactic:
simpa

Result:
no goals

Proof state:
case inr
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
he : Nonempty α
⊢ (∀ (x : α), ‖f x‖ < M) → ‖f‖ < M

Tactic:
obtain ⟨x, hx⟩ := exist_norm_eq h

Result:
case inr.intro
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
he : Nonempty α
x : α
hx : ‖f x‖ = ‖f‖
⊢ (∀ (x : α), ‖f x‖ < M) → ‖f‖ < M

Proof state:
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
⊢ (∀ (x : α), ‖f x‖ < M) → ‖f‖ < M

Tactic:
obtain (he | he) := isEmpty_or_nonempty α

Result:
case inl
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
he : IsEmpty α
⊢ (∀ (x : α), ‖f x‖ < M) → ‖f‖ < M

case inr
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
he : Nonempty α
⊢ (∀ (x : α), ‖f x‖ < M) → ‖f‖ < M

Proof state:
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

Tactic:
refine ⟨fun hn x ↦ lt_of_le_of_lt (norm_coe_le_norm f x) hn, ?_⟩

Result:
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
⊢ (∀ (x : α), ‖f x‖ < M) → ‖f‖ < M
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_erase [LawfulBEq α] (h : m.1.WF) {k a : α} :
    (m.erase k).get? a = if k == a then none else m.get? a

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k a : α
⊢ (m.erase k).get? a = if (k == a) = true then none else m.get? a

Tactic:
simp_to_model [erase] using List.getValueCast?_eraseKey

Result:
no goals
-- Mathlib/Data/PNat/Prime.lean
theorem gcd_eq_left {m n : ℕ+} : m ∣ n → m.gcd n = m

Proof state:
m n : ℕ+
⊢ ↑m ∣ ↑n → m.gcd n = m

Tactic:
intro h

Result:
m n : ℕ+
h : ↑m ∣ ↑n
⊢ m.gcd n = m

Proof state:
m n : ℕ+
⊢ m ∣ n → m.gcd n = m

Tactic:
rw [dvd_iff]

Result:
m n : ℕ+
⊢ ↑m ∣ ↑n → m.gcd n = m

Proof state:
case a
m n : ℕ+
h : ↑m ∣ ↑n
⊢ ↑(m.gcd n) = ↑m

Tactic:
simp only [gcd_coe]

Result:
case a
m n : ℕ+
h : ↑m ∣ ↑n
⊢ (↑m).gcd ↑n = ↑m

Proof state:
case a
m n : ℕ+
h : ↑m ∣ ↑n
⊢ (↑m).gcd ↑n = ↑m

Tactic:
apply Nat.gcd_eq_left h

Result:
no goals

Proof state:
m n : ℕ+
h : ↑m ∣ ↑n
⊢ m.gcd n = m

Tactic:
apply eq

Result:
case a
m n : ℕ+
h : ↑m ∣ ↑n
⊢ ↑(m.gcd n) = ↑m
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem merge_of_le : ∀ {xs ys : List α} (_ : ∀ a b, a ∈ xs → b ∈ ys → le a b),
    merge xs ys le = xs ++ ys
  | [], ys, _
  | xs, [], _ => by simp [merge]
  | x :: xs, y :: ys, h => by
    simp only [merge, cons_append]
    rw [if_pos, merge_of_le]
    · intro a b ma mb
      exact h a b (mem_cons_of_mem _ ma) mb
    · exact h x y (mem_cons_self _ _) (mem_cons_self _ _)

Proof state:
α : Type u_1
le : α → α → Bool
x : α
xs : List α
y : α
ys : List α
h : ∀ (a b : α), a ∈ x :: xs → b ∈ y :: ys → le a b = true
⊢ ∀ (a b : α), a ∈ xs → b ∈ y :: ys → le a b = true

Tactic:
intro a b ma mb

Result:
α : Type u_1
le : α → α → Bool
x : α
xs : List α
y : α
ys : List α
h : ∀ (a b : α), a ∈ x :: xs → b ∈ y :: ys → le a b = true
a b : α
ma : a ∈ xs
mb : b ∈ y :: ys
⊢ le a b = true

Proof state:
α : Type u_1
le : α → α → Bool
x : α
xs : List α
y : α
ys : List α
h : ∀ (a b : α), a ∈ x :: xs → b ∈ y :: ys → le a b = true
⊢ (x :: xs).merge (y :: ys) le = x :: xs ++ y :: ys

Tactic:
simp only [merge, cons_append]

Result:
α : Type u_1
le : α → α → Bool
x : α
xs : List α
y : α
ys : List α
h : ∀ (a b : α), a ∈ x :: xs → b ∈ y :: ys → le a b = true
⊢ (if le x y = true then x :: xs.merge (y :: ys) le else y :: (x :: xs).merge ys le) = x :: (xs ++ y :: ys)

Proof state:
α : Type u_1
le : α → α → Bool
xs : List α
x✝ : ∀ (a b : α), a ∈ xs → b ∈ [] → le a b = true
⊢ xs.merge [] le = xs ++ []

Tactic:
simp [merge]

Result:
no goals

Proof state:
case hc
α : Type u_1
le : α → α → Bool
x : α
xs : List α
y : α
ys : List α
h : ∀ (a b : α), a ∈ x :: xs → b ∈ y :: ys → le a b = true
⊢ le x y = true

Tactic:
exact h x y (mem_cons_self _ _) (mem_cons_self _ _)

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
x : α
xs : List α
y : α
ys : List α
h : ∀ (a b : α), a ∈ x :: xs → b ∈ y :: ys → le a b = true
⊢ (if le x y = true then x :: xs.merge (y :: ys) le else y :: (x :: xs).merge ys le) = x :: (xs ++ y :: ys)

Tactic:
rw [if_pos, merge_of_le]

Result:
α : Type u_1
le : α → α → Bool
x : α
xs : List α
y : α
ys : List α
h : ∀ (a b : α), a ∈ x :: xs → b ∈ y :: ys → le a b = true
⊢ ∀ (a b : α), a ∈ xs → b ∈ y :: ys → le a b = true

case hc
α : Type u_1
le : α → α → Bool
x : α
xs : List α
y : α
ys : List α
h : ∀ (a b : α), a ∈ x :: xs → b ∈ y :: ys → le a b = true
⊢ le x y = true

Proof state:
α : Type u_1
le : α → α → Bool
x : α
xs : List α
y : α
ys : List α
h : ∀ (a b : α), a ∈ x :: xs → b ∈ y :: ys → le a b = true
a b : α
ma : a ∈ xs
mb : b ∈ y :: ys
⊢ le a b = true

Tactic:
exact h a b (mem_cons_of_mem _ ma) mb

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Grp_.lean
theorem eq_lift_inv_right {A : C} {B : Grp_ C} (f g h : A ⟶ B.X) :
    f = lift g (h ≫ B.inv) ≫ B.mul ↔ lift f h ≫ B.mul = g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Grp_ C
f g h : A ⟶ B.X
⊢ f = lift g (h ≫ B.inv) ≫ B.mul ↔ lift f h ≫ B.mul = g

Tactic:
refine ⟨?_, ?_⟩ <;> (rintro rfl; simp [lift_lift_assoc])

Result:
no goals

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Grp_ C
f g h : A ⟶ B.X
⊢ lift f h ≫ B.mul = g → f = lift g (h ≫ B.inv) ≫ B.mul

Tactic:
rintro rfl

Result:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Grp_ C
f h : A ⟶ B.X
⊢ f = lift (lift f h ≫ B.mul) (h ≫ B.inv) ≫ B.mul

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Grp_ C
f h : A ⟶ B.X
⊢ f = lift (lift f h ≫ B.mul) (h ≫ B.inv) ≫ B.mul

Tactic:
simp [lift_lift_assoc]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem graph_injective (α M) [Zero M] : Injective (@graph α M _)

Proof state:
α : Type u_13
M : Type u_14
inst✝ : Zero M
f g : α →₀ M
h : f.graph = g.graph
⊢ f = g

Tactic:
have hsup : f.support = g.support := by rw [← image_fst_graph, h, image_fst_graph]

Result:
α : Type u_13
M : Type u_14
inst✝ : Zero M
f g : α →₀ M
h : f.graph = g.graph
hsup : f.support = g.support
⊢ f = g

Proof state:
α : Type u_13
M : Type u_14
inst✝ : Zero M
f g : α →₀ M
h : f.graph = g.graph
⊢ f = g

Tactic:
classical
  have hsup : f.support = g.support := by rw [← image_fst_graph, h, image_fst_graph]
  refine ext_iff'.2 ⟨hsup, fun x hx => apply_eq_of_mem_graph <| h.symm ▸ ?_⟩
  exact mk_mem_graph _ (hsup ▸ hx)

Result:
no goals

Proof state:
α : Type u_13
M : Type u_14
inst✝ : Zero M
f g : α →₀ M
h : f.graph = g.graph
hsup : f.support = g.support
x : α
hx : x ∈ f.support
⊢ (x, g x) ∈ g.graph

Tactic:
exact mk_mem_graph _ (hsup ▸ hx)

Result:
no goals

Proof state:
α : Type u_13
M : Type u_14
inst✝ : Zero M
⊢ Injective graph

Tactic:
intro f g h

Result:
α : Type u_13
M : Type u_14
inst✝ : Zero M
f g : α →₀ M
h : f.graph = g.graph
⊢ f = g

Proof state:
α : Type u_13
M : Type u_14
inst✝ : Zero M
f g : α →₀ M
h : f.graph = g.graph
⊢ f.support = g.support

Tactic:
rw [← image_fst_graph, h, image_fst_graph]

Result:
no goals

Proof state:
α : Type u_13
M : Type u_14
inst✝ : Zero M
f g : α →₀ M
h : f.graph = g.graph
hsup : f.support = g.support
⊢ f = g

Tactic:
refine ext_iff'.2 ⟨hsup, fun x hx => apply_eq_of_mem_graph <| h.symm ▸ ?_⟩

Result:
α : Type u_13
M : Type u_14
inst✝ : Zero M
f g : α →₀ M
h : f.graph = g.graph
hsup : f.support = g.support
x : α
hx : x ∈ f.support
⊢ (x, g x) ∈ g.graph
-- Mathlib/Algebra/Category/MonCat/Basic.lean
theorem MonoidHom.id_monCat_comp {G : Type u} [Monoid G] {H : MonCat.{u}} (f : G →* H) :
    MonoidHom.comp (MonCat.Hom.hom (𝟙 H)) f = f

Proof state:
G : Type u
inst✝ : Monoid G
H : MonCat
f : G →* ↑H
⊢ (MonCat.Hom.hom (𝟙 H)).comp f = f

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
@[simp, norm_cast]
lemma ofReal_lt_ofReal {x y : ℝ} : (x : K) < (y : K) ↔ x < y

Proof state:
K : Type u_1
inst✝ : RCLike K
x y : ℝ
⊢ re ↑x < re ↑y ∧ im ↑x = im ↑y ↔ x < y

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
x y : ℝ
⊢ ↑x < ↑y ↔ x < y

Tactic:
rw [lt_iff_re_im]

Result:
K : Type u_1
inst✝ : RCLike K
x y : ℝ
⊢ re ↑x < re ↑y ∧ im ↑x = im ↑y ↔ x < y
-- Mathlib/Topology/MetricSpace/Gluing.lean
theorem isOpen_iff (s : Set (Σi, E i)) :
    IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ y, dist x y < ε → y ∈ s

Proof state:
case mp.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : ⟨i, x⟩ ∈ s
⊢ ∃ ε > 0, ∀ (y : (i : ι) × E i), dist ⟨i, x⟩ y < ε → y ∈ s

Tactic:
obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, ball x ε ⊆ Sigma.mk i ⁻¹' s :=
  Metric.isOpen_iff.1 (isOpen_sigma_iff.1 hs i) x hx

Result:
case mp.mk.intro.intro
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : ⟨i, x⟩ ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
⊢ ∃ ε > 0, ∀ (y : (i : ι) × E i), dist ⟨i, x⟩ y < ε → y ∈ s

Proof state:
case mp.mk.intro.intro.mk.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : ⟨i, x⟩ ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
j : ι
y : E j
hy : dist ⟨i, x⟩ ⟨j, y⟩ < ε ⊓ 1
hij : i ≠ j
⊢ ⟨j, y⟩ ∈ s

Tactic:
apply (lt_irrefl (1 : ℝ) _).elim

Result:
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : ⟨i, x⟩ ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
j : ι
y : E j
hy : dist ⟨i, x⟩ ⟨j, y⟩ < ε ⊓ 1
hij : i ≠ j
⊢ 1 < 1

Proof state:
case mpr.intro.intro
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist ⟨i, x⟩ y < ε → y ∈ s
y : E i
hy : y ∈ ball x ε
⊢ dist x y < ε

Tactic:
exact mem_ball'.1 hy

Result:
no goals

Proof state:
case mp
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
⊢ IsOpen s → ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s

Tactic:
rintro hs ⟨i, x⟩ hx

Result:
case mp.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : ⟨i, x⟩ ∈ s
⊢ ∃ ε > 0, ∀ (y : (i : ι) × E i), dist ⟨i, x⟩ y < ε → y ∈ s
-- Mathlib/Analysis/Normed/Group/Basic.lean
lemma nnnorm_two : ‖(2 : ℝ)‖₊ = 2 := NNReal.eq <| by simp

Proof state:
⊢ ↑‖2‖₊ = ↑2

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem Fork.hom_comp_ι {s t : Fork f g} (f : s ⟶ t) : f.hom ≫ t.ι = s.ι

Proof state:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f✝ g : X ⟶ Y
pt✝¹ : C
π✝¹ : (Functor.const WalkingParallelPair).obj pt✝¹ ⟶ parallelPair f✝ g
pt✝ : C
π✝ : (Functor.const WalkingParallelPair).obj pt✝ ⟶ parallelPair f✝ g
f : { pt := pt✝¹, π := π✝¹ } ⟶ { pt := pt✝, π := π✝ }
⊢ f.hom ≫ ι { pt := pt✝, π := π✝ } = ι { pt := pt✝¹, π := π✝¹ }

Tactic:
cases f

Result:
case mk.mk.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
pt✝¹ : C
π✝¹ : (Functor.const WalkingParallelPair).obj pt✝¹ ⟶ parallelPair f g
pt✝ : C
π✝ : (Functor.const WalkingParallelPair).obj pt✝ ⟶ parallelPair f g
hom✝ : { pt := pt✝¹, π := π✝¹ }.pt ⟶ { pt := pt✝, π := π✝ }.pt
w✝ : ∀ (j : WalkingParallelPair), hom✝ ≫ { pt := pt✝, π := π✝ }.π.app j = { pt := pt✝¹, π := π✝¹ }.π.app j
⊢ { hom := hom✝, w := w✝ }.hom ≫ ι { pt := pt✝, π := π✝ } = ι { pt := pt✝¹, π := π✝¹ }

Proof state:
case mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f✝ g : X ⟶ Y
t : Fork f✝ g
pt✝ : C
π✝ : (Functor.const WalkingParallelPair).obj pt✝ ⟶ parallelPair f✝ g
f : { pt := pt✝, π := π✝ } ⟶ t
⊢ f.hom ≫ t.ι = ι { pt := pt✝, π := π✝ }

Tactic:
cases t

Result:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f✝ g : X ⟶ Y
pt✝¹ : C
π✝¹ : (Functor.const WalkingParallelPair).obj pt✝¹ ⟶ parallelPair f✝ g
pt✝ : C
π✝ : (Functor.const WalkingParallelPair).obj pt✝ ⟶ parallelPair f✝ g
f : { pt := pt✝¹, π := π✝¹ } ⟶ { pt := pt✝, π := π✝ }
⊢ f.hom ≫ ι { pt := pt✝, π := π✝ } = ι { pt := pt✝¹, π := π✝¹ }

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f✝ g : X ⟶ Y
s t : Fork f✝ g
f : s ⟶ t
⊢ f.hom ≫ t.ι = s.ι

Tactic:
cases s

Result:
case mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f✝ g : X ⟶ Y
t : Fork f✝ g
pt✝ : C
π✝ : (Functor.const WalkingParallelPair).obj pt✝ ⟶ parallelPair f✝ g
f : { pt := pt✝, π := π✝ } ⟶ t
⊢ f.hom ≫ t.ι = ι { pt := pt✝, π := π✝ }

Proof state:
case mk.mk.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
pt✝¹ : C
π✝¹ : (Functor.const WalkingParallelPair).obj pt✝¹ ⟶ parallelPair f g
pt✝ : C
π✝ : (Functor.const WalkingParallelPair).obj pt✝ ⟶ parallelPair f g
hom✝ : { pt := pt✝¹, π := π✝¹ }.pt ⟶ { pt := pt✝, π := π✝ }.pt
w✝ : ∀ (j : WalkingParallelPair), hom✝ ≫ { pt := pt✝, π := π✝ }.π.app j = { pt := pt✝¹, π := π✝¹ }.π.app j
⊢ { hom := hom✝, w := w✝ }.hom ≫ ι { pt := pt✝, π := π✝ } = ι { pt := pt✝¹, π := π✝¹ }

Tactic:
aesop

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean
lemma differentiable_Gammaℝ_inv : Differentiable ℂ (fun s ↦ (Gammaℝ s)⁻¹)

Proof state:
case refine_2

⊢ Differentiable ℂ fun s => (Gamma (s / 2))⁻¹

Tactic:
exact differentiable_one_div_Gamma.comp (differentiable_id.div_const _)

Result:
no goals

Proof state:
⊢ Differentiable ℂ fun s => (↑π ^ (-s / 2))⁻¹ * (Gamma (s / 2))⁻¹

Tactic:
refine Differentiable.mul (fun s ↦ .inv ?_ (by simp [pi_ne_zero])) ?_

Result:
case refine_1
s : ℂ
⊢ DifferentiableAt ℂ (fun s => ↑π ^ (-s / 2)) s

case refine_2

⊢ Differentiable ℂ fun s => (Gamma (s / 2))⁻¹

Proof state:
case refine_1
s : ℂ
⊢ DifferentiableAt ℂ (fun s => ↑π ^ (-s / 2)) s

Tactic:
refine ((differentiableAt_id.neg.div_const (2 : ℂ)).const_cpow ?_)

Result:
case refine_1
s : ℂ
⊢ ↑π ≠ 0 ∨ -s / 2 ≠ 0

Proof state:
⊢ Differentiable ℂ fun s => s.Gammaℝ⁻¹

Tactic:
conv => enter [2, s]; rw [Gammaℝ, mul_inv]

Result:
⊢ Differentiable ℂ fun s => (↑π ^ (-s / 2))⁻¹ * (Gamma (s / 2))⁻¹

Proof state:
case refine_1
s : ℂ
⊢ ↑π ≠ 0 ∨ -s / 2 ≠ 0

Tactic:
exact Or.inl (ofReal_ne_zero.mpr pi_ne_zero)

Result:
no goals

Proof state:
s : ℂ
⊢ ↑π ^ (-s / 2) ≠ 0

Tactic:
simp [pi_ne_zero]

Result:
no goals
-- Mathlib/FieldTheory/PerfectClosure.lean
theorem intCast (x : ℤ) : (x : PerfectClosure K p) = mk K p (0, x)

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℤ
⊢ ↑x = mk K p (0, ↑x)

Tactic:
cases x <;> simp [natCast K p 0]

Result:
no goals
-- Mathlib/Algebra/Order/Kleene.lean
theorem kstar_le_of_mul_le_right (hb : 1 ≤ b) : a * b ≤ b → a∗ ≤ b

Proof state:
α : Type u_1
inst✝ : KleeneAlgebra α
a b : α
hb : 1 ≤ b
⊢ a * b ≤ b → a∗ ≤ b

Tactic:
simpa using kstar_mul_le hb

Result:
no goals
-- Mathlib/Analysis/Complex/TaylorSeries.lean
/-- A function that is complex differentiable on the open ball of radius `r` around `c`
is given by evaluating its Taylor series at `c` on this open ball. -/
lemma hasSum_taylorSeries_on_ball :
    HasSum (fun n : ℕ ↦ (n ! : ℂ)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : ↑r' < r
hr'₀ : 0 < ↑r'
hzr' : z ∈ Metric.ball c ↑r'
⊢ z - c ∈ EMetric.ball 0 ↑r'

Tactic:
rw [Metric.emetric_ball_nnreal]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : ↑r' < r
hr'₀ : 0 < ↑r'
hzr' : z ∈ Metric.ball c ↑r'
⊢ z - c ∈ Metric.ball 0 ↑r'

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : ↑r' < r
hr'₀ : 0 < ↑r'
hzr' : z ∈ Metric.ball c ↑r'
⊢ z - c ∈ Metric.ball 0 ↑r'

Tactic:
exact mem_ball_zero_iff.mpr hzr'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem coordinate_eval_3 :
    (coordinate 3).eval (.ofList (a0 :: a1 :: a2 :: a3 :: t)) = a3

Proof state:
a0 a1 a2 a3 : Int
t : List Int
⊢ (coordinate 3).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: t)) = a3

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem nextn : ∀ {it}, ValidFor l r it →
      ∀ n, n ≤ r.length → ValidFor ((r.take n).reverse ++ l) (r.drop n) (it.nextn n)
  | it, h, 0, _ => by simp [h, Iterator.nextn]
  | it, h, n+1, hn => by
    simp only [Iterator.nextn]
    have a::r := r
    simpa using h.next.nextn _ (Nat.le_of_succ_le_succ hn)

Proof state:
l r : List Char
it : Iterator
h : ValidFor l r it
n : Nat
hn : n + 1 ≤ r.length
⊢ ValidFor ((List.take (n + 1) r).reverse ++ l) (List.drop (n + 1) r) (it.next.nextn n)

Tactic:
have a::r := r

Result:
l r✝ : List Char
it : Iterator
n : Nat
a : Char
r : List Char
h : ValidFor l (a :: r) it
hn : n + 1 ≤ (a :: r).length
⊢ ValidFor ((List.take (n + 1) (a :: r)).reverse ++ l) (List.drop (n + 1) (a :: r)) (it.next.nextn n)

Proof state:
l r : List Char
it : Iterator
h : ValidFor l r it
x✝ : 0 ≤ r.length
⊢ ValidFor ((List.take 0 r).reverse ++ l) (List.drop 0 r) (it.nextn 0)

Tactic:
simp [h, Iterator.nextn]

Result:
no goals

Proof state:
l r : List Char
it : Iterator
h : ValidFor l r it
n : Nat
hn : n + 1 ≤ r.length
⊢ ValidFor ((List.take (n + 1) r).reverse ++ l) (List.drop (n + 1) r) (it.nextn (n + 1))

Tactic:
simp only [Iterator.nextn]

Result:
l r : List Char
it : Iterator
h : ValidFor l r it
n : Nat
hn : n + 1 ≤ r.length
⊢ ValidFor ((List.take (n + 1) r).reverse ++ l) (List.drop (n + 1) r) (it.next.nextn n)

Proof state:
l r✝ : List Char
it : Iterator
n : Nat
a : Char
r : List Char
h : ValidFor l (a :: r) it
hn : n + 1 ≤ (a :: r).length
⊢ ValidFor ((List.take (n + 1) (a :: r)).reverse ++ l) (List.drop (n + 1) (a :: r)) (it.next.nextn n)

Tactic:
simpa using h.next.nextn _ (Nat.le_of_succ_le_succ hn)

Result:
no goals
-- Mathlib/Data/Nat/Multiplicity.lean
theorem emultiplicity_factorial {p : ℕ} (hp : p.Prime) :
    ∀ {n b : ℕ}, log p n < b → emultiplicity p n ! = (∑ i ∈ Ico 1 b, n / p ^ i : ℕ)
  | 0, b, _ => by simp [Ico, hp.emultiplicity_one]
  | n + 1, b, hb =>
    calc
      emultiplicity p (n + 1)! = emultiplicity p n ! + emultiplicity p (n + 1)

Proof state:
p : ℕ
hp : Prime p
b : ℕ
x✝ : log p 0 < b
⊢ emultiplicity p 0! = ↑(∑ i ∈ Ico 1 b, 0 / p ^ i)

Tactic:
simp [Ico, hp.emultiplicity_one]

Result:
no goals

Proof state:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ emultiplicity p (n + 1)! = emultiplicity p n ! + emultiplicity p (n + 1)

Tactic:
rw [factorial_succ, hp.emultiplicity_mul, add_comm]

Result:
no goals

Proof state:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ↑(∑ i ∈ Ico 1 b, n / p ^ i) + ↑(#(filter (fun i => p ^ i ∣ n + 1) (Ico 1 b))) =
    ↑(∑ x ∈ Ico 1 b, n / p ^ x + ↑(#(filter (fun x => p ^ x ∣ n + 1) (Ico 1 b))))

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ emultiplicity p n ! + emultiplicity p (n + 1) =
    ↑(∑ i ∈ Ico 1 b, n / p ^ i) + ↑(#(filter (fun i => p ^ i ∣ n + 1) (Ico 1 b)))

Tactic:
rw [emultiplicity_factorial hp ((log_mono_right <| le_succ _).trans_lt hb), ←
  emultiplicity_eq_card_pow_dvd hp.ne_one (succ_pos _) hb]

Result:
no goals

Proof state:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ↑(∑ i ∈ Ico 1 b, n / p ^ i) + ↑(#(filter (fun i => p ^ i ∣ n + 1) (Ico 1 b))) =
    ↑(∑ i ∈ Ico 1 b, (n / p ^ i + if p ^ i ∣ n + 1 then 1 else 0))

Tactic:
rw [sum_add_distrib, sum_boole]

Result:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ↑(∑ i ∈ Ico 1 b, n / p ^ i) + ↑(#(filter (fun i => p ^ i ∣ n + 1) (Ico 1 b))) =
    ↑(∑ x ∈ Ico 1 b, n / p ^ x + ↑(#(filter (fun x => p ^ x ∣ n + 1) (Ico 1 b))))