harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Separation/Basic.lean
theorem Dense.diff_finset [T1Space X] [∀ x : X, NeBot (𝓝[≠] x)] {s : Set X} (hs : Dense s)
    (t : Finset X) : Dense (s \ t)

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Finset X
⊢ Dense (s \ ↑t)

Tactic:
classical
induction t using Finset.induction_on with
| empty => simpa using hs
| insert _ ih =>
  rw [Finset.coe_insert, ← union_singleton, ← diff_diff]
  exact ih.diff_singleton _

Result:
no goals

Proof state:
case empty
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
⊢ Dense (s \ ↑∅)

Tactic:
simpa using hs

Result:
no goals

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Finset X
⊢ Dense (s \ ↑t)

Tactic:
induction t using Finset.induction_on with
| empty => simpa using hs
| insert _ ih =>
  rw [Finset.coe_insert, ← union_singleton, ← diff_diff]
  exact ih.diff_singleton _

Result:
no goals

Proof state:
case insert
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
a✝¹ : X
s✝ : Finset X
a✝ : a✝¹ ∉ s✝
ih : Dense (s \ ↑s✝)
⊢ Dense ((s \ ↑s✝) \ {a✝¹})

Tactic:
exact ih.diff_singleton _

Result:
no goals

Proof state:
case insert
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
a✝¹ : X
s✝ : Finset X
a✝ : a✝¹ ∉ s✝
ih : Dense (s \ ↑s✝)
⊢ Dense (s \ ↑(insert a✝¹ s✝))

Tactic:
rw [Finset.coe_insert, ← union_singleton, ← diff_diff]

Result:
case insert
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
a✝¹ : X
s✝ : Finset X
a✝ : a✝¹ ∉ s✝
ih : Dense (s \ ↑s✝)
⊢ Dense ((s \ ↑s✝) \ {a✝¹})
-- Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean
/-- If G preserves coequalizers and finite coproducts, it preserves finite colimits. -/
lemma preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts
    [HasCoequalizers C] [HasFiniteCoproducts C] (G : C ⥤ D)
    [PreservesColimitsOfShape WalkingParallelPair G]
    [PreservesFiniteCoproducts G] : PreservesFiniteColimits G where
  preservesFiniteColimits

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasCoequalizers C
inst✝² : HasFiniteCoproducts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteCoproducts G
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ PreservesColimitsOfShape J G

Tactic:
apply preservesColimit_of_preservesCoequalizers_and_coproduct

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasCoequalizers C
inst✝² : HasFiniteCoproducts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteCoproducts G
⊢ ∀ (J : Type) [inst : SmallCategory J] [inst_1 : FinCategory J], PreservesColimitsOfShape J G

Tactic:
intro J sJ fJ

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasCoequalizers C
inst✝² : HasFiniteCoproducts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteCoproducts G
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ PreservesColimitsOfShape J G
-- Mathlib/Topology/Sets/Opens.lean
theorem isBasis_iff_nbhd {B : Set (Opens α)} :
    IsBasis B ↔ ∀ {U : Opens α} {x}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U

