harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The L-series of the twist of `f` by a Dirichlet character converges at `s` if the L-series
of `f` does. -/
lemma LSeriesSummable_mul {N : ℕ} (χ : DirichletCharacter ℂ N) {f : ℕ → ℂ} {s : ℂ}
    (h : LSeriesSummable f s) :
    LSeriesSummable (↗χ * f) s

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ LSeriesSummable ((fun n => χ ↑n) * f) s

Tactic:
refine .of_norm <| h.norm.of_nonneg_of_le (fun _ ↦ norm_nonneg _) fun n ↦ norm_term_le s ?_

Result:
N : ℕ
χ : DirichletCharacter ℂ N
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
n : ℕ
⊢ ‖((fun n => χ ↑n) * f) n‖ ≤ ‖f n‖

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
n : ℕ
⊢ ‖((fun n => χ ↑n) * f) n‖ ≤ ‖f n‖

Tactic:
simpa using mul_le_of_le_one_left (norm_nonneg <| f n) <| χ.norm_le_one n

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem colimit.ι_post (j : J) :
    colimit.ι (F ⋙ G) j ≫ colimit.post F G = G.map (colimit.ι F j)

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
j : J
⊢ ι (F ⋙ G) j ≫ post F G = G.map (ι F j)

Tactic:
erw [IsColimit.fac]

Result:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
j : J
⊢ (G.mapCocone (cocone F)).ι.app j = G.map (ι F j)

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
j : J
⊢ (G.mapCocone (cocone F)).ι.app j = G.map (ι F j)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean
theorem integrableAtFilter_rpow_atTop_iff {s : ℝ} :
    IntegrableAtFilter (fun x : ℝ ↦ x ^ s) atTop ↔ s < -1

Proof state:
s : ℝ
x✝ : IntegrableAtFilter (fun x => x ^ s) atTop volume
t : Set ℝ
ht : t ∈ atTop
hint : IntegrableOn (fun x => x ^ s) t volume
⊢ s < -1

Tactic:
obtain ⟨a, ha⟩ := mem_atTop_sets.mp ht

Result:
case intro
s : ℝ
x✝ : IntegrableAtFilter (fun x => x ^ s) atTop volume
t : Set ℝ
ht : t ∈ atTop
hint : IntegrableOn (fun x => x ^ s) t volume
a : ℝ
ha : ∀ b ≥ a, b ∈ t
⊢ s < -1

Proof state:
case intro
s : ℝ
x✝ : IntegrableAtFilter (fun x => x ^ s) atTop volume
t : Set ℝ
ht : t ∈ atTop
hint : IntegrableOn (fun x => x ^ s) t volume
a : ℝ
ha : ∀ b ≥ a, b ∈ t
⊢ IntegrableOn (fun x => x ^ s) (Ioi (a ⊔ 1)) volume

Tactic:
exact hint.mono_set <| fun x hx ↦ ha _ <| (le_max_left a 1).trans hx.le

Result:
no goals

Proof state:
case intro
s : ℝ
x✝ : IntegrableAtFilter (fun x => x ^ s) atTop volume
t : Set ℝ
ht : t ∈ atTop
hint : IntegrableOn (fun x => x ^ s) t volume
a : ℝ
ha : ∀ b ≥ a, b ∈ t
⊢ s < -1

Tactic:
refine (integrableOn_Ioi_rpow_iff (zero_lt_one.trans_le (le_max_right a 1))).mp ?_

Result:
case intro
s : ℝ
x✝ : IntegrableAtFilter (fun x => x ^ s) atTop volume
t : Set ℝ
ht : t ∈ atTop
hint : IntegrableOn (fun x => x ^ s) t volume
a : ℝ
ha : ∀ b ≥ a, b ∈ t
⊢ IntegrableOn (fun x => x ^ s) (Ioi (a ⊔ 1)) volume

Proof state:
s : ℝ
⊢ IntegrableAtFilter (fun x => x ^ s) atTop volume ↔ s < -1

Tactic:
refine ⟨fun ⟨t, ht, hint⟩ ↦ ?_, fun h ↦
  ⟨Set.Ioi 1, Ioi_mem_atTop 1, (integrableOn_Ioi_rpow_iff zero_lt_one).mpr h⟩⟩

