harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
theorem colimit_obj_ext {H : J ⥤ K ⥤ C} [HasColimitsOfShape J C] {k : K} {W : C}
    {f g : (colimit H).obj k ⟶ W} (w : ∀ j, (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g) :
    f = g

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
H : J ⥤ K ⥤ C
inst✝ : HasColimitsOfShape J C
k : K
W : C
f g : (colimit H).obj k ⟶ W
w : ∀ (j : J), (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g
⊢ (colimitObjIsoColimitCompEvaluation H k).inv ≫ f = (colimitObjIsoColimitCompEvaluation H k).inv ≫ g

Tactic:
ext j

Result:
case w
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
H : J ⥤ K ⥤ C
inst✝ : HasColimitsOfShape J C
k : K
W : C
f g : (colimit H).obj k ⟶ W
w : ∀ (j : J), (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g
j : J
⊢ colimit.ι (H ⋙ (evaluation K C).obj k) j ≫ (colimitObjIsoColimitCompEvaluation H k).inv ≫ f =
    colimit.ι (H ⋙ (evaluation K C).obj k) j ≫ (colimitObjIsoColimitCompEvaluation H k).inv ≫ g

Proof state:
case w
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
H : J ⥤ K ⥤ C
inst✝ : HasColimitsOfShape J C
k : K
W : C
f g : (colimit H).obj k ⟶ W
w : ∀ (j : J), (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g
j : J
⊢ colimit.ι (H ⋙ (evaluation K C).obj k) j ≫ (colimitObjIsoColimitCompEvaluation H k).inv ≫ f =
    colimit.ι (H ⋙ (evaluation K C).obj k) j ≫ (colimitObjIsoColimitCompEvaluation H k).inv ≫ g

Tactic:
simpa using w j

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
H : J ⥤ K ⥤ C
inst✝ : HasColimitsOfShape J C
k : K
W : C
f g : (colimit H).obj k ⟶ W
w : ∀ (j : J), (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g
⊢ f = g

Tactic:
apply (cancel_epi (colimitObjIsoColimitCompEvaluation H k).inv).1

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
H : J ⥤ K ⥤ C
inst✝ : HasColimitsOfShape J C
k : K
W : C
f g : (colimit H).obj k ⟶ W
w : ∀ (j : J), (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g
⊢ (colimitObjIsoColimitCompEvaluation H k).inv ≫ f = (colimitObjIsoColimitCompEvaluation H k).inv ≫ g
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem tendsto_card_div_pow₆ :
    (fun x ↦ (Nat.card ↑(s ∩ (⌈x⌉₊ : ℝ)⁻¹ • L) : ℝ) / ⌈x⌉₊ ^ card ι * (⌈x⌉₊ / x) ^ card ι)
          =ᶠ[atTop] (fun x ↦ (Nat.card ↑(s ∩ (⌈x⌉₊ : ℝ)⁻¹ • L) : ℝ) / x ^ card ι)

Proof state:
case h
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ℝ
hx : 1 ≤ x
⊢ ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌈x⌉₊ ^ card ι * (↑⌈x⌉₊ / x) ^ card ι =
    ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι

Tactic:
have : 0 < ⌊x⌋₊ := Nat.floor_pos.mpr hx

Result:
case h
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ℝ
hx : 1 ≤ x
this : 0 < ⌊x⌋₊
⊢ ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌈x⌉₊ ^ card ι * (↑⌈x⌉₊ / x) ^ card ι =
    ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
⊢ (fun x =>
      ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌈x⌉₊ ^ card ι *
        (↑⌈x⌉₊ / x) ^ card ι) =ᶠ[atTop]
    fun x => ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι

Tactic:
filter_upwards [eventually_ge_atTop 1] with x hx

Result:
case h
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ℝ
hx : 1 ≤ x
⊢ ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌈x⌉₊ ^ card ι * (↑⌈x⌉₊ / x) ^ card ι =
    ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι

Proof state:
case h
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ℝ
hx : 1 ≤ x
this : 0 < ⌊x⌋₊
⊢ ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌈x⌉₊ ^ card ι * (↑⌈x⌉₊ / x) ^ card ι =
    ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι

Tactic:
rw [div_pow, mul_div, div_mul_cancel₀ _ (by positivity)]

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ℝ
hx : 1 ≤ x
this : 0 < ⌊x⌋₊
⊢ ↑⌈x⌉₊ ^ card ι ≠ 0

Tactic:
positivity

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem Complex.logDeriv_cosh : logDeriv (Complex.cosh) = Complex.tanh

Proof state:
case h
x✝ : ℂ
⊢ logDeriv cosh x✝ = tanh x✝

Tactic:
rw [logDeriv, Complex.deriv_cosh, Pi.div_apply, Complex.tanh]

Result:
no goals

Proof state:
⊢ logDeriv cosh = tanh

Tactic:
ext

Result:
case h
x✝ : ℂ
⊢ logDeriv cosh x✝ = tanh x✝
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem Left.inv_le_one_iff : a⁻¹ ≤ 1 ↔ 1 ≤ a

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

Tactic:
simp

Result:
no goals

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

Tactic:
rw [← mul_le_mul_iff_left a]

Result:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a : α
⊢ a * a⁻¹ ≤ a * 1 ↔ 1 ≤ a
-- Mathlib/Algebra/Group/Units/Defs.lean
@[to_additive] lemma IsUnit.mul : IsUnit a → IsUnit b → IsUnit (a * b)

Proof state:
case intro.intro
M : Type u_1
inst✝ : Monoid M
x y : Mˣ
⊢ IsUnit (↑x * ↑y)

Tactic:
exact ⟨x * y, rfl⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
a b : M
⊢ IsUnit a → IsUnit b → IsUnit (a * b)

Tactic:
rintro ⟨x, rfl⟩ ⟨y, rfl⟩

Result:
case intro.intro
M : Type u_1
inst✝ : Monoid M
x y : Mˣ
⊢ IsUnit (↑x * ↑y)
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem eq_of_apply_eq_same (hx : IsPeriodicPt f n x) (hy : IsPeriodicPt f n y) (hn : 0 < n)
    (h : f x = f y) : x = y

Proof state:
α : Type u_1
f : α → α
x y : α
n : ℕ
hx : IsPeriodicPt f n x
hy : IsPeriodicPt f n y
hn : 0 < n
h : f x = f y
⊢ x = y

Tactic:
rw [← hx.eq, ← hy.eq, ← iterate_pred_comp_of_pos f hn, comp_apply, comp_apply, h]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem δ_comp_δ_self' {n} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : j = i.castSucc) :
    δ i ≫ δ j = δ i ≫ δ i.succ

Proof state:
n : ℕ
i : Fin (n + 2)
⊢ δ i ≫ δ i.castSucc = δ i ≫ δ i.succ

Tactic:
rw [δ_comp_δ_self]

Result:
no goals

Proof state:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : j = i.castSucc
⊢ δ i ≫ δ j = δ i ≫ δ i.succ

Tactic:
subst H

Result:
n : ℕ
i : Fin (n + 2)
⊢ δ i ≫ δ i.castSucc = δ i ≫ δ i.succ
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
@[simp] lemma vectorSpan_vadd (s : Set P) (v : V) : vectorSpan k (v +ᵥ s) = vectorSpan k s

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
v : V
⊢ vectorSpan k (v +ᵥ s) = vectorSpan k s

Tactic:
simp [vectorSpan]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem range_pow_padicValNat_subset_divisors' {n : ℕ} [hp : Fact p.Prime] :
    ((Finset.range (padicValNat p n)).image fun t => p ^ (t + 1)) ⊆ n.divisors.erase 1

Proof state:
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p n)) ⊆ n.divisors.erase 1

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

Result:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p 0)) ⊆ (divisors 0).erase 1

case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p n)) ⊆ n.divisors.erase 1