Proof state:
case mp.mk.intro.intro.intro.intro.mk
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
carrier✝ : Set α
is_open'✝ : IsOpen carrier✝
H₁ : { carrier := carrier✝, is_open' := is_open'✝ } ∈ B
hsV : x ∈ carrier✝ ∧ carrier✝ ⊆ sU
⊢ x ∈ { carrier := carrier✝, is_open' := is_open'✝ } ∧
    { carrier := carrier✝, is_open' := is_open'✝ } ≤ { carrier := sU, is_open' := hU }

Tactic:
exact hsV

Result:
no goals

Proof state:
case mpr.refine_1.intro.intro
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
U : Opens α
⊢ IsOpen ↑U

Tactic:
exact U.2

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
lemma map'_inv_eq_inv_map' {n m : ℕ} (h : n+1 ≤ m) {f g : ComposableArrows C m}
    (app : f.obj' n ≅ g.obj' n) (app' : f.obj' (n+1) ≅ g.obj' (n+1))
    (w : f.map' n (n+1) ≫ app'.hom = app.hom ≫ g.map' n (n+1)) :
    map' g n (n+1) ≫ app'.inv = app.inv ≫ map' f n (n+1)

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n m : ℕ
h : n + 1 ≤ m
f g : ComposableArrows C m
app : f.obj' n ⋯ ≅ g.obj' n ⋯
app' : f.obj' (n + 1) h ≅ g.obj' (n + 1) h
w : f.map' n (n + 1) ⋯ h ≫ app'.hom = app.hom ≫ g.map' n (n + 1) ⋯ h
⊢ g.map' n (n + 1) ⋯ h ≫ app'.inv = app.inv ≫ f.map' n (n + 1) ⋯ h

Tactic:
rw [← cancel_epi app.hom, ← reassoc_of% w, app'.hom_inv_id, comp_id, app.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Plus.lean
theorem isoToPlus_inv (hP : Presheaf.IsSheaf J P) :
    (J.isoToPlus P hP).inv = J.plusLift (𝟙 _) hP

Proof state:
case hγ
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ J.toPlus P ≫ (J.isoToPlus P hP).inv = 𝟙 P

Tactic:
rw [Iso.comp_inv_eq, Category.id_comp]

Result:
case hγ
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ J.toPlus P = (J.isoToPlus P hP).hom

Proof state:
case hγ
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ J.toPlus P = (J.isoToPlus P hP).hom

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ (J.isoToPlus P hP).inv = J.plusLift (𝟙 P) hP

Tactic:
apply J.plusLift_unique

Result:
case hγ
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ J.toPlus P ≫ (J.isoToPlus P hP).inv = 𝟙 P
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem Iio_mul_Iic_subset' (a b : α) : Iio a * Iic b ⊆ Iio (a * b)

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
⊢ Iio a * Iic b ⊆ Iio (a * b)

Tactic:
have := mulLeftMono_of_mulLeftStrictMono α

Result:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulLeftMono α
⊢ Iio a * Iic b ⊆ Iio (a * b)

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulLeftMono α
⊢ Iio a * Iic b ⊆ Iio (a * b)

Tactic:
rintro x ⟨y, hya, z, hzb, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulLeftMono α
y : α
hya : y ∈ Iio a
z : α
hzb : z ∈ Iic b
⊢ (fun x1 x2 => x1 * x2) y z ∈ Iio (a * b)

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulLeftMono α
y : α
hya : y ∈ Iio a
z : α
hzb : z ∈ Iic b
⊢ (fun x1 x2 => x1 * x2) y z ∈ Iio (a * b)

Tactic:
exact mul_lt_mul_of_lt_of_le hya hzb

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem length_eraseP {l : List α} : (l.eraseP p).length = if l.any p then l.length - 1 else l.length

Proof state:
case isFalse
α : Type u_1
p : α → Bool
l : List α
h : ¬l.any p = true
⊢ (eraseP p l).length = l.length

Tactic:
simp only [any_eq_true] at h

Result:
case isFalse
α : Type u_1
p : α → Bool
l : List α
h : ¬∃ x, x ∈ l ∧ p x = true
⊢ (eraseP p l).length = l.length

Proof state:
case isTrue
α : Type u_1
p : α → Bool
l : List α
h : l.any p = true
⊢ (eraseP p l).length = l.length - 1

Tactic:
simp only [any_eq_true] at h

Result:
case isTrue
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
⊢ (eraseP p l).length = l.length - 1

Proof state:
case isTrue
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
⊢ (eraseP p l).length = l.length - 1

Tactic:
obtain ⟨x, m, h⟩ := h

Result:
case isTrue.intro.intro
α : Type u_1
p : α → Bool
l : List α
x : α
m : x ∈ l
h : p x = true
⊢ (eraseP p l).length = l.length - 1

Proof state:
case isFalse
α : Type u_1
p : α → Bool
l : List α
h : ¬∃ x, x ∈ l ∧ p x = true
⊢ (eraseP p l).length = l.length

Tactic:
rw [eraseP_of_forall_not]

Result:
case isFalse
α : Type u_1
p : α → Bool
l : List α
h : ¬∃ x, x ∈ l ∧ p x = true
⊢ ∀ (a : α), a ∈ l → ¬p a = true

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ (eraseP p l).length = if l.any p = true then l.length - 1 else l.length

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
p : α → Bool
l : List α
h : l.any p = true
⊢ (eraseP p l).length = l.length - 1

case isFalse
α : Type u_1
p : α → Bool
l : List α
h : ¬l.any p = true
⊢ (eraseP p l).length = l.length

Proof state:
case isTrue.intro.intro
α : Type u_1
p : α → Bool
l : List α
x : α
m : x ∈ l
h : p x = true
⊢ (eraseP p l).length = l.length - 1

Tactic:
simp [length_eraseP_of_mem m h]

Result:
no goals

Proof state:
case isFalse
α : Type u_1
p : α → Bool
l : List α
h : ¬∃ x, x ∈ l ∧ p x = true
⊢ ∀ (a : α), a ∈ l → ¬p a = true

Tactic:
simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mkArray_eq_empty_iff {n : Nat} (a : α) : mkArray n a = #[] ↔ n = 0

Proof state:
α : Type u_1
n : Nat
a : α
⊢ mkArray n a = #[] ↔ n = 0

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
theorem toOuterMeasure_ofMultiset_apply :
    (ofMultiset s hs).toOuterMeasure t =
      (∑' x, (s.filter (· ∈ t)).count x : ℝ≥0∞) / (Multiset.card s)

Proof state:
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
⊢ (ofMultiset s hs).toOuterMeasure t = (∑' (x : α), ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s))) / ↑s.card

Tactic:
simp_rw [div_eq_mul_inv, ← ENNReal.tsum_mul_right, toOuterMeasure_apply]

Result:
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
⊢ ∑' (x : α), t.indicator (⇑(ofMultiset s hs)) x =
    ∑' (i : α), ↑(Multiset.count i (Multiset.filter (fun x => x ∈ t) s)) * (↑s.card)⁻¹

Proof state:
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
x : α
⊢ t.indicator (⇑(ofMultiset s hs)) x = ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s)) * (↑s.card)⁻¹

Tactic:
by_cases hx : x ∈ t <;> simp [Set.indicator, hx, div_eq_mul_inv]

Result:
no goals

Proof state:
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
⊢ ∑' (x : α), t.indicator (⇑(ofMultiset s hs)) x =
    ∑' (i : α), ↑(Multiset.count i (Multiset.filter (fun x => x ∈ t) s)) * (↑s.card)⁻¹

Tactic:
refine tsum_congr fun x => ?_

Result:
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
x : α
⊢ t.indicator (⇑(ofMultiset s hs)) x = ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s)) * (↑s.card)⁻¹
-- Mathlib/RingTheory/WittVector/Compare.lean
theorem fromPadicInt_comp_toPadicInt_ext (x) :
    (fromPadicInt p).comp (toPadicInt p) x = RingHom.id (𝕎 (ZMod p)) x

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : 𝕎 (ZMod p)
⊢ ((fromPadicInt p).comp (toPadicInt p)) x = (RingHom.id (𝕎 (ZMod p))) x

Tactic:
rw [fromPadicInt_comp_toPadicInt]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
lemma strictConvexOn_mul_log : StrictConvexOn ℝ (Set.Ici (0 : ℝ)) (fun x ↦ x * log x)

Proof state:
x : ℝ
hx : x ∈ interior (Set.Ici 0)
⊢ 0 < deriv^[2] (fun x => x * log x) x

Tactic:
simp only [Set.nonempty_Iio, interior_Ici', Set.mem_Ioi] at hx

Result:
x : ℝ
hx : 0 < x
⊢ 0 < deriv^[2] (fun x => x * log x) x

Proof state:
⊢ ∀ x ∈ interior (Set.Ici 0), 0 < deriv^[2] (fun x => x * log x) x

Tactic:
intro x hx

Result:
x : ℝ
hx : x ∈ interior (Set.Ici 0)
⊢ 0 < deriv^[2] (fun x => x * log x) x

Proof state:
⊢ StrictConvexOn ℝ (Set.Ici 0) fun x => x * log x

Tactic:
refine strictConvexOn_of_deriv2_pos (convex_Ici 0) (continuous_mul_log.continuousOn) ?_

Result:
⊢ ∀ x ∈ interior (Set.Ici 0), 0 < deriv^[2] (fun x => x * log x) x

Proof state:
x : ℝ
hx : 0 < x
⊢ 0 < deriv^[2] (fun x => x * log x) x

Tactic:
rw [deriv2_mul_log]

Result:
x : ℝ
hx : 0 < x
⊢ 0 < x⁻¹

Proof state:
x : ℝ
hx : 0 < x
⊢ 0 < x⁻¹

Tactic:
positivity

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@[simp]
lemma map₁_comp {G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v} (η : F ⟶ G) (μ : G ⟶ H) :
    YonedaCollection.map₁ (η ≫ μ) (X := X) =
      YonedaCollection.map₁ μ (X := X) ∘ YonedaCollection.map₁ η (X := X)

Proof state:
case h.h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
μ : G ⟶ H
x✝ : YonedaCollection F X
⊢ H.map (eqToHom ⋯) ((map₁ μ ∘ map₁ η) x✝).snd = (map₁ (η ≫ μ) x✝).snd

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
μ : G ⟶ H
⊢ map₁ (η ≫ μ) = map₁ μ ∘ map₁ η

Tactic:
ext

Result:
case h.h.w.h.h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
μ : G ⟶ H
x✝¹ : YonedaCollection F X
x✝ : Cᵒᵖ
a✝ : (yoneda.obj X).obj x✝
⊢ (map₁ (η ≫ μ) x✝¹).fst.app x✝ a✝ = ((map₁ μ ∘ map₁ η) x✝¹).fst.app x✝ a✝

case h.h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
μ : G ⟶ H
x✝ : YonedaCollection F X
⊢ H.map (eqToHom ⋯) ((map₁ μ ∘ map₁ η) x✝).snd = (map₁ (η ≫ μ) x✝).snd

Proof state:
case h.h.w.h.h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
μ : G ⟶ H
x✝¹ : YonedaCollection F X
x✝ : Cᵒᵖ
a✝ : (yoneda.obj X).obj x✝
⊢ (map₁ (η ≫ μ) x✝¹).fst.app x✝ a✝ = ((map₁ μ ∘ map₁ η) x✝¹).fst.app x✝ a✝

case h.h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
μ : G ⟶ H
x✝ : YonedaCollection F X
⊢ H.map (eqToHom ⋯) ((map₁ μ ∘ map₁ η) x✝).snd = (map₁ (η ≫ μ) x✝).snd

Tactic:
all_goals simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul {x : E} {r : 𝕜} (hx : x ≠ 0)
    (hr : r ≠ 0) : ‖⟪x, r • x⟫‖ / (‖x‖ * ‖r • x‖) = 1

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
⊢ ‖r‖ ≠ 0

Tactic:
simp [hr]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
hr' : ‖r‖ ≠ 0
⊢ ‖r‖ * (‖x‖ * ‖x‖) / (‖x‖ * (‖r‖ * ‖x‖)) = 1

Tactic:
rw [← mul_assoc, ← div_div, mul_div_cancel_right₀ _ hx', ← div_div, mul_comm,
  mul_div_cancel_right₀ _ hr', div_self hx']

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
hr' : ‖r‖ ≠ 0
⊢ ‖⟪x, r • x⟫_𝕜‖ / (‖x‖ * ‖r • x‖) = 1

Tactic:
rw [inner_smul_right, norm_mul, ← inner_self_re_eq_norm, inner_self_eq_norm_mul_norm, norm_smul]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
hr' : ‖r‖ ≠ 0
⊢ ‖r‖ * (‖x‖ * ‖x‖) / (‖x‖ * (‖r‖ * ‖x‖)) = 1

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
⊢ ‖⟪x, r • x⟫_𝕜‖ / (‖x‖ * ‖r • x‖) = 1

Tactic:
have hr' : ‖r‖ ≠ 0 := by simp [hr]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
hr' : ‖r‖ ≠ 0
⊢ ‖⟪x, r • x⟫_𝕜‖ / (‖x‖ * ‖r • x‖) = 1

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
simp [hx]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
⊢ ‖⟪x, r • x⟫_𝕜‖ / (‖x‖ * ‖r • x‖) = 1

Tactic:
have hx' : ‖x‖ ≠ 0 := by simp [hx]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
⊢ ‖⟪x, r • x⟫_𝕜‖ / (‖x‖ * ‖r • x‖) = 1
-- Mathlib/Analysis/MeanInequalities.lean
theorem isGreatest_Lp (f : ι → ℝ≥0) {p q : ℝ} (hpq : p.IsConjExponent q) :
    IsGreatest ((fun g : ι → ℝ≥0 => ∑ i ∈ s, f i * g i) '' { g | ∑ i ∈ s, g i ^ q ≤ 1 })
      ((∑ i ∈ s, f i ^ p) ^ (1 / p))

Proof state:
case right.intro.intro
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
g : ι → ℝ≥0
hg : g ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1}
⊢ (fun g => ∑ i ∈ s, f i * g i) g ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p)

Tactic:
apply le_trans (inner_le_Lp_mul_Lq s f g hpq)

Result:
case right.intro.intro
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
g : ι → ℝ≥0
hg : g ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1}
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p)
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem Filter.EventuallyEq.div_mul_cancel_atTop {α K : Type*} [LinearOrderedSemifield K]
    {f g : α → K} {l : Filter α} (hg : Tendsto g l atTop) :
    (fun x ↦ f x / g x * g x) =ᶠ[l] fun x ↦ f x :=
  div_mul_cancel <| hg.mono_right <| le_principal_iff.mpr <|
    mem_of_superset (Ioi_mem_atTop 0) <| by simp

