harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem exists_lt_succ_right' {p : (m : Nat) → (m < n + 1) → Prop} :
    (∃ m, ∃ (h : m < n + 1), p m h) ↔ (∃ m, ∃ (h : m < n), p m (by omega)) ∨ p n (by omega)

Proof state:
case mp
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ (∃ m h, p m ⋯) → (∃ m h, p m ⋯) ∨ p n ⋯

Tactic:
rintro ⟨m, (h|rfl), w⟩

Result:
case mp.intro.intro.inl
n : Nat
p : (m : Nat) → m < n + 1 → Prop
m : Nat
h : m < n
w : p m ⋯
⊢ (∃ m h, p m ⋯) ∨ p n ⋯

case mp.intro.intro.inr
m : Nat
p : (m_1 : Nat) → m_1 < m + 1 → Prop
w : p m ⋯
⊢ (∃ m_1 h, p m_1 ⋯) ∨ p m ⋯

Proof state:
case mpr.inr
n : Nat
p : (m : Nat) → m < n + 1 → Prop
w : p n ⋯
⊢ ∃ m h, p m ⋯

Tactic:
exact ⟨n, by omega, w⟩

Result:
no goals

Proof state:
case mpr.inl.intro.intro
n : Nat
p : (m : Nat) → m < n + 1 → Prop
m : Nat
h : m < n
w : p m ⋯
⊢ ∃ m h, p m ⋯

Tactic:
exact ⟨m, by omega, w⟩

Result:
no goals

Proof state:
case mp.intro.intro.inl
n : Nat
p : (m : Nat) → m < n + 1 → Prop
m : Nat
h : m < n
w : p m ⋯
⊢ (∃ m h, p m ⋯) ∨ p n ⋯

Tactic:
exact .inl ⟨m, h, w⟩

Result:
no goals

Proof state:
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ (∃ m h, p m ⋯) ↔ (∃ m h, p m ⋯) ∨ p n ⋯

Tactic:
constructor

Result:
case mp
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ (∃ m h, p m ⋯) → (∃ m h, p m ⋯) ∨ p n ⋯

case mpr
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ (∃ m h, p m ⋯) ∨ p n ⋯ → ∃ m h, p m ⋯

Proof state:
case mp.intro.intro.inr
m : Nat
p : (m_1 : Nat) → m_1 < m + 1 → Prop
w : p m ⋯
⊢ (∃ m_1 h, p m_1 ⋯) ∨ p m ⋯

Tactic:
exact .inr w

Result:
no goals

Proof state:
n : Nat
p : (m : Nat) → m < n + 1 → Prop
w : p n ⋯
⊢ n < n ∨ n = n

Tactic:
omega

Result:
no goals

Proof state:
case mpr
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ (∃ m h, p m ⋯) ∨ p n ⋯ → ∃ m h, p m ⋯

Tactic:
rintro (⟨m, h, w⟩ | w)

Result:
case mpr.inl.intro.intro
n : Nat
p : (m : Nat) → m < n + 1 → Prop
m : Nat
h : m < n
w : p m ⋯
⊢ ∃ m h, p m ⋯

case mpr.inr
n : Nat
p : (m : Nat) → m < n + 1 → Prop
w : p n ⋯
⊢ ∃ m h, p m ⋯

Proof state:
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ n < n + 1

Tactic:
omega

Result:
no goals

Proof state:
n : Nat
p : (m : Nat) → m < n + 1 → Prop
m : Nat
h : m < n
w : p m ⋯
⊢ m < n ∨ m = n

Tactic:
omega

Result:
no goals

Proof state:
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ (∃ m h, p m h) ↔ (∃ m h, p m ⋯) ∨ p n ⋯

Tactic:
simp only [Nat.lt_succ_iff, Nat.le_iff_lt_or_eq]

Result:
n : Nat
p : (m : Nat) → m < n + 1 → Prop
⊢ (∃ m h, p m ⋯) ↔ (∃ m h, p m ⋯) ∨ p n ⋯

Proof state:
n : Nat
p : (m : Nat) → m < n + 1 → Prop
m : Nat
h : m < n
⊢ m < n + 1

