harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_arithShiftRight :
    eval assign (.arithShiftRight lhs rhs) = BitVec.sshiftRight' (eval assign lhs) (eval assign rhs)

Proof state:
assign : Assignment
a✝¹ : Nat
lhs : BVExpr a✝¹
a✝ : Nat
rhs : BVExpr a✝
⊢ eval assign (lhs.arithShiftRight rhs) = (eval assign lhs).sshiftRight' (eval assign rhs)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem foldl1_eq_foldr1 [hassoc : Std.Associative f] :
    ∀ a b l, foldl f a (l ++ [b]) = foldr f b (a :: l)
  | _, _, nil => rfl
  | a, b, c :: l => by
    simp only [cons_append, foldl_cons, foldr_cons, foldl1_eq_foldr1 _ _ l]
    rw [hassoc.assoc]

Proof state:
α : Type u
f : α → α → α
hassoc : Std.Associative f
a b c : α
l : List α
⊢ f (f a c) (foldr f b l) = f a (f c (foldr f b l))

Tactic:
rw [hassoc.assoc]

Result:
no goals

Proof state:
α : Type u
f : α → α → α
hassoc : Std.Associative f
a b c : α
l : List α
⊢ foldl f a (c :: l ++ [b]) = foldr f b (a :: c :: l)

Tactic:
simp only [cons_append, foldl_cons, foldr_cons, foldl1_eq_foldr1 _ _ l]

Result:
α : Type u
f : α → α → α
hassoc : Std.Associative f
a b c : α
l : List α
⊢ f (f a c) (foldr f b l) = f a (f c (foldr f b l))
-- Mathlib/Data/Nat/Init.lean
lemma add_mod_eq_add_mod_right (c : ℕ) (H : a % d = b % d) : (a + c) % d = (b + c) % d

Proof state:
a b d c : ℕ
H : a % d = b % d
⊢ (a + c) % d = (b + c) % d

Tactic:
rw [← mod_add_mod, ← mod_add_mod b, H]

