harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Monoidal/Mon_.lean
theorem whiskerRight_hom (X : Mon_ C) {Y Z : Mon_ C} (f : Y ⟶ Z) :
    (X ◁ f).hom = X.X ◁ f.hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : Mon_ C
f : Y ⟶ Z
⊢ (X ◁ f).hom = X.X ◁ f.hom

Tactic:
rw [← id_tensorHom]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : Mon_ C
f : Y ⟶ Z
⊢ (X ◁ f).hom = 𝟙 X.X ⊗ f.hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : Mon_ C
f : Y ⟶ Z
⊢ (X ◁ f).hom = 𝟙 X.X ⊗ f.hom

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Antichain.lean
theorem image (hs : IsStrongAntichain r s) {f : α → β} (hf : Surjective f)
    (h : ∀ a b, r' (f a) (f b) → r a b) : IsStrongAntichain r' (f '' s)

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : f a ≠ f b
c : β
⊢ ¬r' (f a) c ∨ ¬r' (f b) c

Tactic:
obtain ⟨c, rfl⟩ := hf c

Result:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : f a ≠ f b
c : α
⊢ ¬r' (f a) (f c) ∨ ¬r' (f b) (f c)

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
⊢ IsStrongAntichain r' (f '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ hab c

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : f a ≠ f b
c : β
⊢ ¬r' (f a) c ∨ ¬r' (f b) c

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : f a ≠ f b
c : α
⊢ ¬r' (f a) (f c) ∨ ¬r' (f b) (f c)

Tactic:
exact (hs ha hb (ne_of_apply_ne _ hab) _).imp (mt <| h _ _) (mt <| h _ _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem splitInTwo_snd (l : { l : List α // l.length = n }) :
    (splitInTwo l).2 = ⟨l.1.drop ((n+1)/2), by simp [splitInTwo, splitAt_eq, l.2]; omega⟩

Proof state:
α : Type ?u.1090
n : Nat
l : { l // l.length = n }
⊢ n - (n + 1) / 2 = n / 2

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.1090
n : Nat
l : { l // l.length = n }
⊢ (drop ((n + 1) / 2) l.val).length = n / 2

Tactic:
simp [splitInTwo, splitAt_eq, l.2]

Result:
α : Type ?u.1090
n : Nat
l : { l // l.length = n }
⊢ n - (n + 1) / 2 = n / 2

Proof state:
α : Type u_1
n : Nat
l : { l // l.length = n }
⊢ (splitInTwo l).snd = ⟨drop ((n + 1) / 2) l.val, ⋯⟩

Tactic:
simp [splitInTwo, splitAt_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mkVector_eq_mk_mkArray (a : α) (n : Nat) :
    mkVector n a = mk (mkArray n a) (by simp)

Proof state:
α : Type ?u.74966
a : α
n : Nat
⊢ (mkArray n a).size = n

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
n : Nat
⊢ mkVector n a = { toArray := mkArray n a, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals
-- Mathlib/Data/PNat/Interval.lean
theorem card_fintype_Ioo : Fintype.card (Set.Ioo a b) = b - a - 1

Proof state:
a b : ℕ+
⊢ Fintype.card ↑(Set.Ioo a b) = ↑b - ↑a - 1

Tactic:
rw [← card_Ioo, Fintype.card_ofFinset]

Result:
no goals
-- Mathlib/Data/Multiset/Count.lean
theorem ext {s t : Multiset α} : s = t ↔ ∀ a, count a s = count a t :=
  Quotient.inductionOn₂ s t fun _l₁ _l₂ => Quotient.eq.trans <| by
    simp only [quot_mk_to_coe, mem_coe, coe_count, decide_eq_true_eq]
    apply perm_iff_count

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
_l₁ _l₂ : List α
⊢ (isSetoid α) _l₁ _l₂ ↔ ∀ (a : α), List.count a _l₁ = List.count a _l₂

Tactic:
apply perm_iff_count

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
_l₁ _l₂ : List α
⊢ (isSetoid α) _l₁ _l₂ ↔ ∀ (a : α), count a ⟦_l₁⟧ = count a ⟦_l₂⟧

Tactic:
simp only [quot_mk_to_coe, mem_coe, coe_count, decide_eq_true_eq]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
_l₁ _l₂ : List α
⊢ (isSetoid α) _l₁ _l₂ ↔ ∀ (a : α), List.count a _l₁ = List.count a _l₂
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_sub_const_Ioo : (fun x => x - a) ⁻¹' Ioo b c = Ioo (b + a) (c + a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' Ioo b c = Ioo (b + a) (c + a)

Tactic:
simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem gateToCNF_eval :
    (gateToCNF output lhs rhs linv rinv).eval assign
      =
    (assign output == (((assign lhs) ^^ linv) && ((assign rhs) ^^ rinv)))

Proof state:
α✝ : Type u_1
output lhs rhs : α✝
linv rinv : Bool
assign : α✝ → Bool
⊢ CNF.eval assign (gateToCNF output lhs rhs linv rinv) =
    (assign output == ((assign lhs ^^ linv) && (assign rhs ^^ rinv)))

Tactic:
simp only [CNF.eval, gateToCNF, CNF.Clause.eval, List.all_cons, List.any_cons, beq_false,
  List.any_nil, Bool.or_false, beq_true, List.all_nil, Bool.and_true]

Result:
α✝ : Type u_1
output lhs rhs : α✝
linv rinv : Bool
assign : α✝ → Bool
⊢ ((!assign output || assign lhs == !linv) &&
      ((!assign output || assign rhs == !rinv) && (assign output || (assign lhs == linv || assign rhs == rinv)))) =
    (assign output == ((assign lhs ^^ linv) && (assign rhs ^^ rinv)))

Proof state:
α✝ : Type u_1
output lhs rhs : α✝
linv rinv : Bool
assign : α✝ → Bool
⊢ ((!assign output || assign lhs == !linv) &&
      ((!assign output || assign rhs == !rinv) && (assign output || (assign lhs == linv || assign rhs == rinv)))) =
    (assign output == ((assign lhs ^^ linv) && (assign rhs ^^ rinv)))

Tactic:
cases assign output
  <;> cases assign lhs
    <;> cases assign rhs
      <;> cases linv
        <;> cases rinv
          <;> decide

Result:
no goals
-- Mathlib/Algebra/Polynomial/UnitTrinomial.lean
theorem trinomial_natDegree (hkm : k < m) (hmn : m < n) (hw : w ≠ 0) :
    (trinomial k m n u v w).natDegree = n

Proof state:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
i : ℕ
h : i ∈ (trinomial k m n u v w).support
⊢ ↑i ≤ ↑n

Tactic:
replace h := support_trinomial' k m n u v w h

Result:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
i : ℕ
h : i ∈ {k, m, n}
⊢ ↑i ≤ ↑n

Proof state:
case inr.inl
R : Type u_1
inst✝ : Semiring R
k n : ℕ
u v w : R
hw : w ≠ 0
i : ℕ
hkm : k < i
hmn : i < n
⊢ ↑i ≤ ↑n

Tactic:
exact WithBot.coe_le_coe.mpr hmn.le

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
⊢ (trinomial k m n u v w).coeff n ≠ 0

Tactic:
rwa [trinomial_leading_coeff' hkm hmn]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
i : ℕ
h : i ∈ {k, m, n}
⊢ ↑i ≤ ↑n

Tactic:
rw [mem_insert, mem_insert, mem_singleton] at h

Result:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
i : ℕ
h : i = k ∨ i = m ∨ i = n
⊢ ↑i ≤ ↑n

Proof state:
case inr.inr
R : Type u_1
inst✝ : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hw : w ≠ 0
i : ℕ
hmn : m < i
⊢ ↑i ≤ ↑i

Tactic:
exact le_rfl

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝ : Semiring R
m n : ℕ
u v w : R
hmn : m < n
hw : w ≠ 0
i : ℕ
hkm : i < m
⊢ ↑i ≤ ↑n

Tactic:
exact WithBot.coe_le_coe.mpr (hkm.trans hmn).le

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
⊢ (trinomial k m n u v w).natDegree = n

Tactic:
refine
  natDegree_eq_of_degree_eq_some
    ((Finset.sup_le fun i h => ?_).antisymm <|
      le_degree_of_ne_zero <| by rwa [trinomial_leading_coeff' hkm hmn])

Result:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
i : ℕ
h : i ∈ (trinomial k m n u v w).support
⊢ ↑i ≤ ↑n

Proof state:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
i : ℕ
h : i = k ∨ i = m ∨ i = n
⊢ ↑i ≤ ↑n

Tactic:
rcases h with (rfl | rfl | rfl)

Result:
case inl
R : Type u_1
inst✝ : Semiring R
m n : ℕ
u v w : R
hmn : m < n
hw : w ≠ 0
i : ℕ
hkm : i < m
⊢ ↑i ≤ ↑n

case inr.inl
R : Type u_1
inst✝ : Semiring R
k n : ℕ
u v w : R
hw : w ≠ 0
i : ℕ
hkm : k < i
hmn : i < n
⊢ ↑i ≤ ↑n

case inr.inr
R : Type u_1
inst✝ : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hw : w ≠ 0
i : ℕ
hmn : m < i
⊢ ↑i ≤ ↑i
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem Icc_factorization_eq_pow_dvd (n : ℕ) {p : ℕ} (pp : Prime p) :
    Icc 1 (n.factorization p) = {i ∈ Ico 1 n | p ^ i ∣ n}

Proof state:
case inr.h
n p : ℕ
pp : Prime p
hn : n ≠ 0
x : ℕ
⊢ x ∈ Icc 1 (n.factorization p) ↔ x ∈ Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n)

Tactic:
simp only [mem_Icc, Finset.mem_filter, mem_Ico, and_assoc, and_congr_right_iff,
  pp.pow_dvd_iff_le_factorization hn, iff_and_self]

Result:
case inr.h
n p : ℕ
pp : Prime p
hn : n ≠ 0
x : ℕ
⊢ 1 ≤ x → x ≤ n.factorization p → x < n

Proof state:
case inl
p : ℕ
pp : Prime p
⊢ Icc 1 ((factorization 0) p) = Finset.filter (fun i => p ^ i ∣ 0) (Ico 1 0)

Tactic:
simp

Result:
no goals

Proof state:
n p : ℕ
pp : Prime p
⊢ Icc 1 (n.factorization p) = Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n)

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Result:
case inl
p : ℕ
pp : Prime p
⊢ Icc 1 ((factorization 0) p) = Finset.filter (fun i => p ^ i ∣ 0) (Ico 1 0)

case inr
n p : ℕ
pp : Prime p
hn : n ≠ 0
⊢ Icc 1 (n.factorization p) = Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n)

Proof state:
case inr
n p : ℕ
pp : Prime p
hn : n ≠ 0
⊢ Icc 1 (n.factorization p) = Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n)

Tactic:
ext x

Result:
case inr.h
n p : ℕ
pp : Prime p
hn : n ≠ 0
x : ℕ
⊢ x ∈ Icc 1 (n.factorization p) ↔ x ∈ Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n)

Proof state:
case inr.h
n p : ℕ
pp : Prime p
hn : n ≠ 0
x : ℕ
⊢ 1 ≤ x → x ≤ n.factorization p → x < n

Tactic:
exact fun _ H => lt_of_le_of_lt H (factorization_lt p hn)

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem w₀ {X Y : Augmented C} (f : X ⟶ Y) :
    (Augmented.drop.map f).app (op (SimplexCategory.mk 0)) ≫ Y.hom.app (op (SimplexCategory.mk 0)) =
      X.hom.app (op (SimplexCategory.mk 0)) ≫ Augmented.point.map f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : Augmented C
f : X ⟶ Y
⊢ (drop.map f).app (op ⦋0⦌) ≫ Y.hom.app (op ⦋0⦌) = X.hom.app (op ⦋0⦌) ≫ point.map f

Tactic:
convert congr_app f.w (op (SimplexCategory.mk 0))

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_nfp_blsub₂ (op : Ordinal → Ordinal → Ordinal) (o : Ordinal) :
    Principal op (nfp (fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b)) o)

Proof state:
case h
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
h : (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o ≤ (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
⊢ op a b < ((fun o' => o'.blsub₂ o' fun a x b x => op a b) ∘ (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n]) o

Tactic:
exact lt_blsub₂ (@fun a _ b _ => op a b) (hm.trans_le h) hn

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/Basic.lean
theorem mem_rootsOfUnity' (k : ℕ) (ζ : Mˣ) : ζ ∈ rootsOfUnity k M ↔ (ζ : M) ^ k = 1

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : Mˣ
⊢ ζ ^ k = 1 ↔ ↑ζ ^ k = 1

Tactic:
norm_cast

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : Mˣ
⊢ ζ ∈ rootsOfUnity k M ↔ ↑ζ ^ k = 1

Tactic:
rw [mem_rootsOfUnity]

Result:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : Mˣ
⊢ ζ ^ k = 1 ↔ ↑ζ ^ k = 1
-- Mathlib/GroupTheory/NoncommPiCoprod.lean
theorem injective_noncommPiCoprod_of_iSupIndep
    {hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y}
    (hind : iSupIndep H) :
    Function.Injective (noncommPiCoprod hcomm)

Proof state:
case hinj
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
inst✝ : Fintype ι
hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : iSupIndep H
⊢ ∀ (i : ι), Function.Injective ⇑(H i).subtype

Tactic:
intro i

Result:
case hinj
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
inst✝ : Fintype ι
hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : iSupIndep H
i : ι
⊢ Function.Injective ⇑(H i).subtype

Proof state:
case hind
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
inst✝ : Fintype ι
hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : iSupIndep H
⊢ iSupIndep fun i => (H i).subtype.range

Tactic:
simpa using hind

Result:
no goals

Proof state:
case hinj
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
inst✝ : Fintype ι
hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : iSupIndep H
i : ι
⊢ Function.Injective ⇑(H i).subtype

Tactic:
exact Subtype.coe_injective

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
inst✝ : Fintype ι
hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : iSupIndep H
⊢ Function.Injective ⇑(noncommPiCoprod hcomm)

Tactic:
apply MonoidHom.injective_noncommPiCoprod_of_iSupIndep

Result:
case hind
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
inst✝ : Fintype ι
hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : iSupIndep H
⊢ iSupIndep fun i => (H i).subtype.range

case hinj
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
inst✝ : Fintype ι
hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : iSupIndep H
⊢ ∀ (i : ι), Function.Injective ⇑(H i).subtype
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem tendsto_translationNumber_of_dist_bounded_aux (x : ℕ → ℝ) (C : ℝ)
    (H : ∀ n : ℕ, dist ((f ^ n) 0) (x n) ≤ C) :
    Tendsto (fun n : ℕ => x (2 ^ n) / 2 ^ n) atTop (𝓝 <| τ f)

Proof state:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
⊢ Tendsto (fun n => x (2 ^ n) / 2 ^ n) atTop (𝓝 (τ f))

Tactic:
apply f.tendsto_translationNumber_aux.congr_dist (squeeze_zero (fun _ => dist_nonneg) _ _)

Result:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
⊢ ℕ → ℝ

f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
⊢ ∀ (t : ℕ), dist (f.transnumAuxSeq t) (x (2 ^ t) / 2 ^ t) ≤ ?m.111236 t

f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
⊢ Tendsto ?m.111236 atTop (𝓝 0)

Proof state:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
⊢ ∀ (t : ℕ), dist (f.transnumAuxSeq t) (x (2 ^ t) / 2 ^ t) ≤ C / 2 ^ t

Tactic:
intro n

Result:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
n : ℕ
⊢ dist (f.transnumAuxSeq n) (x (2 ^ n) / 2 ^ n) ≤ C / 2 ^ n

Proof state:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
n : ℕ
⊢ dist (f.transnumAuxSeq n) (x (2 ^ n) / 2 ^ n) ≤ C / 2 ^ n

Tactic:
have : 0 < (2 ^ n : ℝ) := pow_pos zero_lt_two _

Result:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
n : ℕ
this : 0 < 2 ^ n
⊢ dist (f.transnumAuxSeq n) (x (2 ^ n) / 2 ^ n) ≤ C / 2 ^ n

Proof state:
case h.e'_3
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
n : ℕ
this : 0 < 2 ^ n
⊢ dist (f.transnumAuxSeq n) (x (2 ^ n) / 2 ^ n) = dist ((f ^ 2 ^ n) 0) (x (2 ^ n)) / 2 ^ n

Tactic:
rw [transnumAuxSeq, Real.dist_eq, ← sub_div, abs_div, abs_of_pos this, Real.dist_eq]

Result:
no goals

Proof state:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
⊢ Tendsto (fun n => C / 2 ^ n) atTop (𝓝 0)

Tactic:
exact mul_zero C ▸ tendsto_const_nhds.mul <| tendsto_inv_atTop_zero.comp <|
  tendsto_pow_atTop_atTop_of_one_lt one_lt_two

Result:
no goals

Proof state:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
n : ℕ
this : 0 < 2 ^ n
⊢ dist (f.transnumAuxSeq n) (x (2 ^ n) / 2 ^ n) ≤ C / 2 ^ n

Tactic:
convert (div_le_div_iff_of_pos_right this).2 (H (2 ^ n)) using 1

Result:
case h.e'_3
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
n : ℕ
this : 0 < 2 ^ n
⊢ dist (f.transnumAuxSeq n) (x (2 ^ n) / 2 ^ n) = dist ((f ^ 2 ^ n) 0) (x (2 ^ n)) / 2 ^ n

Proof state:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C
⊢ ℕ → ℝ

Tactic:
exact fun n => C / 2 ^ n

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem tensorLeftHomEquiv_symm_coevaluation_comp_whiskerRight {X Y : C} [HasRightDual X]
    [HasRightDual Y] (f : X ⟶ Y) :
    (tensorLeftHomEquiv _ _ _ _).symm (η_ _ _ ≫ f ▷ (Xᘁ)) = (ρ_ _).hom ≫ fᘁ

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ Yᘁ ◁ (η_ X Xᘁ ≫ f ▷ Xᘁ) ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom =
    (ρ_ Yᘁ).hom ≫ (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ (tensorLeftHomEquiv (𝟙_ C) Y Yᘁ Xᘁ).symm (η_ X Xᘁ ≫ f ▷ Xᘁ) = (ρ_ Yᘁ).hom ≫ fᘁ

Tactic:
dsimp [tensorLeftHomEquiv, rightAdjointMate]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ Yᘁ ◁ (η_ X Xᘁ ≫ f ▷ Xᘁ) ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom =
    (ρ_ Yᘁ).hom ≫ (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom
-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
lemma ΓSpec_adjunction_homEquiv_eq {X : Scheme.{u}} {B : CommRingCat} (φ : B ⟶ Γ(X, ⊤)) :
    ((ΓSpec.adjunction.homEquiv X (op B)) φ.op).appTop = (Scheme.ΓSpecIso B).hom ≫ φ

Proof state:
X : Scheme
B : CommRingCat
φ : B ⟶ Γ(X, ⊤)
⊢ Scheme.Hom.appTop ((ΓSpec.adjunction.homEquiv X (op B)) φ.op) = (Scheme.ΓSpecIso B).hom ≫ φ

Tactic:
rw [← Iso.inv_comp_eq, ΓSpecIso_inv_ΓSpec_adjunction_homEquiv]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem le_inv_mul_iff_mul_le : b ≤ a⁻¹ * c ↔ a * b ≤ c

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c : α
⊢ b ≤ a⁻¹ * c ↔ a * b ≤ c

Tactic:
rw [← mul_le_mul_iff_left a]

Result:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c : α
⊢ a * b ≤ a * (a⁻¹ * c) ↔ a * b ≤ c

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c : α
⊢ a * b ≤ a * (a⁻¹ * c) ↔ a * b ≤ c

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WeakDual.lean
theorem toSeminorm_ball_zero {f : E →ₗ[𝕜] 𝕜} {r : ℝ} :
    Seminorm.ball f.toSeminorm 0 r = { x : E | ‖f x‖ < r }

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E →ₗ[𝕜] 𝕜
r : ℝ
⊢ f.toSeminorm.ball 0 r = {x | ‖f x‖ < r}

Tactic:
simp only [Seminorm.ball_zero_eq, toSeminorm_apply]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
lemma sigma_mk_preimage_image' (h : i ≠ j) : Sigma.mk j ⁻¹' (Sigma.mk i '' s) = ∅

Proof state:
α : Type u_1
β : α → Type u_2
i j : α
s : Set (β i)
h : i ≠ j
⊢ Sigma.mk j ⁻¹' (Sigma.mk i '' s) = ∅

Tactic:
simp [image, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.truncate_eq_zeroExtend (x : BitVec w) : x.truncate n = x.zeroExtend n

Proof state:
w n : Nat
x : BitVec w
⊢ BitVec.truncate n x = BitVec.zeroExtend n x

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
/-- A functor between preadditive categories that preserves (zero morphisms and) binary coproducts
    preserves binary biproducts. -/
lemma preservesBinaryBiproduct_of_preservesBinaryCoproduct {X Y : C}
    [PreservesColimit (pair X Y) F] :
    PreservesBinaryBiproduct X Y F where
  preserves {b} hb :=
    ⟨isBinaryBilimitOfIsColimit _ <|
      IsColimit.ofIsoColimit
          ((IsColimit.precomposeInvEquiv (diagramIsoPair _) (F.mapCocone b.toCocone)).symm
            (isColimitOfPreserves F hb.isColimit)) <|
        Cocones.ext (Iso.refl _) fun j => by
          rcases j with ⟨⟨⟩⟩ <;> simp⟩

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesColimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ ((Cocones.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).ι.app j ≫
      (Iso.refl ((Cocones.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).pt).hom =
    (F.mapBinaryBicone b).toCocone.ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩ <;> simp

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean
theorem opNorm_zero_iff [RingHomIsometric σ₁₂] : ‖f‖ = 0 ↔ f = 0 :=
  Iff.intro
    (fun hn => ContinuousLinearMap.ext fun x => norm_le_zero_iff.1
      (calc
        _ ≤ ‖f‖ * ‖x‖ := le_opNorm _ _
        _ = _

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst✝ : RingHomIsometric σ₁₂
⊢ f = 0 → ‖f‖ = 0

Tactic:
rintro rfl

Result:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
⊢ ‖0‖ = 0

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
⊢ ‖0‖ = 0

Tactic:
exact opNorm_zero

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst✝ : RingHomIsometric σ₁₂
hn : ‖f‖ = 0
x : E
⊢ ‖f‖ * ‖x‖ = 0

Tactic:
rw [hn, zero_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : Array α) :
    elem a as = decide (a ∈ as)

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : Array α
⊢ elem a as = decide (a ∈ as)

Tactic:
rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem lt_nfp_iff {a b} : a < nfp f b ↔ ∃ n, a < f^[n] b

Proof state:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ a < nfp f b ↔ ∃ n, a < f^[n] b

Tactic:
rw [← iSup_iterate_eq_nfp]

Result:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ a < ⨆ n, f^[n] b ↔ ∃ n, a < f^[n] b

Proof state:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ a < ⨆ n, f^[n] b ↔ ∃ n, a < f^[n] b

Tactic:
exact Ordinal.lt_iSup_iff

Result:
no goals