harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth_succ (x : BitVec w) :
    setWidth (i+1) x = cons (getLsbD x i) (setWidth i x)

Proof state:
w i : Nat
x : BitVec w
j : Nat
h : j < i + 1
j_eq : ¬j = i
⊢ x.getLsbD j = if j = i then x.getLsbD i else decide (j < i) && x.getLsbD j

Tactic:
have j_lt : j < i := Nat.lt_of_le_of_ne (Nat.le_of_succ_le_succ h) j_eq

Result:
w i : Nat
x : BitVec w
j : Nat
h : j < i + 1
j_eq : ¬j = i
j_lt : j < i
⊢ x.getLsbD j = if j = i then x.getLsbD i else decide (j < i) && x.getLsbD j

Proof state:
w i : Nat
x : BitVec w
⊢ setWidth (i + 1) x = cons (x.getLsbD i) (setWidth i x)

Tactic:
ext j h

Result:
case pred
w i : Nat
x : BitVec w
j : Nat
h : j < i + 1
⊢ (setWidth (i + 1) x).getLsbD j = (cons (x.getLsbD i) (setWidth i x)).getLsbD j

Proof state:
w i : Nat
x : BitVec w
j : Nat
h : j < i + 1
j_eq : ¬j = i
j_lt : j < i
⊢ x.getLsbD j = if j = i then x.getLsbD i else decide (j < i) && x.getLsbD j

Tactic:
simp [j_eq, j_lt]

Result:
no goals

Proof state:
case pred
w i : Nat
x : BitVec w
j : Nat
h : j < i + 1
⊢ (setWidth (i + 1) x).getLsbD j = (cons (x.getLsbD i) (setWidth i x)).getLsbD j

Tactic:
simp only [getLsbD_setWidth, getLsbD_cons, h, decide_true, Bool.true_and]

Result:
case pred
w i : Nat
x : BitVec w
j : Nat
h : j < i + 1
⊢ x.getLsbD j = if j = i then x.getLsbD i else decide (j < i) && x.getLsbD j

Proof state:
w i : Nat
x : BitVec w
j : Nat
h : j < i + 1
j_eq : j = i
⊢ x.getLsbD j = if j = i then x.getLsbD i else decide (j < i) && x.getLsbD j

Tactic:
simp [j_eq]

Result:
no goals

Proof state:
case pred
w i : Nat
x : BitVec w
j : Nat
h : j < i + 1
⊢ x.getLsbD j = if j = i then x.getLsbD i else decide (j < i) && x.getLsbD j

Tactic:
if j_eq : j = i then
  simp [j_eq]
else
  have j_lt : j < i := Nat.lt_of_le_of_ne (Nat.le_of_succ_le_succ h) j_eq
  simp [j_eq, j_lt]

Result:
no goals
-- Mathlib/FieldTheory/Perfect.lean
lemma polynomial_expand_eq (f : R[X]) :
    expand R p f = (f.map (frobeniusEquiv R p).symm) ^ p

Proof state:
R : Type u_1
p : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
f : R[X]
⊢ (expand R p) f = map (↑(frobeniusEquiv R p).symm) f ^ p

Tactic:
rw [← (f.map (S := R) (frobeniusEquiv R p).symm).expand_char p, map_expand, map_map,
  frobenius_comp_frobeniusEquiv_symm, map_id]

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
theorem refl_trans (e : α ≃ β) : (Equiv.refl α).trans e = e

Proof state:
α : Sort u
β : Sort v
e : α ≃ β
⊢ (Equiv.refl α).trans e = e

Tactic:
cases e

Result:
case mk
α : Sort u
β : Sort v
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : RightInverse invFun✝ toFun✝
⊢ (Equiv.refl α).trans { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }

