harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/BifunctorAssociator.lean
@[reassoc (attr := simp)]
lemma ι_D₃ :
    ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h ≫ D₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j' =
      d₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝²³ : Category.{u_15, u_1} C₁
inst✝²² : Category.{u_17, u_2} C₂
inst✝²¹ : Category.{u_16, u_5} C₃
inst✝²⁰ : Category.{u_13, u_6} C₄
inst✝¹⁹ : Category.{u_14, u_4} C₂₃
inst✝¹⁸ : HasZeroMorphisms C₁
inst✝¹⁷ : HasZeroMorphisms C₂
inst✝¹⁶ : HasZeroMorphisms C₃
inst✝¹⁵ : Preadditive C₂₃
inst✝¹⁴ : Preadditive C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹³ : G₂₃.PreservesZeroMorphisms
inst✝¹² : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹¹ : F.PreservesZeroMorphisms
inst✝¹⁰ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝⁹ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁸ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁷ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁶ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁵ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁴ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝³ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝² : DecidableEq ι₂₃
inst✝¹ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
⊢ ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h ≫ D₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j' =
    d₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'

Tactic:
simp [D₃]

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem sup_inf_self : a ⊔ a ⊓ b = a

Proof state:
α : Type u
inst✝ : Lattice α
a b : α
⊢ a ⊔ a ⊓ b = a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem nodup_replicate {n : Nat} {a : α} :
    (replicate n a).Nodup ↔ n ≤ 1

Proof state:
α : Type u_1
n : Nat
a : α
⊢ (replicate n a).Nodup ↔ n ≤ 1

Tactic:
simp [Nodup]

Result:
no goals
-- Mathlib/Data/Nat/GCD/BigOperators.lean
theorem coprime_fintype_prod_right_iff [Fintype ι] {x : ℕ} {s : ι → ℕ} :
    Coprime x (∏ i, s i) ↔ ∀ i, Coprime x (s i)

Proof state:
ι : Type u_1
inst✝ : Fintype ι
x : ℕ
s : ι → ℕ
⊢ x.Coprime (∏ i : ι, s i) ↔ ∀ (i : ι), x.Coprime (s i)

