harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
@[simp]
lemma idemFst_add_idemSnd :
    idemFst + idemSnd = (1 : AddMonoid.End (WithLp p (α × β))) := AddMonoidHom.ext
  fun x => by
    rw [AddMonoidHom.add_apply, idemFst_apply, idemSnd_apply, AddMonoid.End.coe_one, id_eq,
      ← WithLp.equiv_symm_add, Prod.mk_add_mk, zero_add, add_zero]
    rfl

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
p : ℝ≥0∞
x : WithLp p (α × β)
⊢ (WithLp.equiv p (α × β)).symm (x.1, x.2) = x

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
p : ℝ≥0∞
x : WithLp p (α × β)
⊢ (idemFst + idemSnd) x = 1 x

Tactic:
rw [AddMonoidHom.add_apply, idemFst_apply, idemSnd_apply, AddMonoid.End.coe_one, id_eq,
  ← WithLp.equiv_symm_add, Prod.mk_add_mk, zero_add, add_zero]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
p : ℝ≥0∞
x : WithLp p (α × β)
⊢ (WithLp.equiv p (α × β)).symm (x.1, x.2) = x
-- Mathlib/NumberTheory/DiophantineApproximation/Basic.lean
theorem convergent_of_int {ξ : ℤ} (n : ℕ) : convergent ξ n = ξ

Proof state:
case succ
ξ : ℤ
n✝ : ℕ
⊢ (↑ξ).convergent (n✝ + 1) = ↑ξ

Tactic:
simp only [convergent_succ, floor_intCast, fract_intCast, convergent_of_zero, add_zero,
  inv_zero]

Result:
no goals

Proof state:
ξ : ℤ
n : ℕ
⊢ (↑ξ).convergent n = ↑ξ

Tactic:
cases n

Result:
case zero
ξ : ℤ
⊢ (↑ξ).convergent 0 = ↑ξ

case succ
ξ : ℤ
n✝ : ℕ
⊢ (↑ξ).convergent (n✝ + 1) = ↑ξ

Proof state:
case zero
ξ : ℤ
⊢ (↑ξ).convergent 0 = ↑ξ

Tactic:
simp only [convergent_zero, floor_intCast]

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
theorem lieBracketWithin_inter (ht : t ∈ 𝓝 x) :
    lieBracketWithin 𝕜 V W (s ∩ t) x = lieBracketWithin 𝕜 V W s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s t : Set E
x : E
ht : t ∈ 𝓝 x
⊢ lieBracketWithin 𝕜 V W (s ∩ t) x = lieBracketWithin 𝕜 V W s x

Tactic:
simp [lieBracketWithin, fderivWithin_inter, ht]

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem IsWF.min_eq_of_lt (hs : s.IsWF) (ha : a ∈ s) (hlt : ∀ b ∈ s, b ≠ a → a < b) :
    hs.min (nonempty_of_mem ha) = a

Proof state:
α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
hs : s.IsWF
ha : a ∈ s
hlt : ∀ b ∈ s, b ≠ a → a < b
⊢ hs.min ⋯ = a

Tactic:
by_contra h

Result:
α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
hs : s.IsWF
ha : a ∈ s
hlt : ∀ b ∈ s, b ≠ a → a < b
h : ¬hs.min ⋯ = a
⊢ False

Proof state:
α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
hs : s.IsWF
ha : a ∈ s
hlt : ∀ b ∈ s, b ≠ a → a < b
h : ¬hs.min ⋯ = a
⊢ False

Tactic:
exact (hs.not_lt_min (nonempty_of_mem ha) ha) (hlt (hs.min (nonempty_of_mem ha))
  (hs.min_mem (nonempty_of_mem ha)) h)

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
/-- **Vertical line test** for linear maps.

Let `G ≤ H × I` be a submodule of a product of modules. Assume that `G` maps bijectively to the
first factor. Then `G` is the graph of some linear map `f : H →ₗ[R] I`. -/
lemma Submodule.exists_eq_graph {G : Submodule S (H × I)} (hf₁ : Bijective (Prod.fst ∘ G.subtype)) :
    ∃ f : H →ₗ[S] I, G = LinearMap.graph f

Proof state:
S : Type u_4
H : Type u_6
I : Type u_7
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
G : Submodule S (H × I)
hf₁ : Bijective (Prod.fst ∘ ⇑G.subtype)
⊢ ∃ f, G = f.graph

