harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContDiff.div {f g : E → 𝕜} {n} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g)
    (h0 : ∀ x, g x ≠ 0) : ContDiff 𝕜 n fun x => f x / g x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type uE
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : E → 𝕜
n : WithTop ℕ∞
hf : ContDiff 𝕜 n f
hg : ContDiff 𝕜 n g
h0 : ∀ (x : E), g x ≠ 0
⊢ ContDiff 𝕜 n fun x => f x / g x

Tactic:
simp only [contDiff_iff_contDiffAt] at *

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type uE
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : E → 𝕜
n : WithTop ℕ∞
h0 : ∀ (x : E), g x ≠ 0
hf : ∀ (x : E), ContDiffAt 𝕜 n f x
hg : ∀ (x : E), ContDiffAt 𝕜 n g x
⊢ ∀ (x : E), ContDiffAt 𝕜 n (fun x => f x / g x) x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type uE
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : E → 𝕜
n : WithTop ℕ∞
h0 : ∀ (x : E), g x ≠ 0
hf : ∀ (x : E), ContDiffAt 𝕜 n f x
hg : ∀ (x : E), ContDiffAt 𝕜 n g x
⊢ ∀ (x : E), ContDiffAt 𝕜 n (fun x => f x / g x) x

Tactic:
exact fun x => (hf x).div (hg x) (h0 x)

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem fderiv_const_sub (c : F) : fderiv 𝕜 (fun y => c - f y) x = -fderiv 𝕜 f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
c : F
⊢ fderiv 𝕜 (fun y => c - f y) x = -fderiv 𝕜 f x

Tactic:
simp only [← fderivWithin_univ, fderivWithin_const_sub uniqueDiffWithinAt_univ]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem _root_.IsClosed.analyticSet [PolishSpace α] {s : Set α} (hs : IsClosed s) :
    AnalyticSet s

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this : PolishSpace ↑s
⊢ AnalyticSet s

Tactic:
rw [← @Subtype.range_val α s]

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this : PolishSpace ↑s
⊢ AnalyticSet (range Subtype.val)

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this : PolishSpace ↑s
⊢ AnalyticSet (range Subtype.val)

Tactic:
exact analyticSet_range_of_polishSpace continuous_subtype_val

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
⊢ AnalyticSet s

Tactic:
haveI : PolishSpace s := hs.polishSpace

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this : PolishSpace ↑s
⊢ AnalyticSet s
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
@[simp]
lemma add_lt_top [LT α] : x + y < ⊤ ↔ x < ⊤ ∧ y < ⊤

Proof state:
α : Type u
inst✝¹ : Add α
x y : WithTop α
inst✝ : LT α
⊢ x + y < ⊤ ↔ x < ⊤ ∧ y < ⊤

Tactic:
simp_rw [WithTop.lt_top_iff_ne_top, add_ne_top]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x

Proof state:
case nil
α✝ : Type u_1
p : α✝ → Bool
x : α✝
⊢ x ∈ filter p [] ↔ x ∈ [] ∧ p x = true

Tactic:
simp [filter]

Result:
no goals

Proof state:
case neg
α✝ : Type u_1
p : α✝ → Bool
x a : α✝
as : List α✝
ih : x ∈ filter p as ↔ x ∈ as ∧ p x = true
h : ¬p a = true
⊢ x ∈ filter p (a :: as) ↔ x ∈ a :: as ∧ p x = true

Tactic:
simp_all [or_and_right]

Result:
no goals

Proof state:
case pos
α✝ : Type u_1
p : α✝ → Bool
x a : α✝
as : List α✝
ih : x ∈ filter p as ↔ x ∈ as ∧ p x = true
h : p a = true
⊢ x ∈ filter p (a :: as) ↔ x ∈ a :: as ∧ p x = true

Tactic:
simp_all [or_and_left]

Result:
no goals

Proof state:
case cons
α✝ : Type u_1
p : α✝ → Bool
x a : α✝
as : List α✝
ih : x ∈ filter p as ↔ x ∈ as ∧ p x = true
⊢ x ∈ filter p (a :: as) ↔ x ∈ a :: as ∧ p x = true

Tactic:
by_cases h : p a

Result:
case pos
α✝ : Type u_1
p : α✝ → Bool
x a : α✝
as : List α✝
ih : x ∈ filter p as ↔ x ∈ as ∧ p x = true
h : p a = true
⊢ x ∈ filter p (a :: as) ↔ x ∈ a :: as ∧ p x = true

