harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/IsConnected.lean
theorem isConnected_iff_of_final (F : C ⥤ D) [F.Final] : IsConnected C ↔ IsConnected D

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Final
⊢ Nonempty (Limits.colimit (constPUnitFunctor C) ≅ PUnit.{(max v u v₂ u₂) + 1}) ↔
    Nonempty (Limits.colimit (constPUnitFunctor D) ≅ PUnit.{(max v u v₂ u₂) + 1})

Tactic:
exact Equiv.nonempty_congr <| Iso.isoCongrLeft <|
  CategoryTheory.Functor.Final.colimitIso F <| constPUnitFunctor.{max u v u₂ v₂} D

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Final
⊢ IsConnected C ↔ IsConnected D

Tactic:
rw [isConnected_iff_colimit_constPUnitFunctor_iso_pUnit.{max v u v₂ u₂} C,
  isConnected_iff_colimit_constPUnitFunctor_iso_pUnit.{max v u v₂ u₂} D]

Result:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Final
⊢ Nonempty (Limits.colimit (constPUnitFunctor C) ≅ PUnit.{(max v u v₂ u₂) + 1}) ↔
    Nonempty (Limits.colimit (constPUnitFunctor D) ≅ PUnit.{(max v u v₂ u₂) + 1})
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma IsStableUnderProductsOfShape.mk (J : Type*) [W.RespectsIso]
    (hW : ∀ (X₁ X₂ : J → C) [HasProduct X₁] [HasProduct X₂]
      (f : ∀ j, X₁ j ⟶ X₂ j) (_ : ∀ (j : J), W (f j)),
      W (Limits.Pi.map f)) : W.IsStableUnderProductsOfShape J

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Pi.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
hc₁ : IsLimit c₁
hc₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j => f.app { as := j }
this✝ : HasLimit X₁
this : HasLimit X₂
⊢ W (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f })

Tactic:
have : HasProduct fun j ↦ X₁.obj (Discrete.mk j) :=
  hasLimitOfIso (Discrete.natIso (fun j ↦ Iso.refl (X₁.obj j)))

Result:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Pi.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
hc₁ : IsLimit c₁
hc₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j => f.app { as := j }
this✝¹ : HasLimit X₁
this✝ : HasLimit X₂
this : HasProduct fun j => X₁.obj { as := j }
⊢ W (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f })

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Pi.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
hc₁ : IsLimit c₁
hc₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j => f.app { as := j }
this : HasLimit X₁
⊢ W (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f })

Tactic:
have : HasLimit X₂ := ⟨c₂, hc₂⟩

Result:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Pi.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
hc₁ : IsLimit c₁
hc₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j => f.app { as := j }
this✝ : HasLimit X₁
this : HasLimit X₂
⊢ W (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f })
-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem integrable_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) :
    Integrable fun x : ℝ => exp (-b * x ^ 2)

Proof state:
b : ℝ
hb : 0 < b
⊢ -1 < 0

Tactic:
norm_num

Result:
no goals

Proof state:
b : ℝ
hb : 0 < b
⊢ Integrable (fun x => rexp (-b * x ^ 2)) volume

Tactic:
simpa using integrable_rpow_mul_exp_neg_mul_sq hb (by norm_num : (-1 : ℝ) < 0)

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
@[reassoc (attr := simp)]
lemma inlX_desc_f (i j : ι) (hjk : c.Rel j i) :
    inlX φ i j hjk ≫ (desc φ α hα).f j = hα.hom i j

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hjk : c.Rel j (c.next j)
⊢ (inlX φ (c.next j) j hjk ≫
      if hj : c.Rel j (c.next j) then fstX φ j (c.next j) hj ≫ hα.hom (c.next j) j + sndX φ j ≫ α.f j
      else sndX φ j ≫ α.f j) =
    hα.hom (c.next j) j

Tactic:
rw [dif_pos hjk, comp_add, inlX_fstX_assoc, inlX_sndX_assoc, zero_comp, add_zero]

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
i j : ι
hjk : c.Rel j i
⊢ inlX φ i j hjk ≫ (desc φ α hα).f j = hα.hom i j