Tactic:
simp [coprime_prod_right_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Trace.lean
theorem trace_eq : trace (stdBasisMatrix i i c) = c

Proof state:
n : Type u_10
α : Type u_12
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : AddCommMonoid α
i : n
c : α
⊢ (stdBasisMatrix i i c).trace = c

Tactic:
simp [trace, -diag_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem isEmpty_alter (h : m.1.WF) {k : α} {f : Option β → Option β} :
    (Const.alter m k f).1.isEmpty = ((m.1.isEmpty || (m.1.size == 1 && m.contains k)) &&
      (f (Const.get? m k)).isNone)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k : α
f : Option β → Option β
⊢ (alter m k f).val.isEmpty = ((m.val.isEmpty || m.val.size == 1 && m.contains k) && (f (get? m k)).isNone)

Tactic:
simp_to_model [Const.alter] using List.Const.isEmpty_alterKey

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem tendsto_nhds_Prop {l : Filter α} {p : α → Prop} {q : Prop} :
    Tendsto p l (𝓝 q) ↔ (q → ∀ᶠ x in l, p x)

Proof state:
α : Type u_1
l : Filter α
p : α → Prop
q : Prop
⊢ Tendsto p l (𝓝 q) ↔ q → ∀ᶠ (x : α) in l, p x

Tactic:
by_cases q <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/Algebra/Tower.lean
theorem algebraMap_apply (x : R) : algebraMap R A x = algebraMap S A (algebraMap R S x)

Proof state:
R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
x : R
⊢ (algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)

Tactic:
rw [algebraMap_eq R S A, RingHom.comp_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapIdx_push {l : Vector α n} {a : α} :
    mapIdx f (l.push a) = (mapIdx f l).push (f l.size a)

Proof state:
α : Type u_1
n : Nat
α✝ : Type u_2
f : Nat → α → α✝
l : Vector α n
a : α
⊢ mapIdx f (l.push a) = (mapIdx f l).push (f l.size a)

Tactic:
simp [← append_singleton, mapIdx_append]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem Any_reverse {t : RBNode α} : t.reverse.Any p ↔ t.Any p

Proof state:
α : Type u_1
p : α → Prop
t : RBNode α
⊢ Any p t.reverse ↔ Any p t

Tactic:
simp [Any_def]

Result:
no goals
-- Mathlib/CategoryTheory/Enriched/FunctorCategory.lean
@[reassoc (attr := simp)]
lemma enrichedId_π (j : J) : enrichedId V F₁ ≫ end_.π _ j = eId V (F₁.obj j)

Proof state:
V : Type u₁
inst✝⁵ : Category.{v₁, u₁} V
inst✝⁴ : MonoidalCategory V
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
J : Type u₃
inst✝² : Category.{v₃, u₃} J
inst✝¹ : EnrichedOrdinaryCategory V C
F₁ : J ⥤ C
inst✝ : HasEnrichedHom V F₁ F₁
j : J
⊢ enrichedId V F₁ ≫ end_.π (diagram V F₁ F₁) j = eId V (F₁.obj j)

Tactic:
simp [enrichedId]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem getElem_idxOf [DecidableEq α] {a : α} : ∀ {l : List α} (h : idxOf a l < l.length),
    l[idxOf a l] = a
  | b :: l, h => by
    by_cases h' : b = a <;>
    simp [h', if_pos, if_false, getElem_idxOf]

Proof state:
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
h : idxOf a (b :: l) < (b :: l).length
⊢ (b :: l)[idxOf a (b :: l)] = a

Tactic:
by_cases h' : b = a <;>
simp [h', if_pos, if_false, getElem_idxOf]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/FourFunctions.lean
private lemma four_functions_theorem_aux (h₁ : 0 ≤ f₁) (h₂ : 0 ≤ f₂) (h₃ : 0 ≤ f₃) (h₄ : 0 ≤ f₄)
    (h : ∀ s t, f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)) (𝒜 ℬ : Finset (Finset α)) :
    (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : LinearOrderedCommSemiring β
f₁ f₂ f₃ f₄ : Finset α → β
inst✝¹ : ExistsAddOfLE β
inst✝ : Fintype α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (s t : Finset α), f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
⊢ (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s

Tactic:
refine univ.four_functions_theorem h₁ h₂ h₃ h₄ ?_ ?_ ?_ <;> simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldr_reverse (l : List α) (f : α → β → β) (b) :
    l.reverse.foldr f b = l.foldl (fun x y => f y x) b :=
  (foldl_reverse ..).symm.trans <| by simp

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → β → β
b : β
⊢ foldl (fun y x => f x y) b l.reverse.reverse = foldl (fun x y => f y x) b l

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Fold.lean
theorem foldrM_loop_succ [Monad m] (f : Fin n → α → m α) (x) (h : i < n) :
    foldrM.loop n f ⟨i+1, h⟩ x = f ⟨i, h⟩ x >>= foldrM.loop n f ⟨i, Nat.le_of_lt h⟩

Proof state:
m : Type u_1 → Type u_2
n : Nat
α : Type u_1
i : Nat
inst✝ : Monad m
f : Fin n → α → m α
x : α
h : i < n
⊢ foldrM.loop n f ⟨i + 1, h⟩ x = f ⟨i, h⟩ x >>= foldrM.loop n f ⟨i, ⋯⟩

Tactic:
rw [foldrM.loop]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem modifyHead_modifyHead {l : List α} {f g : α → α} :
    (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f)

Proof state:
α : Type u_1
l : List α
f g : α → α
⊢ modifyHead g (modifyHead f l) = modifyHead (g ∘ f) l

Tactic:
cases l <;> simp [modifyHead]

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsRestriction.eq_or_isStrictRestriction (h : N ≤r M) : N = M ∨ N <r M

Proof state:
α : Type u_1
M N : Matroid α
h : N ≤r M
⊢ N = M ∨ N <r M

Tactic:
simpa using eq_or_lt_of_le (ofMatroid_le_iff.2 h)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
    m.1.keys.Pairwise (fun a b => (a == b) = false)

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
⊢ List.Pairwise (fun a b => (a == b) = false) m.val.keys

Tactic:
simp_to_model using (Raw.WF.out h).distinct.distinct

Result:
no goals
-- Mathlib/RingTheory/Coalgebra/MonoidAlgebra.lean
theorem comul_C_mul_T_self (a : R) (n : ℤ) :
    Coalgebra.comul (C a * T n) = T n ⊗ₜ[R] (C a * T n)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a : R
n : ℤ
⊢ CoalgebraStruct.comul (C a * T n) = T n ⊗ₜ[R] (C a * T n)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/Image.lean
lemma MonotoneOn.mapsTo_Iic (h : MonotoneOn f (Iic b)) : MapsTo f (Iic b) (Iic (f b)) :=
  fun _ _ ↦ by aesop

Proof state:
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
b : α
h : MonotoneOn f (Iic b)
x✝¹ : α
x✝ : x✝¹ ∈ Iic b
⊢ f x✝¹ ∈ Iic (f b)

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma lift' (hS : S.Exact) {A : C} (k : A ⟶ S.X₂) (hk : k ≫ S.g = 0) [Mono S.f] :
    ∃ (l : A ⟶ S.X₁), l ≫ S.f = k :=
  ⟨hS.lift k hk, by simp⟩

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
hS : S.Exact
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝ : Mono S.f
⊢ hS.lift k hk ≫ S.f = k

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem castSucc_eq_zero_iff' [NeZero n] (a : Fin n) : castSucc a = 0 ↔ a = 0 :=
  Fin.ext_iff.trans <| (Fin.ext_iff.trans <| by simp).symm

Proof state:
n : ℕ
inst✝ : NeZero n
a : Fin n
⊢ ↑a = ↑0 ↔ ↑a.castSucc = ↑0

Tactic:
simp

Result:
no goals
-- Mathlib/ModelTheory/Order.lean
theorem noBotOrder_of_dlo [M ⊨ L.dlo] : NoBotOrder M :=
  realize_noBotOrder_iff.1 (L.dlo.realize_sentence_of_mem (by
    simp only [dlo, Set.union_insert, Set.union_singleton, Set.mem_insert_iff, true_or, or_true]))

Proof state:
L : Language
M : Type w'
inst✝⁴ : L.IsOrdered
inst✝³ : L.Structure M
inst✝² : LE M
inst✝¹ : L.OrderedStructure M
inst✝ : M ⊨ L.dlo
⊢ L.noBotOrderSentence ∈ L.dlo

Tactic:
simp only [dlo, Set.union_insert, Set.union_singleton, Set.mem_insert_iff, true_or, or_true]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/PureCoherence.lean
theorem naturality_comp {p f g h pf : C} {η : f ≅ g} {θ : g ≅ h}
    (η_f : p ⊗ f ≅ pf) (η_g : p ⊗ g ≅ pf) (η_h : p ⊗ h ≅ pf)
    (ih_η : p ◁ η ≪≫ η_g = η_f) (ih_θ : p ◁ θ ≪≫ η_h = η_g) :
    p ◁ (η ≪≫ θ) ≪≫ η_h = η_f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf : C
η : f ≅ g
θ : g ≅ h
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
η_h : p ⊗ h ≅ pf
ih_η : p ◁ η ≪≫ η_g = η_f
ih_θ : p ◁ θ ≪≫ η_h = η_g
⊢ p ◁ (η ≪≫ θ) ≪≫ η_h = η_f

Tactic:
simp_all

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem succ_le_succ_iff_of_not_isMax (ha : ¬IsMax a) (hb : ¬IsMax b) :
    succ a ≤ succ b ↔ a ≤ b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
hb : ¬IsMax b
⊢ succ a ≤ succ b ↔ a ≤ b

Tactic:
rw [succ_le_iff_of_not_isMax ha, lt_succ_iff_of_not_isMax hb]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem sq_one {a : ℤ} {b : ℕ} (h : a.gcd b = 1) : J(a | b) ^ 2 = 1

Proof state:
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
⊢ J(a | b) ^ 2 = 1

Tactic:
rcases eq_one_or_neg_one h with h₁ | h₁ <;> rw [h₁] <;> rfl

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem sign_neg (ha : a < 0) : sign a = -1

Proof state:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a : α
ha : a < 0
⊢ sign a = -1

Tactic:
rwa [sign_apply, if_neg <| asymm ha, if_pos]

Result:
no goals
-- Mathlib/Topology/Compactness/SigmaCompact.lean
protected lemma Topology.IsClosedEmbedding.sigmaCompactSpace {e : Y → X}
    (he : IsClosedEmbedding e) : SigmaCompactSpace Y :=
  ⟨⟨fun n => e ⁻¹' compactCovering X n, fun _ =>
      he.isCompact_preimage (isCompact_compactCovering _ _), by
      rw [← preimage_iUnion, iUnion_compactCovering, preimage_univ]⟩⟩

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : SigmaCompactSpace X
e : Y → X
he : IsClosedEmbedding e
⊢ ⋃ n, (fun n => e ⁻¹' compactCovering X n) n = univ

Tactic:
rw [← preimage_iUnion, iUnion_compactCovering, preimage_univ]

Result:
no goals
-- Mathlib/Data/List/OfFn.lean
theorem forall_mem_ofFn_iff {n : ℕ} {f : Fin n → α} {P : α → Prop} :
    (∀ i ∈ ofFn f, P i) ↔ ∀ j : Fin n, P (f j)

Proof state:
α : Type u
n : ℕ
f : Fin n → α
P : α → Prop
⊢ (∀ i ∈ ofFn f, P i) ↔ ∀ (j : Fin n), P (f j)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem coprodMap_apply_single (f : ∀ i : ι, M i →ₗ[R] N) (i : ι) (x : M i) :
    coprodMap f (single i x) = f i x

Proof state:
ι : Type u_1
R : Type u_2
M : ι → Type u_4
N : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
f : (i : ι) → M i →ₗ[R] N
i : ι
x : M i
⊢ (coprodMap f) (single i x) = (f i) x

Tactic:
simp [coprodMap]

Result:
no goals
-- Mathlib/Data/Multiset/Dedup.lean
theorem Subset.dedup_add_left {s t : Multiset α} (h : t ⊆ s) :
    dedup (s + t) = dedup s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : t ⊆ s
⊢ (s + t).dedup = s.dedup

Tactic:
rw [s.add_comm, Subset.dedup_add_right h]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem le_trailingDegree_monomial : ↑n ≤ trailingDegree (monomial n a) :=
  letI := Classical.decEq R
  if ha : a = 0 then by simp [ha] else (trailingDegree_monomial ha).ge

Proof state:
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
this : DecidableEq R := Classical.decEq R
ha : a = 0
⊢ ↑n ≤ ((monomial n) a).trailingDegree

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem lt_cons_self (s : Multiset α) (a : α) : s < a ::ₘ s :=
  Quot.inductionOn s fun l =>
    suffices l <+~ a :: l ∧ ¬l ~ a :: l by simpa [lt_iff_le_and_ne]
    ⟨(sublist_cons_self _ _).subperm,
      fun p => _root_.ne_of_lt (lt_succ_self (length l)) p.length_eq⟩

Proof state:
α : Type u_1
s : Multiset α
a : α
l : List α
this : l <+~ a :: l ∧ ¬l ~ a :: l
⊢ Quot.mk (⇑(isSetoid α)) l < a ::ₘ Quot.mk (⇑(isSetoid α)) l

Tactic:
simpa [lt_iff_le_and_ne]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_option {α : Type u} : #(Option α) = #α + 1

Proof state:
α : Type u
⊢ #(Option α) = #α + 1

Tactic:
rw [(Equiv.optionEquivSumPUnit.{u, u} α).cardinal_eq, mk_sum, mk_eq_one PUnit, lift_id, lift_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem forM_append [Monad m] [LawfulMonad m] (l₁ l₂ : List α) (f : α → m PUnit) :
    forM (l₁ ++ l₂) f = (do forM l₁ f; forM l₂ f)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l₁ l₂ : List α
f : α → m PUnit
⊢ forM (l₁ ++ l₂) f = do
    forM l₁ f
    forM l₂ f

Tactic:
induction l₁ <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem IsPartition.compl_eq_bot {π : Prepartition I} (h : IsPartition π) : π.compl = ⊥

Proof state:
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
h : π.IsPartition
⊢ π.compl = ⊥

Tactic:
rw [← iUnion_eq_empty, iUnion_compl, h.iUnion_eq, diff_self]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem le_and : ∀ {x y z : Bool}, x ≤ y → x ≤ z → x ≤ (y && z)

Proof state:
⊢ ∀ {x y z : Bool}, x ≤ y → x ≤ z → x ≤ (y && z)

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem bne_self_eq_false' [DecidableEq α] (a : α) : (a != a) = false

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ (a != a) = false

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
theorem norm_apply_eq_norm_coef : ‖p n‖ = ‖coeff p n‖

Proof state:
𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
⊢ ‖p n‖ = ‖p.coeff n‖

Tactic:
rw [← mkPiRing_coeff_eq p, ContinuousMultilinearMap.norm_mkPiRing]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean
@[simp]
lemma rightDerivedNatTrans_id :
    rightDerivedNatTrans RF RF α α W (𝟙 F) = 𝟙 RF :=
  rightDerived_ext RF α W _ _ _ (by simp)

Proof state:
C : Type u_5
D : Type u_1
H : Type u_3
inst✝⁴ : Category.{u_6, u_5} C
inst✝³ : Category.{u_4, u_1} D
inst✝² : Category.{u_2, u_3} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
⊢ α ≫ whiskerLeft L (RF.rightDerivedNatTrans RF α α W (𝟙 F)) = α ≫ whiskerLeft L (𝟙 RF)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Star/Basic.lean
theorem eq_star_of_eq_star [InvolutiveStar R] {r s : R} (h : r = star s) : s = star r

Proof state:
R : Type u
inst✝ : InvolutiveStar R
r s : R
h : r = star s
⊢ s = star r

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Diam.lean
theorem diam_pos_iff : 0 < diam s ↔ s.Nontrivial

Proof state:
β : Type u_2
inst✝ : EMetricSpace β
s : Set β
⊢ 0 < diam s ↔ s.Nontrivial

Tactic:
simp only [pos_iff_ne_zero, Ne, diam_eq_zero_iff, Set.not_subsingleton_iff]

Result:
no goals
-- Mathlib/Data/Finsupp/NeLocus.lean
theorem neLocus_self_sub_left : neLocus (f - g) f = g.support

Proof state:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ (f - g).neLocus f = g.support

Tactic:
rw [neLocus_comm, neLocus_self_sub_right]

Result:
no goals
-- Mathlib/Order/Cover.lean
theorem mk_covBy_mk_iff_left : (a₁, b) ⋖ (a₂, b) ↔ a₁ ⋖ a₂

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b : β
⊢ (a₁, b) ⋖ (a₂, b) ↔ a₁ ⋖ a₂

Tactic:
simp_rw [covBy_iff_wcovBy_and_lt, mk_wcovBy_mk_iff_left, mk_lt_mk_iff_left]

Result:
no goals
-- Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
theorem apply_eq_prod_smul_coeff : p n y = (∏ i, y i) • p.coeff n

Proof state:
𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
y : Fin n → 𝕜
⊢ (p n) y = (∏ i : Fin n, y i) • p.coeff n

Tactic:
convert (p n).toMultilinearMap.map_smul_univ y 1

Result:
case h.e'_2.h.e'_1.h
𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
y : Fin n → 𝕜
x✝ : Fin n
⊢ y x✝ = y x✝ • 1 x✝

Proof state:
case h.e'_2.h.e'_1.h
𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
y : Fin n → 𝕜
x✝ : Fin n
⊢ y x✝ = y x✝ • 1 x✝

Tactic:
simp only [Pi.one_apply, Algebra.id.smul_eq_mul, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem cond_false (discr : Bool) (lhs rhs : BitVec w) :
    (discr || ((bif discr then lhs else rhs) == rhs)) = true

Proof state:
w : Nat
discr : Bool
lhs rhs : BitVec w
⊢ (discr || (bif discr then lhs else rhs) == rhs) = true

Tactic:
cases discr <;> simp

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Basic.lean
lemma term_congr {f g : ℕ → ℂ} (h : ∀ {n}, n ≠ 0 → f n = g n) (s : ℂ) (n : ℕ) :
    term f s n = term g s n

Proof state:
f g : ℕ → ℂ
h : ∀ {n : ℕ}, n ≠ 0 → f n = g n
s : ℂ
n : ℕ
⊢ term f s n = term g s n

Tactic:
rcases eq_or_ne n 0 with hn | hn <;> simp [hn, h]

Result:
no goals
-- Mathlib/Data/Set/Accumulate.lean
theorem mem_accumulate [LE α] {x : α} {z : β} : z ∈ Accumulate s x ↔ ∃ y ≤ x, z ∈ s y

Proof state:
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : LE α
x : α
z : β
⊢ z ∈ Accumulate s x ↔ ∃ y ≤ x, z ∈ s y

Tactic:
simp_rw [accumulate_def, mem_iUnion₂, exists_prop]

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
theorem app_invApp' (U) (hU : U ≤ f.opensRange) :
    f.app U ≫ (f.appIso (f ⁻¹ᵁ U)).inv =
      Y.presheaf.map (eqToHom (Opens.ext <| by simpa [Set.image_preimage_eq_inter_range])).op :=
  PresheafedSpace.IsOpenImmersion.app_invApp _ _

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U : Y.Opens
hU : U ≤ f.opensRange
⊢ ↑(f ''ᵁ f ⁻¹ᵁ U) = ↑U

Tactic:
simpa [Set.image_preimage_eq_inter_range]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem digits_zero (b : ℕ) : digits b 0 = []

Proof state:
b : ℕ
⊢ b.digits 0 = []

Tactic:
rcases b with (_ | ⟨_ | ⟨_⟩⟩) <;> simp [digits, digitsAux0, digitsAux1]

Result:
no goals
-- Mathlib/Analysis/Complex/Basic.lean
@[simp]
lemma neg_ofReal_mem_slitPlane {x : ℝ} : -↑x ∈ slitPlane ↔ x < 0

Proof state:
x : ℝ
⊢ -↑x ∈ slitPlane ↔ x < 0

Tactic:
simpa using ofReal_mem_slitPlane (x := -x)

Result:
no goals
-- Mathlib/Data/List/Nodup.lean
theorem Nodup.mem_diff_iff [DecidableEq α] (hl₁ : l₁.Nodup) : a ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ a ∉ l₂

Proof state:
α : Type u
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
hl₁ : l₁.Nodup
⊢ a ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ a ∉ l₂

Tactic:
rw [hl₁.diff_eq_filter, mem_filter, decide_eq_true_iff]

Result:
no goals
-- Mathlib/Analysis/Complex/RealDeriv.lean
theorem HasDerivAt.comp_ofReal (hf : HasDerivAt e e' ↑z) : HasDerivAt (fun y : ℝ => e ↑y) e' z

Proof state:
e : ℂ → ℂ
e' : ℂ
z : ℝ
hf : HasDerivAt e e' ↑z
⊢ HasDerivAt (fun y => e ↑y) e' z

Tactic:
simpa only [ofRealCLM_apply, ofReal_one, mul_one] using hf.comp z ofRealCLM.hasDerivAt

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem tensor_dite {P : Prop} [Decidable P] {W X Y Z : C} (f : W ⟶ X) (g : P → (Y ⟶ Z))
    (g' : ¬P → (Y ⟶ Z)) : (f ⊗ if h : P then g h else g' h) =
    if h : P then f ⊗ g h else f ⊗ g' h

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
⊢ (f ⊗ if h : P then g h else g' h) = if h : P then f ⊗ g h else f ⊗ g' h

Tactic:
split_ifs <;> rfl

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem symm_map_nhds_eq {x} (hx : x ∈ e.source) : map e.symm (𝓝 (e x)) = 𝓝 x :=
  (e.symm.map_nhds_eq <| e.map_source hx).trans <| by rw [e.left_inv hx]

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : X
hx : x ∈ e.source
⊢ 𝓝 (↑e.symm (↑e x)) = 𝓝 x

Tactic:
rw [e.left_inv hx]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem frequently_bot {p : α → Prop} : ¬∃ᶠ x in ⊥, p x

Proof state:
α : Type u
p : α → Prop
⊢ ¬∃ᶠ (x : α) in ⊥, p x

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Perfection.lean
theorem mk' {f : P →+* R} (g : P ≃+* Ring.Perfection R p) (hfg : Perfection.lift p P R f = g) :
    PerfectionMap p f :=
  { injective := fun x y hxy =>
      g.injective <|
        (RingHom.ext_iff.1 hfg x).symm.trans <|
          Eq.symm <| (RingHom.ext_iff.1 hfg y).symm.trans <| Perfection.ext fun n => (hxy n).symm
    surjective := fun y hy =>
      let ⟨x, hx⟩ := g.surjective ⟨y, hy⟩
      ⟨x, fun n =>
        show Perfection.coeff R p n (Perfection.lift p P R f x) = Perfection.coeff R p n ⟨y, hy⟩ by
          simp [hfg, hx]⟩ }

Proof state:
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
R : Type u₁
inst✝⁴ : CommSemiring R
inst✝³ : CharP R p
P : Type u₃
inst✝² : CommSemiring P
inst✝¹ : CharP P p
inst✝ : PerfectRing P p
f : P →+* R
g : P ≃+* Ring.Perfection R p
hfg : (Perfection.lift p P R) f = ↑g
y : ℕ → R
hy : ∀ (n : ℕ), y (n + 1) ^ p = y n
x : P
hx : g x = ⟨y, hy⟩
n : ℕ
⊢ (Perfection.coeff R p n) (((Perfection.lift p P R) f) x) = (Perfection.coeff R p n) ⟨y, hy⟩

Tactic:
simp [hfg, hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem bne_self_right : ∀(a b : Bool), ((a != b) != b) = a

Proof state:
⊢ ∀ (a b : Bool), ((a != b) != b) = a

Tactic:
decide

Result:
no goals