harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Minimal.lean
theorem Minimal.or (h : Minimal (fun x ↦ P x ∨ Q x) x) : Minimal P x ∨ Minimal Q x

Proof state:
α : Type u_1
P Q : α → Prop
x : α
inst✝ : LE α
h : Minimal (fun x => P x ∨ Q x) x
⊢ Minimal P x ∨ Minimal Q x

Tactic:
obtain ⟨h | h, hmin⟩ := h

Result:
case intro.inl
α : Type u_1
P Q : α → Prop
x : α
inst✝ : LE α
hmin : ∀ ⦃y : α⦄, (fun x => P x ∨ Q x) y → y ≤ x → x ≤ y
h : P x
⊢ Minimal P x ∨ Minimal Q x

case intro.inr
α : Type u_1
P Q : α → Prop
x : α
inst✝ : LE α
hmin : ∀ ⦃y : α⦄, (fun x => P x ∨ Q x) y → y ≤ x → x ≤ y
h : Q x
⊢ Minimal P x ∨ Minimal Q x

Proof state:
case intro.inr
α : Type u_1
P Q : α → Prop
x : α
inst✝ : LE α
hmin : ∀ ⦃y : α⦄, (fun x => P x ∨ Q x) y → y ≤ x → x ≤ y
h : Q x
⊢ Minimal P x ∨ Minimal Q x

Tactic:
exact .inr ⟨h, fun y hy hyx ↦ hmin (Or.inr hy) hyx⟩

Result:
no goals

Proof state:
case intro.inl
α : Type u_1
P Q : α → Prop
x : α
inst✝ : LE α
hmin : ∀ ⦃y : α⦄, (fun x => P x ∨ Q x) y → y ≤ x → x ≤ y
h : P x
⊢ Minimal P x ∨ Minimal Q x

Tactic:
exact .inl ⟨h, fun y hy hyx ↦ hmin (Or.inl hy) hyx⟩

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem lookupAll_eq_dlookup (a : α) {l : List (Sigma β)} (h : l.NodupKeys) :
    lookupAll a l = (dlookup a l).toList

Proof state:
case cons.nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
b : β a
h1 : [b].length ≤ 1
⊢ [b] = [b].head?.toList

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ (lookupAll a l).length ≤ 1 → lookupAll a l = (lookupAll a l).head?.toList

Tactic:
rcases lookupAll a l with (_ | ⟨b, _ | ⟨c, l⟩⟩) <;> intro h1 <;> try rfl

Result:
case cons.cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l✝ : List (Sigma β)
h : l✝.NodupKeys
b c : β a
l : List (β a)
h1 : (b :: c :: l).length ≤ 1
⊢ b :: c :: l = (b :: c :: l).head?.toList

Proof state:
case cons.cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l✝ : List (Sigma β)
h : l✝.NodupKeys
b c : β a
l : List (β a)
h1 : (b :: c :: l).length ≤ 1
⊢ b :: c :: l = (b :: c :: l).head?.toList

Tactic:
exact absurd h1 (by simp)

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ lookupAll a l = (dlookup a l).toList

Tactic:
rw [← head?_lookupAll]

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ lookupAll a l = (lookupAll a l).head?.toList

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
h1 : (lookupAll a l).length ≤ 1
⊢ lookupAll a l = (lookupAll a l).head?.toList

Tactic:
revert h1

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ (lookupAll a l).length ≤ 1 → lookupAll a l = (lookupAll a l).head?.toList

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l✝ : List (Sigma β)
h : l✝.NodupKeys
b c : β a
l : List (β a)
h1 : (b :: c :: l).length ≤ 1
⊢ ¬(b :: c :: l).length ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ lookupAll a l = (lookupAll a l).head?.toList

Tactic:
have h1 := lookupAll_length_le_one a h

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
h1 : (lookupAll a l).length ≤ 1
⊢ lookupAll a l = (lookupAll a l).head?.toList
-- Mathlib/SetTheory/Ordinal/Topology.lean
theorem isClosed_iff_iSup :
    IsClosed s ↔
      ∀ {ι : Type u}, Nonempty ι → ∀ f : ι → Ordinal, (∀ i, f i ∈ s) → ⨆ i, f i ∈ s

