harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem continuousAt_clog {x : ℂ} (h : x ∈ slitPlane) : ContinuousAt log x

Proof state:
case refine_2
x : ℂ
h : x ∈ slitPlane
h_cont_mul : Continuous fun x => x * I
⊢ ContinuousAt (fun x => ↑x.arg * I) x

Tactic:
refine h_cont_mul.continuousAt.comp (continuous_ofReal.continuousAt.comp ?_)

Result:
case refine_2
x : ℂ
h : x ∈ slitPlane
h_cont_mul : Continuous fun x => x * I
⊢ ContinuousAt arg x

Proof state:
case refine_1
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt (fun x => ↑(Real.log ‖x‖)) x

Tactic:
refine continuous_ofReal.continuousAt.comp ?_

Result:
case refine_1
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt (fun x => Real.log ‖x‖) x

Proof state:
case refine_2
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt (fun x => ↑x.arg * I) x

Tactic:
have h_cont_mul : Continuous fun x : ℂ => x * I := continuous_id'.mul continuous_const

Result:
case refine_2
x : ℂ
h : x ∈ slitPlane
h_cont_mul : Continuous fun x => x * I
⊢ ContinuousAt (fun x => ↑x.arg * I) x

Proof state:
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt log x

Tactic:
refine ContinuousAt.add ?_ ?_

Result:
case refine_1
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt (fun x => ↑(Real.log ‖x‖)) x

case refine_2
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt (fun x => ↑x.arg * I) x

Proof state:
case refine_1
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt (fun x => Real.log ‖x‖) x

Tactic:
refine (Real.continuousAt_log ?_).comp continuous_norm.continuousAt

Result:
case refine_1
x : ℂ
h : x ∈ slitPlane
⊢ ‖x‖ ≠ 0

Proof state:
case refine_1
x : ℂ
h : x ∈ slitPlane
⊢ ‖x‖ ≠ 0

Tactic:
exact norm_ne_zero_iff.mpr <| slitPlane_ne_zero h

Result:
no goals

Proof state:
case refine_2
x : ℂ
h : x ∈ slitPlane
h_cont_mul : Continuous fun x => x * I
⊢ ContinuousAt arg x

Tactic:
exact continuousAt_arg h

