harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/ContinuousOn.lean
theorem continuous_if' {p : α → Prop} [∀ a, Decidable (p a)]
    (hpf : ∀ a ∈ frontier { x | p x }, Tendsto f (𝓝[{ x | p x }] a) (𝓝 <| ite (p a) (f a) (g a)))
    (hpg : ∀ a ∈ frontier { x | p x }, Tendsto g (𝓝[{ x | ¬p x }] a) (𝓝 <| ite (p a) (f a) (g a)))
    (hf : ContinuousOn f { x | p x }) (hg : ContinuousOn g { x | ¬p x }) :
    Continuous fun a => ite (p a) (f a) (g a)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ frontier {x | p x}, Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ frontier {x | p x}, Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ ContinuousOn (fun a => if p a then f a else g a) univ

Tactic:
apply ContinuousOn.if' <;> simp [*] <;> assumption

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ frontier {x | p x}, Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ frontier {x | p x}, Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ Continuous fun a => if p a then f a else g a

Tactic:
rw [continuous_iff_continuousOn_univ]

Result:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ frontier {x | p x}, Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ frontier {x | p x}, Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ ContinuousOn (fun a => if p a then f a else g a) univ
-- Mathlib/Algebra/FreeMonoid/Basic.lean
theorem ofList_flatten (xs : List (List α)) : ofList xs.flatten = (xs.map ofList).prod :=
  toList.injective <| by simp