Proof state:
case mpr
s : Set Ordinal.{u}
h : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s
x : Ordinal.{u}
hx : x ∈ closure s
⊢ x ∈ s

Tactic:
rcases mem_closure_iff_iSup.1 hx with ⟨ι, hι, f, hf, rfl⟩

Result:
case mpr.intro.intro.intro.intro
s : Set Ordinal.{u}
h : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
hx : ⨆ i, f i ∈ closure s
⊢ ⨆ i, f i ∈ s

Proof state:
s : Set Ordinal.{u}
⊢ IsClosed s ↔ ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s

Tactic:
use fun hs ι hι f hf => (mem_iff_iSup_of_isClosed hs).2 ⟨ι, hι, f, hf, rfl⟩

Result:
case mpr
s : Set Ordinal.{u}
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s) → IsClosed s

Proof state:
case mpr
s : Set Ordinal.{u}
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s) → closure s ⊆ s

Tactic:
intro h x hx

Result:
case mpr
s : Set Ordinal.{u}
h : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s
x : Ordinal.{u}
hx : x ∈ closure s
⊢ x ∈ s

Proof state:
case mpr
s : Set Ordinal.{u}
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s) → IsClosed s

Tactic:
rw [← closure_subset_iff_isClosed]

Result:
case mpr
s : Set Ordinal.{u}
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s) → closure s ⊆ s

Proof state:
case mpr.intro.intro.intro.intro
s : Set Ordinal.{u}
h : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
hx : ⨆ i, f i ∈ closure s
⊢ ⨆ i, f i ∈ s

Tactic:
exact h hι f hf

Result:
no goals
-- Mathlib/NumberTheory/Bernoulli.lean
theorem bernoulli'_zero : bernoulli' 0 = 1

Proof state:
⊢ bernoulli' 0 = 1