Proof state:
case inr.intro.intro
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ≠ 1 ∧ p ^ (k + 1) ∣ n ∧ n ≠ 0

Tactic:
refine ⟨?_, (pow_dvd_pow p <| succ_le_iff.2 hk).trans pow_padicValNat_dvd, hn⟩

Result:
case inr.intro.intro
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ≠ 1

Proof state:
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p n)) ⊆ n.divisors.erase 1

Tactic:
intro t ht

Result:
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
t : ℕ
ht : t ∈ Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p n))
⊢ t ∈ n.divisors.erase 1

Proof state:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p 0)) ⊆ (divisors 0).erase 1

Tactic:
simp

Result:
no goals

Proof state:
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
t : ℕ
ht : t ∈ Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p n))
⊢ t ∈ n.divisors.erase 1

Tactic:
simp only [exists_prop, Finset.mem_image, Finset.mem_range] at ht

Result:
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
t : ℕ
ht : ∃ a < padicValNat p n, p ^ (a + 1) = t
⊢ t ∈ n.divisors.erase 1

Proof state:
case inr.intro.intro
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ∈ n.divisors.erase 1

Tactic:
rw [Finset.mem_erase, Nat.mem_divisors]

Result:
case inr.intro.intro
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ≠ 1 ∧ p ^ (k + 1) ∣ n ∧ n ≠ 0