Result:
s : ℝ
x✝ : IntegrableAtFilter (fun x => x ^ s) atTop volume
t : Set ℝ
ht : t ∈ atTop
hint : IntegrableOn (fun x => x ^ s) t volume
⊢ s < -1
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem dist_eq_iSup : dist f g = ⨆ x : α, dist (f x) (g x)

Proof state:
case inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
h✝ : Nonempty α
⊢ BddAbove (range fun x => dist (f x) (g x))

Tactic:
exact dist_set_exists.imp fun C hC => forall_mem_range.2 hC.2

Result:
no goals

Proof state:
case inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
h✝ : Nonempty α
⊢ dist f g = ⨆ x, dist (f x) (g x)

Tactic:
refine (dist_le_iff_of_nonempty.mpr <| le_ciSup ?_).antisymm (ciSup_le dist_coe_le_dist)

Result:
case inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
h✝ : Nonempty α
⊢ BddAbove (range fun x => dist (f x) (g x))

Proof state:
case inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
h✝ : IsEmpty α
⊢ dist f g = ⨆ x, dist (f x) (g x)

Tactic:
rw [iSup_of_empty', Real.sSup_empty, dist_zero_of_empty]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
⊢ dist f g = ⨆ x, dist (f x) (g x)

Tactic:
cases isEmpty_or_nonempty α

Result:
case inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
h✝ : IsEmpty α
⊢ dist f g = ⨆ x, dist (f x) (g x)

case inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
h✝ : Nonempty α
⊢ dist f g = ⨆ x, dist (f x) (g x)
-- Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean
theorem Finset.smul_prod_perm [Fintype G] (b : β) (g : G) :
    (g • ∏ h : G, h • b) = ∏ h : G, h • b

Proof state:
β : Type u_2
inst✝³ : CommMonoid β
G : Type u_4
inst✝² : Group G
inst✝¹ : MulDistribMulAction G β
inst✝ : Fintype G
b : β
g : G
⊢ ∀ (i : G), i ∈ univ ↔ (fun x => g * x) i ∈ univ

Tactic:
simp

Result:
no goals

Proof state:
β : Type u_2
inst✝³ : CommMonoid β
G : Type u_4
inst✝² : Group G
inst✝¹ : MulDistribMulAction G β
inst✝ : Fintype G
b : β
g : G
⊢ g • ∏ h : G, h • b = ∏ h : G, h • b

Tactic:
simp only [smul_prod', smul_smul]

Result:
β : Type u_2
inst✝³ : CommMonoid β
G : Type u_4
inst✝² : Group G
inst✝¹ : MulDistribMulAction G β
inst✝ : Fintype G
b : β
g : G
⊢ ∏ x : G, (g * x) • b = ∏ h : G, h • b
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem colimit.isoColimitCocone_ι_hom {F : J ⥤ C} [HasColimit F] (t : ColimitCocone F) (j : J) :
    colimit.ι F j ≫ (colimit.isoColimitCocone t).hom = t.cocone.ι.app j

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimit F
t : ColimitCocone F
j : J
⊢ ι F j ≫ (isoColimitCocone t).hom = t.cocone.ι.app j

Tactic:
dsimp [colimit.isoColimitCocone, IsColimit.coconePointUniqueUpToIso]

Result:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimit F
t : ColimitCocone F
j : J
⊢ ι F j ≫ desc F t.cocone = t.cocone.ι.app j

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimit F
t : ColimitCocone F
j : J
⊢ ι F j ≫ desc F t.cocone = t.cocone.ι.app j

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Relation.lean
lemma reflGen_eq_self (hr : Reflexive r) : ReflGen r = r

Proof state:
α : Type u_1
r : α → α → Prop
hr : Reflexive r
⊢ ReflGen r = r

Tactic:
ext x y

Result:
case h.h.a
α : Type u_1
r : α → α → Prop
hr : Reflexive r
x y : α
⊢ ReflGen r x y ↔ r x y

Proof state:
case h.h.a
α : Type u_1
r : α → α → Prop
hr : Reflexive r
x y : α
⊢ ReflGen r x y ↔ r x y

Tactic:
simpa only [reflGen_iff, or_iff_right_iff_imp] using fun h ↦ h ▸ hr y

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
/-- A walk with its endpoints defeq is `Nil` if and only if it is equal to `nil`. -/
lemma nil_iff_eq_nil : ∀ {p : G.Walk v v}, p.Nil ↔ p = nil
  | .nil | .cons _ _ => by simp

Proof state:
V : Type u
G : SimpleGraph V
v v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).Nil ↔ cons h✝ p✝ = nil

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Card.lean
theorem cardinal_generateMeasurable_le (s : Set (Set α)) :
    #{ t | GenerateMeasurable s t } ≤ max #s 2 ^ ℵ₀

Proof state:
α : Type u
s : Set (Set α)
⊢ #↑(generateMeasurableRec s (ω_ 1)) ≤ (#↑s ⊔ 2) ^ ℵ₀

Tactic:
exact cardinal_generateMeasurableRec_le s _

Result:
no goals

Proof state:
α : Type u
s : Set (Set α)
⊢ #↑{t | GenerateMeasurable s t} ≤ (#↑s ⊔ 2) ^ ℵ₀

Tactic:
rw [generateMeasurable_eq_rec.{u, 0}]

Result:
α : Type u
s : Set (Set α)
⊢ #↑(generateMeasurableRec s (ω_ 1)) ≤ (#↑s ⊔ 2) ^ ℵ₀
-- Mathlib/Tactic/NormNum/Prime.lean
theorem isNat_minFac_3 : {n n' : ℕ} → (k : ℕ) →
    IsNat n n' → MinFacHelper n' k → nat_lit 0 = n' % k → IsNat (minFac n) k
  | n, _, k, ⟨rfl⟩, h1, h2 => by
    rw [eq_comm, ← Nat.dvd_iff_mod_eq_zero] at h2
    exact ⟨le_antisymm (minFac_le_of_dvd h1.1.le h2) h1.2.2⟩

Proof state:
n k : ℕ
h1 : MinFacHelper n k
h2 : 0 = n % k
⊢ IsNat n.minFac k

Tactic:
rw [eq_comm, ← Nat.dvd_iff_mod_eq_zero] at h2

Result:
n k : ℕ
h1 : MinFacHelper n k
h2 : k ∣ n
⊢ IsNat n.minFac k

Proof state:
n k : ℕ
h1 : MinFacHelper n k
h2 : k ∣ n
⊢ IsNat n.minFac k

Tactic:
exact ⟨le_antisymm (minFac_le_of_dvd h1.1.le h2) h1.2.2⟩

Result:
no goals
-- Mathlib/Order/Interval/Set/Pi.lean
theorem pi_univ_Ioc_update_left {x y : ∀ i, α i} {i₀ : ι} {m : α i₀} (hm : x i₀ ≤ m) :
    (pi univ fun i ↦ Ioc (update x i₀ m i) (y i)) =
      { z | m < z i₀ } ∩ pi univ fun i ↦ Ioc (x i) (y i)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
⊢ Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)

Tactic:
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, ← inter_assoc,
  inter_eq_self_of_subset_left (Ioi_subset_Ioi hm)]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