case neg
α✝ : Type u_1
p : α✝ → Bool
x a : α✝
as : List α✝
ih : x ∈ filter p as ↔ x ∈ as ∧ p x = true
h : ¬p a = true
⊢ x ∈ filter p (a :: as) ↔ x ∈ a :: as ∧ p x = true
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.of_isZero (ctx : Context) {p : Poly} (h : isZero p = true) : p.denote ctx = 0

Proof state:
ctx : Context
p : Poly
h :
  (match p with
    | [] => true
    | x => false) =
    true
⊢ denote ctx p = 0

Tactic:
split at h

Result:
case h_1
ctx : Context
p✝ : Poly
h : true = true
⊢ denote ctx [] = 0

case h_2
ctx : Context
p p✝ : Poly
x✝ : p = [] → False
h : false = true
⊢ denote ctx p = 0

Proof state:
case h_2
ctx : Context
p p✝ : Poly
x✝ : p = [] → False
h : false = true
⊢ denote ctx p = 0

Tactic:
contradiction

Result:
no goals

Proof state:
case h_1
ctx : Context
p✝ : Poly
h : true = true
⊢ denote ctx [] = 0

Tactic:
simp

Result:
no goals

Proof state:
ctx : Context
p : Poly
h : p.isZero = true
⊢ denote ctx p = 0

Tactic:
simp [isZero] at h

Result:
ctx : Context
p : Poly
h :
  (match p with
    | [] => true
    | x => false) =
    true
⊢ denote ctx p = 0
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma IsRatCondKernelCDFAux.bddBelow_range (hf : IsRatCondKernelCDFAux f κ ν) (a : α) :
    ∀ᵐ t ∂(ν a), ∀ q : ℚ, BddBelow (range fun (r : Ioi q) ↦ f (a, t) r)

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
c : β
hc : ∀ (q : ℚ), 0 ≤ f (a, c) q
⊢ ∀ (q : ℚ), BddBelow (range fun r => f (a, c) ↑r)

Tactic:
refine fun q ↦ ⟨0, ?_⟩

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
c : β
hc : ∀ (q : ℚ), 0 ≤ f (a, c) q
q : ℚ
⊢ 0 ∈ lowerBounds (range fun r => f (a, c) ↑r)

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
c : β
hc : ∀ (q : ℚ), 0 ≤ f (a, c) q
q : ℚ
⊢ 0 ∈ lowerBounds (range fun r => f (a, c) ↑r)

Tactic:
simp [mem_lowerBounds, hc]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
⊢ ∀ᵐ (t : β) ∂ν a, ∀ (q : ℚ), BddBelow (range fun r => f (a, t) ↑r)

Tactic:
filter_upwards [hf.nonneg a] with c hc

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
c : β
hc : ∀ (q : ℚ), 0 ≤ f (a, c) q
⊢ ∀ (q : ℚ), BddBelow (range fun r => f (a, c) ↑r)
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_univ_get [CommMonoid α] (l : List α) : ∏ i : Fin l.length, l[i.1] = l.prod

Proof state:
α : Type u_1
inst✝ : CommMonoid α
l : List α
⊢ ∏ i : Fin l.length, l[↑i] = l.prod

Tactic:
simp [Finset.prod_eq_multiset_prod]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem unop_inl {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) :
    c.unop.inl = c.fst.unop

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ c.unop.inl = c.fst.unop

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem is_compatible_of_exists_amalgamation (x : FamilyOfElements P R)
    (h : ∃ t, x.IsAmalgamation t) : x.Compatible

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
h : ∃ t, x.IsAmalgamation t
⊢ x.Compatible

Tactic:
obtain ⟨t, ht⟩ := h

Result:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
⊢ x.Compatible

Proof state:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map g₁.op (x f₁ h₁) = P.map g₂.op (x f₂ h₂)

Tactic:
rw [← ht _ h₁, ← ht _ h₂, ← FunctorToTypes.map_comp_apply, ← op_comp, comm]

Result:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map (g₂ ≫ f₂).op t = P.map g₂.op (P.map f₂.op t)

Proof state:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
⊢ x.Compatible

Tactic:
intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ comm

Result:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map g₁.op (x f₁ h₁) = P.map g₂.op (x f₂ h₂)