Proof state:
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
t : ℕ
ht : ∃ a < padicValNat p n, p ^ (a + 1) = t
⊢ t ∈ n.divisors.erase 1

Tactic:
obtain ⟨k, hk, rfl⟩ := ht

Result:
case inr.intro.intro
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ∈ n.divisors.erase 1

Proof state:
case inr.intro.intro
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ≠ 1

Tactic:
exact (Nat.one_lt_pow k.succ_ne_zero hp.out.one_lt).ne'

Result:
no goals
-- Mathlib/Data/Vector/Snoc.lean
theorem map_snoc {f : α → β} : map f (xs.snoc x) = (map f xs).snoc (f x)

Proof state:
α : Type u_1
β : Type u_2
n : ℕ
x : α
xs : Vector α n
f : α → β
⊢ map f (xs.snoc x) = (map f xs).snoc (f x)

Tactic:
induction xs <;> simp_all

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem setOf_sSameSide_eq_image2 {s : AffineSubspace R P} {x p : P} (hx : x ∉ s) (hp : p ∈ s) :
    { y | s.SSameSide x y } = Set.image2 (fun (t : R) q => t • (x -ᵥ p) +ᵥ q) (Set.Ioi 0) s

Proof state:
case h.mp.intro.intro.intro.intro.inr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : y = p₂
⊢ ∃ a, 0 < a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
exact False.elim (hy (h.symm ▸ hp₂))

Result:
no goals

Proof state:
case h.mp.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : x = p
⊢ ∃ a, 0 < a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
exact False.elim (hx (h.symm ▸ hp))

Result:
no goals

Proof state:
case h
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ y ∈ {y | s.SSameSide x y} ↔ y ∈ Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Ioi 0) ↑s

Tactic:
simp_rw [Set.mem_setOf, Set.mem_image2, Set.mem_Ioi]

Result:
case h
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ s.SSameSide x y ↔ ∃ a, 0 < a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
-- Mathlib/Algebra/Ring/Equiv.lean
theorem coe_ringHom_inj_iff {R S : Type*} [NonAssocSemiring R] [NonAssocSemiring S]
    (f g : R ≃+* S) : f = g ↔ (f : R →+* S) = g :=
  ⟨fun h => by rw [h], fun h => ext <| RingHom.ext_iff.mp h⟩

Proof state:
R : Type u_7
S : Type u_8
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f g : R ≃+* S
h : f = g
⊢ ↑f = ↑g

Tactic:
rw [h]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/Pi.lean
theorem LinearEquiv.finsuppUnique_symm_apply (m : M) :
    (LinearEquiv.finsuppUnique R M α).symm m = Finsupp.single default m

Proof state:
case h
R : Type u_1
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
α : Type u_4
inst✝ : Unique α
m : M
⊢ ((finsuppUnique R M α).symm m) default = (single default m) default

Tactic:
simp [LinearEquiv.finsuppUnique, Equiv.funUnique, single, Pi.single,
equivFunOnFinite, Function.update]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
α : Type u_4
inst✝ : Unique α
m : M
⊢ (finsuppUnique R M α).symm m = single default m

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
α : Type u_4
inst✝ : Unique α
m : M
⊢ ((finsuppUnique R M α).symm m) default = (single default m) default
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedGatesLemmas.lean
theorem mkOrCached_le_size (aig : AIG α) (input : BinaryInput aig) :
    aig.decls.size ≤ (aig.mkOrCached input).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ (aig.mkOrCached input).aig.decls.size

Tactic:
simp only [mkOrCached]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤
    (((aig.mkGateCached (input.asGateInput true true)).aig.mkConstCached true).aig.mkGateCached
            {
              lhs :=
                { ref := ((aig.mkGateCached (input.asGateInput true true)).aig.mkConstCached true).ref, inv := false },
              rhs :=
                { ref := (aig.mkGateCached (input.asGateInput true true)).ref.cast ⋯, inv := true } }).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤
    (((aig.mkGateCached (input.asGateInput true true)).aig.mkConstCached true).aig.mkGateCached
            {
              lhs :=
                { ref := ((aig.mkGateCached (input.asGateInput true true)).aig.mkConstCached true).ref, inv := false },
              rhs :=
                { ref := (aig.mkGateCached (input.asGateInput true true)).ref.cast ⋯, inv := true } }).aig.decls.size