Tactic:
omega

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem measure_set_eq (hs : IsFundamentalDomain G s μ) (ht : IsFundamentalDomain G t μ) {A : Set α}
    (hA₀ : MeasurableSet A) (hA : ∀ g : G, (fun x => g • x) ⁻¹' A = A) : μ (A ∩ s) = μ (A ∩ t)

Proof state:
case h.e'_3.h.e'_4
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
A : Set α
hA₀ : MeasurableSet A
hA : ∀ (g : G), (fun x => g • x) ⁻¹' A = A
g : G
x : α
⊢ A = (fun x => g • x) ⁻¹' A

Tactic:
rw [hA g]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
A : Set α
hA₀ : MeasurableSet A
hA : ∀ (g : G), (fun x => g • x) ⁻¹' A = A
this : ∫⁻ (x : α) in s, A.indicator 1 x ∂μ = ∫⁻ (x : α) in t, A.indicator 1 x ∂μ
⊢ μ (A ∩ s) = μ (A ∩ t)

Tactic:
simpa [Measure.restrict_apply hA₀, lintegral_indicator hA₀] using this

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
A : Set α
hA₀ : MeasurableSet A
hA : ∀ (g : G), (fun x => g • x) ⁻¹' A = A
⊢ ∫⁻ (x : α) in s, A.indicator 1 x ∂μ = ∫⁻ (x : α) in t, A.indicator 1 x ∂μ

Tactic:
refine hs.setLIntegral_eq ht (Set.indicator A fun _ => 1) fun g x ↦ ?_

Result:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
A : Set α
hA₀ : MeasurableSet A
hA : ∀ (g : G), (fun x => g • x) ⁻¹' A = A
g : G
x : α
⊢ A.indicator (fun x => 1) (g • x) = A.indicator (fun x => 1) x
-- Mathlib/Combinatorics/Quiver/Path.lean
theorem toList_injective (a : V) : ∀ b, Injective (toList : Path a b → List V)
  | _, nil, nil, _ => rfl
  | _, nil, @cons _ _ _ c _ p f, h => by cases h
  | _, @cons _ _ _ c _ p f, nil, h => by cases h
  | _, @cons _ _ _ c _ p f, @cons _ _ _ t _ C D, h => by
    simp only [toList, List.cons.injEq] at h
    obtain ⟨rfl, hAC⟩ := h
    simp [toList_injective _ _ hAC, eq_iff_true_of_subsingleton]

Proof state:
V : Type u
inst✝¹ : Quiver V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a c : V
p : Path a c
f : c ⟶ a
h : nil.toList = (p.cons f).toList
⊢ nil = p.cons f

Tactic:
cases h

Result:
no goals

Proof state:
V : Type u
inst✝¹ : Quiver V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a x✝ c : V
p : Path a c
f : c ⟶ x✝
t : V
C : Path a t
D : t ⟶ x✝
h : (p.cons f).toList = (C.cons D).toList
⊢ p.cons f = C.cons D

Tactic:
simp only [toList, List.cons.injEq] at h

Result:
V : Type u
inst✝¹ : Quiver V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a x✝ c : V
p : Path a c
f : c ⟶ x✝
t : V
C : Path a t
D : t ⟶ x✝
h : c = t ∧ p.toList = C.toList
⊢ p.cons f = C.cons D

Proof state:
case intro
V : Type u
inst✝¹ : Quiver V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a x✝ c : V
p : Path a c
f : c ⟶ x✝
C : Path a c
D : c ⟶ x✝
hAC : p.toList = C.toList
⊢ p.cons f = C.cons D

Tactic:
simp [toList_injective _ _ hAC, eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
V : Type u
inst✝¹ : Quiver V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a c : V
p : Path a c
f : c ⟶ a
h : (p.cons f).toList = nil.toList
⊢ p.cons f = nil

Tactic:
cases h

Result:
no goals

Proof state:
V : Type u
inst✝¹ : Quiver V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a x✝ c : V
p : Path a c
f : c ⟶ x✝
t : V
C : Path a t
D : t ⟶ x✝
h : c = t ∧ p.toList = C.toList
⊢ p.cons f = C.cons D

Tactic:
obtain ⟨rfl, hAC⟩ := h

Result:
case intro
V : Type u
inst✝¹ : Quiver V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a x✝ c : V
p : Path a c
f : c ⟶ x✝
C : Path a c
D : c ⟶ x✝
hAC : p.toList = C.toList
⊢ p.cons f = C.cons D
-- Mathlib/Control/Fold.lean
theorem toList_eq_self {xs : List α} : toList xs = xs

Proof state:
case cons
α : Type u
head✝ : α
tail✝ : List α
ih : FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) = head✝ :: tail✝

Tactic:
(conv_rhs => rw [← ih])

Result:
case cons
α : Type u
head✝ : α
tail✝ : List α
ih : FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) =
    head✝ :: FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝)