Result:
no goals
-- Mathlib/Data/List/Nodup.lean
theorem Nodup.insert [DecidableEq α] (h : l.Nodup) : (l.insert a).Nodup :=
  if h' : a ∈ l then by rw [insert_of_mem h']; exact h
  else by rw [insert_of_not_mem h', nodup_cons]; constructor <;> assumption

Proof state:
α : Type u
l : List α
a : α
inst✝ : DecidableEq α
h : l.Nodup
h' : a ∈ l
⊢ l.Nodup

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u
l : List α
a : α
inst✝ : DecidableEq α
h : l.Nodup
h' : a ∉ l
⊢ a ∉ l ∧ l.Nodup

Tactic:
constructor <;> assumption

Result:
no goals

Proof state:
α : Type u
l : List α
a : α
inst✝ : DecidableEq α
h : l.Nodup
h' : a ∈ l
⊢ (List.insert a l).Nodup

Tactic:
rw [insert_of_mem h']

Result:
α : Type u
l : List α
a : α
inst✝ : DecidableEq α
h : l.Nodup
h' : a ∈ l
⊢ l.Nodup

Proof state:
α : Type u
l : List α
a : α
inst✝ : DecidableEq α
h : l.Nodup
h' : a ∉ l
⊢ (List.insert a l).Nodup

Tactic:
rw [insert_of_not_mem h', nodup_cons]

Result:
α : Type u
l : List α
a : α
inst✝ : DecidableEq α
h : l.Nodup
h' : a ∉ l
⊢ a ∉ l ∧ l.Nodup
-- Mathlib/FieldTheory/Minpoly/IsConjRoot.lean
theorem eq_algebraMap_of_injective [Nontrivial R] [NoZeroSMulDivisors R S] {r : R} {x : S}
    (h : IsConjRoot R (algebraMap R S r) x) (hf : Function.Injective (algebraMap R S)) :
    x = algebraMap R S r

Proof state:
R : Type u_1
S : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R S
r : R
x : S
h : X - C r = minpoly R x
hf : Function.Injective ⇑(algebraMap R S)
⊢ x ∈ (X - C r).aroots S

Tactic:
rw [mem_aroots]

Result:
R : Type u_1
S : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R S
r : R
x : S
h : X - C r = minpoly R x
hf : Function.Injective ⇑(algebraMap R S)
⊢ X - C r ≠ 0 ∧ (Polynomial.aeval x) (X - C r) = 0

Proof state:
R : Type u_1
S : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R S
r : R
x : S
h : IsConjRoot R ((algebraMap R S) r) x
hf : Function.Injective ⇑(algebraMap R S)
⊢ x = (algebraMap R S) r

Tactic:
rw [IsConjRoot, minpoly.eq_X_sub_C_of_algebraMap_inj _ hf] at h

Result:
R : Type u_1
S : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R S
r : R
x : S
h : X - C r = minpoly R x
hf : Function.Injective ⇑(algebraMap R S)
⊢ x = (algebraMap R S) r

Proof state:
R : Type u_1
S : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R S
r : R
x : S
h : X - C r = minpoly R x
hf : Function.Injective ⇑(algebraMap R S)
this : x ∈ (X - C r).aroots S
⊢ x = (algebraMap R S) r

Tactic:
simpa [aroots_X_sub_C] using this

Result:
no goals

Proof state:
R : Type u_1
S : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R S
r : R
x : S
h : X - C r = minpoly R x
hf : Function.Injective ⇑(algebraMap R S)
⊢ x = (algebraMap R S) r

Tactic:
have : x ∈ (X - C r).aroots S := by
  rw [mem_aroots]
  simp [X_sub_C_ne_zero, h ▸ minpoly.aeval R x]

Result:
R : Type u_1
S : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R S
r : R
x : S
h : X - C r = minpoly R x
hf : Function.Injective ⇑(algebraMap R S)
this : x ∈ (X - C r).aroots S
⊢ x = (algebraMap R S) r

Proof state:
R : Type u_1
S : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R S
r : R
x : S
h : X - C r = minpoly R x
hf : Function.Injective ⇑(algebraMap R S)
⊢ X - C r ≠ 0 ∧ (Polynomial.aeval x) (X - C r) = 0

Tactic:
simp [X_sub_C_ne_zero, h ▸ minpoly.aeval R x]

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
theorem iteratedDerivWithin_add
    (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) :
    iteratedDerivWithin n (f + g) s x =
      iteratedDerivWithin n f s x + iteratedDerivWithin n g s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
f g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑n) f s x
hg : ContDiffWithinAt 𝕜 (↑n) g s x
⊢ iteratedDerivWithin n (f + g) s x = iteratedDerivWithin n f s x + iteratedDerivWithin n g s x

Tactic:
simp_rw [iteratedDerivWithin, iteratedFDerivWithin_add_apply hf hg h hx,
  ContinuousMultilinearMap.add_apply]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem Iic_iInf₂ (f : ∀ i, κ i → α) : Iic (⨅ (i) (j), f i j) = ⨅ (i) (j), Iic (f i j)

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Iic (⨅ i, ⨅ j, f i j) = ⨅ i, ⨅ j, Iic (f i j)

Tactic:
simp_rw [Iic_iInf]

Result:
no goals
-- Mathlib/Data/Multiset/Nodup.lean
theorem count_eq_of_nodup [DecidableEq α] {a : α} {s : Multiset α} (d : Nodup s) :
    count a s = if a ∈ s then 1 else 0

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
h : a ∈ s
⊢ count a s = 1

Tactic:
exact count_eq_one_of_mem d h

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
h : a ∉ s
⊢ count a s = 0

Tactic:
exact count_eq_zero_of_not_mem h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
⊢ count a s = if a ∈ s then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
h : a ∈ s
⊢ count a s = 1

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
h : a ∉ s
⊢ count a s = 0
-- Mathlib/Analysis/CStarAlgebra/Matrix.lean
theorem entrywise_sup_norm_bound_of_unitary {U : Matrix n n 𝕜} (hU : U ∈ Matrix.unitaryGroup n 𝕜) :
    ‖U‖ ≤ 1

Proof state:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
⊢ ‖U‖ ≤ 1

Tactic:
conv => rw [pi_norm_le_iff_of_nonneg zero_le_one]
  intro
  rw [pi_norm_le_iff_of_nonneg zero_le_one]

Result:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
⊢ ∀ (i i_1 : n), ‖U i i_1‖ ≤ 1

Proof state:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i✝¹ i✝ : n
⊢ ‖U i✝¹ i✝‖ ≤ 1

Tactic:
exact entry_norm_bound_of_unitary hU _ _

Result:
no goals

Proof state:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
⊢ ∀ (i i_1 : n), ‖U i i_1‖ ≤ 1

Tactic:
intros

Result:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i✝¹ i✝ : n
⊢ ‖U i✝¹ i✝‖ ≤ 1
-- Mathlib/Data/Fintype/Defs.lean
theorem nodup_map_iff_injOn {f : α → β} {s : Finset α} :
    (Multiset.map f s.val).Nodup ↔ Set.InjOn f s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Finset α
⊢ (Multiset.map f s.val).Nodup ↔ Set.InjOn f ↑s

Tactic:
simp [Multiset.nodup_map_iff_inj_on s.nodup, Set.InjOn]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Adjunction.lean
/-- Given an adjunction `adj : F ⊣ G`, `a` in `A` and commutation isomorphisms
`e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a` and
`e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a`, if `e₁` and `e₂` are compatible with the
unit of the adjunction `adj`, then `e₁` uniquely determines `e₂`.
-/
lemma compatibilityUnit_unique_right (h : CompatibilityUnit adj e₁ e₂)
    (h' : CompatibilityUnit adj e₁ e₂') : e₂ = e₂'

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
⊢ e₂ = e₂'

Tactic:
rw [← Iso.symm_eq_iff]

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
⊢ e₂.symm = e₂'.symm

Proof state:
case w.w.h
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
x✝ : D
⊢ e₂.symm.hom.app x✝ = e₂'.symm.hom.app x✝

Tactic:
rw [Iso.symm_hom, Iso.symm_hom, compatibilityUnit_right adj e₁ e₂ h,
  compatibilityUnit_right adj e₁ e₂' h']

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
⊢ e₂.symm = e₂'.symm

Tactic:
ext

Result:
case w.w.h
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
x✝ : D
⊢ e₂.symm.hom.app x✝ = e₂'.symm.hom.app x✝
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem totalDegree_finset_sum {ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ R) :
    (s.sum f).totalDegree ≤ Finset.sup s fun i => (f i).totalDegree

Proof state:
case cons
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hind : (s.sum f).totalDegree ≤ s.sup fun i => (f i).totalDegree
⊢ ((Finset.cons a s has).sum f).totalDegree ≤ (Finset.cons a s has).sup fun i => (f i).totalDegree

Tactic:
rw [Finset.sum_cons, Finset.sup_cons]

Result:
case cons
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hind : (s.sum f).totalDegree ≤ s.sup fun i => (f i).totalDegree
⊢ (f a + ∑ x ∈ s, f x).totalDegree ≤ (f a).totalDegree ⊔ s.sup fun i => (f i).totalDegree

Proof state:
case cons
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hind : (s.sum f).totalDegree ≤ s.sup fun i => (f i).totalDegree
⊢ (f a + ∑ x ∈ s, f x).totalDegree ≤ (f a).totalDegree ⊔ s.sup fun i => (f i).totalDegree

Tactic:
exact (MvPolynomial.totalDegree_add _ _).trans (max_le_max le_rfl hind)

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ (s.sum f).totalDegree ≤ s.sup fun i => (f i).totalDegree

Tactic:
induction' s using Finset.cons_induction with a s has hind

Result:
case empty
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
f : ι → MvPolynomial σ R
⊢ (∅.sum f).totalDegree ≤ ∅.sup fun i => (f i).totalDegree

case cons
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hind : (s.sum f).totalDegree ≤ s.sup fun i => (f i).totalDegree
⊢ ((Finset.cons a s has).sum f).totalDegree ≤ (Finset.cons a s has).sup fun i => (f i).totalDegree

Proof state:
case empty
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
f : ι → MvPolynomial σ R
⊢ (∅.sum f).totalDegree ≤ ∅.sup fun i => (f i).totalDegree

Tactic:
exact zero_le _

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean
/-- If the initial comparison map for `G` is an isomorphism, then `G` preserves initial objects.
-/
lemma PreservesInitial.of_iso_comparison [i : IsIso (initialComparison G)] :
    PreservesColimit (Functor.empty.{0} C) G

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasInitial C
inst✝ : HasInitial D
i : IsIso (initialComparison G)
⊢ IsInitial (G.obj (⊥_ C))

Tactic:
exact @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (Functor.empty.{0} D)) i

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasInitial C
inst✝ : HasInitial D
i : IsIso (initialComparison G)
⊢ PreservesColimit (Functor.empty C) G

Tactic:
apply preservesColimit_of_preserves_colimit_cocone initialIsInitial

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasInitial C
inst✝ : HasInitial D
i : IsIso (initialComparison G)
⊢ IsColimit (G.mapCocone (asEmptyCocone (⊥_ C)))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasInitial C
inst✝ : HasInitial D
i : IsIso (initialComparison G)
⊢ IsColimit (G.mapCocone (asEmptyCocone (⊥_ C)))

Tactic:
apply (isColimitMapCoconeEmptyCoconeEquiv _ _).symm _

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasInitial C
inst✝ : HasInitial D
i : IsIso (initialComparison G)
⊢ IsInitial (G.obj (⊥_ C))
-- Mathlib/Order/Filter/CardinalInter.lean
theorem le_cardinalGenerate_iff_of_cardinalInterFilter {f : Filter α} [CardinalInterFilter f c]
    (hc : 2 < c) : f ≤ cardinalGenerate g hc ↔ g ⊆ f.sets

Proof state:
case mpr
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
⊢ f ≤ cardinalGenerate g hc

Tactic:
intro s hs

Result:
case mpr
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s : Set α
hs : s ∈ cardinalGenerate g hc
⊢ s ∈ f

Proof state:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
⊢ f ≤ cardinalGenerate g hc ↔ g ⊆ f.sets

Tactic:
constructor <;> intro h

Result:
case mp
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
h : f ≤ cardinalGenerate g hc
⊢ g ⊆ f.sets

case mpr
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
⊢ f ≤ cardinalGenerate g hc

Proof state:
case mpr.superset
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s s✝ t✝ : Set α
a✝ : CardinalGenerateSets g s✝
st : s✝ ⊆ t✝
ih : s✝ ∈ f
⊢ t✝ ∈ f

Tactic:
exact mem_of_superset ih st

Result:
no goals

Proof state:
case mpr.univ
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s : Set α
⊢ Set.univ ∈ f

Tactic:
exact univ_mem

Result:
no goals

Proof state:
case mpr.sInter
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s : Set α
S✝ : Set (Set α)
Sct : #↑S✝ < c
a✝ : ∀ s ∈ S✝, CardinalGenerateSets g s
ih : ∀ s ∈ S✝, s ∈ f
⊢ ⋂₀ S✝ ∈ f

Tactic:
exact (cardinal_sInter_mem Sct).mpr ih

Result:
no goals

Proof state:
case mp
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
h : f ≤ cardinalGenerate g hc
⊢ g ⊆ f.sets

Tactic:
exact subset_trans (fun s => CardinalGenerateSets.basic) h

Result:
no goals

Proof state:
case mpr.basic
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s s✝ : Set α
hs : s✝ ∈ g
⊢ s✝ ∈ f

Tactic:
exact h hs

Result:
no goals

Proof state:
case mpr
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s : Set α
hs : s ∈ cardinalGenerate g hc
⊢ s ∈ f

Tactic:
induction hs with
| basic hs => exact h hs
| univ => exact univ_mem
| superset _ st ih => exact mem_of_superset ih st
| sInter Sct _ ih => exact (cardinal_sInter_mem Sct).mpr ih

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_eq_toInt {x : BitVec w}:
    x.msb = decide (x.toInt < 0)

Proof state:
case neg
w : Nat
x : BitVec w
h : ¬x.msb = true
⊢ ¬↑x.toNat < 0

Tactic:
omega

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
h : ¬x.msb = true
⊢ x.msb = decide (x.toInt < 0)

Tactic:
simp [h, toInt_eq_msb_cond]

Result:
case neg
w : Nat
x : BitVec w
h : ¬x.msb = true
⊢ ¬↑x.toNat < 0
-- Mathlib/CategoryTheory/Quotient.lean
theorem compClosure.congruence :
    Congruence fun X Y => Relation.EqvGen (@CompClosure C _ r X Y)

Proof state:
case h.e'_3.h.h.h.h.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ Relation.EqvGen (CompClosure r) x✝¹ x✝ ↔ (functor r).homRel x✝¹ x✝

Tactic:
rw [functor_homRel_eq_compClosure_eqvGen]

Result:
no goals

Proof state:
case h.e'_3.h.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
x✝¹ x✝ : C
⊢ Relation.EqvGen (CompClosure r) = (functor r).homRel

Tactic:
ext

Result:
case h.e'_3.h.h.h.h.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ Relation.EqvGen (CompClosure r) x✝¹ x✝ ↔ (functor r).homRel x✝¹ x✝

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
⊢ Congruence fun X Y => Relation.EqvGen (CompClosure r)

Tactic:
convert inferInstanceAs (Congruence (functor r).homRel)

Result:
case h.e'_3.h.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
x✝¹ x✝ : C
⊢ Relation.EqvGen (CompClosure r) = (functor r).homRel
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem reflection_eq_iff_orthogonalProjection_eq (s₁ s₂ : AffineSubspace ℝ P) [Nonempty s₁]
    [Nonempty s₂] [HasOrthogonalProjection s₁.direction] [HasOrthogonalProjection s₂.direction]
    (p : P) :
    reflection s₁ p = reflection s₂ p ↔
      (orthogonalProjection s₁ p : P) = orthogonalProjection s₂ p

Proof state:
case mp
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : HasOrthogonalProjection s₁.direction
inst✝ : HasOrthogonalProjection s₂.direction
p : P
h :
  (↑((orthogonalProjection s₁) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₁) p) =
    (↑((orthogonalProjection s₂) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₂) p)
⊢ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)

