harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapIdx_append {K : Vector α n} {L : Vector α m} :
    (K ++ L).mapIdx f = K.mapIdx f ++ L.mapIdx fun i => f (i + K.size)

Proof state:
case mk
α : Type u_1
m : Nat
α✝ : Type u_2
f : Nat → α → α✝
L : Vector α m
K : Array α
⊢ mapIdx f ({ toArray := K, size_toArray := ⋯ } ++ L) =
    mapIdx f { toArray := K, size_toArray := ⋯ } ++ mapIdx (fun i => f (i + { toArray := K, size_toArray := ⋯ }.size)) L

Tactic:
rcases L with ⟨L, rfl⟩

Result:
case mk.mk
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
K L : Array α
⊢ mapIdx f ({ toArray := K, size_toArray := ⋯ } ++ { toArray := L, size_toArray := ⋯ }) =
    mapIdx f { toArray := K, size_toArray := ⋯ } ++
      mapIdx (fun i => f (i + { toArray := K, size_toArray := ⋯ }.size)) { toArray := L, size_toArray := ⋯ }

Proof state:
case mk.mk
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
K L : Array α
⊢ mapIdx f ({ toArray := K, size_toArray := ⋯ } ++ { toArray := L, size_toArray := ⋯ }) =
    mapIdx f { toArray := K, size_toArray := ⋯ } ++
      mapIdx (fun i => f (i + { toArray := K, size_toArray := ⋯ }.size)) { toArray := L, size_toArray := ⋯ }

Tactic:
simp [Array.mapIdx_append]

Result:
no goals

Proof state:
α : Type u_1
n m : Nat
α✝ : Type u_2
f : Nat → α → α✝
K : Vector α n
L : Vector α m
⊢ mapIdx f (K ++ L) = mapIdx f K ++ mapIdx (fun i => f (i + K.size)) L

Tactic:
rcases K with ⟨K, rfl⟩

Result:
case mk
α : Type u_1
m : Nat
α✝ : Type u_2
f : Nat → α → α✝
L : Vector α m
K : Array α
⊢ mapIdx f ({ toArray := K, size_toArray := ⋯ } ++ L) =
    mapIdx f { toArray := K, size_toArray := ⋯ } ++ mapIdx (fun i => f (i + { toArray := K, size_toArray := ⋯ }.size)) L
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem getElem_neg {i : Nat} {x : BitVec w} (h : i < w) :
    (-x)[i] = (x[i] ^^ decide (∃ j < i, x.getLsbD j = true))

Proof state:
w i : Nat
x : BitVec w
h : i < w
⊢ (-x)[i] = (x[i] ^^ decide (∃ j, j < i ∧ x.getLsbD j = true))

Tactic:
simp [← getLsbD_eq_getElem, getLsbD_neg, h]

Result:
no goals
-- Mathlib/RingTheory/HopfAlgebra/MonoidAlgebra.lean
theorem antipode_T (n : ℤ) :
    HopfAlgebra.antipode (R := R) (T n : A[T;T⁻¹]) = T (-n)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
n : ℤ
⊢ antipode (T n) = T (-n)

Tactic:
unfold T

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
n : ℤ
⊢ antipode (single n 1) = single (-n) 1

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
n : ℤ
⊢ AddMonoidAlgebra.single (-n) (antipode 1) = single (-n) 1

Tactic:
simp only [HopfAlgebra.antipode_one, single_eq_C_mul_T, map_one, one_mul]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
n : ℤ
⊢ antipode (single n 1) = single (-n) 1

Tactic:
rw [AddMonoidAlgebra.antipode_single]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
n : ℤ
⊢ AddMonoidAlgebra.single (-n) (antipode 1) = single (-n) 1
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
@[simp]
lemma centralizer_centralizer_centralizer {R} [Semiring R] {s : Set R} :
    centralizer s.centralizer.centralizer = centralizer s

Proof state:
R : Type u_1
inst✝ : Semiring R
s : Set R
⊢ centralizer s.centralizer.centralizer = centralizer s

Tactic:
apply SetLike.coe_injective