⊢ (univ.pi fun i => Ioc (update x i₀ m i) (y i)) = {z | m < z i₀} ∩ univ.pi fun i => Ioc (x i) (y i)

Tactic:
have : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀) := by
  rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, ← inter_assoc,
    inter_eq_self_of_subset_left (Ioi_subset_Ioi hm)]

Result:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
⊢ (univ.pi fun i => Ioc (update x i₀ m i) (y i)) = {z | m < z i₀} ∩ univ.pi fun i => Ioc (x i) (y i)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
⊢ ({x_1 | x_1 i₀ ∈ Ioi m ∩ Ioc (x i₀) (y i₀)} ∩ {i₀}ᶜ.pi fun j => Ioc (x j) (y j)) =
    {z | m < z i₀} ∩ {x_1 | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩ {i₀}ᶜ.pi fun j => Ioc (x j) (y j)

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
⊢ (univ.pi fun i => Ioc (update x i₀ m i) (y i)) = {z | m < z i₀} ∩ univ.pi fun i => Ioc (x i) (y i)

Tactic:
simp_rw [univ_pi_update i₀ _ _ fun i z ↦ Ioc z (y i), ← pi_inter_compl ({i₀} : Set ι),
  singleton_pi', ← inter_assoc, this]

Result:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
⊢ ({x_1 | x_1 i₀ ∈ Ioi m ∩ Ioc (x i₀) (y i₀)} ∩ {i₀}ᶜ.pi fun j => Ioc (x j) (y j)) =
    {z | m < z i₀} ∩ {x_1 | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩ {i₀}ᶜ.pi fun j => Ioc (x j) (y j)
-- Mathlib/Data/Int/Init.lean
lemma dvd_of_mul_dvd_mul_right (ha : a ≠ 0) (h : m * a ∣ n * a) : m ∣ n :=
  dvd_of_mul_dvd_mul_left ha (by simpa [Int.mul_comm] using h)

Proof state:
a m n : ℤ
ha : a ≠ 0
h : m * a ∣ n * a
⊢ a * m ∣ a * n

Tactic:
simpa [Int.mul_comm] using h

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem find?_reverse (t : RBNode α) (cut : α → Ordering) :
    t.reverse.find? cut = t.find? (cut · |>.swap)

Proof state:
case node
α : Type u_1
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : find? cut l✝.reverse = find? (fun x => (cut x).swap) l✝
r_ih✝ : find? cut r✝.reverse = find? (fun x => (cut x).swap) r✝
⊢ (match cut v✝ with
    | Ordering.lt => find? (fun x => (cut x).swap) r✝
    | Ordering.gt => find? (fun x => (cut x).swap) l✝
    | Ordering.eq => some v✝) =
    match (cut v✝).swap with
    | Ordering.lt => find? (fun x => (cut x).swap) l✝
    | Ordering.gt => find? (fun x => (cut x).swap) r✝
    | Ordering.eq => some v✝

Tactic:
cases cut _ <;> simp [Ordering.swap]

Result:
no goals

Proof state:
α : Type u_1
t : RBNode α
cut : α → Ordering
⊢ find? cut t.reverse = find? (fun x => (cut x).swap) t

Tactic:
induction t <;> simp [*, find?]

Result:
case node
α : Type u_1
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : find? cut l✝.reverse = find? (fun x => (cut x).swap) l✝
r_ih✝ : find? cut r✝.reverse = find? (fun x => (cut x).swap) r✝
⊢ (match cut v✝ with
    | Ordering.lt => find? (fun x => (cut x).swap) r✝
    | Ordering.gt => find? (fun x => (cut x).swap) l✝
    | Ordering.eq => some v✝) =
    match (cut v✝).swap with
    | Ordering.lt => find? (fun x => (cut x).swap) l✝
    | Ordering.gt => find? (fun x => (cut x).swap) r✝
    | Ordering.eq => some v✝
-- Mathlib/Algebra/Group/Basic.lean
theorem eq_inv_mul_iff_mul_eq : a = b⁻¹ * c ↔ b * a = c :=
  ⟨fun h ↦ by rw [h, mul_inv_cancel_left], fun h ↦ by rw [← h, inv_mul_cancel_left]⟩

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
h : a = b⁻¹ * c
⊢ b * a = c

Tactic:
rw [h, mul_inv_cancel_left]

Result:
no goals

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
h : b * a = c
⊢ a = b⁻¹ * c

Tactic:
rw [← h, inv_mul_cancel_left]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Basic.lean
theorem dense_induction {p : M → Prop} (s : Set M) (closure : closure s = ⊤) (mem : ∀ x ∈ s, p x)
    (one : p 1) (mul : ∀ x y, p x → p y → p (x * y)) (x : M) : p x

Proof state:
case mem
M : Type u_1
inst✝ : MulOneClass M
p : M → Prop
s : Set M
closure : Submonoid.closure s = ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
x x✝ : M
h : x✝ ∈ s
⊢ p x✝

Tactic:
exact mem _ h

Result:
no goals

Proof state:
M : Type u_1
inst✝ : MulOneClass M
p : M → Prop
s : Set M
closure : Submonoid.closure s = ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
⊢ p x

Tactic:
induction closure.symm ▸ mem_top x using closure_induction with
| mem _ h => exact mem _ h
| one => exact one
| mul _ _ _ _ h₁ h₂ => exact mul _ _ h₁ h₂

Result:
no goals

Proof state:
case mul
M : Type u_1
inst✝ : MulOneClass M
p : M → Prop
s : Set M
closure : Submonoid.closure s = ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
x x✝ y✝ : M
hx✝ : x✝ ∈ Submonoid.closure s
hy✝ : y✝ ∈ Submonoid.closure s
h₁ : p x✝
h₂ : p y✝
⊢ p (x✝ * y✝)

Tactic:
exact mul _ _ h₁ h₂

Result:
no goals

Proof state:
case one
M : Type u_1
inst✝ : MulOneClass M
p : M → Prop
s : Set M
closure : Submonoid.closure s = ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
⊢ p 1

Tactic:
exact one

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
theorem filter_add_filter (q) [DecidablePred q] (s : Multiset α) :
    filter p s + filter q s = filter (fun a => p a ∨ q a) s + filter (fun a => p a ∧ q a) s :=
  Multiset.induction_on s rfl fun a s IH => by by_cases p a <;> by_cases q a <;> simp [*]

Proof state:
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a => p a ∨ q a) s + filter (fun a => p a ∧ q a) s
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun a => p a ∨ q a) (a ::ₘ s) + filter (fun a => p a ∧ q a) (a ::ₘ s)

Tactic:
by_cases p a <;> by_cases q a <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
    (m.insert k v).contains k

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
v : β k
⊢ (m.insert k v).contains k = true

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem lintegral_rnDeriv_lt_top (μ ν : Measure α) [IsFiniteMeasure μ] :
    ∫⁻ x, μ.rnDeriv ν x ∂ν < ∞

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
⊢ ∫⁻ (x : α), μ.rnDeriv ν x ∂ν < ⊤

Tactic:
rw [← setLIntegral_univ]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
⊢ ∫⁻ (x : α) in univ, μ.rnDeriv ν x ∂ν < ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
⊢ ∫⁻ (x : α) in univ, μ.rnDeriv ν x ∂ν < ⊤

Tactic:
exact lintegral_rnDeriv_lt_top_of_measure_ne_top _ (measure_lt_top _ _).ne

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/Noetherian.lean
lemma IsHausdorff.of_le_jacobson (h : I ≤ Ideal.jacobson ⊥) : IsHausdorff I M :=
  ⟨fun x hx ↦ (Ideal.iInf_pow_smul_eq_bot_of_le_jacobson I h).le (by simpa [SModEq.zero] using hx)⟩

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
⊢ x ∈ ⨅ i, I ^ i • ⊤

Tactic:
simpa [SModEq.zero] using hx

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

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

Tactic:
cases a with simp | cons a as => ?_

Result:
case cons
α✝ : Type u_1
b : List α✝
x : α✝
c : List α✝
a : α✝
as : List α✝
⊢ a = x ∧ as ++ b = c ↔ ∃ a', (a = x ∧ as = a') ∧ c = a' ++ b