Proof state:
α : Type u_4
K : Type u_5
inst✝ : LinearOrderedSemifield K
f g : α → K
l : Filter α
hg : Tendsto g l atTop
⊢ Set.Ioi 0 ⊆ {0}ᶜ

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exponential.lean
theorem hasFDerivAt_exp_of_mem_ball [CharZero 𝕂] {x : 𝔸}
    (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
    HasFDerivAt (exp 𝕂) (exp 𝕂 x • (1 : 𝔸 →L[𝕂] 𝔸)) x

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
⊢ (fun h => exp 𝕂 (x + h) - exp 𝕂 x - (exp 𝕂 x • 1) h) =o[𝓝 0] fun h => h

Tactic:
suffices
  (fun h => exp 𝕂 x * (exp 𝕂 (0 + h) - exp 𝕂 0 - ContinuousLinearMap.id 𝕂 𝔸 h)) =ᶠ[𝓝 0] fun h =>
    exp 𝕂 (x + h) - exp 𝕂 x - exp 𝕂 x • ContinuousLinearMap.id 𝕂 𝔸 h by
  refine (IsLittleO.const_mul_left ?_ _).congr' this (EventuallyEq.refl _ _)
  rw [← hasFDerivAt_iff_isLittleO_nhds_zero]
  exact hasFDerivAt_exp_zero_of_radius_pos hpos

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
⊢ (fun h => exp 𝕂 x * (exp 𝕂 (0 + h) - exp 𝕂 0 - (ContinuousLinearMap.id 𝕂 𝔸) h)) =ᶠ[𝓝 0] fun h =>
    exp 𝕂 (x + h) - exp 𝕂 x - exp 𝕂 x • (ContinuousLinearMap.id 𝕂 𝔸) h

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ (fun h => exp 𝕂 x * (exp 𝕂 (0 + h) - exp 𝕂 0 - (ContinuousLinearMap.id 𝕂 𝔸) h)) =ᶠ[𝓝 0] fun h =>
    exp 𝕂 (x + h) - exp 𝕂 x - exp 𝕂 x • (ContinuousLinearMap.id 𝕂 𝔸) h

Tactic:
filter_upwards [this] with _ hh

Result:
case h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
a✝ : 𝔸
hh : a✝ ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ exp 𝕂 x * (exp 𝕂 (0 + a✝) - exp 𝕂 0 - (ContinuousLinearMap.id 𝕂 𝔸) a✝) =
    exp 𝕂 (x + a✝) - exp 𝕂 x - exp 𝕂 x • (ContinuousLinearMap.id 𝕂 𝔸) a✝
-- Mathlib/SetTheory/Nimber/Field.lean
theorem mul_nonempty (a b : Nimber.{u}) :
    {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ.Nonempty

Proof state:
case h.e'_2.h.e'_3.h
a b x✝ : Nimber
⊢ (∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x✝) ↔
    ∃ a_1 b_1, (a_1 < a ∧ b_1 < b) ∧ a_1 * b + a * b_1 + a_1 * b_1 = x✝

Tactic:
tauto

Result:
no goals

Proof state:
a b : Nimber
⊢ {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ.Nonempty

Tactic:
convert nonempty_of_not_bddAbove <| not_bddAbove_compl_of_small
  ((fun x ↦ x.1 * b + a * x.2 + x.1 * x.2) '' Set.Iio a ×ˢ Set.Iio b)

Result:
case h.e'_2.h.e'_3
a b : Nimber
⊢ {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x} =
    (fun x => x.1 * b + a * x.2 + x.1 * x.2) '' Set.Iio a ×ˢ Set.Iio b

Proof state:
case h.e'_2.h.e'_3.h
a b x✝ : Nimber
⊢ x✝ ∈ {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x} ↔
    x✝ ∈ (fun x => x.1 * b + a * x.2 + x.1 * x.2) '' Set.Iio a ×ˢ Set.Iio b

Tactic:
simp_rw [Set.mem_setOf_eq, Set.mem_image, Set.mem_prod, Set.mem_Iio, Prod.exists]

Result:
case h.e'_2.h.e'_3.h
a b x✝ : Nimber
⊢ (∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x✝) ↔
    ∃ a_1 b_1, (a_1 < a ∧ b_1 < b) ∧ a_1 * b + a * b_1 + a_1 * b_1 = x✝

Proof state:
case h.e'_2.h.e'_3
a b : Nimber
⊢ {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x} =
    (fun x => x.1 * b + a * x.2 + x.1 * x.2) '' Set.Iio a ×ˢ Set.Iio b

Tactic:
ext

Result:
case h.e'_2.h.e'_3.h
a b x✝ : Nimber
⊢ x✝ ∈ {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x} ↔
    x✝ ∈ (fun x => x.1 * b + a * x.2 + x.1 * x.2) '' Set.Iio a ×ˢ Set.Iio b
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma one_le_formalMultilinearSeries_geometric_radius (𝕜 : Type*) [NontriviallyNormedField 𝕜]
    (A : Type*) [NormedRing A] [NormedAlgebra 𝕜 A] :
    1 ≤ (formalMultilinearSeries_geometric 𝕜 A).radius

Proof state:
𝕜 : Type u_9
inst✝² : NontriviallyNormedField 𝕜
A : Type u_10
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ 1 ≤ (formalMultilinearSeries_geometric 𝕜 A).radius

Tactic:
convert formalMultilinearSeries_geometric_eq_ofScalars 𝕜 A ▸
  FormalMultilinearSeries.ofScalars_radius_ge_inv_of_tendsto A _ one_ne_zero (by simp) |>.le

Result:
case h.e'_3
𝕜 : Type u_9
inst✝² : NontriviallyNormedField 𝕜
A : Type u_10
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ 1 = ↑1⁻¹

Proof state:
case h.e'_3
𝕜 : Type u_9
inst✝² : NontriviallyNormedField 𝕜
A : Type u_10
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ 1 = ↑1⁻¹

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_9
inst✝² : NontriviallyNormedField 𝕜
A : Type u_10
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ Tendsto (fun n => ‖1‖ / ‖1‖) atTop (𝓝 ↑1)

Tactic:
simp

Result:
no goals