Result:
case a
R : Type u_1
inst✝ : Semiring R
s : Set R
⊢ ↑(centralizer s.centralizer.centralizer) = ↑(centralizer s)

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
s : Set R
⊢ ↑(centralizer s.centralizer.centralizer) = ↑(centralizer s)

Tactic:
simp only [coe_centralizer, Set.centralizer_centralizer_centralizer]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem bne_eq_false_iff_eq [BEq α] [LawfulBEq α] {a b : α} : (a != b) = false ↔ a = b

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (a != b) = false ↔ a = b

Tactic:
rw [bne, ← beq_iff_eq (a := a) (b := b)]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (!a == b) = false ↔ (a == b) = true

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (!a == b) = false ↔ (a == b) = true

Tactic:
cases a == b <;> decide

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem cauchySeq_iff {u : ℕ → α} :
    CauchySeq u ↔ ∀ V ∈ 𝓤 α, ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V

Proof state:
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
⊢ CauchySeq u ↔ ∀ V ∈ 𝓤 α, ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V

Tactic:
simp only [cauchySeq_iff', Filter.eventually_atTop_prod_self', mem_preimage, Prod.map_apply]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Basic.lean
theorem Prime.not_coprime_iff_dvd {m n : ℕ} : ¬Coprime m n ↔ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n

Proof state:
case mpr
m n : ℕ
⊢ (∃ p, Prime p ∧ p ∣ m ∧ p ∣ n) → ¬m.Coprime n

Tactic:
intro h

Result:
case mpr
m n : ℕ
h : ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n
⊢ ¬m.Coprime n

Proof state:
case mpr.intro
m n p : ℕ
hp : Prime p ∧ p ∣ m ∧ p ∣ n
⊢ ¬m.Coprime n

Tactic:
apply Nat.not_coprime_of_dvd_of_dvd (Prime.one_lt hp.1) hp.2.1 hp.2.2

Result:
no goals

Proof state:
case mp
m n : ℕ
h : ¬m.Coprime n
⊢ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n

Tactic:
exact
  ⟨minFac (gcd m n), minFac_prime h, (minFac_dvd (gcd m n)).trans (gcd_dvd_left m n),
    (minFac_dvd (gcd m n)).trans (gcd_dvd_right m n)⟩

Result:
no goals

Proof state:
case mpr
m n : ℕ
h : ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n
⊢ ¬m.Coprime n

Tactic:
obtain ⟨p, hp⟩ := h

Result:
case mpr.intro
m n p : ℕ
hp : Prime p ∧ p ∣ m ∧ p ∣ n
⊢ ¬m.Coprime n

Proof state:
case mp
m n : ℕ
⊢ ¬m.Coprime n → ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n

Tactic:
intro h

Result:
case mp
m n : ℕ
h : ¬m.Coprime n
⊢ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n

Proof state:
m n : ℕ
⊢ ¬m.Coprime n ↔ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n

Tactic:
apply Iff.intro

Result:
case mp
m n : ℕ
⊢ ¬m.Coprime n → ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n

case mpr
m n : ℕ
⊢ (∃ p, Prime p ∧ p ∣ m ∧ p ∣ n) → ¬m.Coprime n
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Icc_sub_one_right_eq_Ico_of_not_isMin (hb : ¬ IsMin b) (a : α) : Icc a (b - 1) = Ico a b

Proof state:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
b : α
hb : ¬IsMin b
a : α
⊢ Icc a (b - 1) = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Icc_pred_right_eq_Ico_of_not_isMin hb a

Result:
no goals
-- Mathlib/Algebra/Order/Field/Defs.lean
/-- Equality holds when `a ≠ 0`. See `inv_mul_cancel_left`. -/
lemma inv_mul_left_le (hb : 0 ≤ b) : a⁻¹ * (a * b) ≤ b

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b : α
hb : 0 ≤ b
⊢ a⁻¹ * (a * b) ≤ b

Tactic:
obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get!_alter_self [LawfulBEq α] {k : α} [Inhabited (β k)] {f : Option (β k) → Option (β k)} :
    (m.alter k f).get! k = (f (m.get? k)).get!

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
k : α
inst✝ : Inhabited (β k)
f : Option (β k) → Option (β k)
⊢ (m.alter k f).get! k = (f (m.get? k)).get!