Proof state:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map (g₂ ≫ f₂).op t = P.map g₂.op (P.map f₂.op t)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma cyclesIsoSc'_inv_iCycles :
    (K.cyclesIsoSc' i j k hi hk).inv ≫ K.iCycles j = (K.sc' i j k).iCycles

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.sc' i j k).iCycles ≫ ((natIsoSc' C c i j k hi hk).inv.app K).τ₂ = (K.sc' i j k).iCycles

Tactic:
apply comp_id

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.cyclesIsoSc' i j k hi hk).inv ≫ K.iCycles j = (K.sc' i j k).iCycles

Tactic:
dsimp [cyclesIsoSc']

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ ShortComplex.cyclesMap ((natIsoSc' C c i j k hi hk).inv.app K) ≫ K.iCycles j = (K.sc' i j k).iCycles

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ ShortComplex.cyclesMap ((natIsoSc' C c i j k hi hk).inv.app K) ≫ K.iCycles j = (K.sc' i j k).iCycles

Tactic:
erw [ShortComplex.cyclesMap_i]

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.sc' i j k).iCycles ≫ ((natIsoSc' C c i j k hi hk).inv.app K).τ₂ = (K.sc' i j k).iCycles
-- Mathlib/CategoryTheory/EqToHom.lean
theorem eqToIso_map (F : C ⥤ D) {X Y : C} (p : X = Y) :
    F.mapIso (eqToIso p) = eqToIso (congr_arg F.obj p)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
p : X = Y
⊢ F.mapIso (eqToIso p) = eqToIso ⋯

Tactic:
ext

Result:
case w
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
p : X = Y
⊢ (F.mapIso (eqToIso p)).hom = (eqToIso ⋯).hom

Proof state:
case w
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
p : X = Y
⊢ (F.mapIso (eqToIso p)).hom = (eqToIso ⋯).hom

Tactic:
cases p

Result:
case w.refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ (F.mapIso (eqToIso ⋯)).hom = (eqToIso ⋯).hom

Proof state:
case w.refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ (F.mapIso (eqToIso ⋯)).hom = (eqToIso ⋯).hom

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Congruence/Defs.lean
theorem mapOfSurjective_eq_mapGen {c : Con M} {f : M → N} (H : ∀ x y, f (x * y) = f x * f y)
    (h : mulKer f H ≤ c) (hf : Surjective f) : c.mapGen f = c.mapOfSurjective f H h hf

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
c : Con M
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
h : mulKer f H ≤ c
hf : Surjective f
⊢ c.mapGen f = conGen ⇑(c.mapOfSurjective f H h hf)

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
c : Con M
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
h : mulKer f H ≤ c
hf : Surjective f
⊢ c.mapGen f = c.mapOfSurjective f H h hf

Tactic:
rw [← conGen_of_con (c.mapOfSurjective f H h hf)]

Result:
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
c : Con M
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
h : mulKer f H ≤ c
hf : Surjective f
⊢ c.mapGen f = conGen ⇑(c.mapOfSurjective f H h hf)
-- Mathlib/Data/Set/Subsingleton.lean
theorem univ_eq_true_false : univ = ({True, False} : Set Prop) :=
  Eq.symm <| eq_univ_of_forall fun x => by
    rw [mem_insert_iff, mem_singleton_iff]
    exact Classical.propComplete x

Proof state:
x : Prop
⊢ x = True ∨ x = False

Tactic:
exact Classical.propComplete x

Result:
no goals

Proof state:
x : Prop
⊢ x ∈ {True, False}

Tactic:
rw [mem_insert_iff, mem_singleton_iff]

Result:
x : Prop
⊢ x = True ∨ x = False
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc]
lemma cyclesMap_comp : cyclesMap (φ ≫ ψ) i = cyclesMap φ i ≫ cyclesMap ψ i

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
⊢ ShortComplex.cyclesMap ((shortComplexFunctor C c i).map (φ ≫ ψ)) =
    ShortComplex.cyclesMap ((shortComplexFunctor C c i).map φ) ≫
      ShortComplex.cyclesMap ((shortComplexFunctor C c i).map ψ)

Tactic:
rw [Functor.map_comp, ShortComplex.cyclesMap_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
⊢ cyclesMap (φ ≫ ψ) i = cyclesMap φ i ≫ cyclesMap ψ i

Tactic:
dsimp [cyclesMap]

Result:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
⊢ ShortComplex.cyclesMap ((shortComplexFunctor C c i).map (φ ≫ ψ)) =
    ShortComplex.cyclesMap ((shortComplexFunctor C c i).map φ) ≫
      ShortComplex.cyclesMap ((shortComplexFunctor C c i).map ψ)
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem _root_.Nat.map_cast_int_atTop : map ((↑) : ℕ → ℤ) atTop = atTop

Proof state:
⊢ map Nat.cast atTop = atTop

Tactic:
refine map_atTop_eq_of_gc_preorder (fun _ _ ↦ Int.ofNat_le.2) 0 fun n hn ↦ ?_

Result:
n : ℤ
hn : n ≥ 0
⊢ ∃ x, ↑x = n ∧ ∀ (a : ℕ), ↑a ≤ n ↔ a ≤ x

Proof state:
n : ℤ
hn : n ≥ 0
⊢ ∃ x, ↑x = n ∧ ∀ (a : ℕ), ↑a ≤ n ↔ a ≤ x

Tactic:
lift n to ℕ using hn

Result:
case intro
n : ℕ
⊢ ∃ x, ↑x = ↑n ∧ ∀ (a : ℕ), ↑a ≤ ↑n ↔ a ≤ x

Proof state:
case intro
n : ℕ
⊢ ∃ x, ↑x = ↑n ∧ ∀ (a : ℕ), ↑a ≤ ↑n ↔ a ≤ x

Tactic:
exact ⟨n, rfl, fun _ ↦ Int.ofNat_le⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem all_iff_forall {p : α → Bool} {xs : Vector α n} :
    xs.all p ↔ ∀ (i : Nat) (_ : i < n), p xs[i]

Proof state:
α : Type u_1
n : Nat
p : α → Bool
xs : Vector α n
⊢ xs.all p = true ↔ ∀ (i : Nat) (x : i < n), p xs[i] = true

Tactic:
rcases xs with ⟨xs, rfl⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ { toArray := xs, size_toArray := ⋯ }.all p = true ↔
    ∀ (i : Nat) (x : i < xs.size), p { toArray := xs, size_toArray := ⋯ }[i] = true

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ { toArray := xs, size_toArray := ⋯ }.all p = true ↔
    ∀ (i : Nat) (x : i < xs.size), p { toArray := xs, size_toArray := ⋯ }[i] = true

Tactic:
simp [Array.all_iff_forall]

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isCodetector_iff_reflectsIsomorphisms_yoneda_obj (G : C) :
    IsCodetector G ↔ (yoneda.obj G).ReflectsIsomorphisms

Proof state:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (yoneda.obj G).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso ((yoneda.obj G).map f.op)

Tactic:
rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique]

Result:
no goals

Proof state:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (yoneda.obj G).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f

Tactic:
rw [← isIso_op_iff]

Result:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (yoneda.obj G).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f.op

Proof state:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsCodetector G
A✝ B✝ : Cᵒᵖ
f : A✝ ⟶ B✝
hf : IsIso ((yoneda.obj G).map f)
⊢ IsIso f

Tactic:
refine (isIso_unop_iff _).1 (hG.def _ ?_)

Result:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsCodetector G
A✝ B✝ : Cᵒᵖ
f : A✝ ⟶ B✝
hf : IsIso ((yoneda.obj G).map f)
⊢ ∀ (h : unop B✝ ⟶ G), ∃! h', f.unop ≫ h' = h

Proof state:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsCodetector G
A✝ B✝ : Cᵒᵖ
f : A✝ ⟶ B✝
hf : IsIso ((yoneda.obj G).map f)
⊢ ∀ (h : unop B✝ ⟶ G), ∃! h', f.unop ≫ h' = h

Tactic:
rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf

Result:
no goals

Proof state:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (yoneda.obj G).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f.op

Tactic:
suffices IsIso ((yoneda.obj G).map f.op) by
  exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (yoneda.obj G) _ h

Result:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (yoneda.obj G).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso ((yoneda.obj G).map f.op)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
⊢ IsCodetector G ↔ (yoneda.obj G).ReflectsIsomorphisms

Tactic:
refine ⟨fun hG => ⟨fun f hf => ?_⟩, fun h => (isCodetector_def _).2 fun X Y f hf => ?_⟩

Result:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsCodetector G
A✝ B✝ : Cᵒᵖ
f : A✝ ⟶ B✝
hf : IsIso ((yoneda.obj G).map f)
⊢ IsIso f

case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (yoneda.obj G).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (yoneda.obj G).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
this : IsIso ((yoneda.obj G).map f.op)
⊢ IsIso f.op

Tactic:
exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (yoneda.obj G) _ h

Result:
no goals
-- Mathlib/FieldTheory/Cardinality.lean
theorem Fintype.nonempty_field_iff {α} [Fintype α] : Nonempty (Field α) ↔ IsPrimePow ‖α‖

Proof state:
α : Type u_1
inst✝ : Fintype α
⊢ IsPrimePow ‖α‖ → Nonempty (Field α)

Tactic:
rintro ⟨p, n, hp, hn, hα⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Prime p
hn : 0 < n
hα : p ^ n = ‖α‖
⊢ Nonempty (Field α)

Proof state:
α : Type u_1
inst✝ : Fintype α
⊢ Nonempty (Field α) ↔ IsPrimePow ‖α‖

Tactic:
refine ⟨fun ⟨h⟩ => Fintype.isPrimePow_card_of_field, ?_⟩

Result:
α : Type u_1
inst✝ : Fintype α
⊢ IsPrimePow ‖α‖ → Nonempty (Field α)

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Prime p
hn : 0 < n
hα : p ^ n = ‖α‖
this : Fact (Nat.Prime p)
⊢ Nonempty (Field α)

Tactic:
haveI : Fintype (GaloisField p n) := Fintype.ofFinite (GaloisField p n)

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Prime p
hn : 0 < n
hα : p ^ n = ‖α‖
this✝ : Fact (Nat.Prime p)
this : Fintype (GaloisField p n)
⊢ Nonempty (Field α)

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Prime p
hn : 0 < n
hα : p ^ n = ‖α‖
this✝ : Fact (Nat.Prime p)
this : Fintype (GaloisField p n)
⊢ Nonempty (Field α)

Tactic:
exact ⟨(Fintype.equivOfCardEq
  (((Fintype.card_eq_nat_card).trans (GaloisField.card p n hn.ne')).trans hα)).symm.field⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Prime p
hn : 0 < n
hα : p ^ n = ‖α‖
⊢ Nonempty (Field α)

Tactic:
haveI := Fact.mk hp.nat_prime

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Prime p
hn : 0 < n
hα : p ^ n = ‖α‖
this : Fact (Nat.Prime p)
⊢ Nonempty (Field α)
-- Mathlib/MeasureTheory/Group/Action.lean
theorem eventuallyConst_smul_set_ae (c : G) {s : Set α} :
    EventuallyConst (c • s : Set α) (ae μ) ↔ EventuallyConst s (ae μ)

Proof state:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s : Set α
⊢ EventuallyConst (c • s) (ae μ) ↔ EventuallyConst s (ae μ)

Tactic:
rw [← preimage_smul_inv, eventuallyConst_preimage, Filter.map_smul, smul_ae]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sheafification.lean
theorem sheafifyMap_comp {P Q R : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (γ : Q ⟶ R) :
    sheafifyMap J (η ≫ γ) = sheafifyMap J η ≫ sheafifyMap J γ

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
⊢ sheafifyMap J (η ≫ γ) = sheafifyMap J η ≫ sheafifyMap J γ

Tactic:
simp [sheafifyMap, sheafify]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/LawfulOperator.lean
theorem denote_input_entry (entry : Entrypoint α) {input} {h} :
    ⟦(f entry.aig input).aig, ⟨entry.ref.gate, h⟩, assign⟧
      =
    ⟦entry, assign⟧ :=  by
  apply denote.eq_of_isPrefix
  apply isPrefix_aig

Proof state:
case hprefix
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
assign : α → Bool
entry : Entrypoint α
input : β entry.aig
h : entry.ref.gate < (f entry.aig input).aig.decls.size
⊢ IsPrefix entry.aig.decls (f entry.aig input).aig.decls

Tactic:
apply isPrefix_aig

Result:
no goals

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
assign : α → Bool
entry : Entrypoint α
input : β entry.aig
h : entry.ref.gate < (f entry.aig input).aig.decls.size
⊢ ⟦assign, { aig := (f entry.aig input).aig, ref := { gate := entry.ref.gate, hgate := h } }⟧ = ⟦assign, entry⟧

Tactic:
apply denote.eq_of_isPrefix

Result:
case hprefix
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
assign : α → Bool
entry : Entrypoint α
input : β entry.aig
h : entry.ref.gate < (f entry.aig input).aig.decls.size
⊢ IsPrefix entry.aig.decls (f entry.aig input).aig.decls