Proof state:
case cons
α✝ : Type u_1
b : List α✝
x : α✝
c : List α✝
a : α✝
as : List α✝
⊢ a = x ∧ as ++ b = c ↔ ∃ a', (a = x ∧ as = a') ∧ c = a' ++ b

Tactic:
exact ⟨fun h => ⟨as, by simp [h]⟩, fun ⟨a', ⟨aeq, aseq⟩, h⟩ => ⟨aeq, by rw [aseq, h]⟩⟩

Result:
no goals

Proof state:
α✝ : Type u_1
b : List α✝
x : α✝
c : List α✝
a : α✝
as : List α✝
x✝ : ∃ a', (a = x ∧ as = a') ∧ c = a' ++ b
a' : List α✝
aeq : a = x
aseq : as = a'
h : c = a' ++ b
⊢ as ++ b = c

Tactic:
rw [aseq, h]

Result:
no goals

Proof state:
α✝ : Type u_1
b : List α✝
x : α✝
c : List α✝
a : α✝
as : List α✝
h : a = x ∧ as ++ b = c
⊢ (a = x ∧ as = as) ∧ c = as ++ b

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/BoundedCompactlySupported.lean
theorem norm_lt_iff_of_nonempty_compactlySupported [c : Nonempty α] {f : α →ᵇ γ}
    (h : f ∈ C_cb(α, γ)) {M : ℝ} : ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