Tactic:
simp only [get!_alter, beq_self_eq_true, reduceDIte, cast_eq, Option.map_cast_apply]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mdifferentiableWithinAt_univ :
    MDifferentiableWithinAt I I' f univ x ↔ MDifferentiableAt I I' f x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
⊢ MDifferentiableWithinAt I I' f univ x ↔ MDifferentiableAt I I' f x

Tactic:
simp_rw [MDifferentiableWithinAt, MDifferentiableAt, ChartedSpace.LiftPropAt]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffEdist_le_of_infEdist {r : ℝ≥0∞} (H1 : ∀ x ∈ s, infEdist x t ≤ r)
    (H2 : ∀ x ∈ t, infEdist x s ≤ r) : hausdorffEdist s t ≤ r

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, infEdist x t ≤ r
H2 : ∀ x ∈ t, infEdist x s ≤ r
⊢ hausdorffEdist s t ≤ r

Tactic:
simp only [hausdorffEdist_def, sup_le_iff, iSup_le_iff]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, infEdist x t ≤ r
H2 : ∀ x ∈ t, infEdist x s ≤ r
⊢ (∀ i ∈ s, infEdist i t ≤ r) ∧ ∀ i ∈ t, infEdist i s ≤ r

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, infEdist x t ≤ r
H2 : ∀ x ∈ t, infEdist x s ≤ r
⊢ (∀ i ∈ s, infEdist i t ≤ r) ∧ ∀ i ∈ t, infEdist i s ≤ r

Tactic:
exact ⟨H1, H2⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tmod_def (a b : Int) : tmod a b = a - b * a.tdiv b

Proof state:
a b : Int
⊢ a.tmod b = a - b * a.tdiv b

Tactic:
rw [← Int.add_sub_cancel (tmod a b), tmod_add_tdiv]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem eq_singleton_bot_of_sSup_eq_bot_of_nonempty {s : Set α} (h_sup : sSup s = ⊥)
    (hne : s.Nonempty) : s = {⊥}

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
h_sup : sSup s = ⊥
hne : s.Nonempty
⊢ s.Nonempty ∧ ∀ x ∈ s, x = ⊥

Tactic:
rw [sSup_eq_bot] at h_sup

Result:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
h_sup : ∀ a ∈ s, a = ⊥
hne : s.Nonempty
⊢ s.Nonempty ∧ ∀ x ∈ s, x = ⊥

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
h_sup : sSup s = ⊥
hne : s.Nonempty
⊢ s = {⊥}

Tactic:
rw [Set.eq_singleton_iff_nonempty_unique_mem]

Result:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
h_sup : sSup s = ⊥
hne : s.Nonempty
⊢ s.Nonempty ∧ ∀ x ∈ s, x = ⊥

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
h_sup : ∀ a ∈ s, a = ⊥
hne : s.Nonempty
⊢ s.Nonempty ∧ ∀ x ∈ s, x = ⊥

Tactic:
exact ⟨hne, h_sup⟩

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma Walk.IsCycle.isCycles_spanningCoe_toSubgraph {u : V} {p : G.Walk u u} (hpc : p.IsCycle) :
    p.toSubgraph.spanningCoe.IsCycles

Proof state:
V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hv : (p.toSubgraph.spanningCoe.neighborSet v).Nonempty
⊢ v ∈ p.support

Tactic:
obtain ⟨_, hw⟩ := hv

Result:
case intro
V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v w✝ : V
hw : w✝ ∈ p.toSubgraph.spanningCoe.neighborSet v
⊢ v ∈ p.support

Proof state:
V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hv : (p.toSubgraph.spanningCoe.neighborSet v).Nonempty
⊢ (p.toSubgraph.spanningCoe.neighborSet v).ncard = 2

Tactic:
apply hpc.ncard_neighborSet_toSubgraph_eq_two

Result:
V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hv : (p.toSubgraph.spanningCoe.neighborSet v).Nonempty
⊢ v ∈ p.support

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v w✝ : V
hw : w✝ ∈ p.toSubgraph.spanningCoe.neighborSet v
⊢ v ∈ p.support

Tactic:
exact p.mem_verts_toSubgraph.mp <| p.toSubgraph.edge_vert hw

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
⊢ p.toSubgraph.spanningCoe.IsCycles