Tactic:
simpa only [range_subtype] using LinearMap.exists_range_eq_graph hf₁.surjective
    (fun a b h ↦ congr_arg (Prod.snd ∘ G.subtype) (hf₁.injective h))

Result:
no goals
-- Mathlib/Analysis/Convolution.lean
theorem _root_.HasCompactSupport.hasFDerivAt_convolution_left [IsNegInvariant μ]
    (hcf : HasCompactSupport f) (hf : ContDiff 𝕜 1 f) (hg : LocallyIntegrable g μ) (x₀ : G) :
    HasFDerivAt (f ⋆[L, μ] g) ((fderiv 𝕜 f ⋆[L.precompL G, μ] g) x₀) x₀

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedSpace 𝕜 E'
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : BorelSpace G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SFinite μ
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : μ.IsNegInvariant
hcf : HasCompactSupport f
hf : ContDiff 𝕜 1 f
hg : LocallyIntegrable g μ
x₀ : G
⊢ HasFDerivAt (g ⋆[L.flip, μ] f) ((g ⋆[(precompL G L).flip, μ] fderiv 𝕜 f) x₀) x₀

Tactic:
exact hcf.hasFDerivAt_convolution_right L.flip hg hf x₀

Result:
no goals

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedSpace 𝕜 E'
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : BorelSpace G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SFinite μ
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : μ.IsNegInvariant
hcf : HasCompactSupport f
hf : ContDiff 𝕜 1 f
hg : LocallyIntegrable g μ
x₀ : G
⊢ HasFDerivAt (f ⋆[L, μ] g) ((fderiv 𝕜 f ⋆[precompL G L, μ] g) x₀) x₀

Tactic:
simp (config := { singlePass := true }) only [← convolution_flip]

Result:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedSpace 𝕜 E'
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : BorelSpace G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SFinite μ
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : μ.IsNegInvariant
hcf : HasCompactSupport f
hf : ContDiff 𝕜 1 f
hg : LocallyIntegrable g μ
x₀ : G
⊢ HasFDerivAt (g ⋆[L.flip, μ] f) ((g ⋆[(precompL G L).flip, μ] fderiv 𝕜 f) x₀) x₀
-- Mathlib/CategoryTheory/Subterminal.lean
theorem isSubterminal_of_terminal [HasTerminal C] : IsSubterminal (⊤_ C) := fun _ _ _ => by
  subsingleton

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasTerminal C
x✝² : C
x✝¹ x✝ : x✝² ⟶ ⊤_ C
⊢ x✝¹ = x✝

Tactic:
subsingleton

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_insertListIfNewUnit [BEq α] [PartialEquivBEq α]
    {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α}:
    getValue? k (insertListIfNewUnit l toInsert) =
    if containsKey k l ∨ toInsert.contains k then some () else none

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
⊢ getValue? k (insertListIfNewUnit l toInsert) =
    if containsKey k l = true ∨ toInsert.contains k = true then some () else none

Tactic:
simp [containsKey_insertListIfNewUnit, getValue?_list_unit]

Result:
no goals
-- Mathlib/Algebra/Star/Module.lean
theorem selfAdjointPart_comp_subtype_skewAdjoint :
    (selfAdjointPart R).comp (skewAdjoint.submodule R A).subtype = 0 :=
  LinearMap.ext fun ⟨x, (hx : _ = _)⟩ ↦ Subtype.eq <| by simp [hx]

Proof state:
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x✝ : ↥(skewAdjoint.submodule R A)
x : A
hx : star x = -x
⊢ ↑((selfAdjointPart R ∘ₗ (skewAdjoint.submodule R A).subtype) ⟨x, hx⟩) = ↑(0 ⟨x, hx⟩)

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_eq_empty_iff {f : α → β} {l : Array α} : map f l = #[] ↔ l = #[]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ map f l = #[] ↔ l = #[]

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
toList✝ : List α
⊢ map f { toList := toList✝ } = #[] ↔ { toList := toList✝ } = #[]

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
toList✝ : List α
⊢ map f { toList := toList✝ } = #[] ↔ { toList := toList✝ } = #[]

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem le_einfsep_iff {d} :
    d ≤ s.einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ edist x y

Proof state:
α : Type u_1
inst✝ : EDist α
s : Set α
d : ℝ≥0∞
⊢ d ≤ s.einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ edist x y