Proof state:
α : Type u_1
xs : List (List α)
⊢ toList (ofList xs.flatten) = toList (List.map (⇑ofList) xs).prod

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem le_ncard_diff (s t : Set α) (hs : s.Finite

Proof state:
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
⊢ t.ncard ≤ (t \ s).ncard + s.ncard

Tactic:
apply ncard_le_ncard_diff_add_ncard _ _ hs

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
⊢ t.ncard ≤ s.ncard + (t \ s).ncard

Tactic:
rw [add_comm]

Result:
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
⊢ t.ncard ≤ (t \ s).ncard + s.ncard
-- Mathlib/Algebra/Lie/Subalgebra.lean
theorem toSubmodule_mk (p : Submodule R L) (h) :
    (({ p with lie_mem' := h } : LieSubalgebra R L) : Submodule R L) = p

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : ∀ {x y : L}, x ∈ p.carrier → y ∈ p.carrier → ⁅x, y⁆ ∈ p.carrier
⊢ { toSubmodule := p, lie_mem' := h }.toSubmodule = p

Tactic:
cases p

Result:
case mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
toAddSubmonoid✝ : AddSubmonoid L
smul_mem'✝ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
h :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier
⊢ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝, lie_mem' := h }.toSubmodule =
    { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }

Proof state:
case mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
toAddSubmonoid✝ : AddSubmonoid L
smul_mem'✝ : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
h :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier
⊢ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝, lie_mem' := h }.toSubmodule =
    { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head?_insert (l : List α) (a : α) :
    (l.insert a).head? = some (if h : a ∈ l then l.head (ne_nil_of_mem h) else a)

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ (List.insert a l).head? = some (if h : a ∈ l then l.head ⋯ else a)

Tactic:
simp only [insert_eq]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ (if a ∈ l then l else a :: l).head? = some (if h : a ∈ l then l.head ⋯ else a)

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ (if a ∈ l then l else a :: l).head? = some (if h : a ∈ l then l.head ⋯ else a)

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : a ∈ l
⊢ l.head? = some (l.head ⋯)

case isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : ¬a ∈ l
⊢ (a :: l).head? = some a

Proof state:
case isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : ¬a ∈ l
⊢ (a :: l).head? = some a

Tactic:
rfl

Result:
no goals

Proof state:
case isTrue
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : a ∈ l
⊢ l.head? = some (l.head ⋯)

Tactic:
simp [head?_eq_head (ne_nil_of_mem h)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem mem_zipIdx {x : α} {i : Nat} {xs : List α} {k : Nat} (h : (x, i) ∈ xs.zipIdx k) :
    k ≤ i ∧ i < k + xs.length ∧
      x = xs[i - k]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega) :=
  ⟨le_snd_of_mem_zipIdx h, snd_lt_add_of_mem_zipIdx h, fst_eq_of_mem_zipIdx h⟩

Proof state:
α : Type ?u.51817
x : α
i : Nat
xs : List α
k : Nat
h : (x, i) ∈ xs.zipIdx k
this✝ : k ≤ (x, i).snd
this : (x, i).snd < k + xs.length
⊢ i - k < xs.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.51817
x : α
i : Nat
xs : List α
k : Nat
h : (x, i) ∈ xs.zipIdx k
⊢ i - k < xs.length

Tactic:
have := le_snd_of_mem_zipIdx h

Result:
α : Type ?u.51817
x : α
i : Nat
xs : List α
k : Nat
h : (x, i) ∈ xs.zipIdx k
this : k ≤ (x, i).snd
⊢ i - k < xs.length

Proof state:
α : Type ?u.51817
x : α
i : Nat
xs : List α
k : Nat
h : (x, i) ∈ xs.zipIdx k
this : k ≤ (x, i).snd
⊢ i - k < xs.length

Tactic:
have := snd_lt_add_of_mem_zipIdx h

Result:
α : Type ?u.51817
x : α
i : Nat
xs : List α
k : Nat
h : (x, i) ∈ xs.zipIdx k
this✝ : k ≤ (x, i).snd
this : (x, i).snd < k + xs.length
⊢ i - k < xs.length
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem foldl (f) (init : α) : ∀ {s}, Valid s → s.foldl f init = s.toString.1.foldl f init
  | _, h => let ⟨_, _, _, h⟩ := h.validFor; by simp [h.foldl, h.toString]

Proof state:
α : Type u_1
f : α → Char → α
init : α
x✝ : Substring
h✝ : x✝.Valid
w✝² w✝¹ w✝ : List Char
h : ValidFor w✝² w✝¹ w✝ x✝
⊢ Substring.foldl f init x✝ = List.foldl f init x✝.toString.data

Tactic:
simp [h.foldl, h.toString]

Result:
no goals
-- Mathlib/RingTheory/LocalProperties/Submodule.lean
theorem Submodule.eq_bot_of_localization₀_maximal (N : Submodule R M)
    (h : ∀ (P : Ideal R) [P.IsMaximal], N.localized₀ P.primeCompl (f P) = ⊥) :
    N = ⊥ :=
  Submodule.eq_of_localization₀_maximal Mₚ f fun P hP ↦ by simpa using h P

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
N : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], localized₀ P.primeCompl (f P) N = ⊥
P : Ideal R
hP : P.IsMaximal
⊢ localized₀ P.primeCompl (f P) N = localized₀ P.primeCompl (f P) ⊥

Tactic:
simpa using h P

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem invOneSubPow_add (e : ℕ) :
    invOneSubPow S (d + e) = invOneSubPow S d * invOneSubPow S e

Proof state:
S : Type u_1
inst✝ : CommRing S
d e : ℕ
⊢ invOneSubPow S (d + e) = invOneSubPow S d * invOneSubPow S e

Tactic:
simp_rw [invOneSubPow_eq_inv_one_sub_pow, pow_add]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
@[simp]
lemma generateFrom_empty : generateFrom (∅ : Set (Set α)) = ⊥ :=
  le_bot_iff.mp (generateFrom_le (by simp))

Proof state:
α : Type u_1
⊢ ∀ t ∈ ∅, MeasurableSet t

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem Multipliable.comp_injective {i : γ → β} (hf : Multipliable f) (hi : Injective i) :
    Multipliable (f ∘ i)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : CommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformGroup α
f : β → α
inst✝ : CompleteSpace α
i : γ → β
hf : Multipliable f
hi : Injective i
⊢ Multipliable (f ∘ i)

Tactic:
simpa only [Set.mulIndicator_range_comp] using
  (hi.multipliable_iff (fun x hx ↦ Set.mulIndicator_of_not_mem hx _)).2
  (hf.mulIndicator (Set.range i))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Impl.lean
theorem foldr_eq_foldrTR : @foldr = @foldrTR

Proof state:
case h.h.h.h.h
α : Type u_2
β : Type u_1
f : α → β → β
init : β
l : List α
⊢ foldr f init l = foldrTR f init l

Tactic:
simp [foldrTR, ← Array.foldr_toList, -Array.size_toArray]

Result:
no goals

Proof state:
⊢ @foldr = @foldrTR

Tactic:
funext α β f init l

Result:
case h.h.h.h.h
α : Type u_2
β : Type u_1
f : α → β → β
init : β
l : List α
⊢ foldr f init l = foldrTR f init l
-- Mathlib/Analysis/Complex/Convex.lean
lemma Complex.isConnected_of_upperHalfPlane {r} {s : Set ℂ} (hs₁ : {z | r < z.im} ⊆ s)
    (hs₂ : s ⊆ {z | r ≤ z.im}) : IsConnected s

Proof state:
r : ℝ
s : Set ℂ
hs₁ : {z | r < z.im} ⊆ s
hs₂ : s ⊆ {z | r ≤ z.im}
⊢ (↑r + 1) * I ∈ {c | r < c.im}

Tactic:
simp

Result:
no goals

Proof state:
r : ℝ
s : Set ℂ
hs₁ : {z | r < z.im} ⊆ s
hs₂ : s ⊆ {z | r ≤ z.im}
⊢ IsConnected s

Tactic:
refine .subset_closure ?_ hs₁ (by simpa only [closure_setOf_lt_im] using hs₂)

Result:
r : ℝ
s : Set ℂ
hs₁ : {z | r < z.im} ⊆ s
hs₂ : s ⊆ {z | r ≤ z.im}
⊢ IsConnected {z | r < z.im}

Proof state:
r : ℝ
s : Set ℂ
hs₁ : {z | r < z.im} ⊆ s
hs₂ : s ⊆ {z | r ≤ z.im}
⊢ s ⊆ closure {z | r < z.im}

Tactic:
simpa only [closure_setOf_lt_im] using hs₂

Result:
no goals

Proof state:
r : ℝ
s : Set ℂ
hs₁ : {z | r < z.im} ⊆ s
hs₂ : s ⊆ {z | r ≤ z.im}
⊢ IsConnected {z | r < z.im}

Tactic:
exact (convex_halfSpace_im_gt r).isConnected ⟨(r + 1) * I, by simp⟩

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
lemma dvd_prod : a ∈ s → a ∣ s.prod :=
  Quotient.inductionOn s (fun l a h ↦ by simpa using List.dvd_prod h) a

Proof state:
α : Type u_3
inst✝ : CommMonoid α
s : Multiset α
a✝ : α
l : List α
a : α
h : a ∈ ⟦l⟧
⊢ a ∣ prod ⟦l⟧

Tactic:
simpa using List.dvd_prod h

Result:
no goals
-- Mathlib/RingTheory/ClassGroup.lean
theorem ClassGroup.mk_mk0 [IsDedekindDomain R] (I : (Ideal R)⁰) :
    ClassGroup.mk (FractionalIdeal.mk0 K I) = ClassGroup.mk0 I

Proof state:
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : ↥(Ideal R)⁰
⊢ mk ((FractionalIdeal.mk0 K) I) = mk0 I

Tactic:
rw [ClassGroup.mk0, MonoidHom.comp_apply, ← ClassGroup.mk_canonicalEquiv K (FractionRing R),
  FractionalIdeal.map_canonicalEquiv_mk0]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean
theorem S_two_mul_complex_cosh (n : ℤ) : (S ℂ n).eval (2 * cosh θ) * sinh θ =
    sinh ((n + 1) * θ)

Proof state:
θ : ℂ
n : ℤ
⊢ eval (2 * cosh θ) (S ℂ n) * sinh θ = sinh ((↑n + 1) * θ)

Tactic:
simp [S_eq_U_comp_half_mul_X]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem normalCore_le (H : Subgroup G) : H.normalCore ≤ H := fun a h => by
  rw [← mul_one a, ← inv_one, ← one_mul a]
  exact h 1

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
h : a ∈ H.normalCore
⊢ a ∈ H

Tactic:
rw [← mul_one a, ← inv_one, ← one_mul a]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
h : a ∈ H.normalCore
⊢ 1 * a * 1⁻¹ ∈ H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
h : a ∈ H.normalCore
⊢ 1 * a * 1⁻¹ ∈ H

Tactic:
exact h 1

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma le_of_lt_add_of_dvd (h : a < b + n) : n ∣ a → n ∣ b → a ≤ b

Proof state:
a b n : ℕ
h : a < b + n
⊢ n ∣ a → n ∣ b → a ≤ b

Tactic:
rintro ⟨a, rfl⟩ ⟨b, rfl⟩

Result:
case intro.intro
n a b : ℕ
h : n * a < n * b + n
⊢ n * a ≤ n * b

Proof state:
case intro.intro
n a b : ℕ
h : n * a < n * b.succ
⊢ n * a ≤ n * b

Tactic:
exact Nat.mul_le_mul_left _ (Nat.lt_succ_iff.1 <| Nat.lt_of_mul_lt_mul_left h)

Result:
no goals

Proof state:
case intro.intro
n a b : ℕ
h : n * a < n * b + n
⊢ n * a ≤ n * b

Tactic:
rw [← mul_succ] at h

Result:
case intro.intro
n a b : ℕ
h : n * a < n * b.succ
⊢ n * a ≤ n * b
-- Mathlib/Data/List/Sublists.lean
theorem sublistsLenAux_zero (l : List α) (f : List α → β) (r) :
    sublistsLenAux 0 l f r = f [] :: r

Proof state:
α : Type u
β : Type v
l : List α
f : List α → β
r : List β
⊢ sublistsLenAux 0 l f r = f [] :: r

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_inter_nonempty_iff {f : α → β} {s : Set α} {t : Set β} :
    (f '' s ∩ t).Nonempty ↔ (s ∩ f ⁻¹' t).Nonempty

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ (f '' s ∩ t).Nonempty ↔ (s ∩ f ⁻¹' t).Nonempty

Tactic:
rw [← image_inter_preimage, image_nonempty]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_sq' : cos x ^ 2 = 1 - sin x ^ 2

Proof state:
x : ℂ
⊢ cos x ^ 2 = 1 - sin x ^ 2

Tactic:
rw [← sin_sq_add_cos_sq x, add_sub_cancel_left]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
lemma Nil.append {p : G.Walk u v} {q : G.Walk v w} (hp : p.Nil) (hq : q.Nil) : (p.append q).Nil :=
  by simp [hp, hq]

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hp : p.Nil
hq : q.Nil
⊢ (p.append q).Nil

Tactic:
simp [hp, hq]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
theorem completedHurwitzZetaOdd_one_sub (a : UnitAddCircle) (s : ℂ) :
    completedHurwitzZetaOdd a (1 - s) = completedSinZeta a s

Proof state:
a : UnitAddCircle
s : ℂ
⊢ (1 - s + 1) / 2 = ↑(3 / 2) - (s + 1) / 2

Tactic:
push_cast

Result:
a : UnitAddCircle
s : ℂ
⊢ (1 - s + 1) / 2 = 3 / 2 - (s + 1) / 2

Proof state:
a : UnitAddCircle
s : ℂ
⊢ (1 - s + 1) / 2 = 3 / 2 - (s + 1) / 2

Tactic:
ring

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaOdd a (1 - s) = completedSinZeta a s

Tactic:
rw [completedHurwitzZetaOdd, completedSinZeta,
  (by { push_cast; ring } : (1 - s + 1) / 2 = ↑(3 / 2 : ℝ) - (s + 1) / 2),
  ← hurwitzOddFEPair_k, (hurwitzOddFEPair a).functional_equation ((s + 1) / 2),
  hurwitzOddFEPair_ε, one_smul]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean
theorem exp_diagonal (v : m → 𝔸) : exp 𝕂 (diagonal v) = diagonal (exp 𝕂 v)

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq m
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : TopologicalSpace 𝔸
inst✝² : IsTopologicalRing 𝔸
inst✝¹ : Algebra 𝕂 𝔸
inst✝ : T2Space 𝔸
v : m → 𝔸
⊢ exp 𝕂 (diagonal v) = diagonal (exp 𝕂 v)

Tactic:
simp_rw [exp_eq_tsum, diagonal_pow, ← diagonal_smul, ← diagonal_tsum]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
theorem sup_support_add_le :
    (f + g).support.sup degb ≤ f.support.sup degb ⊔ g.support.sup degb

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : SemilatticeSup B
inst✝¹ : OrderBot B
inst✝ : Semiring R
degb : A → B
f g : R[A]
⊢ (f + g).support.sup degb ≤ f.support.sup degb ⊔ g.support.sup degb

Tactic:
classical
exact (Finset.sup_mono Finsupp.support_add).trans_eq Finset.sup_union

Result:
no goals

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : SemilatticeSup B
inst✝¹ : OrderBot B
inst✝ : Semiring R
degb : A → B
f g : R[A]
⊢ (f + g).support.sup degb ≤ f.support.sup degb ⊔ g.support.sup degb

Tactic:
exact (Finset.sup_mono Finsupp.support_add).trans_eq Finset.sup_union

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Regular.lean
/-- If `μ` is inner regular for measurable finite measure sets with respect to some class of sets,
then its restriction to any finite measure set is also inner regular for measurable sets with
respect to the same class of sets. -/
lemma restrict_of_measure_ne_top (h : InnerRegularWRT μ p (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞))
    {A : Set α} (hA : μ A ≠ ∞) :
    InnerRegularWRT (μ.restrict A) p (fun s ↦ MeasurableSet s)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤
A : Set α
hA : μ A ≠ ⊤
⊢ (μ.restrict A).InnerRegularWRT p fun s => MeasurableSet s

Tactic:
have : Fact (μ A < ∞) := ⟨hA.lt_top⟩

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤
A : Set α
hA : μ A ≠ ⊤
this : Fact (μ A < ⊤)
⊢ (μ.restrict A).InnerRegularWRT p fun s => MeasurableSet s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤
A : Set α
hA : μ A ≠ ⊤
this : Fact (μ A < ⊤)
⊢ (μ.restrict A).InnerRegularWRT p fun s => MeasurableSet s

Tactic:
exact (restrict h A).trans (of_imp (fun s hs ↦ ⟨hs, measure_ne_top _ _⟩))

Result:
no goals
-- Mathlib/Algebra/Order/Group/MinMax.lean
theorem abs_max_sub_max_le_max (a b c d : α) : |max a b - max c d| ≤ max |a - c| |b - d|

Proof state:
case refine_2
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ c ⊔ d - a ⊔ b ≤ |a - c| ⊔ |b - d|

Tactic:
rw [abs_sub_comm a c, abs_sub_comm b d]

Result:
case refine_2
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ c ⊔ d - a ⊔ b ≤ |c - a| ⊔ |d - b|

Proof state:
case refine_2
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ c ⊔ d - a ⊔ b ≤ |c - a| ⊔ |d - b|

Tactic:
exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ |a ⊔ b - c ⊔ d| ≤ |a - c| ⊔ |b - d|

Tactic:
refine abs_sub_le_iff.2 ⟨?_, ?_⟩

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ a ⊔ b - c ⊔ d ≤ |a - c| ⊔ |b - d|

case refine_2
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ c ⊔ d - a ⊔ b ≤ |a - c| ⊔ |b - d|

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ a ⊔ b - c ⊔ d ≤ |a - c| ⊔ |b - d|

Tactic:
exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))

Result:
no goals
-- Mathlib/Topology/UniformSpace/AbstractCompletion.lean
theorem extend_map [CompleteSpace γ] [T0Space γ] {f : β → γ} {g : α → β}
    (hf : UniformContinuous f) (hg : UniformContinuous g) :
    pkg'.extend f ∘ map g = pkg.extend (f ∘ g) :=
  pkg.funext (pkg'.continuous_extend.comp (pkg.continuous_map pkg' _)) pkg.continuous_extend
    fun a => by
    rw [pkg.extend_coe (hf.comp hg), comp_apply, pkg.map_coe pkg' hg, pkg'.extend_coe hf]
    rfl

Proof state:
α : Type u_1
inst✝⁴ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝³ : UniformSpace β
pkg' : AbstractCompletion β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : T0Space γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ (pkg'.extend f ∘ pkg.map pkg' g) (pkg.coe a) = pkg.extend (f ∘ g) (pkg.coe a)

Tactic:
rw [pkg.extend_coe (hf.comp hg), comp_apply, pkg.map_coe pkg' hg, pkg'.extend_coe hf]

Result:
α : Type u_1
inst✝⁴ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝³ : UniformSpace β
pkg' : AbstractCompletion β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : T0Space γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ f (g a) = (f ∘ g) a

Proof state:
α : Type u_1
inst✝⁴ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝³ : UniformSpace β
pkg' : AbstractCompletion β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : T0Space γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ f (g a) = (f ∘ g) a

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma epi_g (s : S.Splitting) : Epi S.g

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s : S.Splitting
⊢ Epi S.g

Tactic:
have := s.isSplitEpi_g

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s : S.Splitting
this : IsSplitEpi S.g
⊢ Epi S.g

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s : S.Splitting
this : IsSplitEpi S.g
⊢ Epi S.g

Tactic:
infer_instance

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bsup_eq_blsub_iff_lt_bsup {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) :
    bsup.{_, v} o f = blsub.{_, v} o f ↔ ∀ i hi, f i hi < bsup.{_, v} o f :=
  ⟨fun h i => by
    rw [h]
    apply lt_blsub, fun h => le_antisymm (bsup_le_blsub f) (blsub_le h)⟩

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : o.bsup f = o.blsub f
i : Ordinal.{u}
⊢ ∀ (hi : i < o), f i hi < o.bsup f

Tactic:
rw [h]

Result:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : o.bsup f = o.blsub f
i : Ordinal.{u}
⊢ ∀ (hi : i < o), f i hi < o.blsub f

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : o.bsup f = o.blsub f
i : Ordinal.{u}
⊢ ∀ (hi : i < o), f i hi < o.blsub f

Tactic:
apply lt_blsub

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem add_lf_add_left {y z : PGame} (h : y ⧏ z) (x) : x + y ⧏ x + z

Proof state:
y z : PGame
h : y ⧏ z
x : PGame
⊢ x + y ⧏ x + z

Tactic:
rw [lf_congr add_comm_equiv add_comm_equiv]

Result:
y z : PGame
h : y ⧏ z
x : PGame
⊢ y + x ⧏ z + x

Proof state:
y z : PGame
h : y ⧏ z
x : PGame
⊢ y + x ⧏ z + x

Tactic:
apply add_lf_add_right h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_some (l : List α) : filterMap some l = l

Proof state:
α : Type u_1
l : List α
⊢ filterMap some l = l

Tactic:
rw [filterMap_some_fun, id]

Result:
no goals
-- Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean
theorem smul_prod [Monoid α] [CommMonoid β] [MulAction α β] [IsScalarTower α β β]
    [SMulCommClass α β β] (s : Multiset β) (b : α) :
    b ^ card s • s.prod = (s.map (b • ·)).prod :=
  Quot.induction_on s <| by simp [List.smul_prod]

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : Monoid α
inst✝³ : CommMonoid β
inst✝² : MulAction α β
inst✝¹ : IsScalarTower α β β
inst✝ : SMulCommClass α β β
s : Multiset β
b : α
⊢ ∀ (a : List β),
    b ^ card (Quot.mk (⇑(List.isSetoid β)) a) • prod (Quot.mk (⇑(List.isSetoid β)) a) =
      (map (fun x => b • x) (Quot.mk (⇑(List.isSetoid β)) a)).prod

Tactic:
simp [List.smul_prod]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivation.lean
theorem derivation_ext {D₁ D₂ : Derivation R R[X] A} (h : D₁ X = D₂ X) : D₁ = D₂ :=
  Derivation.ext fun f => Derivation.eqOn_adjoin (Set.eqOn_singleton.2 h) <| by
    simp only [adjoin_X, Algebra.coe_top, Set.mem_univ]

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module R[X] A
D₁ D₂ : Derivation R R[X] A
h : D₁ X = D₂ X
f : R[X]
⊢ f ∈ ↑(Algebra.adjoin R {X})

Tactic:
simp only [adjoin_X, Algebra.coe_top, Set.mem_univ]

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem nonpos_iff {a : SignType} : a ≤ 0 ↔ a = -1 ∨ a = 0

Proof state:
a : SignType
⊢ a ≤ 0 ↔ a = -1 ∨ a = 0

Tactic:
cases a <;> decide

Result:
no goals