Result:
no goals
-- Mathlib/Algebra/Order/Chebyshev.lean
theorem sum_div_card_sq_le_sum_sq_div_card :
    ((∑ i ∈ s, f i) / #s) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) / #s

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
⊢ ((∑ i ∈ s, f i) / ↑(#s)) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) / ↑(#s)

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Result:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : ExistsAddOfLE α
f : ι → α
⊢ ((∑ i ∈ ∅, f i) / ↑(#∅)) ^ 2 ≤ (∑ i ∈ ∅, f i ^ 2) / ↑(#∅)

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ ((∑ i ∈ s, f i) / ↑(#s)) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) / ↑(#s)

Proof state:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ ((∑ i ∈ s, f i) / ↑(#s)) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) / ↑(#s)

Tactic:
rw [div_pow, div_le_div_iff₀ (by positivity) (by positivity), sq (#s : α), mul_left_comm,
  ← mul_assoc]

Result:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ (∑ i ∈ s, f i) ^ 2 * ↑(#s) ≤ (↑(#s) * ∑ i ∈ s, f i ^ 2) * ↑(#s)

Proof state:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ (∑ i ∈ s, f i) ^ 2 * ↑(#s) ≤ (↑(#s) * ∑ i ∈ s, f i ^ 2) * ↑(#s)

Tactic:
exact mul_le_mul_of_nonneg_right sq_sum_le_card_mul_sum_sq (by positivity)

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ 0 < ↑(#s)

Tactic:
positivity

Result:
no goals

Proof state:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : ExistsAddOfLE α
f : ι → α
⊢ ((∑ i ∈ ∅, f i) / ↑(#∅)) ^ 2 ≤ (∑ i ∈ ∅, f i ^ 2) / ↑(#∅)

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ 0 ≤ ↑(#s)

Tactic:
positivity

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ 0 < ↑(#s) ^ 2

Tactic:
positivity

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem Finite.exists_lt_map_eq_of_forall_mem [LinearOrder α] [Infinite α] {t : Set β} {f : α → β}
    (hf : ∀ a, f a ∈ t) (ht : t.Finite) : ∃ a b, a < b ∧ f a = f b

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Infinite α
t : Set β
f : α → β
hf : MapsTo f univ t
ht : t.Finite
⊢ ∃ a b, a < b ∧ f a = f b

Tactic:
obtain ⟨a, -, b, -, h⟩ := infinite_univ.exists_lt_map_eq_of_mapsTo hf ht

Result:
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Infinite α
t : Set β
f : α → β
hf : MapsTo f univ t
ht : t.Finite
a b : α
h : a < b ∧ f a = f b
⊢ ∃ a b, a < b ∧ f a = f b

Proof state:
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Infinite α
t : Set β
f : α → β
hf : MapsTo f univ t
ht : t.Finite
a b : α
h : a < b ∧ f a = f b
⊢ ∃ a b, a < b ∧ f a = f b

Tactic:
exact ⟨a, b, h⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Infinite α
t : Set β
f : α → β
hf : ∀ (a : α), f a ∈ t
ht : t.Finite
⊢ ∃ a b, a < b ∧ f a = f b

Tactic:
rw [← mapsTo_univ_iff] at hf

Result:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Infinite α
t : Set β
f : α → β
hf : MapsTo f univ t
ht : t.Finite
⊢ ∃ a b, a < b ∧ f a = f b
-- Mathlib/Analysis/Convex/Basic.lean
theorem Convex.translate_preimage_left (hs : Convex 𝕜 s) (z : E) :
    Convex 𝕜 ((fun x => x + z) ⁻¹' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z : E
⊢ Convex 𝕜 ((fun x => x + z) ⁻¹' s)

Tactic:
simpa only [add_comm] using hs.translate_preimage_right z

Result:
no goals
-- Mathlib/Data/Matrix/Bilinear.lean
theorem mulLeftLinearMap_mul [SMulCommClass R A A] (a : Matrix l m A) (b : Matrix m n A) :
    mulLeftLinearMap o R (a * b) = (mulLeftLinearMap o R a).comp (mulLeftLinearMap o R b)

Proof state:
case h.a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : Matrix l m A
b : Matrix m n A
x✝ : Matrix n o A
i✝ : l
j✝ : o
⊢ (mulLeftLinearMap o R (a * b)) x✝ i✝ j✝ = (mulLeftLinearMap o R a ∘ₗ mulLeftLinearMap o R b) x✝ i✝ j✝

Tactic:
simp only [mulLeftLinearMap_apply, LinearMap.comp_apply, Matrix.mul_assoc]

Result:
no goals

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : Matrix l m A
b : Matrix m n A
⊢ mulLeftLinearMap o R (a * b) = mulLeftLinearMap o R a ∘ₗ mulLeftLinearMap o R b

Tactic:
ext

Result:
case h.a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : Matrix l m A
b : Matrix m n A
x✝ : Matrix n o A
i✝ : l
j✝ : o
⊢ (mulLeftLinearMap o R (a * b)) x✝ i✝ j✝ = (mulLeftLinearMap o R a ∘ₗ mulLeftLinearMap o R b) x✝ i✝ j✝
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeff_monomial_succ : coeff (monomial (n + 1) a) 0 = 0

Proof state:
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
⊢ ((monomial (n + 1)) a).coeff 0 = 0

Tactic:
simp [coeff_monomial]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem modEq_nine_digits_sum (n : ℕ) : n ≡ (digits 10 n).sum [MOD 9] :=
  modEq_digits_sum 9 10 (by norm_num) n

Proof state:
n : ℕ
⊢ 10 % 9 = 1

Tactic:
norm_num

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem val_eq_singleton_iff {a : α} {s : Finset α} : s.val = {a} ↔ s = {a}

Proof state:
α : Type u_1
a : α
s : Finset α
⊢ s.val = {a} ↔ s.val = {a}.val

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
a : α
s : Finset α
⊢ s.val = {a} ↔ s = {a}

Tactic:
rw [← val_inj]

Result:
α : Type u_1
a : α
s : Finset α
⊢ s.val = {a} ↔ s.val = {a}.val
-- Mathlib/SetTheory/Nimber/Field.lean
theorem mem_invSet_of_lt_invAux (h : b < invAux a) : b ∈ invSet a

Proof state:
a b : Nimber
h : b < sInf a.invSetᶜ
⊢ b ∈ a.invSet

Tactic:
have := not_mem_of_lt_csInf h ⟨_, bot_mem_lowerBounds _⟩

Result:
a b : Nimber
h : b < sInf a.invSetᶜ
this : b ∉ a.invSetᶜ
⊢ b ∈ a.invSet

Proof state:
a b : Nimber
h : b < sInf a.invSetᶜ
this : b ∉ a.invSetᶜ
⊢ b ∈ a.invSet

Tactic:
rwa [Set.not_mem_compl_iff] at this

Result:
no goals

Proof state:
a b : Nimber
h : b < a.invAux
⊢ b ∈ a.invSet

Tactic:
rw [invAux] at h

Result:
a b : Nimber
h : b < sInf a.invSetᶜ
⊢ b ∈ a.invSet
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma Scheme.zeroLocus_biInf_of_nonempty
    {X : Scheme.{u}} {U : X.Opens} {ι : Type*}
    (I : ι → Ideal Γ(X, U)) {t : Set ι} (ht : t.Finite) (ht' : t.Nonempty) :
    X.zeroLocus (U := U) ↑(⨅ i ∈ t, I i) = ⋃ i ∈ t, X.zeroLocus (U := U) (I i)

Proof state:
case intro
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t : Set ι
ht : t.Finite
i : ι
hi : i ∈ t
⊢ (↑U)ᶜ ⊆ ⋃ i ∈ t, X.zeroLocus ↑(I i)

Tactic:
exact fun x hx ↦ Set.mem_iUnion₂_of_mem hi
  (codisjoint_iff_compl_le_left.mp (X.codisjoint_zeroLocus (U := U) (I i)) hx)

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t : Set ι
ht : t.Finite
ht' : t.Nonempty
⊢ X.zeroLocus ↑(⨅ i ∈ t, I i) = ⋃ i ∈ t, X.zeroLocus ↑(I i)

Tactic:
rw [zeroLocus_biInf I ht, Set.union_eq_left]

Result:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t : Set ι
ht : t.Finite
ht' : t.Nonempty
⊢ (↑U)ᶜ ⊆ ⋃ i ∈ t, X.zeroLocus ↑(I i)

Proof state:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t : Set ι
ht : t.Finite
ht' : t.Nonempty
⊢ (↑U)ᶜ ⊆ ⋃ i ∈ t, X.zeroLocus ↑(I i)

Tactic:
obtain ⟨i, hi⟩ := ht'

Result:
case intro
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t : Set ι
ht : t.Finite
i : ι
hi : i ∈ t
⊢ (↑U)ᶜ ⊆ ⋃ i ∈ t, X.zeroLocus ↑(I i)
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem AlgebraicIndependent.image_of_comp {ι ι'} (s : Set ι) (f : ι → ι') (g : ι' → A)
    (hs : AlgebraicIndependent R fun x : s => g (f x)) :
    AlgebraicIndependent R fun x : f '' s => g x

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι : Type u_7
ι' : Type u_8
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent R fun x => g (f ↑x)
a✝ : Nontrivial R
⊢ AlgebraicIndependent R fun x => g ↑x

Tactic:
have : InjOn f s := injOn_iff_injective.2 hs.injective.of_comp

Result:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι : Type u_7
ι' : Type u_8
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent R fun x => g (f ↑x)
a✝ : Nontrivial R
this : InjOn f s
⊢ AlgebraicIndependent R fun x => g ↑x

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι : Type u_7
ι' : Type u_8
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent R fun x => g (f ↑x)
a✝ : Nontrivial R
this : InjOn f s
⊢ AlgebraicIndependent R fun x => g ↑x

Tactic:
exact (algebraicIndependent_equiv' (Equiv.Set.imageOfInjOn f s this) rfl).1 hs

Result:
no goals

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι : Type u_7
ι' : Type u_8
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent R fun x => g (f ↑x)
⊢ AlgebraicIndependent R fun x => g ↑x

Tactic:
nontriviality R

Result:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι : Type u_7
ι' : Type u_8
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent R fun x => g (f ↑x)
a✝ : Nontrivial R
⊢ AlgebraicIndependent R fun x => g ↑x
-- Mathlib/RingTheory/Ideal/Lattice.lean
theorem eq_bot_or_top : I = ⊥ ∨ I = ⊤

Proof state:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ I = ⊥ ∨ I = ⊤

Tactic:
rw [or_iff_not_imp_right]

Result:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ ¬I = ⊤ → I = ⊥

Proof state:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ 1 ∉ I → I = ⊥

Tactic:
intro h1

Result:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
⊢ I = ⊥

Proof state:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
⊢ I = ⊥

Tactic:
rw [eq_bot_iff]

Result:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
⊢ I ≤ ⊥

Proof state:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ I ≠ ⊤ → I = ⊥

Tactic:
rw [Ideal.ne_top_iff_one]

Result:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ 1 ∉ I → I = ⊥

Proof state:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
hr : r ∈ I
⊢ r ∈ ⊥

Tactic:
by_cases H : r = 0

Result:
case pos
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
hr : r ∈ I
H : r = 0
⊢ r ∈ ⊥

case neg
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
hr : r ∈ I
H : ¬r = 0
⊢ r ∈ ⊥

Proof state:
case neg
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
hr : r ∈ I
H : ¬r = 0
⊢ r ∈ ⊥

Tactic:
simpa [H, h1] using I.mul_mem_left r⁻¹ hr

Result:
no goals

Proof state:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ ¬I = ⊤ → I = ⊥

Tactic:
change _ ≠ _ → _

Result:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ I ≠ ⊤ → I = ⊥

Proof state:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
⊢ I ≤ ⊥

Tactic:
intro r hr

Result:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
hr : r ∈ I
⊢ r ∈ ⊥

Proof state:
case pos
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
hr : r ∈ I
H : r = 0
⊢ r ∈ ⊥

Tactic:
simpa

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean
theorem cyclotomic_mul_prime_dvd_eq_pow (R : Type*) {p n : ℕ} [hp : Fact (Nat.Prime p)] [Ring R]
    [CharP R p] (hn : p ∣ n) : cyclotomic (n * p) R = cyclotomic n R ^ p

Proof state:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ p

Tactic:
rw [← ZMod.expand_card, ← map_cyclotomic_int n, ← map_expand,
  cyclotomic_expand_eq_cyclotomic hp.out hn, map_cyclotomic]

Result:
no goals

Proof state:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : p ∣ n
this✝ : Algebra (ZMod p) R := ZMod.algebra R p
this : cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ p
⊢ cyclotomic (n * p) R = cyclotomic n R ^ p

Tactic:
rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R),
  this, Polynomial.map_pow]

Result:
no goals

Proof state:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : p ∣ n
⊢ cyclotomic (n * p) R = cyclotomic n R ^ p

Tactic:
letI : Algebra (ZMod p) R := ZMod.algebra _ _

Result:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) R = cyclotomic n R ^ p

Proof state:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) R = cyclotomic n R ^ p

Tactic:
suffices cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ p by
  rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R),
    this, Polynomial.map_pow]

Result:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ p
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/LawfulOperator.lean
theorem lt_size (entry : Entrypoint α) (input : β entry.aig) :
    entry.ref.gate < (f entry.aig input).aig.decls.size

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
entry : Entrypoint α
input : β entry.aig
h1 : entry.ref.gate < entry.aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size

Tactic:
have h2 : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size := by
  apply le_size

Result:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
entry : Entrypoint α
input : β entry.aig
h1 : entry.ref.gate < entry.aig.decls.size
h2 : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
entry : Entrypoint α
input : β entry.aig
h1 : entry.ref.gate < entry.aig.decls.size
⊢ entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size

Tactic:
apply le_size

Result:
no goals

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
entry : Entrypoint α
input : β entry.aig
h1 : entry.ref.gate < entry.aig.decls.size
h2 : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
entry : Entrypoint α
input : β entry.aig
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size

Tactic:
have h1 := entry.ref.hgate

Result:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
entry : Entrypoint α
input : β entry.aig
h1 : entry.ref.gate < entry.aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size
-- Mathlib/Data/Nat/Nth.lean
lemma nth_comp_of_strictMono {n : ℕ} {f : ℕ → ℕ} (hf : StrictMono f)
    (h0 : ∀ k, p k → k ∈ Set.range f) (h : ∀ hfi : (setOf p).Finite, n < hfi.toFinset.card) :
    f (nth (fun i ↦ p (f i)) n) = nth p n

Proof state:
p : ℕ → Prop
n : ℕ
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
h : ∀ (hfi : (setOf p).Finite), n < #hfi.toFinset
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
⊢ f (nth (fun i => p (f i)) n) = nth p n

Tactic:
induction n using Nat.case_strong_induction_on

Result:
case hz
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
h : ∀ (hfi : (setOf p).Finite), 0 < #hfi.toFinset
⊢ f (nth (fun i => p (f i)) 0) = nth p 0

case hi
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
n✝ : ℕ
a✝ : ∀ m ≤ n✝, (∀ (hfi : (setOf p).Finite), m < #hfi.toFinset) → f (nth (fun i => p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n✝ + 1 < #hfi.toFinset
⊢ f (nth (fun i => p (f i)) (n✝ + 1)) = nth p (n✝ + 1)

Proof state:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
h : ∀ (hfi : (setOf p).Finite), 0 < #hfi.toFinset
⊢ f (nth (fun i => p (f i)) 0) = nth p 0

Tactic:
simp_rw [nth_zero]

Result:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
h : ∀ (hfi : (setOf p).Finite), 0 < #hfi.toFinset
⊢ f (sInf {i | p (f i)}) = sInf (setOf p)

Proof state:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (setOf p).Finite), m < #hfi.toFinset) → f (nth (fun i => p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #hfi.toFinset
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
⊢ {i | p (f i) ∧ ∀ k < n + 1, nth p k < f i}.Nonempty

Tactic:
rcases h0 _ (nth_mem _ h) with ⟨t, ht⟩

Result:
case intro
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (setOf p).Finite), m < #hfi.toFinset) → f (nth (fun i => p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #hfi.toFinset
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
t : ℕ
ht : f t = nth p (n + 1)
⊢ {i | p (f i) ∧ ∀ k < n + 1, nth p k < f i}.Nonempty
-- Mathlib/Order/SuccPred/WithBot.lean
lemma succ_strictMono [NoMaxOrder α] : StrictMono (succ : WithBot α → α)
  | ⊥, (b : α), hab => by simp
  | (a : α), (b : α), hab => Order.succ_lt_succ (by simpa using hab)

Proof state:
α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
b : α
hab : ⊥ < ↑b
⊢ ⊥.succ < (↑b).succ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a b : α
hab : ↑a < ↑b
⊢ a < b

Tactic:
simpa using hab

Result:
no goals
-- Mathlib/CategoryTheory/Filtered/Basic.lean
theorem of_cocone_nonempty (h : ∀ {J : Type w} [SmallCategory J] [FinCategory J] (F : J ⥤ C),
    Nonempty (Cocone F)) : IsFiltered C

Proof state:
case refine_2.intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
h₁ :
  (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map { down := WalkingParallelPairHom.left } ≫
      c.ι.app { down := WalkingParallelPair.one } =
    c.ι.app { down := WalkingParallelPair.zero } ≫
      ((Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))).obj c.pt).map
        { down := WalkingParallelPairHom.left }
h₂ :
  (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map { down := WalkingParallelPairHom.right } ≫
      c.ι.app { down := WalkingParallelPair.one } =
    c.ι.app { down := WalkingParallelPair.zero } ≫
      ((Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))).obj c.pt).map
        { down := WalkingParallelPairHom.right }
⊢ f ≫ c.ι.app { down := WalkingParallelPair.one } = g ≫ c.ι.app { down := WalkingParallelPair.one }

Tactic:
simp_all

Result:
no goals

Proof state:
case refine_1.intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)
this : Nonempty C
X Y : C
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ pair X Y)
⊢ ∃ Z x x, True

Tactic:
exact ⟨c.pt, c.ι.app ⟨⟨WalkingPair.left⟩⟩, c.ι.app ⟨⟨WalkingPair.right⟩⟩, trivial⟩

Result:
no goals

Proof state:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)
this : Nonempty C
⊢ ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), ∃ Z h, f ≫ h = g ≫ h

Tactic:
intros X Y f g

Result:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
⊢ ∃ Z h, f ≫ h = g ≫ h