Tactic:
obtain rfl := c.next_eq' hjk

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hjk : c.Rel j (c.next j)
⊢ inlX φ (c.next j) j hjk ≫ (desc φ α hα).f j = hα.hom (c.next j) j

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hjk : c.Rel j (c.next j)
⊢ inlX φ (c.next j) j hjk ≫ (desc φ α hα).f j = hα.hom (c.next j) j

Tactic:
dsimp [desc]

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hjk : c.Rel j (c.next j)
⊢ (inlX φ (c.next j) j hjk ≫
      if hj : c.Rel j (c.next j) then fstX φ j (c.next j) hj ≫ hα.hom (c.next j) j + sndX φ j ≫ α.f j
      else sndX φ j ≫ α.f j) =
    hα.hom (c.next j) j
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem card_of_subsingleton (a : α) [Subsingleton α] : Nat.card α = 1

Proof state:
α : Type u_1
a : α
inst✝ : Subsingleton α
⊢ Nat.card α = 1

Tactic:
letI := Fintype.ofSubsingleton a

Result:
α : Type u_1
a : α
inst✝ : Subsingleton α
this : Fintype α := Fintype.ofSubsingleton a
⊢ Nat.card α = 1

Proof state:
α : Type u_1
a : α
inst✝ : Subsingleton α
this : Fintype α := Fintype.ofSubsingleton a
⊢ Nat.card α = 1

Tactic:
rw [card_eq_fintype_card, Fintype.card_ofSubsingleton a]

Result:
no goals
-- Mathlib/Data/Nat/Bits.lean
lemma testBit_bit_succ (m b n) : testBit (bit b n) (succ m) = testBit n m

Proof state:
m : ℕ
b : Bool
n : ℕ
this : (bit b n >>> 1 >>> m).bodd = (n >>> m).bodd
⊢ (bit b n).testBit m.succ = n.testBit m

Tactic:
rw [← shiftRight_add, Nat.add_comm] at this

Result:
m : ℕ
b : Bool
n : ℕ
this : (bit b n >>> (m + 1)).bodd = (n >>> m).bodd
⊢ (bit b n).testBit m.succ = n.testBit m

Proof state:
m : ℕ
b : Bool
n : ℕ
this : (1 &&& bit b n >>> (m + 1) != 0) = (1 &&& n >>> m != 0)
⊢ (bit b n).testBit m.succ = n.testBit m

Tactic:
exact this

Result:
no goals

Proof state:
m : ℕ
b : Bool
n : ℕ
⊢ (bit b n >>> 1 >>> m).bodd = (n >>> m).bodd

Tactic:
simp only [shiftRight_eq_div_pow]

Result:
m : ℕ
b : Bool
n : ℕ
⊢ (bit b n / 2 ^ 1 / 2 ^ m).bodd = (n / 2 ^ m).bodd

Proof state:
m : ℕ
b : Bool
n : ℕ
⊢ (bit b n / 2 ^ 1 / 2 ^ m).bodd = (n / 2 ^ m).bodd

Tactic:
simp [← div2_val, div2_bit]

Result:
no goals

Proof state:
m : ℕ
b : Bool
n : ℕ
this : (bit b n >>> (m + 1)).bodd = (n >>> m).bodd
⊢ (bit b n).testBit m.succ = n.testBit m

Tactic:
simp only [bodd_eq_one_and_ne_zero] at this

Result:
m : ℕ
b : Bool
n : ℕ
this : (1 &&& bit b n >>> (m + 1) != 0) = (1 &&& n >>> m != 0)
⊢ (bit b n).testBit m.succ = n.testBit m

Proof state:
m : ℕ
b : Bool
n : ℕ
⊢ (bit b n).testBit m.succ = n.testBit m

Tactic:
have : bodd (((bit b n) >>> 1) >>> m) = bodd (n >>> m) := by
  simp only [shiftRight_eq_div_pow]
  simp [← div2_val, div2_bit]