Tactic:
simp_rw [einfsep, le_iInf_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_le_log_iff (h : 0 < x) (h₁ : 0 < y) : log x ≤ log y ↔ x ≤ y

Proof state:
x y : ℝ
h : 0 < x
h₁ : 0 < y
⊢ log x ≤ log y ↔ x ≤ y

Tactic:
rw [← exp_le_exp, exp_log h, exp_log h₁]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_one : log 1 = 0 :=
  exp_injective <| by rw [exp_log zero_lt_one, exp_zero]

Proof state:
⊢ rexp (log 1) = rexp 0

Tactic:
rw [exp_log zero_lt_one, exp_zero]

Result:
no goals
-- Mathlib/Computability/Halting.lean
theorem part_iff₂ {f : ℕ → ℕ →. ℕ} : (@Partrec' 2 fun v => f v.head v.tail.head) ↔ Partrec₂ f :=
  part_iff.trans
    ⟨fun h =>
      (h.comp <| vector_cons.comp fst <| vector_cons.comp snd (const nil)).of_eq fun v => by
        simp only [head_cons, tail_cons],
      fun h => h.comp vector_head (vector_head.comp vector_tail)⟩

Proof state:
f : ℕ → ℕ →. ℕ
h : _root_.Partrec fun v => f v.head v.tail.head
v : ℕ × ℕ
⊢ f (v.1 ::ᵥ v.2 ::ᵥ nil).head (v.1 ::ᵥ v.2 ::ᵥ nil).tail.head = f v.1 v.2

Tactic:
simp only [head_cons, tail_cons]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Diam.lean
lemma diam_def : G.diam = (⨆ p : α × α, G.edist p.1 p.2).toNat

Proof state:
α : Type u_1
G : SimpleGraph α
⊢ G.diam = (⨆ p, G.edist p.1 p.2).toNat

Tactic:
rw [diam, ediam_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem rev_castAdd (k : Fin n) (m : Nat) : rev (castAdd m k) = addNat (rev k) m := Fin.ext <| by
  rw [val_rev, coe_castAdd, coe_addNat, val_rev, Nat.sub_add_comm (Nat.succ_le_of_lt k.is_lt)]

Proof state:
n : Nat
k : Fin n
m : Nat
⊢ ↑(castAdd m k).rev = ↑(k.rev.addNat m)

Tactic:
rw [val_rev, coe_castAdd, coe_addNat, val_rev, Nat.sub_add_comm (Nat.succ_le_of_lt k.is_lt)]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
@[simp] lemma closure_union_closure_right_eq (M : Matroid α) (X Y : Set α) :
    M.closure (X ∪ M.closure Y) = M.closure (X ∪ Y)

Proof state:
α : Type u_2
M : Matroid α
X Y : Set α
⊢ M.closure (X ∪ M.closure Y) = M.closure (X ∪ Y)

Tactic:
rw [← closure_closure_union_closure_eq_closure_union, closure_closure,
  closure_closure_union_closure_eq_closure_union]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
    ¬a ∈ m → getD m a fallback = fallback

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
a : α
fallback : β
⊢ ¬a ∈ m → getD m a fallback = fallback

Tactic:
simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem isUnit_submatrix_equiv {A : Matrix m m α} (e₁ e₂ : n ≃ m) :
    IsUnit (A.submatrix e₁ e₂) ↔ IsUnit A

Proof state:
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
⊢ IsUnit (A.submatrix ⇑e₁ ⇑e₂) ↔ IsUnit A

Tactic:
simp only [← nonempty_invertible_iff_isUnit,
  (submatrixEquivInvertibleEquivInvertible A _ _).nonempty_congr]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
/-- A general form of Möbius inversion. Based on lemma 2.1.3 of Incidence Algebras by Spiegel and
O'Donnell. -/
lemma moebius_inversion_bot (f g : α → 𝕜) (h : ∀ x, g x = ∑ y ∈ Iic x, f y) (x : α) :
    f x = ∑ y ∈ Iic x, mu 𝕜 y x * g y

Proof state:
case h.e'_3.a.h.e'_5
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Iic x, f y
x x✝ : α
a✝ : x✝ ∈ Ici x
⊢ (mu 𝕜) x✝ x = (mu 𝕜) x x✝

Tactic:
erw [mu_toDual]

Result:
no goals

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Iic x, f y
x : α
⊢ f x = ∑ y ∈ Iic x, (mu 𝕜) y x * g y

Tactic:
convert moebius_inversion_top (α := αᵒᵈ) f g h x using 3

Result:
case h.e'_3.a.h.e'_5
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Iic x, f y
x x✝ : α
a✝ : x✝ ∈ Ici x
⊢ (mu 𝕜) x✝ x = (mu 𝕜) x x✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_eq_none {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} :
    getValue? a l = none ↔ containsKey a l = false

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
a : α
⊢ getValue? a l = none ↔ containsKey a l = false

Tactic:
rw [getValue?_eq_getEntry?, Option.map_eq_none', getEntry?_eq_none]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Taylor.lean
theorem taylor_coeff_zero : (taylor r f).coeff 0 = f.eval r

Proof state:
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ ((taylor r) f).coeff 0 = eval r f

Tactic:
rw [taylor_coeff, hasseDeriv_zero, LinearMap.id_apply]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
lemma zero_pow_eq_one₀ [Nontrivial M₀] : (0 : M₀) ^ n = 1 ↔ n = 0

Proof state:
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
n : ℕ
inst✝ : Nontrivial M₀
⊢ 0 ^ n = 1 ↔ n = 0

Tactic:
rw [zero_pow_eq, one_ne_zero.ite_eq_left_iff]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem mul_one : φ * 1 = φ :=
  ext fun n => by simpa using coeff_add_mul_monomial n 0 φ 1

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff R n) (φ * 1) = (coeff R n) φ

Tactic:
simpa using coeff_add_mul_monomial n 0 φ 1

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
/-- See `inner_smul_left` for the common special when `𝕜 = 𝕝`. -/
lemma inner_smul_left_eq_star_smul (x y : E) (r : 𝕝) : ⟪r • x, y⟫ = r† • ⟪x, y⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst✝⁵ : CommSemiring 𝕝
inst✝⁴ : StarRing 𝕝
inst✝³ : Algebra 𝕝 𝕜
inst✝² : Module 𝕝 E
inst✝¹ : IsScalarTower 𝕝 𝕜 E
inst✝ : StarModule 𝕝 𝕜
x y : E
r : 𝕝
⊢ ⟪r • x, y⟫_𝕜 = (starRingEnd 𝕝) r • ⟪x, y⟫_𝕜

Tactic:
rw [← algebraMap_smul 𝕜 r, InnerProductSpace.smul_left, starRingEnd_apply, starRingEnd_apply,
  ← algebraMap_star_comm, ← smul_eq_mul, algebraMap_smul]

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem hom_inv_id_assoc (f : X ⟶ Y) [I : IsIso f] {Z} (g : X ⟶ Z) : f ≫ inv f ≫ g = g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
I : IsIso f
Z : C
g : X ⟶ Z
⊢ f ≫ inv f ≫ g = g

Tactic:
simp [← Category.assoc]

Result:
no goals
-- Mathlib/Data/List/Perm/Subperm.lean
/-- See also `List.subperm_ext_iff`. -/
lemma subperm_iff_count [DecidableEq α] : l₁ <+~ l₂ ↔ ∀ a, count a l₁ ≤ count a l₂ :=
  subperm_ext_iff.trans <| forall_congr' fun a ↦ by
    by_cases ha : a ∈ l₁ <;> simp [ha, count_eq_zero_of_not_mem]

Proof state:
α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
⊢ a ∈ l₁ → count a l₁ ≤ count a l₂ ↔ count a l₁ ≤ count a l₂

Tactic:
by_cases ha : a ∈ l₁ <;> simp [ha, count_eq_zero_of_not_mem]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
theorem eLpNorm'_le_eLpNormEssSup {q : ℝ} (hq_pos : 0 < q) [IsProbabilityMeasure μ] :
    eLpNorm' f q μ ≤ eLpNormEssSup f μ :=
  (eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ hq_pos).trans_eq (by simp [measure_univ])

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
f : α → E
q : ℝ
hq_pos : 0 < q
inst✝ : IsProbabilityMeasure μ
⊢ eLpNormEssSup f μ * μ Set.univ ^ (1 / q) = eLpNormEssSup f μ

Tactic:
simp [measure_univ]

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem ext {f g : α →ₘ[μ] β} (h : f =ᵐ[μ] g) : f = g

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f g : α →ₘ[μ] β
h : ↑f =ᶠ[ae μ] ↑g
⊢ f = g

Tactic:
rwa [← f.mk_coeFn, ← g.mk_coeFn, mk_eq_mk]

Result:
no goals
-- Mathlib/Order/RelSeries.lean
@[simp]
lemma last_take (p : RelSeries r) (i : Fin (p.length + 1)) :
    (p.take i).last = p i

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
i : Fin (p.length + 1)
⊢ (p.take i).last = p.toFun i

Tactic:
simp [take, last, Fin.last]

Result:
no goals
-- Mathlib/Combinatorics/Schnirelmann.lean
/-- The Schnirelmann density is unaffected by adding `0`. -/
@[simp] lemma schnirelmannDensity_insert_zero [DecidablePred (· ∈ insert 0 A)] :
    schnirelmannDensity (insert 0 A) = schnirelmannDensity A :=
  schnirelmannDensity_congr' (by aesop)

Proof state:
A : Set ℕ
inst✝¹ : DecidablePred fun x => x ∈ A
inst✝ : DecidablePred fun x => x ∈ insert 0 A
⊢ ∀ n > 0, n ∈ insert 0 A ↔ n ∈ A

Tactic:
aesop

Result:
no goals
-- Mathlib/CategoryTheory/CommSq.lean
/-- The horizontal composition of two commutative squares as below is a commutative square.
```
  W ---f---> X ---f'--> X'
  |          |          |
  g          h          h'
  |          |          |
  v          v          v
  Y ---i---> Z ---i'--> Z'

```
-/
lemma horiz_comp {W X X' Y Z Z' : C} {f : W ⟶ X} {f' : X ⟶ X'} {g : W ⟶ Y} {h : X ⟶ Z}
    {h' : X' ⟶ Z'} {i : Y ⟶ Z} {i' : Z ⟶ Z'} (hsq₁ : CommSq f g h i) (hsq₂ : CommSq f' h h' i') :
    CommSq (f ≫ f') g h' (i ≫ i') :=
  ⟨by rw [← Category.assoc, Category.assoc, ← hsq₁.w, hsq₂.w, Category.assoc]⟩

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W X X' Y Z Z' : C
f : W ⟶ X
f' : X ⟶ X'
g : W ⟶ Y
h : X ⟶ Z
h' : X' ⟶ Z'
i : Y ⟶ Z
i' : Z ⟶ Z'
hsq₁ : CommSq f g h i
hsq₂ : CommSq f' h h' i'
⊢ (f ≫ f') ≫ h' = g ≫ i ≫ i'

Tactic:
rw [← Category.assoc, Category.assoc, ← hsq₁.w, hsq₂.w, Category.assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem cons_eq_append_iff :
    x :: c = a ++ b ↔ (a = [] ∧ b = x :: c) ∨ (∃ a', a = x :: a' ∧ c = a' ++ b)

Proof state:
α✝ : Type u_1
x : α✝
c a b : List α✝
⊢ x :: c = a ++ b ↔ a = [] ∧ b = x :: c ∨ ∃ a', a = x :: a' ∧ c = a' ++ b

Tactic:
rw [eq_comm, append_eq_cons_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isSeparator_unop_iff (G : Cᵒᵖ) : IsSeparator (unop G) ↔ IsCoseparator G

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

Tactic:
rw [IsSeparator, IsCoseparator, ← isSeparating_unop_iff, Set.singleton_unop]

Result:
no goals
-- Mathlib/Algebra/BigOperators/WithTop.lean
/-- A sum is infinite iff one term is infinite. -/
@[simp] lemma sum_eq_top : ∑ i ∈ s, f i = ⊤ ↔ ∃ i ∈ s, f i = ⊤

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : AddCommMonoid α
s : Finset ι
f : ι → WithTop α
⊢ ∑ i ∈ s, f i = ⊤ ↔ ∃ i ∈ s, f i = ⊤

Tactic:
induction s using Finset.cons_induction <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Associated.lean
theorem exists_mem_multiset_le_of_prime {s : Multiset (Associates α)} {p : Associates α}
    (hp : Prime p) : p ≤ s.prod → ∃ a ∈ s, p ≤ a :=
  Multiset.induction_on s (fun ⟨_, eq⟩ => (hp.ne_one (mul_eq_one.1 eq.symm).1).elim)
    fun a s ih h =>
    have : p ≤ a * s.prod

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
s✝ : Multiset (Associates α)
p : Associates α
hp : Prime p
a : Associates α
s : Multiset (Associates α)
ih : p ≤ s.prod → ∃ a ∈ s, p ≤ a
h : p ≤ (a ::ₘ s).prod
⊢ p ≤ a * s.prod

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
theorem clog_of_left_le_one {b : ℕ} (hb : b ≤ 1) (n : ℕ) : clog b n = 0

Proof state:
b : ℕ
hb : b ≤ 1
n : ℕ
⊢ clog b n = 0

Tactic:
rw [clog, dif_neg fun h : 1 < b ∧ 1 < n => h.1.not_le hb]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem hasIntegral_iff : HasIntegral I l f vol y ↔
    ∀ ε > (0 : ℝ), ∃ r : ℝ≥0 → ℝⁿ → Ioi (0 : ℝ), (∀ c, l.RCond (r c)) ∧
      ∀ c π, l.MemBaseSet I c (r c) π → IsPartition π → dist (integralSum f vol π) y ≤ ε :=
  ((l.hasBasis_toFilteriUnion_top I).tendsto_iff nhds_basis_closedBall).trans <| by
    simp [@forall_swap ℝ≥0 (TaggedPrepartition I)]

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y : F
⊢ (∀ (ib : ℝ),
      0 < ib →
        ∃ ia,
          (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
            ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.IsPartition}, integralSum f vol x ∈ closedBall y ib) ↔
    ∀ ε > 0,
      ∃ r,
        (∀ (c : ℝ≥0), l.RCond (r c)) ∧
          ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
            l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ ε

Tactic:
simp [@forall_swap ℝ≥0 (TaggedPrepartition I)]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean
theorem eval_whiskerRight
    {f g : a ⟶ b} {h : b ⟶ c}
    {η η' : f ⟶ g} {θ : f ≫ h ⟶ g ≫ h}
    (e_η : η = η') (e_θ : η' ▷ h = θ) :
    η ▷ h = θ

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f g : a ⟶ b
h : b ⟶ c
η η' : f ⟶ g
θ : f ≫ h ⟶ g ≫ h
e_η : η = η'
e_θ : η' ▷ h = θ
⊢ η ▷ h = θ

Tactic:
simp [e_η, e_θ]

Result:
no goals
-- Mathlib/Analysis/Complex/Basic.lean
theorem lipschitz_equivRealProd : LipschitzWith 1 equivRealProd

Proof state:
⊢ LipschitzWith 1 ⇑equivRealProd

Tactic:
simpa using AddMonoidHomClass.lipschitz_of_bound equivRealProdLm 1 equivRealProd_apply_le'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem carry_of_and_eq_zero {x y : BitVec w} (h : x &&& y = 0#w) : carry i x y false = false

Proof state:
case zero
w : Nat
x y : BitVec w
h : x &&& y = 0#w
⊢ carry 0 x y false = false

Tactic:
simp

Result:
no goals

Proof state:
case succ
w : Nat
x y : BitVec w
i : Nat
ih : carry i x y false = false
h : (fun x => x.getLsbD i) (x &&& y) = (fun x => x.getLsbD i) 0#w
⊢ carry (i + 1) x y false = false

Tactic:
simp_all [carry_succ]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Final.lean
theorem initial_of_adjunction {L : C ⥤ D} {R : D ⥤ C} (adj : L ⊣ R) : Initial L :=
  { out := fun d =>
      let u : CostructuredArrow L d := CostructuredArrow.mk (adj.counit.app d)
      @zigzag_isConnected _ _ ⟨u⟩ fun f g =>
        Relation.ReflTransGen.trans
          (Relation.ReflTransGen.single
            (show Zag f u from
              Or.inl ⟨CostructuredArrow.homMk (adj.homEquiv f.left d f.hom) (by simp [u])⟩))
          (Relation.ReflTransGen.single
            (show Zag u g from
              Or.inr ⟨CostructuredArrow.homMk (adj.homEquiv g.left d g.hom) (by simp [u])⟩)) }

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
d : D
u : CostructuredArrow L d := CostructuredArrow.mk (adj.counit.app d)
f g : CostructuredArrow L d
⊢ L.map ((adj.homEquiv g.left d) g.hom) ≫ u.hom = g.hom

Tactic:
simp [u]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
d : D
u : CostructuredArrow L d := CostructuredArrow.mk (adj.counit.app d)
f g : CostructuredArrow L d
⊢ L.map ((adj.homEquiv f.left d) f.hom) ≫ u.hom = f.hom

Tactic:
simp [u]

Result:
no goals