Proof state:
case cons
α : Type u
head✝ : α
tail✝ : List α
ih : FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) =
    head✝ :: FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
xs : List α
⊢ toList xs = xs

Tactic:
simp only [toList_spec, foldMap, traverse]

Result:
α : Type u
xs : List α
⊢ FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) xs) = xs

Proof state:
case cons
α : Type u
head✝ : α
tail✝ : List α
ih : FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) = head✝ :: tail✝

Tactic:
conv_rhs => rw [← ih]

Result:
case cons
α : Type u
head✝ : α
tail✝ : List α
ih : FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) =
    head✝ :: FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝)

Proof state:
case nil
α : Type u
⊢ FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) []) = []

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
xs : List α
⊢ FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) xs) = xs

Tactic:
induction xs with
| nil => rfl
| cons _ _ ih => (conv_rhs => rw [← ih]); rfl

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem of_leftInverse [DecidableEq ι] (i : ι) :
    Function.LeftInverse (lift <| Pi.mulSingle i (MonoidHom.id (M i))) of := fun x => by
  simp only [lift_of, Pi.mulSingle_eq_same, MonoidHom.id_apply]

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : DecidableEq ι
i : ι
x : M i
⊢ (lift (Pi.mulSingle i (MonoidHom.id (M i)))) (of x) = x

Tactic:
simp only [lift_of, Pi.mulSingle_eq_same, MonoidHom.id_apply]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Factorial.lean
theorem coprime_factorial_iff {m n : ℕ} (hm : m ≠ 1) :
    m.Coprime n ! ↔ n < m.minFac

Proof state:
m n : ℕ
hm : m ≠ 1
⊢ m.minFac ≤ n ↔ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n !

Tactic:
constructor

Result:
case mp
m n : ℕ
hm : m ≠ 1
⊢ m.minFac ≤ n → ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n !

case mpr
m n : ℕ
hm : m ≠ 1
⊢ (∃ p, Prime p ∧ p ∣ m ∧ p ∣ n !) → m.minFac ≤ n

Proof state:
case mpr.intro.intro.intro
m n : ℕ
hm : m ≠ 1
p : ℕ
hp : Prime p
hdvd : p ∣ m
hdvd' : p ∣ n !
⊢ m.minFac ≤ n

Tactic:
exact le_trans (minFac_le_of_dvd hp.two_le hdvd) (hp.dvd_factorial.mp hdvd')

Result:
no goals

Proof state:
case mp
m n : ℕ
hm : m ≠ 1
⊢ m.minFac ≤ n → ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n !

Tactic:
intro h

Result:
case mp
m n : ℕ
hm : m ≠ 1
h : m.minFac ≤ n
⊢ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n !

Proof state:
case mp
m n : ℕ
hm : m ≠ 1
h : m.minFac ≤ n
⊢ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n !

Tactic:
exact ⟨m.minFac, minFac_prime hm, minFac_dvd m, Nat.dvd_factorial (minFac_pos m) h⟩

Result:
no goals

Proof state:
case mpr
m n : ℕ
hm : m ≠ 1
⊢ (∃ p, Prime p ∧ p ∣ m ∧ p ∣ n !) → m.minFac ≤ n

Tactic:
rintro ⟨p, hp, hdvd, hdvd'⟩

Result:
case mpr.intro.intro.intro
m n : ℕ
hm : m ≠ 1
p : ℕ
hp : Prime p
hdvd : p ∣ m
hdvd' : p ∣ n !
⊢ m.minFac ≤ n

Proof state:
m n : ℕ
hm : m ≠ 1
⊢ m.Coprime n ! ↔ n < m.minFac

Tactic:
rw [← not_le, iff_not_comm, Nat.Prime.not_coprime_iff_dvd]

Result:
m n : ℕ
hm : m ≠ 1
⊢ m.minFac ≤ n ↔ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n !
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma rnDeriv_def' (κ η : Kernel α γ) :
    rnDeriv κ η = fun a x ↦ ENNReal.ofReal (rnDerivAux κ (κ + η) a x)
      / ENNReal.ofReal (1 - rnDerivAux κ (κ + η) a x)

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
⊢ κ.rnDeriv η = fun a x => ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)

Tactic:
ext