Proof state:
case inl
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
hM : 0 < M
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

Tactic:
exact norm_lt_iff_of_compactlySupported h hM

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h✝ : f ∈ C_cb(α, γ)
M : ℝ
hM : M ≤ 0
h : ‖f‖ < M
⊢ 0 ≤ ‖f‖

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h✝ : f ∈ C_cb(α, γ)
M : ℝ
hM : M ≤ 0
h : ∀ (x : α), ‖f x‖ < M
⊢ 0 ≤ ‖f (Classical.arbitrary α)‖

Tactic:
positivity

Result:
no goals

Proof state:
case inr
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
hM : M ≤ 0
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

Tactic:
exact ⟨fun h ↦ False.elim <| (h.trans_le hM).not_le (by positivity),
  fun h ↦ False.elim <| (h (Classical.arbitrary α) |>.trans_le hM).not_le (by positivity)⟩

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

Tactic:
obtain (hM | hM) := lt_or_le 0 M

Result:
case inl
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
hM : 0 < M
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

case inr
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
hM : M ≤ 0
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M
-- Mathlib/Data/List/Nodup.lean
theorem nodup_iff_get?_ne_get? {l : List α} :
    l.Nodup ↔ ∀ i j : ℕ, i < j → j < l.length → l.get? i ≠ l.get? j