Tactic:
rw [bernoulli'_def]

Result:
⊢ 1 - ∑ k ∈ range 0, ↑(Nat.choose 0 k) / (↑0 - ↑k + 1) * bernoulli' k = 1

Proof state:
⊢ 1 - ∑ k ∈ range 0, ↑(Nat.choose 0 k) / (↑0 - ↑k + 1) * bernoulli' k = 1

Tactic:
norm_num

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_le_card (o) : cof o ≤ card o

Proof state:
o : Ordinal.{u_1}
⊢ sInf {a | ∃ ι f, lsub f = o ∧ #ι = a} ≤ o.card

Tactic:
exact csInf_le' card_mem_cof

Result:
no goals

Proof state:
o : Ordinal.{u_1}
⊢ o.cof ≤ o.card

Tactic:
rw [cof_eq_sInf_lsub]

Result:
o : Ordinal.{u_1}
⊢ sInf {a | ∃ ι f, lsub f = o ∧ #ι = a} ≤ o.card
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContDiffAt.const_smul {f : E → F} {x : E} (c : R) (hf : ContDiffAt 𝕜 n f x) :
    ContDiffAt 𝕜 n (fun y => c • f y) x

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : WithTop ℕ∞
R : Type u_3
inst✝³ : Semiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
f : E → F
x : E
c : R
hf : ContDiffAt 𝕜 n f x
⊢ ContDiffAt 𝕜 n (fun y => c • f y) x

Tactic:
rw [← contDiffWithinAt_univ] at *

Result:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : WithTop ℕ∞
R : Type u_3
inst✝³ : Semiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
f : E → F
x : E
c : R
hf : ContDiffWithinAt 𝕜 n f univ x
⊢ ContDiffWithinAt 𝕜 n (fun y => c • f y) univ x

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : WithTop ℕ∞
R : Type u_3
inst✝³ : Semiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
f : E → F
x : E
c : R
hf : ContDiffWithinAt 𝕜 n f univ x
⊢ ContDiffWithinAt 𝕜 n (fun y => c • f y) univ x

Tactic:
exact hf.const_smul c

Result:
no goals
-- Mathlib/Algebra/Colimit/Module.lean
theorem exists_of₂ [Nonempty ι] [IsDirected ι (· ≤ ·)] (z w : DirectLimit G f) :
    ∃ i x y, of R ι G f i x = z ∧ of R ι G f i y = w :=
  have ⟨i, x, hx⟩ := exists_of z
  have ⟨j, y, hy⟩ := exists_of w
  have ⟨k, hik, hjk⟩ := exists_ge_ge i j
  ⟨k, f i k hik x, f j k hjk y, by rw [of_f, hx], by rw [of_f, hy]⟩

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
z w : DirectLimit G f
i : ι
x : G i
hx : (of R ι G f i) x = z
j : ι
y : G j
hy : (of R ι G f j) y = w
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ (of R ι G f k) ((f i k hik) x) = z

Tactic:
rw [of_f, hx]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
z w : DirectLimit G f
i : ι
x : G i
hx : (of R ι G f i) x = z
j : ι
y : G j
hy : (of R ι G f j) y = w
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ (of R ι G f k) ((f j k hjk) y) = w

Tactic:
rw [of_f, hy]

Result:
no goals
-- Mathlib/CategoryTheory/Filtered/Small.lean
theorem small_fullSubcategory_filteredClosure :
    Small.{max v w} (FullSubcategory (FilteredClosure f))

Proof state:
case mk.coeq.intro.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j j'✝ : C
hj₂ : FilteredClosure f j'✝
ih' :
  ∃ a,
    CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f a =
      { obj := j'✝, property := hj₂ }.obj
n : ℕ
x : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
g g' : CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩ ⟶ j'✝
⊢ ∃ a,
    CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f a =
      { obj := coeq g g', property := ⋯ }.obj

Tactic:
rcases ih' with ⟨⟨m, y⟩, rfl⟩

Result:
case mk.coeq.intro.mk.intro.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
g g' :
  CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩ ⟶
    CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩
⊢ ∃ a,
    CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f a =
      { obj := coeq g g', property := ⋯ }.obj
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem le_of_mul_le_mul_left (a b c : Associates M) (ha : a ≠ 0) : a * b ≤ a * c → b ≤ c
  | ⟨d, hd⟩ => ⟨d, mul_left_cancel₀ ha <| by rwa [← mul_assoc]⟩

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
a b c : Associates M
ha : a ≠ 0
d : Associates M
hd : a * c = a * b * d
⊢ a * c = a * (b * d)

Tactic:
rwa [← mul_assoc]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean
theorem snd_exp (x : tsze R M) : snd (exp 𝕜 x) = exp 𝕜 x.fst • x.snd

Proof state:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁷ : Field 𝕜
inst✝¹⁶ : CharZero 𝕜
inst✝¹⁵ : CommRing R
inst✝¹⁴ : AddCommGroup M
inst✝¹³ : Algebra 𝕜 R
inst✝¹² : Module 𝕜 M
inst✝¹¹ : Module R M
inst✝¹⁰ : Module Rᵐᵒᵖ M
inst✝⁹ : IsCentralScalar R M
inst✝⁸ : IsScalarTower 𝕜 R M
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace M
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : IsTopologicalAddGroup M
inst✝³ : ContinuousSMul R M
inst✝² : ContinuousSMul Rᵐᵒᵖ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : tsze R M
⊢ (exp 𝕜 x).snd = exp 𝕜 x.fst • x.snd

Tactic:
rw [exp_def, snd_add, snd_inl, snd_inr, zero_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_map {f : α → β} : ∀ {l : List α}, b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b
  | [] => by simp
  | _ :: l => by simp [mem_map (l := l), eq_comm (a := b)]

Proof state:
α : Type u_1
β : Type u_2
b : β
f : α → β
head✝ : α
l : List α
⊢ b ∈ map f (head✝ :: l) ↔ ∃ a, a ∈ head✝ :: l ∧ f a = b

Tactic:
simp [mem_map (l := l), eq_comm (a := b)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
b : β
f : α → β
⊢ b ∈ map f [] ↔ ∃ a, a ∈ [] ∧ f a = b

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem neg_one (p : ℕ) [Nontrivial R] [h : CharP R p] (hp : p ≠ 2) :
    IsPrimitiveRoot (-1 : R) 2

Proof state:
case h.e'_4
R : Type u_4
inst✝¹ : CommRing R
p : ℕ
inst✝ : Nontrivial R
h : CharP R p
hp : p ≠ 2
⊢ 2 = orderOf (-1)

Tactic:
rw [orderOf_neg_one, if_neg <| by rwa [ringChar.eq_iff.mpr h]]

Result:
no goals

Proof state:
R : Type u_4
inst✝¹ : CommRing R
p : ℕ
inst✝ : Nontrivial R
h : CharP R p
hp : p ≠ 2
⊢ IsPrimitiveRoot (-1) 2

Tactic:
convert IsPrimitiveRoot.orderOf (-1 : R)

Result:
case h.e'_4
R : Type u_4
inst✝¹ : CommRing R
p : ℕ
inst✝ : Nontrivial R
h : CharP R p
hp : p ≠ 2
⊢ 2 = orderOf (-1)

Proof state:
R : Type u_4
inst✝¹ : CommRing R
p : ℕ
inst✝ : Nontrivial R
h : CharP R p
hp : p ≠ 2
⊢ ¬ringChar R = 2

Tactic:
rwa [ringChar.eq_iff.mpr h]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem zero_lt_lift_iff {a : Cardinal.{u}} :
    (0 : Cardinal) < lift.{v} a ↔ 0 < a

Proof state:
a : Cardinal.{u}
⊢ 0 < lift.{v, u} a ↔ 0 < a

Tactic:
simpa using nat_lt_lift_iff (n := 0)

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Isometry.lean
theorem nndist_map (x y : P) : nndist (f x) (f y) = nndist x y

Proof state:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃⁱ[𝕜] P₂
x y : P
⊢ nndist (f x) (f y) = nndist x y

Tactic:
simp [nndist_dist]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem fst {α β} [Primcodable α] [Primcodable β] : Primrec (@Prod.fst α β) :=
  ((casesOn' zero
            ((casesOn' zero (Nat.Primrec.succ.comp left)).comp
              (pair right ((@Primcodable.prim β).comp left)))).comp
        (pair right ((@Primcodable.prim α).comp left))).of_eq
    fun n => by
    simp only [Nat.unpaired, Nat.unpair_pair, decode_prod_val]
    cases @decode α _ n.unpair.1 <;> simp
    cases @decode β _ n.unpair.2 <;> simp

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih => Nat.rec 0 (fun n n_ih => n_1.succ) (encode (decode (Nat.unpair n).2)))
      (encode (decode (Nat.unpair n).1)) =
    encode
      (Option.map Prod.fst ((decode (Nat.unpair n).1).bind fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).2)))

Tactic:
cases @decode α _ n.unpair.1 <;> simp

Result:
case some
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n n_ih => encode val✝ + 1) (encode (decode (Nat.unpair n).2)) =
    encode (Option.map (Function.const β val✝) (decode (Nat.unpair n).2))

Proof state:
case some
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n n_ih => encode val✝ + 1) (encode (decode (Nat.unpair n).2)) =
    encode (Option.map (Function.const β val✝) (decode (Nat.unpair n).2))

Tactic:
cases @decode β _ n.unpair.2 <;> simp

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.unpaired
      (fun z n =>
        Nat.casesOn n 0 fun y =>
          Nat.unpaired (fun z n => Nat.casesOn n 0 fun y => (Nat.unpair (Nat.pair z y)).1.succ)
            (Nat.pair (Nat.unpair (Nat.pair z y)).2 (encode (decode (Nat.unpair (Nat.pair z y)).1))))
      (Nat.pair (Nat.unpair n).2 (encode (decode (Nat.unpair n).1))) =
    encode (Option.map Prod.fst (decode n))

Tactic:
simp only [Nat.unpaired, Nat.unpair_pair, decode_prod_val]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih => Nat.rec 0 (fun n n_ih => n_1.succ) (encode (decode (Nat.unpair n).2)))
      (encode (decode (Nat.unpair n).1)) =
    encode
      (Option.map Prod.fst ((decode (Nat.unpair n).1).bind fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).2)))
-- Mathlib/Data/Ordmap/Ordset.lean
theorem eraseMin.valid : ∀ {t}, @Valid α _ t → Valid (eraseMin t)
  | nil, _ => valid_nil
  | node _ l x r, h => by rw [h.2.eq_node']; exact h.eraseMin_aux.1.valid

Proof state:
α : Type u_1
inst✝ : Preorder α
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node size✝ l x r).Valid
⊢ (node size✝ l x r).eraseMin.Valid

Tactic:
rw [h.2.eq_node']

Result:
α : Type u_1
inst✝ : Preorder α
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node size✝ l x r).Valid
⊢ (l.node' x r).eraseMin.Valid

Proof state:
α : Type u_1
inst✝ : Preorder α
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node size✝ l x r).Valid
⊢ (l.node' x r).eraseMin.Valid

Tactic:
exact h.eraseMin_aux.1.valid

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tsum_pos {g : α → ℝ≥0} (hg : Summable g) (i : α) (hi : 0 < g i) : 0 < ∑' b, g b

Proof state:
α : Type u_1
g : α → ℝ≥0
hg : Summable g
i : α
hi : 0 < g i
⊢ 0 < ∑' (b : α), g b

Tactic:
rw [← tsum_zero]

Result:
α : Type u_1
g : α → ℝ≥0
hg : Summable g
i : α
hi : 0 < g i
⊢ ∑' (x : ?m.251635), 0 < ∑' (b : α), g b

α : Type u_1
g : α → ℝ≥0
hg : Summable g
i : α
hi : 0 < g i
⊢ Type ?u.251632

Proof state:
α : Type u_1
g : α → ℝ≥0
hg : Summable g
i : α
hi : 0 < g i
⊢ ∑' (x : ?m.251635), 0 < ∑' (b : α), g b

α : Type u_1
g : α → ℝ≥0
hg : Summable g
i : α
hi : 0 < g i
⊢ Type ?u.251632

Tactic:
exact tsum_lt_tsum (fun a => zero_le _) hi hg

Result:
no goals
-- Mathlib/RingTheory/HopkinsLevitzki.lean
theorem IsNoetherianRing.isArtinianRing_of_krullDimLE_zero {R} [CommRing R]
    [IsNoetherianRing R] [Ring.KrullDimLE 0 R] : IsArtinianRing R :=
  have eq := Ring.jacobson_eq_nilradical_of_krullDimLE_zero R
  let Spec := {I : Ideal R | I.IsPrime}
  have : Finite Spec :=
    (minimalPrimes.finite_of_isNoetherianRing R).subset Ideal.mem_minimalPrimes_of_krullDimLE_zero
  have (I : Spec) : I.1.IsPrime := I.2
  have (I : Spec) : IsSemisimpleRing (R ⧸ I.1) := let _ := Ideal.Quotient.field I.1; inferInstance
  have : IsSemisimpleRing (R ⧸ Ring.jacobson R)

Proof state:
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : Ring.KrullDimLE 0 R
eq : Ring.jacobson R = nilradical R
Spec : Set (Ideal R) := {I | I.IsPrime}
this✝¹ : Finite ↑Spec
this✝ : ∀ (I : ↑Spec), (↑I).IsPrime
this : ∀ (I : ↑Spec), IsSemisimpleRing (R ⧸ ↑I)
⊢ IsSemisimpleRing (R ⧸ Ring.jacobson R)

Tactic:
rw [eq, nilradical_eq_sInf, sInf_eq_iInf']

Result:
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : Ring.KrullDimLE 0 R
eq : Ring.jacobson R = nilradical R
Spec : Set (Ideal R) := {I | I.IsPrime}
this✝¹ : Finite ↑Spec
this✝ : ∀ (I : ↑Spec), (↑I).IsPrime
this : ∀ (I : ↑Spec), IsSemisimpleRing (R ⧸ ↑I)
⊢ IsSemisimpleRing (R ⧸ ⨅ a, ↑a)

Proof state:
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : Ring.KrullDimLE 0 R
eq : Ring.jacobson R = nilradical R
Spec : Set (Ideal R) := {I | I.IsPrime}
this✝¹ : Finite ↑Spec
this✝ : ∀ (I : ↑Spec), (↑I).IsPrime
this : ∀ (I : ↑Spec), IsSemisimpleRing (R ⧸ ↑I)
⊢ IsSemisimpleRing (R ⧸ ⨅ a, ↑a)

Tactic:
exact (Ideal.quotientInfRingEquivPiQuotient _ fun I J ne ↦
  Ideal.isCoprime_of_isMaximal <| Subtype.coe_ne_coe.mpr ne).symm.isSemisimpleRing

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Boundary.lean
lemma not_boundaryLE_prev' [e.IsRelIff] {i j : ι} (hj : ¬ e.BoundaryLE j) (hk : c.prev j = i) :
    ¬ e.BoundaryLE i

Proof state:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hj : ¬e.BoundaryLE j
hij : ¬c.Rel (c.prev j) j
⊢ ¬e.BoundaryLE (c.prev j)

Tactic:
simpa only [c.prev_eq_self j hij] using hj

Result:
no goals

Proof state:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hj : ¬e.BoundaryLE j
hk : c.prev j = i
hij : ¬c.Rel i j
⊢ ¬e.BoundaryLE i

Tactic:
subst hk

Result:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hj : ¬e.BoundaryLE j
hij : ¬c.Rel (c.prev j) j
⊢ ¬e.BoundaryLE (c.prev j)

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hj : ¬e.BoundaryLE j
hk : c.prev j = i
⊢ ¬e.BoundaryLE i

Tactic:
by_cases hij : c.Rel i j

Result:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hj : ¬e.BoundaryLE j
hk : c.prev j = i
hij : c.Rel i j
⊢ ¬e.BoundaryLE i

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hj : ¬e.BoundaryLE j
hk : c.prev j = i
hij : ¬c.Rel i j
⊢ ¬e.BoundaryLE i

Proof state:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hj : ¬e.BoundaryLE j
hk : c.prev j = i
hij : c.Rel i j
⊢ ¬e.BoundaryLE i

Tactic:
exact e.not_boundaryLE_prev hij

Result:
no goals
-- Mathlib/ModelTheory/Order.lean
theorem denselyOrdered_of_dlo [M ⊨ L.dlo] : DenselyOrdered M :=
  realize_denselyOrdered_iff.1 (L.dlo.realize_sentence_of_mem (by
    simp only [dlo, Set.union_insert, Set.union_singleton, Set.mem_insert_iff, true_or, or_true]))

Proof state:
L : Language
M : Type w'
inst✝⁴ : L.IsOrdered
inst✝³ : L.Structure M
inst✝² : Preorder M
inst✝¹ : L.OrderedStructure M
inst✝ : M ⊨ L.dlo
⊢ L.denselyOrderedSentence ∈ L.dlo

Tactic:
simp only [dlo, Set.union_insert, Set.union_singleton, Set.mem_insert_iff, true_or, or_true]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace [CompactSpace α] :
    TendstoLocallyUniformly F f p ↔ TendstoUniformly F f p

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
⊢ TendstoLocallyUniformly F f p ↔ TendstoUniformly F f p

Tactic:
refine ⟨fun h V hV => ?_, TendstoUniformly.tendstoLocallyUniformly⟩

Result:
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V