harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Composition/Lemmas.lean
lemma MeasureTheory.Measure.parallelComp_comp_compProd [SFinite μ]
    [IsSFiniteKernel κ] {η : Kernel β γ} [IsSFiniteKernel η] :
    (Kernel.id ∥ₖ η) ∘ₘ (μ ⊗ₘ κ) = μ ⊗ₘ (η ∘ₖ κ)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : IsSFiniteKernel κ
η : Kernel β γ
inst✝ : IsSFiniteKernel η
⊢ ⇑(Kernel.id ∥ₖ η) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)

Tactic:
rw [Measure.compProd_eq_comp_prod, Measure.compProd_eq_comp_prod, Measure.comp_assoc,
  Kernel.parallelComp_comp_prod, Kernel.id_comp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_mkArray_of_neg (h : ¬ p a) : find? p (mkArray n a) = none

Proof state:
α✝ : Type u_1
p : α✝ → Bool
n : Nat
a : α✝
h : ¬p a = true
⊢ find? p (mkArray n a) = none

Tactic:
simp [find?_mkArray, h]

Result:
no goals
-- Mathlib/Data/Fintype/BigOperators.lean
theorem Fintype.prod_eq_mul_prod_subtype_ne [DecidableEq α] (f : α → M) (a : α) :
    ∏ i, f i = f a * ∏ i : {i // i ≠ a}, f i.1

Proof state:
α : Type u_1
M : Type u_4
inst✝² : Fintype α
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a : α
⊢ ∏ i : α, f i = f a * ∏ i : { i // i ≠ a }, f ↑i

Tactic:
simp_rw [← (Equiv.optionSubtypeNe a).prod_comp, prod_option, Equiv.optionSubtypeNe_none,
  Equiv.optionSubtypeNe_some]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
lemma AffineIndependent.eq_of_sum_eq_sum_subtype {s : Finset V}
    (hp : AffineIndependent k ((↑) : s → V)) {w₁ w₂ : V → k} (hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i)
    (hwp : ∑ i ∈ s, w₁ i • i = ∑ i ∈ s, w₂ i • i) : ∀ i ∈ s, w₁ i = w₂ i

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hp : AffineIndependent k Subtype.val
w₁ w₂ : V → k
hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i
hwp : ∑ i ∈ s, w₁ i • i = ∑ i ∈ s, w₂ i • i
⊢ ∀ i ∈ s, w₁ i = w₂ i

Tactic:
refine fun i hi => sub_eq_zero.1 (hp.eq_zero_of_sum_eq_zero_subtype (w := w₁ - w₂) ?_ ?_ _ hi) <;>
  simpa [sub_mul, sub_smul, sub_eq_zero]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Basic.lean
theorem iSup_eq_closure {ι : Sort*} (p : ι → Submonoid M) :
    ⨆ i, p i = Submonoid.closure (⋃ i, (p i : Set M))

Proof state:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
p : ι → Submonoid M
⊢ ⨆ i, p i = closure (⋃ i, ↑(p i))

Tactic:
simp_rw [Submonoid.closure_iUnion, Submonoid.closure_eq]

Result:
no goals
-- Mathlib/Algebra/FreeAlgebra/Cardinality.lean
theorem cardinalMk_eq_max [Nonempty X] [Nontrivial R] : #(FreeAlgebra R X) = #R ⊔ #X ⊔ ℵ₀

Proof state:
R : Type u
inst✝² : CommSemiring R
X : Type u
inst✝¹ : Nonempty X
inst✝ : Nontrivial R
⊢ #(FreeAlgebra R X) = #R ⊔ #X ⊔ ℵ₀

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {fallback : β} :
    getD (m.erase k) a fallback = if k == a then fallback else getD m a fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a : α
fallback : β
⊢ getD (m.erase k) a fallback = if (k == a) = true then fallback else getD m a fallback

Tactic:
simp_to_model [erase] using List.getValueD_eraseKey

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem exp_neg_mul_sq_isLittleO_exp_neg {b : ℝ} (hb : 0 < b) :
    (fun x : ℝ => exp (-b * x ^ 2)) =o[atTop] fun x : ℝ => exp (-x)

Proof state:
b : ℝ
hb : 0 < b
⊢ (fun x => rexp (-b * x ^ 2)) =o[atTop] fun x => rexp (-x)

Tactic:
exact exp_neg_mul_rpow_isLittleO_exp_neg hb one_lt_two

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean
@[simp]
lemma productEquiv_symm_apply_π (x : ∀ j, ToType (F j)) (j : J) :
    Pi.π F j ((productEquiv F).symm x) = x j

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
F : J → C
inst✝¹ : HasProduct F
inst✝ : PreservesLimit (Discrete.functor F) (forget C)
x : (j : J) → ToType (F j)
j : J
⊢ (ConcreteCategory.hom (Pi.π F j)) ((productEquiv F).symm x) = x j

Tactic:
rw [← productEquiv_apply_apply, Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem sdiff_symmDiff_right : b \ a ∆ b = a ⊓ b

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ b \ a ∆ b = a ⊓ b

Tactic:
rw [symmDiff_comm, inf_comm, sdiff_symmDiff_left]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem log_I : log I = π / 2 * I

Proof state:
⊢ log I = ↑π / 2 * I

Tactic:
simp [log]

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem chain_range_succ (r : ℕ → ℕ → Prop) (n : ℕ) :
    Chain r (List.range n.succ) ↔ r n 0 ∧ ∀ m < n, r m m.succ

Proof state:
r : ℕ → ℕ → Prop
n : ℕ
⊢ Chain r ↑(range n.succ) ↔ r n 0 ∧ ∀ m < n, r m m.succ

Tactic:
rw [range_succ, ← coe_cons_eq_coe_append, chain_coe_cons, ← range_succ, chain_range_succ]

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
@[simp] lemma toColex_sdiff_lt_toColex_sdiff' :
 toColex (s \ t) < toColex (t \ s) ↔ toColex s < toColex t

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
s t : Finset α
inst✝ : DecidableEq α
⊢ { ofColex := s \ t } < { ofColex := t \ s } ↔ { ofColex := s } < { ofColex := t }

Tactic:
simpa using toColex_sdiff_lt_toColex_sdiff (inter_subset_left (s₁ := s)) inter_subset_right

Result:
no goals
-- Mathlib/Algebra/Ring/Semiconj.lean
theorem sub_right (h : SemiconjBy a x y) (h' : SemiconjBy a x' y') :
    SemiconjBy a (x - x') (y - y')

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocRing R
a x y x' y' : R
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x - x') (y - y')

Tactic:
simpa only [sub_eq_add_neg] using h.add_right h'.neg_right

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseP_cons_of_neg {l : List α} {p} (h : ¬p a) :
    (a :: l).eraseP p = a :: l.eraseP p

Proof state:
α : Type u_1
a : α
l : List α
p : α → Bool
h : ¬p a = true
⊢ eraseP p (a :: l) = a :: eraseP p l

Tactic:
simp [eraseP_cons, h]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem cliqueSet_zero (G : SimpleGraph α) : G.cliqueSet 0 = {∅} := Set.ext fun s => by simp

Proof state:
α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ s ∈ G.cliqueSet 0 ↔ s ∈ {∅}

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[reassoc]
lemma map_ε_comp_counit_app_unit : F.map (ε G) ≫ adj.counit.app (𝟙_ D) = η F

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.OplaxMonoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
⊢ F.map (ε G) ≫ adj.counit.app (𝟙_ D) = η F

Tactic:
rw [IsMonoidal.leftAdjoint_ε (adj := adj), homEquiv_unit, map_comp,
  assoc, counit_naturality, left_triangle_components_assoc]

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
theorem lieBracketWithin_of_mem_nhds (h : s ∈ 𝓝 x) :
    lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
h : s ∈ 𝓝 x
⊢ lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x

Tactic:
rw [← lieBracketWithin_univ, ← univ_inter s, lieBracketWithin_inter h]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem comap_span (f : P₁ ≃ᵃ[k] P₂) (s : Set P₂) :
    (affineSpan k s).comap (f : P₁ →ᵃ[k] P₂) = affineSpan k (f ⁻¹' s)

Proof state:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ ≃ᵃ[k] P₂
s : Set P₂
⊢ comap (↑f) (affineSpan k s) = affineSpan k (⇑f ⁻¹' s)

Tactic:
rw [← map_symm, map_span, AffineEquiv.coe_coe, f.image_symm]

Result:
no goals
-- Mathlib/Data/Finset/NatDivisors.lean
lemma Nat.Prime.divisors_sq {p : ℕ} (hp : p.Prime) : (p ^ 2).divisors = {p ^ 2, p, 1}

Proof state:
p : ℕ
hp : Prime p
⊢ (p ^ 2).divisors = {p ^ 2, p, 1}

Tactic:
simp [divisors_prime_pow hp, range_succ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem containsThenInsert_snd (h : m.WF) {k : α} {v : β k} :
    (m.containsThenInsert k v).2 = m.insert k v

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝¹ : BEq α
inst✝ : Hashable α
h : m.WF
k : α
v : β k
⊢ (m.containsThenInsert k v).snd = m.insert k v

Tactic:
simp_to_raw using congrArg Subtype.val (Raw₀.containsThenInsert_snd _)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_one : (1 : R[X]).eval₂ f x = 1

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x 1 = 1

Tactic:
rw [← C_1, eval₂_C, f.map_one]

Result:
no goals
-- Mathlib/Data/Multiset/MapFold.lean
lemma erase_attach_map_val (s : Multiset α) (x : {x // x ∈ s}) :
    (s.attach.erase x).map (↑) = s.erase x

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
x : { x // x ∈ s }
⊢ map val (s.attach.erase x) = s.erase ↑x

Tactic:
rw [Multiset.map_erase _ val_injective, attach_map_val]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Basic.lean
theorem length_sub_le : (s - t).length ≤ s.length + t.length

Proof state:
α : Type u_2
inst✝ : OrderedAddCommGroup α
s t : Interval α
⊢ (s - t).length ≤ s.length + t.length

Tactic:
simpa [sub_eq_add_neg] using length_add_le s (-t)

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Defs.lean
theorem injective_of_comp_eq_id : Injective f :=
  .of_comp (f := g) <| by simp_rw [← coe_comp, h, id_coe, bijective_id.1]

Proof state:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ →ₛₗ[σ'] M
h : g.comp f = id
⊢ Injective (⇑g ∘ ⇑f)

Tactic:
simp_rw [← coe_comp, h, id_coe, bijective_id.1]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_one (a : Nat) : a ^ 1 = a

Proof state:
a : Nat
⊢ a ^ 1 = a

Tactic:
rw [Nat.pow_succ, Nat.pow_zero, Nat.one_mul]

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Basic.lean
theorem le_map_div_add_map_div [Group α] [AddCommSemigroup β] [LE β] [MulLEAddHomClass F α β]
    (f : F) (a b c : α) : f (a / c) ≤ f (a / b) + f (b / c)

Proof state:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommSemigroup β
inst✝¹ : LE β
inst✝ : MulLEAddHomClass F α β
f : F
a b c : α
⊢ f (a / c) ≤ f (a / b) + f (b / c)

Tactic:
simpa only [div_mul_div_cancel] using map_mul_le_add f (a / b) (b / c)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem forIn_visit_eq_bindList [Monad m] [LawfulMonad m] {t : RBNode α} :
    forIn.visit (m := m) f t init = (ForInStep.yield init).bindList f t.toList

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
α✝ : Type u_1
f : α → α✝ → m (ForInStep α✝)
init : α✝
inst✝¹ : Monad m
inst✝ : LawfulMonad m
t : RBNode α
⊢ forIn.visit f t init = ForInStep.bindList f t.toList (ForInStep.yield init)

Tactic:
induction t generalizing init <;> simp [*, forIn.visit]

Result:
no goals
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropAt_congr_iff_of_eventuallyEq (h₁ : g' =ᶠ[𝓝 x] g) :
    LiftPropAt P g' x ↔ LiftPropAt P g x :=
  hG.liftPropWithinAt_congr_iff_of_eventuallyEq (by simp_rw [nhdsWithin_univ, h₁]) h₁.eq_of_nhds

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
x : M
hG : G.LocalInvariantProp G' P
h₁ : g' =ᶠ[𝓝 x] g
⊢ g' =ᶠ[𝓝[univ] x] g

Tactic:
simp_rw [nhdsWithin_univ, h₁]

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
lemma toLeft_disjSum_toRight : u.toLeft.disjSum u.toRight = u

Proof state:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ u.toLeft.disjSum u.toRight = u

Tactic:
ext (x | x) <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem forall_eq' {a' : α} : (∀ a, a' = a → p a) ↔ p a'

Proof state:
α : Sort u_1
p : α → Prop
a' : α
⊢ (∀ (a : α), a' = a → p a) ↔ p a'

Tactic:
simp [@eq_comm _ a']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem flatMap_id' (l : Vector (Vector α m) n) : l.flatMap (fun a => a) = l.flatten

Proof state:
α : Type u_1
m n : Nat
l : Vector (Vector α m) n
⊢ (l.flatMap fun a => a) = l.flatten

Tactic:
simp [flatMap_def]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem map_mulVec [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (M : Matrix m n R)
    (v : n → R) (i : m) : f ((M *ᵥ v) i) = (M.map f *ᵥ (f ∘ v)) i

Proof state:
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
inst✝² : Fintype n
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
M : Matrix m n R
v : n → R
i : m
⊢ f ((M *ᵥ v) i) = (M.map ⇑f *ᵥ ⇑f ∘ v) i

Tactic:
simp only [Matrix.mulVec, Matrix.map_apply, RingHom.map_dotProduct, Function.comp_def]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma mul_div_mul_cancel (h₁ : c ≠ ⊥) (h₂ : c ≠ ⊤) (h₃ : c ≠ 0) : a * c / (b * c) = a / b

Proof state:
a b c : EReal
h₁ : c ≠ ⊥
h₂ : c ≠ ⊤
h₃ : c ≠ 0
⊢ a * c / (b * c) = a / b

Tactic:
rw [← mul_div_right a (b * c) c, ← div_div a b c, div_mul_cancel h₁ h₂ h₃]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
theorem CostructuredArrow.overEquivPresheafCostructuredArrow_inverse_map_toOverCompCoyoneda
    {A : Cᵒᵖ ⥤ Type v} {T : Over A} {X : CostructuredArrow yoneda A}
    (f : (CostructuredArrow.toOver yoneda A).obj X ⟶ T) :
    (overEquivPresheafCostructuredArrow A).inverse.map
      (((CostructuredArrow.toOverCompCoyoneda A).hom.app (op X)).app T f) =
      (CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow A).isoCompInverse.inv.app X ≫
        f ≫ (overEquivPresheafCostructuredArrow A).unit.app T

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
T : Over A
X : CostructuredArrow yoneda A
f : (toOver yoneda A).obj X ⟶ T
⊢ (overEquivPresheafCostructuredArrow A).inverse.map (((toOverCompCoyoneda A).hom.app (op X)).app T f) =
    (toOverCompOverEquivPresheafCostructuredArrow A).isoCompInverse.inv.app X ≫
      f ≫ (overEquivPresheafCostructuredArrow A).unit.app T

Tactic:
simp [CostructuredArrow.toOverCompCoyoneda]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldl_eq_foldlM (f : β → α → β) (b) (l : List α) :
    l.foldl f b = l.foldlM (m := Id) f b

Proof state:
β : Type u_1
α : Type u_2
f : β → α → β
b : β
l : List α
⊢ foldl f b l = List.foldlM f b l

Tactic:
induction l generalizing b <;> simp [*, foldl]

Result:
no goals
-- Mathlib/RingTheory/Coalgebra/Basic.lean
theorem counit_comp_inl : counit ∘ₗ inl R A B = counit

Proof state:
case h
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : A
⊢ (counit ∘ₗ inl R A B) x✝ = counit x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ counit ∘ₗ inl R A B = counit

Tactic:
ext

Result:
case h
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : A
⊢ (counit ∘ₗ inl R A B) x✝ = counit x✝
-- Mathlib/Data/Finset/Basic.lean
theorem toFinset_add (s t : Multiset α) : toFinset (s + t) = toFinset s ∪ toFinset t :=
  Finset.ext <| by simp

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ ∀ (a : α), a ∈ (s + t).toFinset ↔ a ∈ s.toFinset ∪ t.toFinset

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/EGauge.lean
lemma egauge_eq_top : egauge 𝕜 s x = ∞ ↔ ∀ c : 𝕜, x ∉ c • s

Proof state:
𝕜 : Type u_1
inst✝¹ : NNNorm 𝕜
E : Type u_2
inst✝ : SMul 𝕜 E
s : Set E
x : E
⊢ egauge 𝕜 s x = ⊤ ↔ ∀ (c : 𝕜), x ∉ c • s

Tactic:
simp [egauge]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem angle_right_midpoint_eq_pi_div_two_of_dist_eq {p₁ p₂ p₃ : P} (h : dist p₃ p₁ = dist p₃ p₂) :
    ∠ p₃ (midpoint ℝ p₁ p₂) p₂ = π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : dist p₃ p₁ = dist p₃ p₂
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₂ = π / 2

Tactic:
rw [midpoint_comm p₁ p₂, angle_left_midpoint_eq_pi_div_two_of_dist_eq h.symm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_mkArray_of_length_pos (h : 0 < n) :
    find? p (mkArray n a) = if p a then some a else none

Proof state:
n : Nat
α✝ : Type u_1
p : α✝ → Bool
a : α✝
h : 0 < n
⊢ find? p (mkArray n a) = if p a = true then some a else none

Tactic:
simp [find?_mkArray, Nat.ne_of_gt h]

Result:
no goals
-- Mathlib/Data/Holor.lean
theorem cprankMax_nil [Monoid α] [AddMonoid α] (x : Holor α nil) : CPRankMax 1 x

Proof state:
α : Type
inst✝¹ : Monoid α
inst✝ : AddMonoid α
x : Holor α []
⊢ CPRankMax 1 x

Tactic:
have h := CPRankMax.succ 0 x 0 (CPRankMax1.nil x) CPRankMax.zero

Result:
α : Type
inst✝¹ : Monoid α
inst✝ : AddMonoid α
x : Holor α []
h : CPRankMax (0 + 1) (x + 0)
⊢ CPRankMax 1 x

Proof state:
α : Type
inst✝¹ : Monoid α
inst✝ : AddMonoid α
x : Holor α []
h : CPRankMax (0 + 1) (x + 0)
⊢ CPRankMax 1 x

Tactic:
rwa [add_zero x, zero_add] at h

Result:
no goals
-- Mathlib/Order/Ideal.lean
theorem _root_.IsCoatom.isMaximal (hI : IsCoatom I) : IsMaximal I :=
  { IsCoatom.isProper hI with maximal_proper := fun _ hJ ↦ by simp [hI.2 _ hJ] }

Proof state:
P : Type u_1
inst✝² : LE P
inst✝¹ : IsDirected P fun x1 x2 => x1 ≤ x2
inst✝ : Nonempty P
I : Ideal P
hI : IsCoatom I
x✝ : Ideal P
hJ : I < x✝
⊢ ↑x✝ = univ

Tactic:
simp [hI.2 _ hJ]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem map_ceil (f : F) (hf : StrictMono f) (a : α) : ⌈f a⌉₊ = ⌈a⌉₊ :=
  ceil_congr fun n => by rw [← map_natCast f, hf.le_iff_le]

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrderedSemiring α
inst✝⁴ : LinearOrderedSemiring β
inst✝³ : FloorSemiring α
inst✝² : FloorSemiring β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
hf : StrictMono ⇑f
a : α
n : ℕ
⊢ f a ≤ ↑n ↔ a ≤ ↑n

Tactic:
rw [← map_natCast f, hf.le_iff_le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem ofNat_mul_negOfNat (m n : Nat) : (m : Nat) * negOfNat n = negOfNat (m * n)

Proof state:
m n : Nat
⊢ ↑m * negOfNat n = negOfNat (m * n)

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
@[simp] lemma sq_abs (a : α) : |a| ^ 2 = a ^ 2

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
a : α
⊢ |a| ^ 2 = a ^ 2

Tactic:
simpa only [sq] using abs_mul_abs_self a

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem coe_two_pi : ↑(2 * π : ℝ) = (0 : Angle) :=
  angle_eq_iff_two_pi_dvd_sub.2 ⟨1, by rw [sub_zero, Int.cast_one, mul_one]⟩

Proof state:
⊢ 2 * π - 0 = 2 * π * ↑1

Tactic:
rw [sub_zero, Int.cast_one, mul_one]

Result:
no goals
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Ioc_pred_left_eq_Icc_of_not_isMin (ha : ¬ IsMin a) (b : α) : Ioc (pred a) b = Icc a b :=
  coe_injective <| by simpa using Set.Ioc_pred_left_eq_Icc_of_not_isMin ha _

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ ↑(Ioc (pred a) b) = ↑(Icc a b)

Tactic:
simpa using Set.Ioc_pred_left_eq_Icc_of_not_isMin ha _

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
lemma nnqsmul_eq_C_mul (q : ℚ≥0) (f : R[X]) : q • f = Polynomial.C (q : R) * f

Proof state:
R : Type u
inst✝ : DivisionSemiring R
q : ℚ≥0
f : R[X]
⊢ q • f = C ↑q * f

Tactic:
rw [← NNRat.smul_one_eq_cast, ← Polynomial.smul_C, C_1, smul_one_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem span_eq_range_linearCombination (s : Set M) :
    span R s = LinearMap.range (linearCombination R ((↑) : s → M))

Proof state:
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ span R s = LinearMap.range (linearCombination R Subtype.val)

Tactic:
rw [range_linearCombination, Subtype.range_coe_subtype, Set.setOf_mem_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List ((a : α) × β a)} {k : α} :
    (m.insertMany l).1.contains k = (m.contains k || (l.map Sigma.fst).contains k)

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List ((a : α) × β a)
k : α
⊢ (m.insertMany l).val.contains k = (m.contains k || (List.map Sigma.fst l).contains k)

Tactic:
simp_to_model [insertMany] using List.containsKey_insertList

Result:
no goals
-- Mathlib/Analysis/Asymptotics/TVS.lean
theorem isLittleOTVS_map {k : β → α} {l : Filter β} :
    f =o[𝕜; map k l] g ↔ (f ∘ k) =o[𝕜;l] (g ∘ k)

Proof state:
α : Type u_1
β : Type u_2
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
f : α → E
g : α → F
k : β → α
l : Filter β
⊢ f =o[𝕜;map k l] g ↔ (f ∘ k) =o[𝕜;l] (g ∘ k)

Tactic:
simp [IsLittleOTVS]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem mapM_cons [Monad m] [LawfulMonad m] (f : α → m β) :
    (a :: l).mapM f = (return (← f a) :: (← l.mapM f))

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
⊢ mapM f (a :: l) = do
    let __do_lift ← f a
    let __do_lift_1 ← mapM f l
    pure (__do_lift :: __do_lift_1)

Tactic:
simp [← mapM'_eq_mapM, mapM']

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem openSegment_eq_image (x y : E) :
    openSegment 𝕜 x y = (fun θ : 𝕜 => (1 - θ) • x + θ • y) '' Ioo (0 : 𝕜) 1 :=
  Set.ext fun _ =>
    ⟨fun ⟨a, b, ha, hb, hab, hz⟩ =>
      ⟨b, ⟨hb, hab ▸ lt_add_of_pos_left _ ha⟩, hab ▸ hz ▸ by simp only [add_sub_cancel_right]⟩,
      fun ⟨θ, ⟨hθ₀, hθ₁⟩, hz⟩ => ⟨1 - θ, θ, sub_pos.2 hθ₁, hθ₀, sub_add_cancel _ _, hz⟩⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y x✝¹ : E
x✝ : x✝¹ ∈ openSegment 𝕜 x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • x + b • y = x✝¹
⊢ (fun θ => (a + b - θ) • x + θ • y) b = a • x + b • y

Tactic:
simp only [add_sub_cancel_right]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem comap_map_eq_self {f : G →* N} {H : Subgroup G} (h : f.ker ≤ H) :
    comap f (map f H) = H

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
h : f.ker ≤ H
⊢ comap f (map f H) = H

Tactic:
rwa [comap_map_eq, sup_eq_left]

Result:
no goals