harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Bounds/Image.lean
theorem BddAbove.image2_bddBelow : BddAbove s → BddAbove t → BddBelow (Set.image2 f s t)

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ BddAbove s → BddAbove t → BddBelow (image2 f s t)

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Result:
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddBelow (image2 f s t)

Proof state:
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddBelow (image2 f s t)

Tactic:
exact ⟨f a b, mem_lowerBounds_image2_of_mem_upperBounds h₀ h₁ ha hb⟩

Result:
no goals
-- Mathlib/RingTheory/RingHom/Unramified.lean
lemma isStableUnderBaseChange :
    IsStableUnderBaseChange FormallyUnramified

Proof state:
⊢ IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => FormallyUnramified

Tactic:
refine .mk _ respectsIso ?_

Result:
⊢ ∀ ⦃R S T : Type u_3⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    (algebraMap R T).FormallyUnramified → Algebra.TensorProduct.includeLeftRingHom.FormallyUnramified

Proof state:
⊢ ∀ ⦃R S T : Type u_3⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    (algebraMap R T).FormallyUnramified → Algebra.TensorProduct.includeLeftRingHom.FormallyUnramified

Tactic:
intros R S T _ _ _ _ _ h

Result:
R S T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : (algebraMap R T).FormallyUnramified
⊢ Algebra.TensorProduct.includeLeftRingHom.FormallyUnramified

Proof state:
R S T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.FormallyUnramified R T
⊢ Algebra.FormallyUnramified S (TensorProduct R S T)

Tactic:
infer_instance

Result:
no goals

Proof state:
R S T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : (algebraMap R T).FormallyUnramified
⊢ Algebra.TensorProduct.includeLeftRingHom.FormallyUnramified

Tactic:
show (algebraMap _ _).FormallyUnramified

Result:
R S T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : (algebraMap R T).FormallyUnramified
⊢ (algebraMap S (TensorProduct R S T)).FormallyUnramified

Proof state:
R S T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : (algebraMap R T).FormallyUnramified
⊢ (algebraMap S (TensorProduct R S T)).FormallyUnramified

Tactic:
rw [formallyUnramified_algebraMap] at h ⊢

Result:
R S T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.FormallyUnramified R T
⊢ Algebra.FormallyUnramified S (TensorProduct R S T)
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem span_singleton_mul_le_span_singleton_mul {x y : R} {I J : Ideal R} :
    span {x} * I ≤ span {y} * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ

Proof state:
R : Type u
inst✝ : CommSemiring R
x y : R
I J : Ideal R
⊢ span {x} * I ≤ span {y} * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ

Tactic:
simp only [span_singleton_mul_le_iff, mem_span_singleton_mul, eq_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem add_le_of_le_sub_left {a b c : Int} (h : b ≤ c - a) : a + b ≤ c

Proof state:
a b c : Int
h✝ : b ≤ c - a
h : a + b ≤ a + (c - a)
⊢ a + b ≤ c

Tactic:
rwa [← Int.add_sub_assoc, Int.add_comm a c, Int.add_sub_cancel] at h

Result:
no goals

Proof state:
a b c : Int
h : b ≤ c - a
⊢ a + b ≤ c

Tactic:
have h := Int.add_le_add_left h a

Result:
a b c : Int
h✝ : b ≤ c - a
h : a + b ≤ a + (c - a)
⊢ a + b ≤ c
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem succ : IsFundamentalSequence (succ o) 1 fun _ _ => o

Proof state:
o : Ordinal.{u}
⊢ (succ o).IsFundamentalSequence 1 fun x x => o

Tactic:
refine ⟨?_, @fun i j hi hj h => ?_, blsub_const Ordinal.one_ne_zero o⟩

Result:
case refine_1
o : Ordinal.{u}
⊢ 1 ≤ (succ o).cof.ord

case refine_2
o i j : Ordinal.{u}
hi : i < 1
hj : j < 1
h : i < j
⊢ (fun x x => o) i hi < (fun x x => o) j hj

Proof state:
case refine_2
o i j : Ordinal.{u}
hi : i < 1
hj : j < 1
h : i < j
⊢ (fun x x => o) i hi < (fun x x => o) j hj

Tactic:
rw [lt_one_iff_zero] at hi hj

Result:
case refine_2
o i j : Ordinal.{u}
hi✝ : i < 1
hi : i = 0
hj✝ : j < 1
hj : j = 0
h : i < j
⊢ (fun x x => o) i hi✝ < (fun x x => o) j hj✝

Proof state:
case refine_2
o i j : Ordinal.{u}
hi✝ : i < 1
hi : i = 0
hj✝ : j < 1
hj : j = 0
h : i < j
⊢ (fun x x => o) i hi✝ < (fun x x => o) j hj✝

Tactic:
rw [hi, hj] at h

Result:
case refine_2
o i j : Ordinal.{u}
hi✝ : i < 1
hi : i = 0
hj✝ : j < 1
hj : j = 0
h : 0 < 0
⊢ (fun x x => o) i hi✝ < (fun x x => o) j hj✝

Proof state:
case refine_2
o i j : Ordinal.{u}
hi✝ : i < 1
hi : i = 0
hj✝ : j < 1
hj : j = 0
h : 0 < 0
⊢ (fun x x => o) i hi✝ < (fun x x => o) j hj✝

Tactic:
exact h.false.elim

Result:
no goals

Proof state:
case refine_1
o : Ordinal.{u}
⊢ 1 ≤ (succ o).cof.ord

Tactic:
rw [cof_succ, ord_one]

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem map_dlookup_eq_find (a : α) :
    ∀ l : List (Sigma β), (dlookup a l).map (Sigma.mk a) = find? (fun s => a = s.1) l
  | [] => rfl
  | ⟨a', b'⟩ :: l => by
    by_cases h : a = a'
    · subst a'
      simp
    · simpa [h] using map_dlookup_eq_find a l

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
⊢ Option.map (Sigma.mk a) (dlookup a (⟨a', b'⟩ :: l)) = find? (fun s => decide (a = s.fst)) (⟨a', b'⟩ :: l)

Tactic:
by_cases h : a = a'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
⊢ Option.map (Sigma.mk a) (dlookup a (⟨a', b'⟩ :: l)) = find? (fun s => decide (a = s.fst)) (⟨a', b'⟩ :: l)

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ Option.map (Sigma.mk a) (dlookup a (⟨a', b'⟩ :: l)) = find? (fun s => decide (a = s.fst)) (⟨a', b'⟩ :: l)

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
⊢ Option.map (Sigma.mk a) (dlookup a (⟨a', b'⟩ :: l)) = find? (fun s => decide (a = s.fst)) (⟨a', b'⟩ :: l)

Tactic:
subst a'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b' : β a
⊢ Option.map (Sigma.mk a) (dlookup a (⟨a, b'⟩ :: l)) = find? (fun s => decide (a = s.fst)) (⟨a, b'⟩ :: l)

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b' : β a
⊢ Option.map (Sigma.mk a) (dlookup a (⟨a, b'⟩ :: l)) = find? (fun s => decide (a = s.fst)) (⟨a, b'⟩ :: l)

Tactic:
simp

Result:
no goals

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ Option.map (Sigma.mk a) (dlookup a (⟨a', b'⟩ :: l)) = find? (fun s => decide (a = s.fst)) (⟨a', b'⟩ :: l)

Tactic:
simpa [h] using map_dlookup_eq_find a l

Result:
no goals
-- Mathlib/Algebra/Ring/SumsOfSquares.lean
theorem coe_sumSq : sumSq T = {s : T | IsSumSq s}

Proof state:
case h
T : Type u_2
inst✝ : NonUnitalCommSemiring T
x✝ : T
⊢ x✝ ∈ ↑(sumSq T) ↔ x✝ ∈ {s | IsSumSq s}

Tactic:
simp

Result:
no goals

Proof state:
T : Type u_2
inst✝ : NonUnitalCommSemiring T
⊢ ↑(sumSq T) = {s | IsSumSq s}

Tactic:
ext

Result:
case h
T : Type u_2
inst✝ : NonUnitalCommSemiring T
x✝ : T
⊢ x✝ ∈ ↑(sumSq T) ↔ x✝ ∈ {s | IsSumSq s}
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_insertIfNew [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    (h : Raw.WFImp m.1) {a : α} {b : β a} :
    Perm (toListModel (m.insertIfNew a b).1.buckets)
      (insertEntryIfNew a b (toListModel m.1.buckets))

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ toListModel (m.insertIfNewₘ a b).val.buckets ~ insertEntryIfNew a b (toListModel m.val.buckets)

Tactic:
exact toListModel_insertIfNewₘ h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ toListModel (m.insertIfNew a b).val.buckets ~ insertEntryIfNew a b (toListModel m.val.buckets)

Tactic:
rw [insertIfNew_eq_insertIfNewₘ]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ toListModel (m.insertIfNewₘ a b).val.buckets ~ insertEntryIfNew a b (toListModel m.val.buckets)
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
lemma supDegree_sum_lt (hs : s.Nonempty) {b : B}
    (h : ∀ i ∈ s, (f i).supDegree D < b) : (∑ i ∈ s, f i).supDegree D < b

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : LinearOrder B
inst✝ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
hs : s.Nonempty
b : B
h : ∀ i ∈ s, supDegree D (f i) < b
⊢ ⊥ < b

Tactic:
obtain ⟨i, hi⟩ := hs

Result:
case intro
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : LinearOrder B
inst✝ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
b : B
h : ∀ i ∈ s, supDegree D (f i) < b
i : ι
hi : i ∈ s
⊢ ⊥ < b

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : LinearOrder B
inst✝ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
hs : s.Nonempty
b : B
h : ∀ i ∈ s, supDegree D (f i) < b
⊢ supDegree D (∑ i ∈ s, f i) < b

Tactic:
refine supDegree_sum_le.trans_lt ((Finset.sup_lt_iff ?_).mpr h)

Result:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : LinearOrder B
inst✝ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
hs : s.Nonempty
b : B
h : ∀ i ∈ s, supDegree D (f i) < b
⊢ ⊥ < b

Proof state:
case intro
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : LinearOrder B
inst✝ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
b : B
h : ∀ i ∈ s, supDegree D (f i) < b
i : ι
hi : i ∈ s
⊢ ⊥ < b

Tactic:
exact bot_le.trans_lt (h i hi)

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma compProd_congr [IsSFiniteKernel κ] [IsSFiniteKernel η] (h : κ =ᵐ[μ] η) :
    μ ⊗ₘ κ = μ ⊗ₘ η

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : ⇑κ =ᶠ[ae μ] ⇑η
⊢ μ ⊗ₘ κ = μ ⊗ₘ η

Tactic:
rw [compProd, compProd]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : ⇑κ =ᶠ[ae μ] ⇑η
⊢ (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) () = (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η) ()

Proof state:
case e_a
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : ⇑κ =ᶠ[ae μ] ⇑η
⊢ Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ = Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η

Tactic:
refine Kernel.compProd_congr ?_

Result:
case e_a
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : ⇑κ =ᶠ[ae μ] ⇑η
⊢ ∀ (a : Unit),
    ∀ᵐ (b : α) ∂(Kernel.const Unit μ) a, (Kernel.prodMkLeft Unit κ) (a, b) = (Kernel.prodMkLeft Unit η) (a, b)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : ⇑κ =ᶠ[ae μ] ⇑η
⊢ (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) () = (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η) ()

Tactic:
congr 1

Result:
case e_a
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : ⇑κ =ᶠ[ae μ] ⇑η
⊢ Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ = Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η

Proof state:
case e_a
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : ⇑κ =ᶠ[ae μ] ⇑η
⊢ ∀ (a : Unit),
    ∀ᵐ (b : α) ∂(Kernel.const Unit μ) a, (Kernel.prodMkLeft Unit κ) (a, b) = (Kernel.prodMkLeft Unit η) (a, b)

Tactic:
simpa

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem nfp_add_zero (a) : nfp (a + ·) 0 = a * ω

Proof state:
case e_s
a : Ordinal.{u_1}
⊢ (fun n => (fun x => a + x)^[n] 0) = fun n => a * ↑n

Tactic:
funext n

Result:
case e_s.h
a : Ordinal.{u_1}
n : ℕ
⊢ (fun x => a + x)^[n] 0 = a * ↑n

Proof state:
a : Ordinal.{u_1}
⊢ nfp (fun x => a + x) 0 = a * ω

Tactic:
simp_rw [← iSup_iterate_eq_nfp, ← iSup_mul_nat]

Result:
a : Ordinal.{u_1}
⊢ ⨆ n, (fun x => a + x)^[n] 0 = ⨆ n, a * ↑n

Proof state:
a : Ordinal.{u_1}
⊢ ⨆ n, (fun x => a + x)^[n] 0 = ⨆ n, a * ↑n

Tactic:
congr

Result:
case e_s
a : Ordinal.{u_1}
⊢ (fun n => (fun x => a + x)^[n] 0) = fun n => a * ↑n

Proof state:
case e_s.h.zero
a : Ordinal.{u_1}
⊢ (fun x => a + x)^[0] 0 = a * ↑0

Tactic:
rw [Nat.cast_zero, mul_zero, iterate_zero_apply]

Result:
no goals

Proof state:
case e_s.h.succ
a : Ordinal.{u_1}
n : ℕ
hn : (fun x => a + x)^[n] 0 = a * ↑n
⊢ (fun x => a + x)^[n + 1] 0 = a * ↑(n + 1)

Tactic:
rw [iterate_succ_apply', Nat.add_comm, Nat.cast_add, Nat.cast_one, mul_one_add, hn]

Result:
no goals

Proof state:
case e_s.h
a : Ordinal.{u_1}
n : ℕ
⊢ (fun x => a + x)^[n] 0 = a * ↑n

Tactic:
induction' n with n hn

Result:
case e_s.h.zero
a : Ordinal.{u_1}
⊢ (fun x => a + x)^[0] 0 = a * ↑0

case e_s.h.succ
a : Ordinal.{u_1}
n : ℕ
hn : (fun x => a + x)^[n] 0 = a * ↑n
⊢ (fun x => a + x)^[n + 1] 0 = a * ↑(n + 1)
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigOWith.add (h₁ : IsBigOWith c₁ l f₁ g) (h₂ : IsBigOWith c₂ l f₂ g) :
    IsBigOWith (c₁ + c₂) l (fun x => f₁ x + f₂ x) g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : IsBigOWith c₁ l f₁ g
h₂ : IsBigOWith c₂ l f₂ g
⊢ IsBigOWith (c₁ + c₂) l (fun x => f₁ x + f₂ x) g

Tactic:
rw [IsBigOWith_def] at *

Result:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f₁ x + f₂ x‖ ≤ (c₁ + c₂) * ‖g x‖

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f₁ x + f₂ x‖ ≤ (c₁ + c₂) * ‖g x‖

Tactic:
filter_upwards [h₁, h₂] with x hx₁ hx₂ using
  calc
    ‖f₁ x + f₂ x‖ ≤ c₁ * ‖g x‖ + c₂ * ‖g x‖ := norm_add_le_of_le hx₁ hx₂
    _ = (c₁ + c₂) * ‖g x‖ := (add_mul _ _ _).symm

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Basic.lean
theorem countable_closure_of_compact {s : Set γ} (hs : IsCompact s) :
    ∃ t, t ⊆ s ∧ t.Countable ∧ s = closure t

Proof state:
γ : Type w
inst✝ : EMetricSpace γ
s : Set γ
hs : IsCompact s
⊢ ∃ t ⊆ s, t.Countable ∧ s = closure t

Tactic:
rcases subset_countable_closure_of_compact hs with ⟨t, hts, htc, hsub⟩

Result:
case intro.intro.intro
γ : Type w
inst✝ : EMetricSpace γ
s : Set γ
hs : IsCompact s
t : Set γ
hts : t ⊆ s
htc : t.Countable
hsub : s ⊆ closure t
⊢ ∃ t ⊆ s, t.Countable ∧ s = closure t

Proof state:
case intro.intro.intro
γ : Type w
inst✝ : EMetricSpace γ
s : Set γ
hs : IsCompact s
t : Set γ
hts : t ⊆ s
htc : t.Countable
hsub : s ⊆ closure t
⊢ ∃ t ⊆ s, t.Countable ∧ s = closure t

Tactic:
exact ⟨t, hts, htc, hsub.antisymm (closure_minimal hts hs.isClosed)⟩

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nmul_le_nmul_left (h : a ≤ b) (c) : c ⨳ a ≤ c ⨳ b

Proof state:
case inl.inr
a b : Ordinal.{u}
h : a ≤ b
h₁ : a < b
⊢ 0 ⨳ a ≤ 0 ⨳ b

case inr.inl
a c : Ordinal.{u}
h : a ≤ a
h₂ : 0 < c
⊢ c ⨳ a ≤ c ⨳ a

case inr.inr
a : Ordinal.{u}
h : a ≤ a
⊢ 0 ⨳ a ≤ 0 ⨳ a

Tactic:
all_goals simp

Result:
no goals

Proof state:
a b : Ordinal.{u}
h : a ≤ b
c : Ordinal.{u}
⊢ c ⨳ a ≤ c ⨳ b

Tactic:
rcases lt_or_eq_of_le h with (h₁ | rfl) <;> rcases (eq_zero_or_pos c).symm with (h₂ | rfl)

Result:
case inl.inl
a b : Ordinal.{u}
h : a ≤ b
c : Ordinal.{u}
h₁ : a < b
h₂ : 0 < c
⊢ c ⨳ a ≤ c ⨳ b

case inl.inr
a b : Ordinal.{u}
h : a ≤ b
h₁ : a < b
⊢ 0 ⨳ a ≤ 0 ⨳ b

case inr.inl
a c : Ordinal.{u}
h : a ≤ a
h₂ : 0 < c
⊢ c ⨳ a ≤ c ⨳ a

case inr.inr
a : Ordinal.{u}
h : a ≤ a
⊢ 0 ⨳ a ≤ 0 ⨳ a

Proof state:
case inl.inl
a b : Ordinal.{u}
h : a ≤ b
c : Ordinal.{u}
h₁ : a < b
h₂ : 0 < c
⊢ c ⨳ a ≤ c ⨳ b

Tactic:
exact (nmul_lt_nmul_of_pos_left h₁ h₂).le

Result:
no goals

Proof state:
case inr.inr
a : Ordinal.{u}
h : a ≤ a
⊢ 0 ⨳ a ≤ 0 ⨳ a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Perm/Basic.lean
theorem Perm.foldr_eq {f : α → β → β} {l₁ l₂ : List α} [lcomm : LeftCommutative f] (p : l₁ ~ l₂) :
    ∀ b, foldr f b l₁ = foldr f b l₂

Proof state:
case swap'
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
x✝ y✝ : α
l₁✝ l₂✝ : List α
h✝ : l₁✝ ~ l₂✝
r : ∀ (b : β), foldr f b l₁✝ = foldr f b l₂✝
b : β
⊢ f y✝ (f x✝ (foldr f b l₁✝)) = f x✝ (f y✝ (foldr f b l₂✝))

Tactic:
rw [lcomm.left_comm, r b]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
p : l₁ ~ l₂
⊢ ∀ (b : β), foldr f b l₁ = foldr f b l₂

Tactic:
intro b

Result:
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
p : l₁ ~ l₂
b : β
⊢ foldr f b l₁ = foldr f b l₂

Proof state:
case swap'
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
x✝ y✝ : α
l₁✝ l₂✝ : List α
h✝ : l₁✝ ~ l₂✝
r : ∀ (b : β), foldr f b l₁✝ = foldr f b l₂✝
b : β
⊢ foldr f b (y✝ :: x✝ :: l₁✝) = foldr f b (x✝ :: y✝ :: l₂✝)

Tactic:
simp only [foldr_cons]

Result:
case swap'
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
x✝ y✝ : α
l₁✝ l₂✝ : List α
h✝ : l₁✝ ~ l₂✝
r : ∀ (b : β), foldr f b l₁✝ = foldr f b l₂✝
b : β
⊢ f y✝ (f x✝ (foldr f b l₁✝)) = f x✝ (f y✝ (foldr f b l₂✝))

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
p : l₁ ~ l₂
b : β
⊢ foldr f b l₁ = foldr f b l₂

Tactic:
induction p using Perm.recOnSwap' generalizing b with
| nil => rfl
| cons _ _ r  => simp [r b]
| swap' _ _ _ r => simp only [foldr_cons]; rw [lcomm.left_comm, r b]
| trans _ _ r₁ r₂ => exact Eq.trans (r₁ b) (r₂ b)

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
x✝ : α
l₁✝ l₂✝ : List α
h✝ : l₁✝ ~ l₂✝
r : ∀ (b : β), foldr f b l₁✝ = foldr f b l₂✝
b : β
⊢ foldr f b (x✝ :: l₁✝) = foldr f b (x✝ :: l₂✝)

Tactic:
simp [r b]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
b : β
⊢ foldr f b [] = foldr f b []

Tactic:
rfl

Result:
no goals

Proof state:
case trans
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
l₁✝ l₂✝ l₃✝ : List α
h₁✝ : l₁✝ ~ l₂✝
h₂✝ : l₂✝ ~ l₃✝
r₁ : ∀ (b : β), foldr f b l₁✝ = foldr f b l₂✝
r₂ : ∀ (b : β), foldr f b l₂✝ = foldr f b l₃✝
b : β
⊢ foldr f b l₁✝ = foldr f b l₃✝

Tactic:
exact Eq.trans (r₁ b) (r₂ b)

Result:
no goals
-- Mathlib/Order/SupIndep.lean
theorem supIndep_map {s : Finset ι'} {g : ι' ↪ ι} : (s.map g).SupIndep f ↔ s.SupIndep (f ∘ g)

Proof state:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : (map g s).SupIndep f
t : Finset ι'
ht : t ⊆ s
i : ι'
hi : i ∈ s
hit : i ∉ t
⊢ g i ∉ map g t

Tactic:
rwa [mem_map']

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
⊢ (map g s).SupIndep f ↔ s.SupIndep (f ∘ ⇑g)

Tactic:
refine ⟨fun hs t ht i hi hit => ?_, fun hs => ?_⟩

Result:
case refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : (map g s).SupIndep f
t : Finset ι'
ht : t ⊆ s
i : ι'
hi : i ∈ s
hit : i ∉ t
⊢ Disjoint ((f ∘ ⇑g) i) (t.sup (f ∘ ⇑g))

case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : s.SupIndep (f ∘ ⇑g)
⊢ (map g s).SupIndep f

Proof state:
case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : s.SupIndep (f ∘ ⇑g)
⊢ (map g s).SupIndep f

Tactic:
classical
rw [map_eq_image]
exact hs.image

Result:
no goals

Proof state:
case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : s.SupIndep (f ∘ ⇑g)
⊢ (map g s).SupIndep f

Tactic:
rw [map_eq_image]

Result:
case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : s.SupIndep (f ∘ ⇑g)
⊢ (image (⇑g) s).SupIndep f

Proof state:
case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : s.SupIndep (f ∘ ⇑g)
⊢ (image (⇑g) s).SupIndep f

Tactic:
exact hs.image

Result:
no goals

Proof state:
case refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : (map g s).SupIndep f
t : Finset ι'
ht : t ⊆ s
i : ι'
hi : i ∈ s
hit : i ∉ t
⊢ Disjoint ((f ∘ ⇑g) i) (t.sup (f ∘ ⇑g))

Tactic:
rw [← sup_map]

Result:
case refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : (map g s).SupIndep f
t : Finset ι'
ht : t ⊆ s
i : ι'
hi : i ∈ s
hit : i ∉ t
⊢ Disjoint ((f ∘ ⇑g) i) ((map g t).sup f)

Proof state:
case refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : (map g s).SupIndep f
t : Finset ι'
ht : t ⊆ s
i : ι'
hi : i ∈ s
hit : i ∉ t
⊢ Disjoint ((f ∘ ⇑g) i) ((map g t).sup f)

Tactic:
exact hs (map_subset_map.2 ht) ((mem_map' _).2 hi) (by rwa [mem_map'])

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem bind₁_monomial (f : σ → MvPolynomial τ R) (d : σ →₀ ℕ) (r : R) :
    bind₁ f (monomial d r) = C r * ∏ i ∈ d.support, f i ^ d i

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
f : σ → MvPolynomial τ R
d : σ →₀ ℕ
r : R
⊢ (bind₁ f) ((monomial d) r) = C r * ∏ i ∈ d.support, f i ^ d i

Tactic:
simp only [monomial_eq, map_mul, bind₁_C_right, Finsupp.prod, map_prod,
  map_pow, bind₁_X_right]

Result:
no goals