Tactic:
apply LawfulOperator.le_size_of_le_aig_size

Result:
case h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ ((aig.mkGateCached (input.asGateInput true true)).aig.mkConstCached true).aig.decls.size

Proof state:
case h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ (aig.mkGateCached (input.asGateInput true true)).aig.decls.size

Tactic:
apply LawfulOperator.le_size_of_le_aig_size

Result:
case h.h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ aig.decls.size

Proof state:
case h.h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ aig.decls.size

Tactic:
omega

Result:
no goals

Proof state:
case h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ ((aig.mkGateCached (input.asGateInput true true)).aig.mkConstCached true).aig.decls.size

Tactic:
apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached)

Result:
case h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ (aig.mkGateCached (input.asGateInput true true)).aig.decls.size
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_replicate_of_pos (h : p a) : find? p (replicate n a) = if n = 0 then none else some a

Proof state:
α✝ : Type u_1
p : α✝ → Bool
n : Nat
a : α✝
h : p a = true
⊢ find? p (replicate n a) = if n = 0 then none else some a

Tactic:
simp [find?_replicate, h]

Result:
no goals
-- Mathlib/NumberTheory/Dioph.lean
theorem IsPoly.neg {f : (α → ℕ) → ℤ} : IsPoly f → IsPoly (-f)

Proof state:
α : Type u_1
f : (α → ℕ) → ℤ
⊢ IsPoly f → IsPoly (-f)

Tactic:
rw [← zero_sub]

Result:
α : Type u_1
f : (α → ℕ) → ℤ
⊢ IsPoly f → IsPoly (0 - f)

Proof state:
α : Type u_1
f : (α → ℕ) → ℤ
⊢ IsPoly f → IsPoly (0 - f)

Tactic:
exact (IsPoly.const 0).sub

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem circleMap_mem_sphere' (c : ℂ) (R : ℝ) (θ : ℝ) : circleMap c R θ ∈ sphere c |R|

