harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Defs.lean
theorem sum_fintype [Fintype ι] (κ : ι → Kernel α β) : Kernel.sum κ = ∑ i, κ i

Proof state:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Fintype ι
κ : ι → Kernel α β
a : α
s : Set β
hs : MeasurableSet s
⊢ ((Kernel.sum κ) a) s = ((∑ i : ι, κ i) a) s

Tactic:
simp only [sum_apply' κ a hs, finset_sum_apply' _ κ a s, tsum_fintype]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Fintype ι
κ : ι → Kernel α β
⊢ Kernel.sum κ = ∑ i : ι, κ i

Tactic:
ext a s hs

Result:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Fintype ι
κ : ι → Kernel α β
a : α
s : Set β
hs : MeasurableSet s
⊢ ((Kernel.sum κ) a) s = ((∑ i : ι, κ i) a) s
-- Mathlib/Algebra/RingQuot.lean
theorem smul_quot [Algebra S R] {n : S} {a : R} :
    (n • ⟨Quot.mk _ a⟩ : RingQuot r) = ⟨Quot.mk _ (n • a)⟩

Proof state:
R : Type uR
inst✝² : Semiring R
S : Type uS
inst✝¹ : CommSemiring S
r : R → R → Prop
inst✝ : Algebra S R
n : S
a : R
⊢ n • { toQuot := Quot.mk (Rel r) a } = { toQuot := Quot.mk (Rel r) (n • a) }

Tactic:
show smul r _ _ = _

Result:
R : Type uR
inst✝² : Semiring R
S : Type uS
inst✝¹ : CommSemiring S
r : R → R → Prop
inst✝ : Algebra S R
n : S
a : R
⊢ RingQuot.smul r n { toQuot := Quot.mk (Rel r) a } = { toQuot := Quot.mk (Rel r) (n • a) }

Proof state:
R : Type uR
inst✝² : Semiring R
S : Type uS
inst✝¹ : CommSemiring S
r : R → R → Prop
inst✝ : Algebra S R
n : S
a : R
⊢ { toQuot := Quot.map (fun a => n • a) ⋯ (Quot.mk (Rel r) a) } = { toQuot := Quot.mk (Rel r) (n • a) }

Tactic:
rfl

Result:
no goals

Proof state:
R : Type uR
inst✝² : Semiring R
S : Type uS
inst✝¹ : CommSemiring S
r : R → R → Prop
inst✝ : Algebra S R
n : S
a : R
⊢ RingQuot.smul r n { toQuot := Quot.mk (Rel r) a } = { toQuot := Quot.mk (Rel r) (n • a) }

Tactic:
rw [smul]

Result:
R : Type uR
inst✝² : Semiring R
S : Type uS
inst✝¹ : CommSemiring S
r : R → R → Prop
inst✝ : Algebra S R
n : S
a : R
⊢ { toQuot := Quot.map (fun a => n • a) ⋯ (Quot.mk (Rel r) a) } = { toQuot := Quot.mk (Rel r) (n • a) }
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Pullbacks.lean
theorem inr_comp_pushoutObjIso_hom (f : F ⟶ G) (g : F ⟶ H) (d : D) :
    (pushout.inr f g).app d ≫ (pushoutObjIso f g d).hom = pushout.inr (f.app d) (g.app d)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G H : D ⥤ C
inst✝ : HasPushouts C
f : F ⟶ G
g : F ⟶ H
d : D
⊢ (pushout.inr f g).app d ≫ (pushoutObjIso f g d).hom = pushout.inr (f.app d) (g.app d)

Tactic:
simp [pushoutObjIso]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_sub_const_Ico : (fun x => x - a) '' Ico b c = Ico (b - a) (c - a)

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

Tactic:
simp [sub_eq_neg_add]

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem reindex_trans (e : ι ≃ ι₂) (e' : ι₂ ≃ ι₃) :
    (reindex R s e).trans (reindex R _ e') = reindex R s (e.trans e')

Proof state:
case a
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
e : ι ≃ ι₂
e' : ι₂ ≃ ι₃
⊢ ↑(reindex R s e ≪≫ₗ reindex R (fun i => s (e.symm i)) e') = ↑(reindex R s (e.trans e'))

