harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem coeff_apply_le (h : IsAdjoinRootMonic S f) (z : S) (i : ℕ) (hi : natDegree f ≤ i) :
    h.coeff z i = 0

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
hi : f.natDegree ≤ i
a✝ : Nontrivial R
⊢ { toFun := Polynomial.coeff, map_add' := ⋯ } (h.modByMonicHom z) i = 0

Tactic:
exact
  Polynomial.coeff_eq_zero_of_degree_lt
    ((degree_modByMonic_lt _ h.Monic).trans_le (Polynomial.degree_le_of_natDegree_le hi))

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
hi : f.natDegree ≤ i
⊢ h.coeff z i = 0

Tactic:
simp only [coeff, LinearMap.comp_apply, Finsupp.lcoeFun_apply, Finsupp.lmapDomain_apply,
  LinearEquiv.coe_coe, liftPolyₗ_apply, LinearMap.coe_mk, h.basis_repr]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
hi : f.natDegree ≤ i
⊢ { toFun := Polynomial.coeff, map_add' := ⋯ } (h.modByMonicHom z) i = 0

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
hi : f.natDegree ≤ i
⊢ { toFun := Polynomial.coeff, map_add' := ⋯ } (h.modByMonicHom z) i = 0

Tactic:
nontriviality R

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
hi : f.natDegree ≤ i
a✝ : Nontrivial R
⊢ { toFun := Polynomial.coeff, map_add' := ⋯ } (h.modByMonicHom z) i = 0
-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem mk_size (h) : (mk n h : Buckets α β).size = 0

Proof state:
α : Type u_1
β : Type u_2
n : Nat
h : 0 < n
⊢ (mk n h).size = 0

Tactic:
simp only [mk, mkArray, size_eq]

Result:
α : Type u_1
β : Type u_2
n : Nat
h : 0 < n
⊢ (List.map (fun x => x.toList.length) (List.replicate n AssocList.nil)).sum = 0

Proof state:
α : Type u_1
β : Type u_2
n : Nat
h : 0 < n
⊢ (List.map (fun x => x.toList.length) (List.replicate n AssocList.nil)).sum = 0

Tactic:
clear h

Result:
α : Type u_1
β : Type u_2
n : Nat
⊢ (List.map (fun x => x.toList.length) (List.replicate n AssocList.nil)).sum = 0

Proof state:
α : Type u_1
β : Type u_2
n : Nat
⊢ (List.map (fun x => x.toList.length) (List.replicate n AssocList.nil)).sum = 0

Tactic:
induction n <;> simp_all [List.replicate_succ]

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Basic.lean
theorem map_div_le_add : f (x / y) ≤ f x + f y

Proof state:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f (x * y⁻¹) ≤ f x + f y⁻¹

Tactic:
exact map_mul_le_add _ _ _

Result:
no goals

Proof state:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f (x / y) ≤ f x + f y

Tactic:
rw [div_eq_mul_inv, ← map_inv_eq_map f y]

Result:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f (x * y⁻¹) ≤ f x + f y⁻¹
-- Mathlib/Data/Finsupp/NeLocus.lean
theorem subset_mapRange_neLocus [DecidableEq N] [Zero N] [DecidableEq M] [Zero M] (f g : α →₀ N)
    {F : N → M} (F0 : F 0 = 0) : (f.mapRange F F0).neLocus (g.mapRange F F0) ⊆ f.neLocus g :=
  fun x => by simpa only [mem_neLocus, mapRange_apply, not_imp_not] using congr_arg F

Proof state:
α : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq N
inst✝² : Zero N
inst✝¹ : DecidableEq M
inst✝ : Zero M
f g : α →₀ N
F : N → M
F0 : F 0 = 0
x : α
⊢ x ∈ (mapRange F F0 f).neLocus (mapRange F F0 g) → x ∈ f.neLocus g

Tactic:
simpa only [mem_neLocus, mapRange_apply, not_imp_not] using congr_arg F

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
lemma iIndepFun.comp {β γ : ι → Type*} {mβ : ∀ i, MeasurableSpace (β i)}
    {mγ : ∀ i, MeasurableSpace (γ i)} {f : ∀ i, Ω → β i}
    (h : iIndepFun mβ f κ μ) (g : ∀ i, β i → γ i) (hg : ∀ i, Measurable (g i)) :
    iIndepFun mγ (fun i ↦ g i ∘ f i) κ μ

Proof state:
case h
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
t : Finset ι
s : (i : ι) → Set (γ i)
hs : ∀ i ∈ t, MeasurableSet (s i)
this :
  ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ t, f i ⁻¹' (fun i => g i ⁻¹' s i) i) = ∏ i ∈ t, (κ a) (f i ⁻¹' (fun i => g i ⁻¹' s i) i)
a : α
ha : (κ a) (⋂ i ∈ t, f i ⁻¹' (g i ⁻¹' s i)) = ∏ i ∈ t, (κ a) (f i ⁻¹' (g i ⁻¹' s i))
⊢ (κ a) (⋂ i ∈ t, f i ⁻¹' (g i ⁻¹' s i)) = ∏ x ∈ t, (κ a) (f x ⁻¹' (g x ⁻¹' s x))