Proof state:
case mk
α : Sort u
β : Sort v
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : RightInverse invFun✝ toFun✝
⊢ (Equiv.refl α).trans { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mem_mapFinIdx {b : β} {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
    b ∈ l.mapFinIdx f ↔ ∃ (i : Nat) (h : i < l.length), f i l[i] h = b

Proof state:
case mp
β : Type u_1
α : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ b ∈ l.mapFinIdx f → ∃ i h, f i l[i] h = b

Tactic:
intro h

Result:
case mp
β : Type u_1
α : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < l.length → β
h : b ∈ l.mapFinIdx f
⊢ ∃ i h, f i l[i] h = b

Proof state:
β : Type u_1
α : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
i : Nat
h : i < l.length
⊢ i < (l.mapFinIdx f).length

Tactic:
simpa using h

Result:
no goals

Proof state:
case mpr.intro.intro
β : Type u_1
α : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
i : Nat
h : i < l.length
⊢ f i l[i] h ∈ l.mapFinIdx f

Tactic:
rw [mem_iff_getElem]

Result:
case mpr.intro.intro
β : Type u_1
α : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
i : Nat
h : i < l.length
⊢ ∃ i_1 h_1, (l.mapFinIdx f)[i_1] = f i l[i] h

Proof state:
β : Type u_1
α : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
i : Nat
h : i < l.length
⊢ (l.mapFinIdx f)[i] = f i l[i] h

Tactic:
simp

Result:
no goals

Proof state:
case mp
β : Type u_1
α : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < l.length → β
h : b ∈ l.mapFinIdx f
⊢ ∃ i h, f i l[i] h = b

Tactic:
exact exists_of_mem_mapFinIdx h

Result:
no goals

Proof state:
case mpr.intro.intro
β : Type u_1
α : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
i : Nat
h : i < l.length
⊢ ∃ i_1 h_1, (l.mapFinIdx f)[i_1] = f i l[i] h

Tactic:
exact ⟨i, by simpa using h, by simp⟩

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ b ∈ l.mapFinIdx f ↔ ∃ i h, f i l[i] h = b

Tactic:
constructor

Result:
case mp
β : Type u_1
α : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ b ∈ l.mapFinIdx f → ∃ i h, f i l[i] h = b

case mpr
β : Type u_1
α : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ (∃ i h, f i l[i] h = b) → b ∈ l.mapFinIdx f

Proof state:
case mpr
β : Type u_1
α : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ (∃ i h, f i l[i] h = b) → b ∈ l.mapFinIdx f

Tactic:
rintro ⟨i, h, rfl⟩

Result:
case mpr.intro.intro
β : Type u_1
α : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
i : Nat
h : i < l.length
⊢ f i l[i] h ∈ l.mapFinIdx f
-- Mathlib/Algebra/Polynomial/Degree/Support.lean
theorem sum_fin [AddCommMonoid S] (f : ℕ → R → S) (hf : ∀ i, f i 0 = 0) {n : ℕ} {p : R[X]}
    (hn : p.degree < n) : (∑ i : Fin n, f i (p.coeff i)) = p.sum f

Proof state:
case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < ↑n
hp : p = 0
⊢ ∑ i : Fin n, f (↑i) (p.coeff ↑i) = p.sum f

Tactic:
rw [hp, sum_zero_index, Finset.sum_eq_zero]

Result:
case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < ↑n
hp : p = 0
⊢ ∀ x ∈ univ, f (↑x) (coeff 0 ↑x) = 0

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < ↑n
⊢ ∑ i : Fin n, f (↑i) (p.coeff ↑i) = p.sum f

Tactic:
by_cases hp : p = 0

Result:
case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < ↑n
hp : p = 0
⊢ ∑ i : Fin n, f (↑i) (p.coeff ↑i) = p.sum f

case neg
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < ↑n
hp : ¬p = 0
⊢ ∑ i : Fin n, f (↑i) (p.coeff ↑i) = p.sum f

Proof state:
case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < ↑n
hp : p = 0
i : Fin n
a✝ : i ∈ univ
⊢ f (↑i) (coeff 0 ↑i) = 0

Tactic:
exact hf i

Result:
no goals

Proof state:
case neg
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < ↑n
hp : ¬p = 0
⊢ ∑ i : Fin n, f (↑i) (p.coeff ↑i) = p.sum f

Tactic:
rw [sum_over_range' _ hf n ((natDegree_lt_iff_degree_lt hp).mpr hn),
  Fin.sum_univ_eq_sum_range fun i => f i (p.coeff i)]

Result:
no goals

Proof state:
case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < ↑n
hp : p = 0
⊢ ∀ x ∈ univ, f (↑x) (coeff 0 ↑x) = 0

Tactic:
intro i _

Result:
case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < ↑n
hp : p = 0
i : Fin n
a✝ : i ∈ univ
⊢ f (↑i) (coeff 0 ↑i) = 0
-- Mathlib/Analysis/Convex/Caratheodory.lean
theorem eq_pos_convex_span_of_mem_convexHull {x : E} (hx : x ∈ convexHull 𝕜 s) :
    ∃ (ι : Sort (u + 1)) (_ : Fintype ι),
      ∃ (z : ι → E) (w : ι → 𝕜), Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ i, 0 < w i) ∧
        ∑ i, w i = 1 ∧ ∑ i, w i • z i = x

Proof state:
case intro.intro.intro.intro.intro.intro.refine_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : ∑ y ∈ t, w y = 1
hw₃ : t.centerMass w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ ∑ i ∈ t'.attach, (fun e => w e • e) ↑i = x

Tactic:
rw [Finset.sum_attach (f := fun e => w e • e), Finset.sum_filter_of_ne]

Result:
case intro.intro.intro.intro.intro.intro.refine_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : ∑ y ∈ t, w y = 1
hw₃ : t.centerMass w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ ∑ x ∈ t, w x • x = x

case intro.intro.intro.intro.intro.intro.refine_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : ∑ y ∈ t, w y = 1
hw₃ : t.centerMass w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ ∀ x ∈ t, w x • x ≠ 0 → w x ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx_subtype {p : α → Prop} {l : Array { x // p x }}
    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    l.findIdx f = l.unattach.findIdx g

Proof state:
α : Type u_1
p : α → Prop
l : Array { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ findIdx f l = findIdx g l.unattach

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ findIdx f { toList := toList✝ } = findIdx g { toList := toList✝ }.unattach

Proof state:
case mk
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ findIdx f { toList := toList✝ } = findIdx g { toList := toList✝ }.unattach

Tactic:
simp [hf]

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
lemma preNormEDS_odd (m : ℤ) : preNormEDS b c d (2 * m + 1) =
    preNormEDS b c d (m + 2) * preNormEDS b c d m ^ 3 * (if Even m then b else 1) -
      preNormEDS b c d (m - 1) * preNormEDS b c d (m + 1) ^ 3 * (if Even m then 1 else b)

Proof state:
case neg
R : Type u
inst✝ : CommRing R
b c d : R
h :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
m : ℕ
⊢ preNormEDS b c d (2 * -↑m + 1) =
    (preNormEDS b c d (-↑m + 2) * preNormEDS b c d (-↑m) ^ 3 * if Even (-↑m) then b else 1) -
      preNormEDS b c d (-↑m - 1) * preNormEDS b c d (-↑m + 1) ^ 3 * if Even (-↑m) then 1 else b

Tactic:
rcases m with _ | m

Result:
case neg.zero
R : Type u
inst✝ : CommRing R
b c d : R
h :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
⊢ preNormEDS b c d (2 * -↑0 + 1) =
    (preNormEDS b c d (-↑0 + 2) * preNormEDS b c d (-↑0) ^ 3 * if Even (-↑0) then b else 1) -
      preNormEDS b c d (-↑0 - 1) * preNormEDS b c d (-↑0 + 1) ^ 3 * if Even (-↑0) then 1 else b

case neg.succ
R : Type u
inst✝ : CommRing R
b c d : R
h :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
m : ℕ
⊢ preNormEDS b c d (2 * -↑(m + 1) + 1) =
    (preNormEDS b c d (-↑(m + 1) + 2) * preNormEDS b c d (-↑(m + 1)) ^ 3 * if Even (-↑(m + 1)) then b else 1) -
      preNormEDS b c d (-↑(m + 1) - 1) * preNormEDS b c d (-↑(m + 1) + 1) ^ 3 * if Even (-↑(m + 1)) then 1 else b

Proof state:
case nat.zero
R : Type u
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑0 + 1) =
    (preNormEDS b c d (↑0 + 2) * preNormEDS b c d ↑0 ^ 3 * if Even ↑0 then b else 1) -
      preNormEDS b c d (↑0 - 1) * preNormEDS b c d (↑0 + 1) ^ 3 * if Even ↑0 then 1 else b

Tactic:
simp

Result:
no goals

Proof state:
case nat.succ.zero
R : Type u
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑(0 + 1) + 1) =
    (preNormEDS b c d (↑(0 + 1) + 2) * preNormEDS b c d ↑(0 + 1) ^ 3 * if Even ↑(0 + 1) then b else 1) -
      preNormEDS b c d (↑(0 + 1) - 1) * preNormEDS b c d (↑(0 + 1) + 1) ^ 3 * if Even ↑(0 + 1) then 1 else b

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem isLimit_ord {c} (co : ℵ₀ ≤ c) : (ord c).IsLimit

Proof state:
case refine_2.h
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
a : Ordinal.{u_1}
h : c ≤ (succ a).card
⊢ ℵ₀.ord.IsLimit

Tactic:
rw [ord_aleph0]

Result:
case refine_2.h
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
a : Ordinal.{u_1}
h : c ≤ (succ a).card
⊢ ω.IsLimit

Proof state:
case refine_2
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
a : Ordinal.{u_1}
h : c.ord ≤ succ a
⊢ c.ord ≤ a

Tactic:
rw [ord_le] at h ⊢

Result:
case refine_2
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
a : Ordinal.{u_1}
h : c ≤ (succ a).card
⊢ c ≤ a.card

Proof state:
case refine_2
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
a : Ordinal.{u_1}
h : c ≤ (succ a).card
⊢ c ≤ a.card

Tactic:
rwa [← @add_one_of_aleph0_le (card a), ← card_succ]

Result:
case refine_2
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
a : Ordinal.{u_1}
h : c ≤ (succ a).card
⊢ ℵ₀ ≤ a.card

Proof state:
case refine_1
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
h : c ≤ card 0
⊢ ℵ₀ = 0

Tactic:
simpa only [card_zero, nonpos_iff_eq_zero] using co.trans h

Result:
no goals

Proof state:
case refine_2
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
a : Ordinal.{u_1}
h : c ≤ (succ a).card
⊢ ℵ₀ ≤ (succ a).card

Tactic:
exact co.trans h

Result:
no goals

Proof state:
case refine_1
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
h : c.ord = 0
⊢ ℵ₀ = 0

Tactic:
rw [← Ordinal.le_zero, ord_le] at h

Result:
case refine_1
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
h : c ≤ card 0
⊢ ℵ₀ = 0

Proof state:
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
⊢ c.ord.IsLimit

Tactic:
rw [isLimit_iff, isSuccPrelimit_iff_succ_lt]

Result:
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
⊢ c.ord ≠ 0 ∧ ∀ a < c.ord, succ a < c.ord

Proof state:
case refine_2
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
a : Ordinal.{u_1}
h : c ≤ (succ a).card
⊢ ℵ₀ ≤ a.card

Tactic:
rw [← ord_le, ← le_succ_of_isLimit, ord_le]

Result:
case refine_2
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
a : Ordinal.{u_1}
h : c ≤ (succ a).card
⊢ ℵ₀ ≤ (succ a).card

case refine_2.h
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
a : Ordinal.{u_1}
h : c ≤ (succ a).card
⊢ ℵ₀.ord.IsLimit

Proof state:
case refine_2.h
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
a : Ordinal.{u_1}
h : c ≤ (succ a).card
⊢ ω.IsLimit

Tactic:
exact Ordinal.isLimit_omega0

Result:
no goals

Proof state:
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
⊢ c.ord ≠ 0 ∧ ∀ a < c.ord, succ a < c.ord

Tactic:
refine ⟨fun h => aleph0_ne_zero ?_, fun a => lt_imp_lt_of_le_imp_le fun h => ?_⟩

Result:
case refine_1
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
h : c.ord = 0
⊢ ℵ₀ = 0

case refine_2
c : Cardinal.{u_1}
co : ℵ₀ ≤ c
a : Ordinal.{u_1}
h : c.ord ≤ succ a
⊢ c.ord ≤ a
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem coeff_order (h : order φ < ⊤) : coeff R (φ.order.lift h) φ ≠ 0

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
⊢ (coeff R (φ.order.lift h)) φ ≠ 0

Tactic:
classical
simp only [order, order_finite_iff_ne_zero.mp h, not_false_iff, dif_neg]
generalize_proofs h
exact Nat.find_spec h

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
⊢ (coeff R (φ.order.lift h)) φ ≠ 0

Tactic:
simp only [order, order_finite_iff_ne_zero.mp h, not_false_iff, dif_neg]

Result:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
⊢ (coeff R ((↑(Nat.find ⋯)).lift ⋯)) φ ≠ 0

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h✝ : φ.order < ⊤
h : ∃ n, (coeff R n) φ ≠ 0
pf✝ : ↑(Nat.find h) < ⊤
⊢ (coeff R ((↑(Nat.find h)).lift pf✝)) φ ≠ 0

Tactic:
exact Nat.find_spec h

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
⊢ (coeff R ((↑(Nat.find ⋯)).lift ⋯)) φ ≠ 0

Tactic:
generalize_proofs h

Result:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h✝ : φ.order < ⊤
h : ∃ n, (coeff R n) φ ≠ 0
pf✝ : ↑(Nat.find h) < ⊤
⊢ (coeff R ((↑(Nat.find h)).lift pf✝)) φ ≠ 0
-- Mathlib/Geometry/RingedSpace/SheafedSpace.lean
theorem ext {X Y : SheafedSpace C} (α β : X ⟶ Y) (w : α.base = β.base)
    (h : α.c ≫ whiskerRight (eqToHom (by rw [w])) _ = β.c) : α = β :=
  PresheafedSpace.ext α β w h

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
α β : X ⟶ Y
w : α.base = β.base
⊢ (Opens.map α.base).op = (Opens.map β.base).op

Tactic:
rw [w]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem all_bne' [BEq α] [PartialEquivBEq α] {l : List α} :
    (l.all fun x => x != a) = !l.contains a

Proof state:
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List α
⊢ (l.all fun x => x != a) = !l.contains a

Tactic:
simp only [bne_comm, all_bne]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Lattice.lean
theorem finite_product_eq_finset_inf [SemilatticeInf α] [OrderTop α] {ι : Type u} [Fintype ι]
    (f : ι → α) : ∏ᶜ f = Fintype.elems.inf f

Proof state:
α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ (finiteLimitCone (Discrete.functor f)).cone.pt = Fintype.elems.inf f

Tactic:
change Finset.univ.inf (f ∘ discreteEquiv.toEmbedding) = Fintype.elems.inf f

Result:
α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ Finset.univ.inf (f ∘ ⇑discreteEquiv.toEmbedding) = Fintype.elems.inf f

Proof state:
α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ Finset.univ.inf f = Fintype.elems.inf f

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ∏ᶜ f = Fintype.elems.inf f

Tactic:
trans

Result:
α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ∏ᶜ f = ?m.21816

α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ?m.21816 = Fintype.elems.inf f

α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ α

Proof state:
α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ Finset.univ.inf (f ∘ ⇑discreteEquiv.toEmbedding) = Fintype.elems.inf f

Tactic:
simp only [← Finset.inf_map, Finset.univ_map_equiv_to_embedding]

Result:
α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ Finset.univ.inf f = Fintype.elems.inf f

Proof state:
α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ∏ᶜ f = ?m.21816

Tactic:
exact
  (IsLimit.conePointUniqueUpToIso (limit.isLimit _)
      (finiteLimitCone (Discrete.functor f)).isLimit).to_eq

Result:
no goals
-- Mathlib/CategoryTheory/Sites/DenseSubsite/SheafEquiv.lean
lemma isIso_ranCounit_app_of_isDenseSubsite (Y : Sheaf J A) (U X) :
    IsIso ((yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X))

Proof state:
case refine_2.mk.mk.unit.op.mk.mk.unit.op.mk.up.up.refl.refl.intro.intro.h
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.val).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
W₁ W₂ : C
g : G.obj W₁ ⟶ G.obj U
i : W₂ ⟶ W₁
hi : 𝟙 (op (G.obj U)) ≫ g.op ≫ (G.map i.op.unop).op = g.op ≫ (G.map i.op.unop).op
I : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve (G.map i ≫ g), ⋯⟩
⊢ ⋯.amalgamate ⟨G.imageSieve (G.map i ≫ g), ⋯⟩ (fun I => f ≫ Y.val.map (l I.Y W₂ U I.f (G.map i ≫ g) ⋯).op) ⋯ ≫
      Y.val.map I.f.op =
    (⋯.amalgamate ⟨G.imageSieve g, ⋯⟩ (fun I => f ≫ Y.val.map (l I.Y W₁ U I.f g ⋯).op) ⋯ ≫ Y.val.map i.op) ≫
      Y.val.map I.f.op

Tactic:
simp only [Presheaf.IsSheaf.amalgamate_map, Category.assoc, ← Functor.map_comp, ← op_comp]

Result:
case refine_2.mk.mk.unit.op.mk.mk.unit.op.mk.up.up.refl.refl.intro.intro.h
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.val).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
W₁ W₂ : C
g : G.obj W₁ ⟶ G.obj U
i : W₂ ⟶ W₁
hi : 𝟙 (op (G.obj U)) ≫ g.op ≫ (G.map i.op.unop).op = g.op ≫ (G.map i.op.unop).op
I : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve (G.map i ≫ g), ⋯⟩
⊢ f ≫ Y.val.map (l I.Y W₂ U I.f (G.map i ≫ g) ⋯).op =
    ⋯.amalgamate ⟨G.imageSieve g, ⋯⟩ (fun I => f ≫ Y.val.map (l I.Y W₁ U I.f g ⋯).op) ⋯ ≫ Y.val.map (I.f ≫ i).op
-- Mathlib/RingTheory/Idempotents.lean
lemma mem_corner_iff {r : R} : r ∈ corner e ↔ e * r = r ∧ r * e = r :=
  ⟨by rintro ⟨r, rfl⟩; simp_rw [← mul_assoc, idem.eq, mul_assoc, idem.eq, true_and],
    (⟨r, by simp_rw [·]⟩)⟩

Proof state:
case intro
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
r : R
⊢ e * (fun x => e * x * e) r = (fun x => e * x * e) r ∧ (fun x => e * x * e) r * e = (fun x => e * x * e) r

Tactic:
simp_rw [← mul_assoc, idem.eq, mul_assoc, idem.eq, true_and]

Result:
no goals

Proof state:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
r : R
⊢ r ∈ corner e → e * r = r ∧ r * e = r

Tactic:
rintro ⟨r, rfl⟩

Result:
case intro
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
r : R
⊢ e * (fun x => e * x * e) r = (fun x => e * x * e) r ∧ (fun x => e * x * e) r * e = (fun x => e * x * e) r