Tactic:
ext f

Result:
case a.H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
e : ι ≃ ι₂
e' : ι₂ ≃ ι₃
f : (i : ι) → s i
⊢ ((↑(reindex R s e ≪≫ₗ reindex R (fun i => s (e.symm i)) e')).compMultilinearMap (tprod R)) f =
    ((↑(reindex R s (e.trans e'))).compMultilinearMap (tprod R)) f

Proof state:
case a.H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
e : ι ≃ ι₂
e' : ι₂ ≃ ι₃
f : (i : ι) → s i
⊢ ((tprod R) fun i => f (e.symm (e'.symm i))) =
    ((domDomCongrLinearEquiv' R R s (⨂[R] (i : ι₃), s ((e.trans e').symm i)) (e.trans e')).symm (tprod R)) f

Tactic:
congr

Result:
no goals

Proof state:
case a.H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
e : ι ≃ ι₂
e' : ι₂ ≃ ι₃
f : (i : ι) → s i
⊢ ((↑(reindex R s e ≪≫ₗ reindex R (fun i => s (e.symm i)) e')).compMultilinearMap (tprod R)) f =
    ((↑(reindex R s (e.trans e'))).compMultilinearMap (tprod R)) f

Tactic:
simp only [LinearEquiv.trans_apply, LinearEquiv.coe_coe, reindex_tprod,
  LinearMap.coe_compMultilinearMap, Function.comp_apply, MultilinearMap.domDomCongr_apply,
  reindex_comp_tprod]

Result:
case a.H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
e : ι ≃ ι₂
e' : ι₂ ≃ ι₃
f : (i : ι) → s i
⊢ ((tprod R) fun i => f (e.symm (e'.symm i))) =
    ((domDomCongrLinearEquiv' R R s (⨂[R] (i : ι₃), s ((e.trans e').symm i)) (e.trans e')).symm (tprod R)) f

Proof state:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
e : ι ≃ ι₂
e' : ι₂ ≃ ι₃
⊢ reindex R s e ≪≫ₗ reindex R (fun i => s (e.symm i)) e' = reindex R s (e.trans e')

Tactic:
apply LinearEquiv.toLinearMap_injective

Result:
case a
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
e : ι ≃ ι₂
e' : ι₂ ≃ ι₃
⊢ ↑(reindex R s e ≪≫ₗ reindex R (fun i => s (e.symm i)) e') = ↑(reindex R s (e.trans e'))
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem cokernelIsoOfEq_refl {h : f = f} : cokernelIsoOfEq h = Iso.refl (cokernel f)

Proof state:
case w.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasCokernel f
h : f = f
⊢ coequalizer.π f 0 ≫ (cokernelIsoOfEq h).hom = coequalizer.π f 0 ≫ (Iso.refl (cokernel f)).hom

Tactic:
simp [cokernelIsoOfEq]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasCokernel f
h : f = f
⊢ cokernelIsoOfEq h = Iso.refl (cokernel f)

Tactic:
ext

Result:
case w.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasCokernel f
h : f = f
⊢ coequalizer.π f 0 ≫ (cokernelIsoOfEq h).hom = coequalizer.π f 0 ≫ (Iso.refl (cokernel f)).hom
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₆_of_isShortNF_of_char_three : W.b₆ = W.a₆

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ 4 * W.a₆ = W.a₆

Tactic:
linear_combination W.a₆ * CharP.cast_eq_zero R 3

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ W.b₆ = W.a₆

Tactic:
rw [b₆_of_isShortNF]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ 4 * W.a₆ = W.a₆
-- Mathlib/Computability/TuringMachine.lean
theorem addBottom_map (L : ListBlank (∀ k, Option (Γ k))) :
    (addBottom L).map ⟨Prod.snd, by rfl⟩ = L

Proof state:
case h.e'_2.h.e'_4
K : Type u_1
Γ : K → Type u_2
L L' : ListBlank ((k : K) → Option (Γ k))
l : List ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.mk l)) =
    ListBlank.mk l

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
L : ListBlank ((k : K) → Option (Γ k))
⊢ default.2 = default

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (addBottom L) = L

Tactic:
simp only [addBottom, ListBlank.map_cons]

Result:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.cons L.head
      (ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)) =
    L

Proof state:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.cons L.head
      (ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)) =
    L

Tactic:
convert ListBlank.cons_head_tail L

Result:
case h.e'_2.h.e'_4
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail) = L.tail

Proof state:
case h.e'_2.h.e'_4
K : Type u_1
Γ : K → Type u_2
L L' : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L') = L'

Tactic:
refine L'.induction_on fun l ↦ ?_

Result:
case h.e'_2.h.e'_4
K : Type u_1
Γ : K → Type u_2
L L' : ListBlank ((k : K) → Option (Γ k))
l : List ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.mk l)) =
    ListBlank.mk l

Proof state:
case h.e'_2.h.e'_4
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail) = L.tail

Tactic:
generalize ListBlank.tail L = L'

Result:
case h.e'_2.h.e'_4
K : Type u_1
Γ : K → Type u_2
L L' : ListBlank ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L') = L'
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem getElem?_zero_filterMap (f : α → Option β) (l : Array α) : (l.filterMap f)[0]? = l.findSome? f

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝ : List α
⊢ (filterMap f { toList := toList✝ })[0]? = findSome? f { toList := toList✝ }

Tactic:
simp [← List.head?_eq_getElem?]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
⊢ (filterMap f l)[0]? = findSome? f l

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝ : List α
⊢ (filterMap f { toList := toList✝ })[0]? = findSome? f { toList := toList✝ }
-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem adjoin_toSubmodule_le {s : Set A} {t : Submodule R A} :
    Subalgebra.toSubmodule (adjoin R s) ≤ t ↔ ↑(Submonoid.closure s) ⊆ (t : Set A)

Proof state:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
t : Submodule R A
⊢ Subalgebra.toSubmodule (adjoin R s) ≤ t ↔ ↑(Submonoid.closure s) ⊆ ↑t

Tactic:
rw [adjoin_eq_span, span_le]

Result:
no goals
-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem lie_le_right : ⁅I, N⁆ ≤ N

Proof state:
case intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
m : M
x : ↥I
n : ↥N
hn : ⁅↑x, ↑n⁆ = m
⊢ m ∈ ↑N

Tactic:
rw [← hn]

Result:
case intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
m : M
x : ↥I
n : ↥N
hn : ⁅↑x, ↑n⁆ = m
⊢ ⁅↑x, ↑n⁆ ∈ ↑N

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N⁆ ≤ N

Tactic:
rw [lieIdeal_oper_eq_span, lieSpan_le]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N

Tactic:
rintro m ⟨x, n, hn⟩

Result:
case intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
m : M
x : ↥I
n : ↥N
hn : ⁅↑x, ↑n⁆ = m
⊢ m ∈ ↑N

Proof state:
case intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
m : M
x : ↥I
n : ↥N
hn : ⁅↑x, ↑n⁆ = m
⊢ ⁅↑x, ↑n⁆ ∈ ↑N

Tactic:
exact N.lie_mem n.property

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem zpow {x : R} (hx : IsSelfAdjoint x) (n : ℤ) : IsSelfAdjoint (x ^ n)

Proof state:
R : Type u_1
inst✝¹ : Group R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
n : ℤ
⊢ IsSelfAdjoint (x ^ n)

Tactic:
simp only [isSelfAdjoint_iff, star_zpow, hx.star_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
@[simp] lemma memLp_measure_zero [TopologicalSpace ε] {f : α → ε} : MemLp f p (0 : Measure α)

Proof state:
α : Type u_1
ε : Type u_2
p : ℝ≥0∞
inst✝² : ENorm ε
inst✝¹ : MeasurableSpace α
inst✝ : TopologicalSpace ε
f : α → ε
⊢ MemLp f p 0

Tactic:
simp [MemLp]

Result:
no goals
-- Mathlib/Data/Tree/Traversable.lean
lemma traverse_eq_map_id (f : α → β) (t : Tree α) :
    t.traverse ((pure : β → Id β) ∘ f) = t.map f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
t : Tree α
⊢ traverse (pure ∘ f) t = pure (map f t)

Tactic:
induction t with
| nil => rw [traverse, map]
| node v l r hl hr =>
  rw [traverse, map, hl, hr, Function.comp_apply, map_pure, pure_seq, map_pure, pure_seq,
    map_pure]

Result:
no goals

Proof state:
case node
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : Tree α
hl : traverse (pure ∘ f) l = pure (map f l)
hr : traverse (pure ∘ f) r = pure (map f r)
⊢ traverse (pure ∘ f) (node v l r) = pure (map f (node v l r))

Tactic:
rw [traverse, map, hl, hr, Function.comp_apply, map_pure, pure_seq, map_pure, pure_seq,
  map_pure]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
t : Tree α
⊢ traverse (pure ∘ f) t = map f t

Tactic:
rw [← Id.pure_eq (t.map f)]

Result:
α : Type u_1
β : Type u_2
f : α → β
t : Tree α
⊢ traverse (pure ∘ f) t = pure (map f t)

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → β
⊢ traverse (pure ∘ f) nil = pure (map f nil)

Tactic:
rw [traverse, map]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean
theorem rightUnitor_naturality {X₁ X₂ : C} (f : X₁ ⟶ X₂) :
    tensorHom ℬ f (𝟙 𝒯.cone.pt) ≫ (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X₂ 𝒯.cone.pt).isLimit).hom =
      (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X₁ 𝒯.cone.pt).isLimit).hom ≫ f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ tensorHom ℬ f (𝟙 𝒯.cone.pt) ≫ (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X₂ 𝒯.cone.pt).isLimit).hom =
    (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X₁ 𝒯.cone.pt).isLimit).hom ≫ f

Tactic:
dsimp [tensorHom]

Result:
C : Type u
inst✝ : Category.{v, u} C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ (ℬ X₂ 𝒯.cone.pt).isLimit.lift
        (BinaryFan.mk (BinaryFan.fst (ℬ X₁ 𝒯.cone.pt).cone ≫ f) (BinaryFan.snd (ℬ X₁ 𝒯.cone.pt).cone ≫ 𝟙 𝒯.cone.pt)) ≫
      BinaryFan.fst (ℬ X₂ 𝒯.cone.pt).cone =
    BinaryFan.fst (ℬ X₁ 𝒯.cone.pt).cone ≫ f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ (ℬ X₂ 𝒯.cone.pt).isLimit.lift
        (BinaryFan.mk (BinaryFan.fst (ℬ X₁ 𝒯.cone.pt).cone ≫ f) (BinaryFan.snd (ℬ X₁ 𝒯.cone.pt).cone ≫ 𝟙 𝒯.cone.pt)) ≫
      BinaryFan.fst (ℬ X₂ 𝒯.cone.pt).cone =
    BinaryFan.fst (ℬ X₁ 𝒯.cone.pt).cone ≫ f

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive (attr := simp)]
lemma mul_right_iterate (a : M) : ∀ n : ℕ, (· * a)^[n] = (· * a ^ n)
  | 0 =>  by ext; simp
  | n + 1 => by ext; simp [pow_succ', mul_right_iterate]

Proof state:
M : Type u_4
inst✝ : Monoid M
a : M
n : ℕ
⊢ (fun x => x * a)^[n + 1] = fun x => x * a ^ (n + 1)

Tactic:
ext

Result:
case h
M : Type u_4
inst✝ : Monoid M
a : M
n : ℕ
x✝ : M
⊢ (fun x => x * a)^[n + 1] x✝ = x✝ * a ^ (n + 1)

Proof state:
case h
M : Type u_4
inst✝ : Monoid M
a x✝ : M
⊢ (fun x => x * a)^[0] x✝ = x✝ * a ^ 0

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_4
inst✝ : Monoid M
a : M
⊢ (fun x => x * a)^[0] = fun x => x * a ^ 0

Tactic:
ext

Result:
case h
M : Type u_4
inst✝ : Monoid M
a x✝ : M
⊢ (fun x => x * a)^[0] x✝ = x✝ * a ^ 0

Proof state:
case h
M : Type u_4
inst✝ : Monoid M
a : M
n : ℕ
x✝ : M
⊢ (fun x => x * a)^[n + 1] x✝ = x✝ * a ^ (n + 1)

Tactic:
simp [pow_succ', mul_right_iterate]

Result:
no goals
-- Mathlib/FieldTheory/IsAlgClosed/Basic.lean
theorem IsAlgClosed.splits_codomain {k K : Type*} [Field k] [IsAlgClosed k] [Field K] {f : K →+* k}
    (p : K[X]) : p.Splits f

Proof state:
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : IsAlgClosed k
inst✝ : Field K
f : K →+* k
p : K[X]
⊢ Splits f p

Tactic:
convert IsAlgClosed.splits (p.map f)

Result:
case a
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : IsAlgClosed k
inst✝ : Field K
f : K →+* k
p : K[X]
⊢ Splits f p ↔ Splits (RingHom.id k) (map f p)

Proof state:
case a
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : IsAlgClosed k
inst✝ : Field K
f : K →+* k
p : K[X]
⊢ Splits f p ↔ Splits (RingHom.id k) (map f p)

Tactic:
simp [splits_map_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Localization.lean
lemma W_iff_isIso_map_of_adjunction (adj : G ⊣ sheafToPresheaf J A)
    {P₁ P₂ : Cᵒᵖ ⥤ A} (f : P₁ ⟶ P₂) :
    J.W f ↔ IsIso (G.map f)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_3, u_2} A
G : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj : G ⊣ sheafToPresheaf J A
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
⊢ LeftBousfield.W (fun x => x ∈ Set.range (sheafToPresheaf J A).obj) f ↔ IsIso (G.map f)

Tactic:
exact LeftBousfield.W_iff_isIso_map adj f

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_3, u_2} A
G : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj : G ⊣ sheafToPresheaf J A
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
⊢ J.W f ↔ IsIso (G.map f)

Tactic:
rw [W_eq_W_range_sheafToPresheaf_obj]

Result:
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_3, u_2} A
G : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj : G ⊣ sheafToPresheaf J A
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
⊢ LeftBousfield.W (fun x => x ∈ Set.range (sheafToPresheaf J A).obj) f ↔ IsIso (G.map f)
-- Mathlib/Data/Nat/Log.lean
private lemma logC_aux {m b : ℕ} (hb : 1 < b) (hbm : b ≤ m) : m / (b * b) < m / b

Proof state:
m b : ℕ
hb : 1 < b
hbm : b ≤ m
⊢ m / (b * b) < m / b

Tactic:
have hb' : 0 < b := zero_lt_of_lt hb

Result:
m b : ℕ
hb : 1 < b
hbm : b ≤ m
hb' : 0 < b
⊢ m / (b * b) < m / b

Proof state:
m b : ℕ
hb : 1 < b
hbm : b ≤ m
hb' : 0 < b
⊢ m / b < m / b * b

Tactic:
exact (Nat.lt_mul_iff_one_lt_right (Nat.div_pos hbm hb')).2 hb

Result:
no goals

Proof state:
m b : ℕ
hb : 1 < b
hbm : b ≤ m
hb' : 0 < b
⊢ m / (b * b) < m / b

Tactic:
rw [div_lt_iff_lt_mul (Nat.mul_pos hb' hb'), ← Nat.mul_assoc, ← div_lt_iff_lt_mul hb']

Result:
m b : ℕ
hb : 1 < b
hbm : b ≤ m
hb' : 0 < b
⊢ m / b < m / b * b
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma ofHoms_v_comp_d (ψ : ∀ (p : ℤ), F.X p ⟶ G.X p) (p q q' : ℤ) (hpq : p + 0 = q) :
    (ofHoms ψ).v p q hpq ≫ G.d q q' = ψ p ≫ G.d p q'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q q' : ℤ
hpq✝ : p + 0 = q
hpq : p = q
⊢ (ofHoms ψ).v p q hpq✝ ≫ G.d q q' = ψ p ≫ G.d p q'

Tactic:
subst hpq

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q' : ℤ
hpq : p + 0 = p
⊢ (ofHoms ψ).v p p hpq ≫ G.d p q' = ψ p ≫ G.d p q'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q' : ℤ
hpq : p + 0 = p
⊢ (ofHoms ψ).v p p hpq ≫ G.d p q' = ψ p ≫ G.d p q'

Tactic:
rw [ofHoms_v]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q q' : ℤ
hpq : p + 0 = q
⊢ (ofHoms ψ).v p q hpq ≫ G.d q q' = ψ p ≫ G.d p q'

Tactic:
rw [add_zero] at hpq

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q q' : ℤ
hpq✝ : p + 0 = q
hpq : p = q
⊢ (ofHoms ψ).v p q hpq✝ ≫ G.d q q' = ψ p ≫ G.d p q'
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem leadingCoeff_prod' (h : (∏ i ∈ s, (f i).leadingCoeff) ≠ 0) :
    (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff

Proof state:
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (Multiset.map leadingCoeff (Multiset.map f s.val)).prod ≠ 0

Tactic:
simpa using h

Result:
no goals

Proof state:
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff

Tactic:
simpa using leadingCoeff_multiset_prod' (s.1.map f) (by simpa using h)

Result:
no goals
-- Mathlib/Order/MinMax.lean
theorem MonotoneOn.map_max (hf : MonotoneOn f s) (ha : a ∈ s) (hb : b ∈ s) : f (max a b) =
    max (f a) (f b)

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b : α
hf : MonotoneOn f s
ha : a ∈ s
hb : b ∈ s
⊢ f (a ⊔ b) = f a ⊔ f b

Tactic:
rcases le_total a b with h | h <;>
  simp only [max_eq_right, max_eq_left, hf ha hb, hf hb ha, h]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem nndist_eq_iSup {β : ι → Type*} [∀ i, PseudoMetricSpace (β i)] (x y : PiLp ∞ β) :
    nndist x y = ⨆ i, nndist (x i) (y i) :=
  -- Porting note: was `Subtype.ext`
  NNReal.eq <| by
    push_cast
    exact dist_eq_iSup _ _

Proof state:
ι : Type u_2
inst✝¹ : Fintype ι
β : ι → Type u_5
inst✝ : (i : ι) → PseudoMetricSpace (β i)
x y : PiLp ⊤ β
⊢ ↑(nndist x y) = ↑(⨆ i, nndist (x i) (y i))

Tactic:
push_cast

Result:
ι : Type u_2
inst✝¹ : Fintype ι
β : ι → Type u_5
inst✝ : (i : ι) → PseudoMetricSpace (β i)
x y : PiLp ⊤ β
⊢ dist x y = ⨆ i, dist (x i) (y i)

Proof state:
ι : Type u_2
inst✝¹ : Fintype ι
β : ι → Type u_5
inst✝ : (i : ι) → PseudoMetricSpace (β i)
x y : PiLp ⊤ β
⊢ dist x y = ⨆ i, dist (x i) (y i)

Tactic:
exact dist_eq_iSup _ _

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/DiagramLemmas/KernelCokernelComp.lean
@[reassoc (attr := simp)]
lemma inl_π : biprod.inl ≫ π f g = g ≫ cokernel.π (f ≫ g)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.inl ≫ π f g = g ≫ cokernel.π (f ≫ g)

Tactic:
simp [π]

Result:
no goals
-- Mathlib/Data/PFunctor/Multivariate/Basic.lean
theorem comp.mk_get (x : comp P Q α) : comp.mk (comp.get x) = x

Proof state:
n m : ℕ
P : MvPFunctor.{u} n
Q : Fin2 n → MvPFunctor.{u} m
α : TypeVec.{u} m
x : ↑(P.comp Q) α
⊢ mk (get x) = x

Tactic:
rfl

Result:
no goals