Tactic:
intro v hv

Result:
V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hv : (p.toSubgraph.spanningCoe.neighborSet v).Nonempty
⊢ (p.toSubgraph.spanningCoe.neighborSet v).ncard = 2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zipWithAll_map_right (l₁ : Array α) (l₂ : Array β) (f : β → β') (g : Option α → Option β' → γ) :
    zipWithAll g l₁ (l₂.map f) = zipWithAll (fun a b => g a (f <$> b)) l₁ l₂

Proof state:
case mk
α : Type u_1
β β' : Type u_2
γ : Type u_3
l₂ : Array β
f : β → β'
g : Option α → Option β' → γ
toList✝ : List α
⊢ zipWithAll g { toList := toList✝ } (map f l₂) = zipWithAll (fun a b => g a (f <$> b)) { toList := toList✝ } l₂

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β β' : Type u_2
γ : Type u_3
f : β → β'
g : Option α → Option β' → γ
toList✝¹ : List α
toList✝ : List β
⊢ zipWithAll g { toList := toList✝¹ } (map f { toList := toList✝ }) =
    zipWithAll (fun a b => g a (f <$> b)) { toList := toList✝¹ } { toList := toList✝ }

Proof state:
α : Type u_1
β β' : Type u_2
γ : Type u_3
l₁ : Array α
l₂ : Array β
f : β → β'
g : Option α → Option β' → γ
⊢ zipWithAll g l₁ (map f l₂) = zipWithAll (fun a b => g a (f <$> b)) l₁ l₂

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β β' : Type u_2
γ : Type u_3
l₂ : Array β
f : β → β'
g : Option α → Option β' → γ
toList✝ : List α
⊢ zipWithAll g { toList := toList✝ } (map f l₂) = zipWithAll (fun a b => g a (f <$> b)) { toList := toList✝ } l₂

Proof state:
case mk.mk
α : Type u_1
β β' : Type u_2
γ : Type u_3
f : β → β'
g : Option α → Option β' → γ
toList✝¹ : List α
toList✝ : List β
⊢ zipWithAll g { toList := toList✝¹ } (map f { toList := toList✝ }) =
    zipWithAll (fun a b => g a (f <$> b)) { toList := toList✝¹ } { toList := toList✝ }

Tactic:
simp [List.zipWithAll_map_right]