Tactic:
rw [← @vsub_eq_zero_iff_eq V, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_comm, add_sub_assoc,
  vsub_sub_vsub_cancel_right, ←
  two_smul ℝ ((orthogonalProjection s₁ p : P) -ᵥ orthogonalProjection s₂ p), smul_eq_zero] at h

Result:
case mp
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : HasOrthogonalProjection s₁.direction
inst✝ : HasOrthogonalProjection s₂.direction
p : P
h : 2 = 0 ∨ ↑((orthogonalProjection s₁) p) -ᵥ ↑((orthogonalProjection s₂) p) = 0
⊢ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean
theorem denote_blastUmod (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bool)
      (input : BinaryRefVec aig w)
      (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
      (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
      ∀ (idx : Nat) (hidx : idx < w),
        ⟦(blastUmod aig input).aig, (blastUmod aig input).vec.get idx hidx, assign⟧
          =
        (lhs % rhs).getLsbD idx

Proof state:
case htrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
hdiscr✝ :
  ¬⟦assign,
        {
          aig :=
            (blastUdiv.go
                (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                    { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs,
                      rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).aig
                w { gate := ((blastConst aig 0#w).aig.mkConstCached false).ref.gate, hgate := ⋯ }
                { gate := (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).ref.gate, hgate := ⋯ }
                ((((input.cast ⋯).cast ⋯).cast ⋯).lhs.cast ⋯) ((((input.cast ⋯).cast ⋯).cast ⋯).rhs.cast ⋯) w 0
                ((((blastConst aig 0#w).vec.cast ⋯).cast ⋯).cast ⋯)
                ((((blastConst aig 0#w).vec.cast ⋯).cast ⋯).cast ⋯)).aig,
          ref :=
            {
              gate :=
                (BVPred.mkEq (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig
                      { lhs := (((input.cast ⋯).cast ⋯).cast ⋯).rhs,
                        rhs := ((blastConst aig 0#w).vec.cast ⋯).cast ⋯ }).ref.gate,
              hgate := ⋯ } }⟧ =
      true
hdiscr : ¬(rhs == 0#w) = true
hzero : 0#w < rhs
⊢ ⟦assign,
      { aig := (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).aig,
        ref :=
          { gate := (((blastConst aig 0#w).aig.mkConstCached false).aig.mkConstCached true).ref.gate,
            hgate := ?htrue } }⟧ =
    true

Tactic:
simp

Result:
no goals