Proof state:
α : Type u
l : List α
⊢ l.Nodup ↔ ∀ (i j : ℕ), i < j → j < l.length → l.get? i ≠ l.get? j

Tactic:
simp [nodup_iff_getElem?_ne_getElem?]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
/-- The fundamental cocircuit of `X` and `e` has the junk value `{e}` if `e ∉ M.E` -/
lemma fundCocircuit_eq_of_not_mem_ground (X : Set α) (he : e ∉ M.E) :
    M.fundCocircuit e X = {e}

Proof state:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : e ∉ M.E
⊢ M.fundCocircuit e X = {e}

Tactic:
rwa [fundCocircuit, fundCircuit_eq_of_not_mem_ground]

Result:
no goals
-- Mathlib/Logic/Function/DependsOn.lean
lemma dependsOn_iff_exists_comp [Nonempty β] {f : (Π i, α i) → β} {s : Set ι} :
    DependsOn f s ↔ ∃ g : (Π i : s, α i) → β, f = g ∘ s.restrict

Proof state:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
inst✝ : Nonempty β
f : ((i : ι) → α i) → β
s : Set ι
⊢ DependsOn f s ↔ ∃ g, f = g ∘ s.restrict

Tactic:
rw [dependsOn_iff_factorsThrough, factorsThrough_iff]

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem codom_inv : r.inv.codom = r.dom

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
⊢ r.inv.codom = r.dom

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
r : Rel α β
x : α
⊢ x ∈ r.inv.codom ↔ x ∈ r.dom

Proof state:
case h
α : Type u_1
β : Type u_2
r : Rel α β
x : α
⊢ x ∈ r.inv.codom ↔ x ∈ r.dom

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Basic.lean
theorem coe_injective : Function.Injective ((fun B x y => B x y) : BilinForm R M → M → M → R) :=
  fun B D h => by
    ext x y
    apply congrFun₂ h

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B D : BilinForm R M
h : (fun B x y => (B x) y) B = (fun B x y => (B x) y) D
⊢ B = D

Tactic:
ext x y

Result:
case h.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B D : BilinForm R M
h : (fun B x y => (B x) y) B = (fun B x y => (B x) y) D
x y : M
⊢ (B x) y = (D x) y

Proof state:
case h.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B D : BilinForm R M
h : (fun B x y => (B x) y) B = (fun B x y => (B x) y) D
x y : M
⊢ (B x) y = (D x) y

Tactic:
apply congrFun₂ h

Result:
no goals