Result:
no goals
-- Mathlib/Topology/LocallyClosed.lean
lemma IsLocallyClosed.image {s : Set X} (hs : IsLocallyClosed s)
    {f : X → Y} (hf : IsInducing f) (hf' : IsLocallyClosed (range f)) :
    IsLocallyClosed (f '' s)

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsLocallyClosed (range f)
t : Set Y
ht : IsLocallyClosed t
hs : IsLocallyClosed (f ⁻¹' t)
⊢ IsLocallyClosed (t ∩ range f)

Tactic:
exact ht.inter hf'

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsLocallyClosed s
f : X → Y
hf : IsInducing f
hf' : IsLocallyClosed (range f)
⊢ IsLocallyClosed (f '' s)

Tactic:
obtain ⟨t, ht, rfl⟩ := hf.isLocallyClosed_iff.mp hs

Result:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsLocallyClosed (range f)
t : Set Y
ht : IsLocallyClosed t
hs : IsLocallyClosed (f ⁻¹' t)
⊢ IsLocallyClosed (f '' (f ⁻¹' t))

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsLocallyClosed (range f)
t : Set Y
ht : IsLocallyClosed t
hs : IsLocallyClosed (f ⁻¹' t)
⊢ IsLocallyClosed (f '' (f ⁻¹' t))

Tactic:
rw [image_preimage_eq_inter_range]

Result:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsLocallyClosed (range f)
t : Set Y
ht : IsLocallyClosed t
hs : IsLocallyClosed (f ⁻¹' t)
⊢ IsLocallyClosed (t ∩ range f)
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
@[simp]
lemma DifferentiableAt.add_iff_right (hg : DifferentiableAt 𝕜 f x) :
    DifferentiableAt 𝕜 (fun y => f y + g y) x ↔ DifferentiableAt 𝕜 g 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 g : E → F
x : E
hg : DifferentiableAt 𝕜 f x
⊢ DifferentiableAt 𝕜 (fun y => f y + g y) x ↔ DifferentiableAt 𝕜 g x

Tactic:
simp only [add_comm (f _), hg.add_iff_left]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_apply_of_not_map_zero {f : R → R} (a : A) (hf : ¬ f 0 = 0) :
    cfcₙ f a = 0

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
hf : ¬f 0 = 0
⊢ cfcₙ f a = 0

Tactic:
rw [cfcₙ_def, dif_neg (not_and_of_not_right _ (not_and_of_not_right _ hf))]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem diam_le_of_subset_closedBall {r : ℝ} (hr : 0 ≤ r) (h : s ⊆ closedBall x r) :
    diam s ≤ 2 * r :=
  diam_le_of_forall_dist_le (mul_nonneg zero_le_two hr) fun a ha b hb =>
    calc
      dist a b ≤ dist a x + dist b x := dist_triangle_right _ _ _
      _ ≤ r + r := add_le_add (h ha) (h hb)
      _ = 2 * r

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
r : ℝ
hr : 0 ≤ r
h : s ⊆ closedBall x r
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ r + r = 2 * r

Tactic:
simp [mul_two, mul_comm]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem rootSet_one (S) [CommRing S] [IsDomain S] [Algebra T S] : (1 : T[X]).rootSet S = ∅

Proof state:
T : Type w
inst✝³ : CommRing T
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ rootSet 1 S = ∅

Tactic:
rw [← C_1, rootSet_C]

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isDetector_unop_iff (G : Cᵒᵖ) : IsDetector (unop G) ↔ IsCodetector G

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Cᵒᵖ
⊢ IsDetector (unop G) ↔ IsCodetector G

Tactic:
rw [IsDetector, IsCodetector, ← isDetecting_unop_iff, Set.singleton_unop]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem sup_inf_inf_compl : x ⊓ y ⊔ x ⊓ yᶜ = x

Proof state:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x ⊓ y ⊔ x ⊓ yᶜ = x

Tactic:
rw [← sdiff_eq, sup_inf_sdiff _ _]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem last_eq_zero_iff {n : Nat} : Fin.last n = 0 ↔ n = 0

Proof state:
n : Nat
⊢ last n = 0 ↔ n = 0

Tactic:
simp [eq_comm (a := Fin.last n)]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Types.lean
lemma Quot.desc_toCocone_desc {α : Type u} (f : Quot F → α) (hc : IsColimit c) (x : Quot F) :
    hc.desc (toCocone f) (Quot.desc c x) = f x

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
α : Type u
f : Quot F → α
hc : IsColimit c
x : Quot F
⊢ hc.desc (toCocone f) (desc c x) = f x

Tactic:
obtain ⟨j, y, rfl⟩ := Quot.jointly_surjective x

Result:
case intro.intro
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
α : Type u
f : Quot F → α
hc : IsColimit c
j : J
y : F.obj j
⊢ hc.desc (toCocone f) (desc c (ι F j y)) = f (ι F j y)

Proof state:
case intro.intro
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
α : Type u
f : Quot F → α
hc : IsColimit c
j : J
y : F.obj j
⊢ hc.desc (toCocone f) (desc c (ι F j y)) = f (ι F j y)

Tactic:
simpa using congrFun (hc.fac _ j) y

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_inter_union_subset_union :
    image₂ f (s ∩ s') (t ∪ t') ⊆ image₂ f s t ∪ image₂ f s' t' :=
  coe_subset.1 <| by
    push_cast
    exact Set.image2_inter_union_subset_union

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝² : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ image2 f (↑s ∩ ↑s') (↑t ∪ ↑t') ⊆ image2 f ↑s ↑t ∪ image2 f ↑s' ↑t'

Tactic:
exact Set.image2_inter_union_subset_union

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝² : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ ↑(image₂ f (s ∩ s') (t ∪ t')) ⊆ ↑(image₂ f s t ∪ image₂ f s' t')

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝² : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ image2 f (↑s ∩ ↑s') (↑t ∪ ↑t') ⊆ image2 f ↑s ↑t ∪ image2 f ↑s' ↑t'
-- Mathlib/Data/Nat/PartENat.lean
theorem lt_coe_iff (x : PartENat) (n : ℕ) : x < n ↔ ∃ h : x.Dom, x.get h < n

Proof state:
x : PartENat
n : ℕ
⊢ x < ↑n ↔ ∃ (h : x.Dom), x.get h < n

Tactic:
simp only [lt_def, forall_prop_of_true, get_natCast', dom_natCast]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Over/Basic.lean
theorem eqToHom_right {X : T} {U V : Under X} (e : U = V) :
    (eqToHom e).right = eqToHom (e ▸ rfl : U.right = V.right)

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Under X
e : U = V
⊢ (eqToHom e).right = eqToHom ⋯

Tactic:
subst e

Result:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U : Under X
⊢ (eqToHom ⋯).right = eqToHom ⋯

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U : Under X
⊢ (eqToHom ⋯).right = eqToHom ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem IsLindelof.countable_of_discrete [DiscreteTopology X] (hs : IsLindelof s) :
    s.Countable

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsLindelof s
⊢ ∀ (x : X), {x} ∈ 𝓝 x

Tactic:
simp [nhds_discrete]

Result:
no goals

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsLindelof s
⊢ s.Countable

Tactic:
have : ∀ x : X, ({x} : Set X) ∈ 𝓝 x := by simp [nhds_discrete]

Result:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsLindelof s
this : ∀ (x : X), {x} ∈ 𝓝 x
⊢ s.Countable

Proof state:
case intro.intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsLindelof s
this : ∀ (x : X), {x} ∈ 𝓝 x
t : Set X
ht : t.Countable
left✝ : ∀ x ∈ t, x ∈ s
hssubt : s ⊆ ⋃ x ∈ t, {x}
⊢ s.Countable

Tactic:
rw [biUnion_of_singleton] at hssubt

Result:
case intro.intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsLindelof s
this : ∀ (x : X), {x} ∈ 𝓝 x
t : Set X
ht : t.Countable
left✝ : ∀ x ∈ t, x ∈ s
hssubt : s ⊆ t
⊢ s.Countable

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsLindelof s
this : ∀ (x : X), {x} ∈ 𝓝 x
⊢ s.Countable

Tactic:
rcases hs.elim_nhds_subcover (fun x => {x}) fun x _ => this x with ⟨t, ht, _, hssubt⟩

Result:
case intro.intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsLindelof s
this : ∀ (x : X), {x} ∈ 𝓝 x
t : Set X
ht : t.Countable
left✝ : ∀ x ∈ t, x ∈ s
hssubt : s ⊆ ⋃ x ∈ t, {x}
⊢ s.Countable

Proof state:
case intro.intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsLindelof s
this : ∀ (x : X), {x} ∈ 𝓝 x
t : Set X
ht : t.Countable
left✝ : ∀ x ∈ t, x ∈ s
hssubt : s ⊆ t
⊢ s.Countable

Tactic:
exact ht.mono hssubt

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/StupidTrunc.lean
@[reassoc (attr := simp)]
lemma stupidTruncMap_stupidTruncXIso_hom {i : ι} {i' : ι'} (hi : e.f i = i') :
    (stupidTruncMap φ e).f i' ≫ (L.stupidTruncXIso e hi).hom =
      (K.stupidTruncXIso e hi).hom ≫ φ.f i'

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
i' : ι'
hi : e.f i = i'
⊢ (stupidTruncMap φ e).f i' ≫ (L.stupidTruncXIso e hi).hom = (K.stupidTruncXIso e hi).hom ≫ φ.f i'

Tactic:
subst hi

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
⊢ (stupidTruncMap φ e).f (e.f i) ≫ (L.stupidTruncXIso e ⋯).hom = (K.stupidTruncXIso e ⋯).hom ≫ φ.f (e.f i)

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
⊢ (stupidTruncMap φ e).f (e.f i) ≫ (L.stupidTruncXIso e ⋯).hom = (K.stupidTruncXIso e ⋯).hom ≫ φ.f (e.f i)

Tactic:
simp [stupidTruncMap, stupidTruncXIso, extendMap_f _ _ rfl]

Result:
no goals