Result:
case h.h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
x✝¹ : α
x✝ : γ
⊢ κ.rnDeriv η x✝¹ x✝ = ENNReal.ofReal (κ.rnDerivAux (κ + η) x✝¹ x✝) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) x✝¹ x✝)

Proof state:
case h.h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
x✝¹ : α
x✝ : γ
⊢ κ.rnDeriv η x✝¹ x✝ = ENNReal.ofReal (κ.rnDerivAux (κ + η) x✝¹ x✝) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) x✝¹ x✝)

Tactic:
rw [rnDeriv_def]

Result:
no goals
-- Mathlib/Logic/Equiv/Option.lean
theorem optionSubtype_symm_apply_symm_apply [DecidableEq β] (x : β) (e : α ≃ { y : β // y ≠ x })
    (b : { y : β // y ≠ x }) : ((optionSubtype x).symm e : Option α ≃ β).symm b = e.symm b

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : { y // y ≠ x }
⊢ (↑((optionSubtype x).symm e)).symm ↑b = some (e.symm b)

Tactic:
simp only [optionSubtype, coe_fn_symm_mk, Subtype.coe_mk,
           Subtype.coe_eta, dite_eq_ite, ite_eq_right_iff]

Result:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : { y // y ≠ x }
⊢ ↑b = x → none = some (e.symm b)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : { y // y ≠ x }
⊢ ↑b = x → none = some (e.symm b)

Tactic:
exact fun h => False.elim (b.property h)

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem cons_get_inits_core :
    ∀ (a : α) (n : ℕ) (l : List α) (s : Stream' α),
      (a::get (initsCore l s) n) = get (initsCore (a::l) s) n

Proof state:
case zero
α : Type u
a : α
⊢ ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get 0 = (initsCore (a :: l) s).get 0

Tactic:
intros

Result:
case zero
α : Type u
a : α
l✝ : List α
s✝ : Stream' α
⊢ a :: (initsCore l✝ s✝).get 0 = (initsCore (a :: l✝) s✝).get 0

Proof state:
case succ
α : Type u
a : α
n' : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n' = (initsCore (a :: l) s).get n'
l : List α
s : Stream' α
⊢ a :: (initsCore l s).get (n' + 1) = (initsCore (a :: l) s).get (n' + 1)

Tactic:
rw [get_succ, inits_core_eq, tail_cons, ih, inits_core_eq (a::l) s]

Result:
case succ
α : Type u
a : α
n' : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n' = (initsCore (a :: l) s).get n'
l : List α
s : Stream' α
⊢ (initsCore (a :: (l ++ [s.head])) s.tail).get n' = ((a :: l) :: initsCore (a :: l ++ [s.head]) s.tail).get (n' + 1)

Proof state:
case succ
α : Type u
a : α
n' : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n' = (initsCore (a :: l) s).get n'
l : List α
s : Stream' α
⊢ (initsCore (a :: (l ++ [s.head])) s.tail).get n' = ((a :: l) :: initsCore (a :: l ++ [s.head]) s.tail).get (n' + 1)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
a : α
n : ℕ
⊢ ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n = (initsCore (a :: l) s).get n

Tactic:
induction' n with n' ih

Result:
case zero
α : Type u
a : α
⊢ ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get 0 = (initsCore (a :: l) s).get 0

case succ
α : Type u
a : α
n' : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n' = (initsCore (a :: l) s).get n'
⊢ ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get (n' + 1) = (initsCore (a :: l) s).get (n' + 1)

Proof state:
α : Type u
⊢ ∀ (a : α) (n : ℕ) (l : List α) (s : Stream' α), a :: (initsCore l s).get n = (initsCore (a :: l) s).get n

Tactic:
intro a n

Result:
α : Type u
a : α
n : ℕ
⊢ ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n = (initsCore (a :: l) s).get n

Proof state:
case succ
α : Type u
a : α
n' : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n' = (initsCore (a :: l) s).get n'
⊢ ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get (n' + 1) = (initsCore (a :: l) s).get (n' + 1)

Tactic:
intro l s

Result:
case succ
α : Type u
a : α
n' : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n' = (initsCore (a :: l) s).get n'
l : List α
s : Stream' α
⊢ a :: (initsCore l s).get (n' + 1) = (initsCore (a :: l) s).get (n' + 1)

Proof state:
case zero
α : Type u
a : α
l✝ : List α
s✝ : Stream' α
⊢ a :: (initsCore l✝ s✝).get 0 = (initsCore (a :: l✝) s✝).get 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
private lemma logC_step {m pw q e : ℕ} (hpw : 1 < pw) (hqe : logC.step m pw hpw = (q, e)) :
    pw ^ e * q ≤ m ∧ q < pw ∧ (m < pw ^ e * (q + 1)) ∧ (0 < m → 0 < q)

Proof state:
case case3
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : ¬m < pw
q' e' : ℕ
hqe' : logC.step m (pw * pw) ⋯ = (q', e')
hqpw : ¬q' < pw
ih :
  ∀ {q e : ℕ},
    logC.step m (pw * pw) ⋯ = (q, e) →
      (pw * pw) ^ e * q ≤ m ∧ q < pw * pw ∧ m < (pw * pw) ^ e * (q + 1) ∧ (0 < m → 0 < q)
q e : ℕ
hqe : (q' / pw, 2 * e' + 1) = (q, e)
⊢ pw ^ e * q ≤ m ∧ q < pw ∧ m < pw ^ e * (q + 1) ∧ (0 < m → 0 < q)

Tactic:
cases hqe

Result:
case case3.refl
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : ¬m < pw
q' e' : ℕ
hqe' : logC.step m (pw * pw) ⋯ = (q', e')
hqpw : ¬q' < pw
ih :
  ∀ {q e : ℕ},
    logC.step m (pw * pw) ⋯ = (q, e) →
      (pw * pw) ^ e * q ≤ m ∧ q < pw * pw ∧ m < (pw * pw) ^ e * (q + 1) ∧ (0 < m → 0 < q)
⊢ pw ^ (2 * e' + 1) * (q' / pw) ≤ m ∧ q' / pw < pw ∧ m < pw ^ (2 * e' + 1) * (q' / pw + 1) ∧ (0 < m → 0 < q' / pw)

Proof state:
case case2
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : ¬m < pw
q' e' : ℕ
hqe' : logC.step m (pw * pw) ⋯ = (q', e')
hqpw : q' < pw
ih :
  ∀ {q e : ℕ},
    logC.step m (pw * pw) ⋯ = (q, e) →
      (pw * pw) ^ e * q ≤ m ∧ q < pw * pw ∧ m < (pw * pw) ^ e * (q + 1) ∧ (0 < m → 0 < q)
q e : ℕ
hqe : logC.step m pw hpw = (q, e)
⊢ pw ^ e * q ≤ m ∧ q < pw ∧ m < pw ^ e * (q + 1) ∧ (0 < m → 0 < q)

Tactic:
simp only [logC.step, dif_neg hmpw, hqe', if_pos hqpw] at hqe

Result:
case case2
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : ¬m < pw
q' e' : ℕ
hqe' : logC.step m (pw * pw) ⋯ = (q', e')
hqpw : q' < pw
ih :
  ∀ {q e : ℕ},
    logC.step m (pw * pw) ⋯ = (q, e) →
      (pw * pw) ^ e * q ≤ m ∧ q < pw * pw ∧ m < (pw * pw) ^ e * (q + 1) ∧ (0 < m → 0 < q)
q e : ℕ
hqe : (q', 2 * e') = (q, e)
⊢ pw ^ e * q ≤ m ∧ q < pw ∧ m < pw ^ e * (q + 1) ∧ (0 < m → 0 < q)

Proof state:
case case1
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : m < pw
q e : ℕ
hqe : (m, 0) = (q, e)
⊢ pw ^ e * q ≤ m ∧ q < pw ∧ m < pw ^ e * (q + 1) ∧ (0 < m → 0 < q)

Tactic:
cases hqe

Result:
case case1.refl
m pw✝ pw : ℕ
hpw : 1 < pw
hmpw : m < pw
⊢ pw ^ 0 * m ≤ m ∧ m < pw ∧ m < pw ^ 0 * (m + 1) ∧ (0 < m → 0 < m)
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
/-- If `P : MorphismPropety C` is such that any object in `C` maps to the
target of some morphism in `P`, then `P.pushouts` contains the isomorphisms. -/
lemma isomorphisms_le_pushouts
    (h : ∀ (X : C), ∃ (A B : C) (p : A ⟶ B) (_ : P p) (_ : B ⟶ X), IsIso p) :
    isomorphisms C ≤ P.pushouts

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
X Y : C
f : X ⟶ Y
x✝ : IsIso f
A B : C
p : A ⟶ B
hp : P p
g : B ⟶ X
h✝ : IsIso p
⊢ (p ≫ g) ≫ (Iso.refl X).hom = (Iso.refl A).hom ≫ p ≫ g

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
X Y : C
f : X ⟶ Y
x✝ : IsIso f
A B : C
p : A ⟶ B
hp : P p
g : B ⟶ X
h✝ : IsIso p
⊢ P.pushouts f

Tactic:
exact ⟨A, B, p, p ≫ g, g ≫ f, hp, (IsPushout.of_id_snd (f := p ≫ g)).of_iso
  (Iso.refl _) (Iso.refl _) (asIso p) (asIso f) (by simp) (by simp) (by simp) (by simp)⟩

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
X Y : C
f : X ⟶ Y
x✝ : IsIso f
A B : C
p : A ⟶ B
hp : P p
g : B ⟶ X
h✝ : IsIso p
⊢ 𝟙 X ≫ (asIso f).hom = (Iso.refl X).hom ≫ f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
⊢ isomorphisms C ≤ P.pushouts

Tactic:
intro X Y f (_ : IsIso f)

Result:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
X Y : C
f : X ⟶ Y
x✝ : IsIso f
⊢ P.pushouts f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
X Y : C
f : X ⟶ Y
x✝ : IsIso f
A B : C
p : A ⟶ B
hp : P p
g : B ⟶ X
h✝ : IsIso p
⊢ 𝟙 A ≫ (asIso p).hom = (Iso.refl A).hom ≫ p

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
X Y : C
f : X ⟶ Y
x✝ : IsIso f
⊢ P.pushouts f

Tactic:
obtain ⟨A, B, p, hp, g, _⟩ := h X

Result:
case intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
X Y : C
f : X ⟶ Y
x✝ : IsIso f
A B : C
p : A ⟶ B
hp : P p
g : B ⟶ X
h✝ : IsIso p
⊢ P.pushouts f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
X Y : C
f : X ⟶ Y
x✝ : IsIso f
A B : C
p : A ⟶ B
hp : P p
g : B ⟶ X
h✝ : IsIso p
⊢ (p ≫ g) ≫ (asIso f).hom = (asIso p).hom ≫ g ≫ f

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma div_lt_div_iff₀ (hb : 0 < b) (hd : 0 < d) : a / b < c / d ↔ a * d < c * b

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulStrictMono G₀
a b c d : G₀
hb : 0 < b
hd : 0 < d
this : MulPosStrictMono G₀
⊢ a / b < c / d ↔ a * d < c * b

Tactic:
rw [div_lt_iff₀ hb, ← mul_div_right_comm, lt_div_iff₀ hd]

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulStrictMono G₀
a b c d : G₀
hb : 0 < b
hd : 0 < d
⊢ a / b < c / d ↔ a * d < c * b

Tactic:
have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›

Result:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulStrictMono G₀
a b c d : G₀
hb : 0 < b
hd : 0 < d
this : MulPosStrictMono G₀
⊢ a / b < c / d ↔ a * d < c * b
-- Mathlib/Data/Multiset/Bind.lean
theorem product_singleton : ({a} : Multiset α) ×ˢ ({b} : Multiset β) = {(a, b)}

Proof state:
α : Type u_1
β : Type v
a : α
b : β
⊢ {a} ×ˢ {b} = {(a, b)}

Tactic:
simp only [SProd.sprod, product, bind_singleton, map_singleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/GetElem.lean
theorem getElem_congr_coll [GetElem coll idx elem valid] {c d : coll} {i : idx} {w : valid c i}
    (h : c = d) : c[i] = d[i]'(h ▸ w)

Proof state:
case refl
coll : Type u_1
idx : Type u_2
elem : Type u_3
valid : coll → idx → Prop
inst✝ : GetElem coll idx elem valid
c : coll
i : idx
w : valid c i
⊢ getElem c i w = getElem c i ⋯

Tactic:
rfl

Result:
no goals

Proof state:
coll : Type u_1
idx : Type u_2
elem : Type u_3
valid : coll → idx → Prop
inst✝ : GetElem coll idx elem valid
c d : coll
i : idx
w : valid c i
h : c = d
⊢ getElem c i w = getElem d i ⋯

Tactic:
cases h

Result:
case refl
coll : Type u_1
idx : Type u_2
elem : Type u_3
valid : coll → idx → Prop
inst✝ : GetElem coll idx elem valid
c : coll
i : idx
w : valid c i
⊢ getElem c i w = getElem c i ⋯