Tactic:
exact ha

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean
theorem HasStrictDerivAt.clog {f : ℂ → ℂ} {f' x : ℂ} (h₁ : HasStrictDerivAt f f' x)
    (h₂ : f x ∈ slitPlane) : HasStrictDerivAt (fun t => log (f t)) (f' / f x) x

Proof state:
f : ℂ → ℂ
f' x : ℂ
h₁ : HasStrictDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasStrictDerivAt (fun t => log (f t)) ((f x)⁻¹ * f') x

Tactic:
exact (hasStrictDerivAt_log h₂).comp x h₁

Result:
no goals

Proof state:
f : ℂ → ℂ
f' x : ℂ
h₁ : HasStrictDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasStrictDerivAt (fun t => log (f t)) (f' / f x) x

Tactic:
rw [div_eq_inv_mul]

Result:
f : ℂ → ℂ
f' x : ℂ
h₁ : HasStrictDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasStrictDerivAt (fun t => log (f t)) ((f x)⁻¹ * f') x
-- Mathlib/Topology/UnitInterval.lean
theorem symm_lt_comm {i j : I} : σ i < j ↔ σ j < i

Proof state:
i j : ↑I
⊢ σ i < j ↔ σ j < i

Tactic:
rw [← symm_lt_symm, symm_symm]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma isUnit_cfc_iff (f : R → R) (a : A) (hf : ContinuousOn f (spectrum R a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ IsUnit (cfc f a) ↔ ∀ x ∈ spectrum R a, f x ≠ 0

Tactic:
rw [← spectrum.zero_not_mem_iff R, cfc_map_spectrum ..]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ 0 ∉ f '' spectrum R a ↔ ∀ x ∈ spectrum R a, f x ≠ 0

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ 0 ∉ f '' spectrum R a ↔ ∀ x ∈ spectrum R a, f x ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Functor/OfSequence.lean
@[reassoc]
lemma map_comp (i j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k) :
    map f i k (hij.trans hjk) = map f i j hij ≫ map f j k hjk

Proof state:
case succ.succ.succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
i : ℕ
hi :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k),
    map f i k ⋯ = map f i j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
j k : ℕ
hij✝ : i + 1 ≤ j + 1
hjk✝ : j + 1 ≤ k + 1
⊢ map f (i + 1) (k + 1) ⋯ = map f (i + 1) (j + 1) hij✝ ≫ map f (j + 1) (k + 1) hjk✝

Tactic:
exact hi _ j k (by omega) (by omega)

Result:
no goals

Proof state:
case zero.succ.succ.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ 0) (hjk : 0 ≤ k),
    map f 0 k ⋯ = map f 0 0 hij ≫ map f 0 k hjk
hij : 0 ≤ 0 + 1
hjk : 0 + 1 ≤ 0 + 1
⊢ map f 0 (0 + 1) ⋯ = map f 0 (0 + 1) hij ≫ map f (0 + 1) (0 + 1) hjk

Tactic:
rw [map_id, comp_id]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
lemma IsLimit.hom_ext (hK : IsLimit K) {T : C} {f g : T ⟶ K.pt}
    (h : ∀ a, f ≫ K.ι a = g ≫ K.ι a) : f = g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
⊢ ∀ (j : WalkingMulticospan J), f ≫ K.π.app j = g ≫ K.π.app j

Tactic:
rintro (_|b)

Result:
case left
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
a✝ : J.L
⊢ f ≫ K.π.app (WalkingMulticospan.left a✝) = g ≫ K.π.app (WalkingMulticospan.left a✝)

case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
b : J.R
⊢ f ≫ K.π.app (WalkingMulticospan.right b) = g ≫ K.π.app (WalkingMulticospan.right b)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
⊢ f = g

Tactic:
apply hK.hom_ext

Result:
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
⊢ ∀ (j : WalkingMulticospan J), f ≫ K.π.app j = g ≫ K.π.app j

Proof state:
case left
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
a✝ : J.L
⊢ f ≫ K.π.app (WalkingMulticospan.left a✝) = g ≫ K.π.app (WalkingMulticospan.left a✝)

Tactic:
apply h

Result:
no goals

Proof state:
case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
b : J.R
⊢ f ≫ K.π.app (WalkingMulticospan.right b) = g ≫ K.π.app (WalkingMulticospan.right b)

Tactic:
rw [app_right_eq_ι_comp_fst, reassoc_of% h]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Split.lean
theorem eqId_iff_mono : A.EqId ↔ Mono A.e

Proof state:
case mp
Δ : SimplexCategoryᵒᵖ
⊢ Mono (id Δ).e

Tactic:
dsimp only [id, e]

Result:
case mp
Δ : SimplexCategoryᵒᵖ
⊢ Mono (𝟙 (unop Δ))

Proof state:
case mp
Δ : SimplexCategoryᵒᵖ
⊢ Mono (𝟙 (unop Δ))

Tactic:
infer_instance

Result:
no goals

Proof state:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.EqId → Mono A.e

Tactic:
intro h

Result:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.EqId
⊢ Mono A.e

Proof state:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ Mono A.e

Tactic:
subst h

Result:
case mp
Δ : SimplexCategoryᵒᵖ
⊢ Mono (id Δ).e

Proof state:
case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ Mono A.e → A.EqId

Tactic:
intro h

Result:
case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : Mono A.e
⊢ A.EqId

Proof state:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.EqId ↔ Mono A.e

Tactic:
constructor

Result:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.EqId → Mono A.e

case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ Mono A.e → A.EqId

Proof state:
case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : Mono A.e
⊢ (unop Δ).len ≤ (unop A.fst).len

Tactic:
exact len_le_of_mono h

Result:
no goals

Proof state:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.EqId
⊢ Mono A.e

Tactic:
dsimp at h

Result:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ Mono A.e

Proof state:
case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : Mono A.e
⊢ A.EqId

Tactic:
rw [eqId_iff_len_le]

Result:
case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : Mono A.e
⊢ (unop Δ).len ≤ (unop A.fst).len
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
theorem trunc_trunc_pow (f : R⟦X⟧) (n a : ℕ) :
    trunc n ((trunc n f : R⟦X⟧) ^ a) = trunc n (f ^ a)

Proof state:
R : Type u_2
inst✝ : CommSemiring R
f : R⟦X⟧
n a : ℕ
⊢ trunc n (↑(trunc n f) ^ a) = trunc n (f ^ a)

Tactic:
induction a with
| zero =>
  rw [pow_zero, pow_zero]
| succ a ih =>
  rw [_root_.pow_succ', _root_.pow_succ', trunc_trunc_mul,
    ← trunc_trunc_mul_trunc, ih, trunc_trunc_mul_trunc]

Result:
no goals

Proof state:
case zero
R : Type u_2
inst✝ : CommSemiring R
f : R⟦X⟧
n : ℕ
⊢ trunc n (↑(trunc n f) ^ 0) = trunc n (f ^ 0)

Tactic:
rw [pow_zero, pow_zero]

Result:
no goals

Proof state:
case succ
R : Type u_2
inst✝ : CommSemiring R
f : R⟦X⟧
n a : ℕ
ih : trunc n (↑(trunc n f) ^ a) = trunc n (f ^ a)
⊢ trunc n (↑(trunc n f) ^ (a + 1)) = trunc n (f ^ (a + 1))

Tactic:
rw [_root_.pow_succ', _root_.pow_succ', trunc_trunc_mul,
  ← trunc_trunc_mul_trunc, ih, trunc_trunc_mul_trunc]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[gcongr, bound]
lemma div_lt_div_of_pos_right (h : a < b) (hc : 0 < c) : a / c < b / c

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosStrictMono G₀
h : a < b
hc : 0 < c
⊢ a / c < b / c

Tactic:
rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]

Result:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosStrictMono G₀
h : a < b
hc : 0 < c
⊢ a * (1 / c) < b * (1 / c)

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosStrictMono G₀
h : a < b
hc : 0 < c
⊢ a * (1 / c) < b * (1 / c)

Tactic:
exact mul_lt_mul_of_pos_right h (one_div_pos.2 hc)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem BinaryCofan.mono_inr_of_isVanKampen [HasInitial C] {X Y : C} {c : BinaryCofan X Y}
    (h : IsVanKampenColimit c) : Mono c.inr

Proof state:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ mapPair (initial.to X) (𝟙 Y) ≫ c.ι =
    (BinaryCofan.mk (initial.to Y) (𝟙 Y)).ι ≫ (Functor.const (Discrete WalkingPair)).map c.inr

Tactic:
ext ⟨⟨⟩⟩ <;> dsimp

Result:
case refine_1.w.h.mk.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ initial.to X ≫ c.inl = initial.to Y ≫ c.inr

Proof state:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsColimit (BinaryCofan.mk (initial.to Y) (𝟙 Y))

Tactic:
exact ((BinaryCofan.isColimit_iff_isIso_inr initialIsInitial _).mpr (by
  dsimp
  infer_instance)).some

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsIso (𝟙 Y)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsIso (BinaryCofan.mk (initial.to Y) (𝟙 Y)).inr

Tactic:
dsimp

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsIso (𝟙 Y)

Proof state:
case refine_1.w.h.mk.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ initial.to X ≫ c.inl = initial.to Y ≫ c.inr

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ Mono c.inr

Tactic:
refine PullbackCone.mono_of_isLimitMkIdId _ (IsPullback.isLimit ?_)

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsPullback (𝟙 ((pair X Y).obj { as := WalkingPair.right })) (𝟙 ((pair X Y).obj { as := WalkingPair.right })) c.inr
    c.inr

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsPullback (𝟙 ((pair X Y).obj { as := WalkingPair.right })) (𝟙 ((pair X Y).obj { as := WalkingPair.right })) c.inr
    c.inr

Tactic:
refine (h (BinaryCofan.mk (initial.to Y) (𝟙 Y)) (mapPair (initial.to X) (𝟙 Y)) c.inr ?_
    (mapPair_equifibered _)).mp ⟨?_⟩ ⟨WalkingPair.right⟩

Result:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ mapPair (initial.to X) (𝟙 Y) ≫ c.ι =
    (BinaryCofan.mk (initial.to Y) (𝟙 Y)).ι ≫ (Functor.const (Discrete WalkingPair)).map c.inr

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
X Y : C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsColimit (BinaryCofan.mk (initial.to Y) (𝟙 Y))
-- Mathlib/Algebra/Homology/Opposite.lean
@[reassoc (attr := simp)]
lemma fromOpcycles_op_cyclesOpIso_inv :
    (K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles j i

Proof state:
ι : Type u_1
V : Type u_2
inst✝² : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
⊢ (K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles j i

Tactic:
by_cases hij : c.Rel i j

Result:
case pos
ι : Type u_1
V : Type u_2
inst✝² : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : c.Rel i j
⊢ (K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles j i

case neg
ι : Type u_1
V : Type u_2
inst✝² : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : ¬c.Rel i j
⊢ (K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles j i

Proof state:
case neg
ι : Type u_1
V : Type u_2
inst✝² : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : ¬c.Rel i j
⊢ (K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles j i

Tactic:
rw [K.op.toCycles_eq_zero hij, K.fromOpcycles_eq_zero hij, op_zero, zero_comp]

Result:
no goals

Proof state:
case pos
ι : Type u_1
V : Type u_2
inst✝² : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : c.Rel i j
⊢ (K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles j i

Tactic:
obtain rfl := c.next_eq' hij

Result:
case pos
ι : Type u_1
V : Type u_2
inst✝² : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
hij : c.Rel i (c.next i)
⊢ (K.fromOpcycles i (c.next i)).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles (c.next i) i

Proof state:
case pos
ι : Type u_1
V : Type u_2
inst✝² : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
hij : c.Rel i (c.next i)
⊢ (K.fromOpcycles i (c.next i)).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles (c.next i) i

Tactic:
exact (K.sc i).fromOpcycles_op_cyclesOpIso_inv

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem getElem_mapFinIdx {as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} {i : Nat} {h} :
    (as.mapFinIdx f)[i] = f i (as[i]'(by simp at h; omega)) (by simp at h; omega)

Proof state:
α : Type u_1
β : Type u_2
as : List α
f : (i : Nat) → α → i < as.length → β
i : Nat
h : i < (as.mapFinIdx f).length
⊢ (as.mapFinIdx f)[i] = f i as[i] ⋯

Tactic:
simp [mapFinIdx, getElem_mapFinIdx_go]

Result:
no goals

Proof state:
α : Type ?u.15550
β : Type ?u.15586
as : List α
f : (i : Nat) → α → i < as.length → β
i : Nat
h : i < (as.mapFinIdx f).length
⊢ i < as.length

Tactic:
simp at h

Result:
α : Type ?u.15550
β : Type ?u.15586
as : List α
f : (i : Nat) → α → i < as.length → β
i : Nat
h : i < as.length
⊢ i < as.length

Proof state:
α : Type ?u.15550
β : Type ?u.15586
as : List α
f : (i : Nat) → α → i < as.length → β
i : Nat
h : i < as.length
⊢ i < as.length

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
theorem EqualizerCondition.mk (P : Cᵒᵖ ⥤ Type*)
    (hP : ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [HasPullback π π], Function.Bijective
    (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π)
    pullback.condition)) : EqualizerCondition P

Proof state:
C : Type u_1
inst✝¹ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
hP : Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)
⊢ Nonempty (IsLimit (Fork.ofι (P.map π.op) ⋯))

Tactic:
rw [Types.type_equalizer_iff_unique]

Result:
C : Type u_1
inst✝¹ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
hP : Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)
⊢ ∀ (y : P.obj (op X)), P.map c.fst.op y = P.map c.snd.op y → ∃! x, P.map π.op x = y
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem compProd_eq_sum_compProd (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ)
    [IsSFiniteKernel η] : κ ⊗ₖ η = Kernel.sum fun n => Kernel.sum fun m => seq κ n ⊗ₖ seq η m

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
⊢ κ ⊗ₖ η = Kernel.sum fun n => Kernel.sum fun m => κ.seq n ⊗ₖ η.seq m

Tactic:
ext a s hs

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η) a) s = ((Kernel.sum fun n => Kernel.sum fun m => κ.seq n ⊗ₖ η.seq m) a) s

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η) a) s = ∑' (n : ℕ) (n_1 : ℕ), ((κ.seq n ⊗ₖ η.seq n_1) a) s

Tactic:
rw [compProd_eq_tsum_compProd κ η a hs]

Result:
no goals

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η) a) s = ((Kernel.sum fun n => Kernel.sum fun m => κ.seq n ⊗ₖ η.seq m) a) s

Tactic:
simp_rw [Kernel.sum_apply' _ a hs]

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η) a) s = ∑' (n : ℕ) (n_1 : ℕ), ((κ.seq n ⊗ₖ η.seq n_1) a) s