Result:
m : ℕ
b : Bool
n : ℕ
this : (bit b n >>> 1 >>> m).bodd = (n >>> m).bodd
⊢ (bit b n).testBit m.succ = n.testBit m
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigOWith_iff_exists_eq_mul (hc : 0 ≤ c) :
    IsBigOWith c l u v ↔ ∃ φ : α → 𝕜, (∀ᶠ x in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v

Proof state:
case mpr.intro.intro
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
φ : α → 𝕜
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
⊢ IsBigOWith c l u v

Tactic:
exact isBigOWith_of_eq_mul φ hφ h

Result:
no goals

Proof state:
case h
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
h : IsBigOWith c l u v
y : α
hy : ‖u y‖ ≤ c * ‖v y‖
⊢ ‖(fun x => u x / v x) y‖ ≤ c

Tactic:
simpa using div_le_of_le_mul₀ (norm_nonneg _) hc hy

Result:
no goals

Proof state:
case mp
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
h : IsBigOWith c l u v
⊢ ∃ φ, (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v

Tactic:
use fun x => u x / v x

Result:
case h
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
h : IsBigOWith c l u v
⊢ (∀ᶠ (x : α) in l, ‖(fun x => u x / v x) x‖ ≤ c) ∧ u =ᶠ[l] (fun x => u x / v x) * v

Proof state:
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
⊢ IsBigOWith c l u v ↔ ∃ φ, (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v

Tactic:
constructor

Result:
case mp
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
⊢ IsBigOWith c l u v → ∃ φ, (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v

case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
⊢ (∃ φ, (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v) → IsBigOWith c l u v

Proof state:
case h
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
h : IsBigOWith c l u v
⊢ (∀ᶠ (x : α) in l, ‖(fun x => u x / v x) x‖ ≤ c) ∧ u =ᶠ[l] (fun x => u x / v x) * v

Tactic:
refine ⟨Eventually.mono h.bound fun y hy => ?_, h.eventually_mul_div_cancel.symm⟩

Result:
case h
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
h : IsBigOWith c l u v
y : α
hy : ‖u y‖ ≤ c * ‖v y‖
⊢ ‖(fun x => u x / v x) y‖ ≤ c

Proof state:
case mp
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
⊢ IsBigOWith c l u v → ∃ φ, (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v

Tactic:
intro h

Result:
case mp
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
h : IsBigOWith c l u v
⊢ ∃ φ, (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v

Proof state:
case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
⊢ (∃ φ, (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v) → IsBigOWith c l u v

Tactic:
rintro ⟨φ, hφ, h⟩

Result:
case mpr.intro.intro
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
φ : α → 𝕜
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
⊢ IsBigOWith c l u v
-- Mathlib/Algebra/Module/LinearMap/End.lean
theorem commute_pow_left_of_commute
    [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {σ₁₂ : R →+* R₂}
    {f : M →ₛₗ[σ₁₂] M₂} {g : Module.End R M} {g₂ : Module.End R₂ M₂}
    (h : g₂.comp f = f.comp g) (k : ℕ) : (g₂ ^ k).comp f = f.comp (g ^ k)

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : Module.End R M
g₂ : Module.End R₂ M₂
h : comp g₂ f = f.comp g
k : ℕ
⊢ comp (g₂ ^ k) f = f.comp (g ^ k)

Tactic:
induction k with
| zero => simp only [pow_zero, one_eq_id, id_comp, comp_id]
| succ k ih => rw [pow_succ', pow_succ', LinearMap.mul_eq_comp, LinearMap.comp_assoc, ih,
  ← LinearMap.comp_assoc, h, LinearMap.comp_assoc, LinearMap.mul_eq_comp]

Result:
no goals

Proof state:
case succ
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : Module.End R M
g₂ : Module.End R₂ M₂
h : comp g₂ f = f.comp g
k : ℕ
ih : comp (g₂ ^ k) f = f.comp (g ^ k)
⊢ comp (g₂ ^ (k + 1)) f = f.comp (g ^ (k + 1))

Tactic:
rw [pow_succ', pow_succ', LinearMap.mul_eq_comp, LinearMap.comp_assoc, ih,
← LinearMap.comp_assoc, h, LinearMap.comp_assoc, LinearMap.mul_eq_comp]

Result:
no goals

Proof state:
case zero
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : Module.End R M
g₂ : Module.End R₂ M₂
h : comp g₂ f = f.comp g
⊢ comp (g₂ ^ 0) f = f.comp (g ^ 0)

Tactic:
simp only [pow_zero, one_eq_id, id_comp, comp_id]

Result:
no goals
-- Mathlib/Analysis/Analytic/Order.lean
/-- An analytic function vanishes at a point if its order is nonzero when converted to ℕ. -/
lemma apply_eq_zero_of_order_toNat_ne_zero (hf : AnalyticAt 𝕜 f z₀) :
    hf.order.toNat ≠ 0 → f z₀ = 0

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ hf.order.toNat ≠ 0 → f z₀ = 0

Tactic:
simp [hf.order_eq_zero_iff]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ f z₀ = 0 → ¬hf.order = ⊤ → f z₀ = 0

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ f z₀ = 0 → ¬hf.order = ⊤ → f z₀ = 0

Tactic:
tauto

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem exists_ne_one_of_prod_ne_one (h : ∏ x ∈ s, f x ≠ 1) : ∃ a ∈ s, f a ≠ 1

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝ : CommMonoid β
h : ∏ x ∈ filter (fun x => f x ≠ 1) s, f x ≠ 1
⊢ ∃ a ∈ s, f a ≠ 1

Tactic:
rcases nonempty_of_prod_ne_one h with ⟨x, hx⟩

Result:
case intro
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝ : CommMonoid β
h : ∏ x ∈ filter (fun x => f x ≠ 1) s, f x ≠ 1
x : α
hx : x ∈ filter (fun x => f x ≠ 1) s
⊢ ∃ a ∈ s, f a ≠ 1

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝ : CommMonoid β
h : ∏ x ∈ s, f x ≠ 1
⊢ ∃ a ∈ s, f a ≠ 1

Tactic:
classical
  rw [← prod_filter_ne_one] at h
  rcases nonempty_of_prod_ne_one h with ⟨x, hx⟩
  exact ⟨x, (mem_filter.1 hx).1, by simpa using (mem_filter.1 hx).2⟩

Result:
no goals

Proof state:
case intro
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝ : CommMonoid β
h : ∏ x ∈ filter (fun x => f x ≠ 1) s, f x ≠ 1
x : α
hx : x ∈ filter (fun x => f x ≠ 1) s
⊢ ∃ a ∈ s, f a ≠ 1

Tactic:
exact ⟨x, (mem_filter.1 hx).1, by simpa using (mem_filter.1 hx).2⟩

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝ : CommMonoid β
h : ∏ x ∈ filter (fun x => f x ≠ 1) s, f x ≠ 1
x : α
hx : x ∈ filter (fun x => f x ≠ 1) s
⊢ f x ≠ 1

Tactic:
simpa using (mem_filter.1 hx).2

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝ : CommMonoid β
h : ∏ x ∈ s, f x ≠ 1
⊢ ∃ a ∈ s, f a ≠ 1

Tactic:
rw [← prod_filter_ne_one] at h

Result:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝ : CommMonoid β
h : ∏ x ∈ filter (fun x => f x ≠ 1) s, f x ≠ 1
⊢ ∃ a ∈ s, f a ≠ 1
-- Mathlib/CategoryTheory/Monad/Comonadicity.lean
theorem comparisonAdjunction_unit_app
    [∀ A : adj.toComonad.Coalgebra, HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (B : C) :
    (comparisonAdjunction adj).unit.app B = limit.lift _ (unitFork adj B)

Proof state:
case h
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
B : C
⊢ equalizer.lift ((adj.homEquiv B (F.obj B)) (𝟙 (F.obj B))) ⋯ ≫
      equalizer.ι (G.map ((comparison adj).obj B).a) (adj.unit.app (G.toPrefunctor.1 ((comparison adj).obj B).A)) =
    equalizer.lift (adj.unit.app B) ⋯ ≫ equalizer.ι (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))

Tactic:
simp [Adjunction.homEquiv_unit]

Result:
no goals

Proof state:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
B : C
⊢ (comparisonAdjunction adj).unit.app B =
    limit.lift (parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))) (unitFork adj B)

Tactic:
apply equalizer.hom_ext

Result:
case h
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
B : C
⊢ (comparisonAdjunction adj).unit.app B ≫
      equalizer.ι (G.map ((comparison adj).obj B).a) (adj.unit.app (G.toPrefunctor.1 ((comparison adj).obj B).A)) =
    limit.lift (parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))) (unitFork adj B) ≫
      equalizer.ι (G.map ((comparison adj).obj B).a) (adj.unit.app (G.toPrefunctor.1 ((comparison adj).obj B).A))

Proof state:
case h
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
B : C
⊢ (comparisonAdjunction adj).unit.app B ≫
      equalizer.ι (G.map ((comparison adj).obj B).a) (adj.unit.app (G.toPrefunctor.1 ((comparison adj).obj B).A)) =
    limit.lift (parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))) (unitFork adj B) ≫
      equalizer.ι (G.map ((comparison adj).obj B).a) (adj.unit.app (G.toPrefunctor.1 ((comparison adj).obj B).A))

Tactic:
change
  equalizer.lift ((adj.homEquiv B _) (𝟙 _)) _ ≫ equalizer.ι _ _ =
    equalizer.lift _ _ ≫ equalizer.ι _ _

Result:
case h
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
B : C
⊢ equalizer.lift ((adj.homEquiv B (F.obj B)) (𝟙 (F.obj B))) ⋯ ≫
      equalizer.ι (G.map ((comparison adj).obj B).a) (adj.unit.app (G.toPrefunctor.1 ((comparison adj).obj B).A)) =
    equalizer.lift (adj.unit.app B) ⋯ ≫ equalizer.ι (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))
-- Mathlib/CategoryTheory/Grothendieck.lean
lemma eqToHom_eq {X Y : Grothendieck F} (hF : X = Y) :
    eqToHom hF = { base := eqToHom (by subst hF; rfl), fiber := eqToHom (by subst hF; simp) }

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
hF : X = Y
⊢ X.base = Y.base

Tactic:
subst hF

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X : Grothendieck F
⊢ X.base = X.base

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X : Grothendieck F
⊢ X.base = X.base

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
hF : X = Y
⊢ eqToHom hF = { base := eqToHom ⋯, fiber := eqToHom ⋯ }

Tactic:
subst hF

Result:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ eqToHom ⋯ = { base := eqToHom ⋯, fiber := eqToHom ⋯ }

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
hF : X = Y
⊢ (F.map (eqToHom ⋯)).obj X.fiber = Y.fiber

Tactic:
subst hF

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X : Grothendieck F
⊢ (F.map (eqToHom ⋯)).obj X.fiber = X.fiber

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ eqToHom ⋯ = { base := eqToHom ⋯, fiber := eqToHom ⋯ }

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X : Grothendieck F
⊢ (F.map (eqToHom ⋯)).obj X.fiber = X.fiber

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem mem_of_insertRupUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clause (PosFin n))
    (c : DefaultClause n) :
    c ∈ toList (insertRupUnits f units).1 → c ∈ units.map Clause.unit ∨ c ∈ toList f

Proof state:
case isFalse.inr
n : Nat
f : DefaultFormula n
units : CNF.Clause (PosFin n)
c : DefaultClause n
h :
  some c ∈ f.clauses.toList ∨
    (∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst.toList ∧
            Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst.toList ∧
            Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.toList ∧ Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.ratUnits.toList ∧ Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.rupUnits, f.assignments, false).fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.toList → l ∈ f.rupUnits.toList ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
l_eq_unit : l = (unit.fst, unit.snd)
⊢ (unit.fst, unit.snd) ∈ f.rupUnits.toList ∨ (unit.fst, unit.snd) ∈ units

Tactic:
exact Or.inr unit_in_units

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem neg_eq_self_mod_two (a : ZMod 2) : -a = a

Proof state:
a : ZMod 2
⊢ -a = a

Tactic:
fin_cases a <;> apply Fin.ext <;> simp [Fin.coe_neg, Int.natMod]

Result:
case «1».h

⊢ ↑(-1) = 1

Proof state:
case «1».h

⊢ ↑(-1) = 1

Tactic:
rfl

Result:
no goals