Proof state:
c : ℂ
R θ : ℝ
⊢ circleMap c R θ ∈ sphere c |R|

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/OfFn.lean
theorem getElem?_ofFn (f : Fin n → α) (i) : (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none :=
  if h : i < (ofFn f).length
  then by
    rw [getElem?_eq_getElem h, List.getElem_ofFn]
    · simp only [length_ofFn] at h; simp [h]
  else by
    rw [dif_neg] <;>
    simpa using h

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h✝ : i < (ofFn f).length
h : i < n
⊢ some (f ⟨i, ⋯⟩) = if h : i < n then some (f ⟨i, h⟩) else none

Tactic:
simp [h]

Result:
no goals

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < (ofFn f).length
⊢ some (f ⟨i, ⋯⟩) = if h : i < n then some (f ⟨i, h⟩) else none

Tactic:
simp only [length_ofFn] at h

Result:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h✝ : i < (ofFn f).length
h : i < n
⊢ some (f ⟨i, ⋯⟩) = if h : i < n then some (f ⟨i, h⟩) else none

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : ¬i < (ofFn f).length
⊢ (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none

Tactic:
rw [dif_neg] <;>
simpa using h

Result:
no goals

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < (ofFn f).length
⊢ (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none

Tactic:
rw [getElem?_eq_getElem h, List.getElem_ofFn]

Result:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < (ofFn f).length
⊢ some (f ⟨i, ⋯⟩) = if h : i < n then some (f ⟨i, h⟩) else none
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem toList_unattach {p : α → Prop} {l : Array { x // p x }} :
    l.unattach.toList = l.toList.unattach

Proof state:
α : Type u_1
p : α → Prop
l : Array { x // p x }
⊢ l.unattach.toList = l.toList.unattach

Tactic:
simp only [unattach, toList_map, List.unattach]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrix_id : LinearMap.toMatrix v₁ v₁ id = 1

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
⊢ (toMatrix v₁ v₁) id = 1

Tactic:
ext i j

Result:
case a
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
i j : n
⊢ (toMatrix v₁ v₁) id i j = 1 i j

Proof state:
case a
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
i j : n
⊢ (toMatrix v₁ v₁) id i j = 1 i j

Tactic:
simp [LinearMap.toMatrix_apply, Matrix.one_apply, Finsupp.single_apply, eq_comm]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem natTrailingDegree_monomial (ha : a ≠ 0) : natTrailingDegree (monomial n a) = n

Proof state:
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
ha : a ≠ 0
⊢ (↑n).toNat = n

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
ha : a ≠ 0
⊢ ((monomial n) a).natTrailingDegree = n

Tactic:
rw [natTrailingDegree, trailingDegree_monomial ha]

Result:
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
ha : a ≠ 0
⊢ (↑n).toNat = n
-- Mathlib/Tactic/NormNum/Result.lean
theorem IsInt.to_isRat {α} [Ring α] : ∀ {a : α} {n}, IsInt a n → IsRat a n (nat_lit 1)
  | _, _, ⟨rfl⟩ => ⟨⟨1, by simp, by simp⟩, by simp⟩

Proof state:
α : Type u_1
inst✝ : Ring α
n✝ : ℤ
⊢ ↑1 * 1 = 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Ring α
n✝ : ℤ
⊢ ↑n✝ = ↑n✝ * ⅟↑1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Ring α
n✝ : ℤ
⊢ 1 * ↑1 = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Finite.lean
lemma _root_.Set.Finite.eventuallyLE_iInter {ι : Type*} {s : Set ι} (hs : s.Finite)
    {f g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) : (⋂ i ∈ s, f i) ≤ᶠ[l] (⋂ i ∈ s, g i)

Proof state:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i

Tactic:
rw [biInter_eq_iInter, biInter_eq_iInter]

Result:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋂ x, f ↑x ≤ᶠ[l] ⋂ x, g ↑x

Proof state:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋂ x, f ↑x ≤ᶠ[l] ⋂ x, g ↑x

Tactic:
exact .iInter fun i ↦ hle i.1 i.2

Result:
no goals

Proof state:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
⊢ ⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i

Tactic:
have := hs.to_subtype

Result:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i
-- Mathlib/CategoryTheory/Comma/Arrow.lean
lemma ext {f g : Arrow T}
    (h₁ : f.left = g.left) (h₂ : f.right = g.right)
    (h₃ : f.hom = eqToHom h₁ ≫ g.hom ≫ eqToHom h₂.symm) : f = g :=
  (mk_eq_mk_iff _ _).2 (by aesop)

Proof state:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
h₁ : f.left = g.left
h₂ : f.right = g.right
h₃ : f.hom = eqToHom h₁ ≫ g.hom ≫ eqToHom ⋯
⊢ ∃ hX hY, f.hom = eqToHom hX ≫ g.hom ≫ eqToHom ⋯

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_le_ncard (hst : s ⊆ t) (ht : t.Finite

Proof state:
α : Type u_1
s t : Set α
hst : s ⊆ t
ht : autoParam t.Finite _auto✝
⊢ s.ncard ≤ t.ncard

Tactic:
rw [← Nat.cast_le (α := ℕ∞), ht.cast_ncard_eq, (ht.subset hst).cast_ncard_eq]

Result:
α : Type u_1
s t : Set α
hst : s ⊆ t
ht : autoParam t.Finite _auto✝
⊢ s.encard ≤ t.encard

Proof state:
α : Type u_1
s t : Set α
hst : s ⊆ t
ht : autoParam t.Finite _auto✝
⊢ s.encard ≤ t.encard

Tactic:
exact encard_mono hst

Result:
no goals
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
/-- If `a < b * c`, `b` is positive and `0 < c < 1`, then there is a power `c ^ n` with `n : ℤ`
strictly between `a` and `b`. -/
lemma exists_zpow_btwn_of_lt_mul {a b c : α} (h : a < b * c) (hb₀ : 0 < b) (hc₀ : 0 < c)
    (hc₁ : c < 1) :
    ∃ n : ℤ, a < c ^ n ∧ c ^ n < b

Proof state:
case inr.inr.inl
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : a < 1
⊢ a < 1 ∧ 1 < b

Tactic:
exact ⟨ha₁, hb₁⟩

Result:
no goals

Proof state:
case inr.inr.inr
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
obtain ⟨n, hn₁, hn₂⟩ :=
  exists_pow_btwn_of_lt_mul this (inv_pos_of_pos ha) (inv_le_one_of_one_le₀ ha₁) hc₀ hc₁

Result:
case inr.inr.inr.intro.intro
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
inst✝ : ExistsAddOfLE α
a b c : α
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : c ^ n < a⁻¹
⊢ ∃ n, a < c ^ n ∧ c ^ n < b