harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem closure_Ico {a b : α} (hab : a ≠ b) : closure (Ico a b) = Icc a b

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure (Ioo a b)

Tactic:
rw [closure_Ioo hab]

Result:
no goals

Proof state:
case h₁
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ closure (Ico a b) ⊆ Icc a b

Tactic:
exact closure_minimal Ico_subset_Icc_self isClosed_Icc

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ closure (Ico a b) = Icc a b

Tactic:
apply Subset.antisymm

Result:
case h₁
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ closure (Ico a b) ⊆ Icc a b

case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure (Ico a b)

Proof state:
case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure (Ico a b)

Tactic:
apply Subset.trans _ (closure_mono Ioo_subset_Ico_self)

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure (Ioo a b)
-- Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean
theorem equivalenceCounitIso_eq (hη : τ₀ = τ₁ hF hG η) :
    (equivalence hF hG).counitIso = equivalenceCounitIso η

Proof state:
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_8, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_5, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ eB.inverse.map
        (hF.inv.app (G.obj Y) ≫
          e'.functor.map (eA.functor.map (eA.unitIso.hom.app (G.obj Y))) ≫
            e'.functor.map (eA.functor.map (eA.inverse.map (hG.inv.app Y))) ≫
              e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y))) ≫
                e'.functor.map (hG.hom.app Y) ≫ hF.hom.app (G.obj Y) ≫ η.hom.app Y) ≫
      eB.unitIso.inv.app Y =
    eB.inverse.map (η.hom.app Y) ≫ eB.unitIso.inv.app Y

Tactic:
congr 2

Result:
case w.app.h.e_a.e_a
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_8, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_5, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ hF.inv.app (G.obj Y) ≫
      e'.functor.map (eA.functor.map (eA.unitIso.hom.app (G.obj Y))) ≫
        e'.functor.map (eA.functor.map (eA.inverse.map (hG.inv.app Y))) ≫
          e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y))) ≫
            e'.functor.map (hG.hom.app Y) ≫ hF.hom.app (G.obj Y) ≫ η.hom.app Y =
    η.hom.app Y
-- Mathlib/Algebra/Homology/BifunctorHomotopy.lean
lemma zero₁ (j j' : J) (h : ¬ c.Rel j' j) :
    hom₁ h₁ f₂ F c j j' = 0

Proof state:
case h
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{u_8, u_1} C₁
inst✝¹⁰ : Category.{u_9, u_2} C₂
inst✝⁹ : Category.{u_7, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
j j' : J
h : ¬c.Rel j' j
i₁ : I₁
i₂ : I₂
h' : c₁.π c₂ c (i₁, i₂) = j
⊢ c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
      (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j' =
    0

Tactic:
by_cases h₃ : c₁.Rel (c₁.prev i₁) i₁

Result:
case pos
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{u_8, u_1} C₁
inst✝¹⁰ : Category.{u_9, u_2} C₂
inst✝⁹ : Category.{u_7, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
j j' : J
h : ¬c.Rel j' j
i₁ : I₁
i₂ : I₂
h' : c₁.π c₂ c (i₁, i₂) = j
h₃ : c₁.Rel (c₁.prev i₁) i₁
⊢ c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
      (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j' =
    0

case neg
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{u_8, u_1} C₁
inst✝¹⁰ : Category.{u_9, u_2} C₂
inst✝⁹ : Category.{u_7, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
j j' : J
h : ¬c.Rel j' j
i₁ : I₁
i₂ : I₂
h' : c₁.π c₂ c (i₁, i₂) = j
h₃ : ¬c₁.Rel (c₁.prev i₁) i₁
⊢ c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
      (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j' =
    0
-- Mathlib/GroupTheory/Perm/Support.lean
theorem Disjoint.support_mul (h : Disjoint f g) : (f * g).support = f.support ∪ g.support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
a : α
⊢ f (g a) = a → f a = a ∧ g a = a

Tactic:
exact
  (h a).elim (fun hf h => ⟨hf, f.apply_eq_iff_eq.mp (h.trans hf.symm)⟩) fun hg h =>
    ⟨(congr_arg f hg).symm.trans h, hg⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (f * g).support = f.support ∪ g.support

Tactic:
refine le_antisymm (support_mul_le _ _) fun a => ?_

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
a : α
⊢ a ∈ f.support ∪ g.support → a ∈ (f * g).support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
a : α
⊢ a ∈ f.support ∪ g.support → a ∈ (f * g).support

Tactic:
rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ← not_and_or, not_imp_not]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
a : α
⊢ f (g a) = a → f a = a ∧ g a = a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toArray_mapM [Monad m] [LawfulMonad m] (f : α → m β) (a : Vector α n) :
    toArray <$> a.mapM f = a.toArray.mapM f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : Vector α n
⊢ toArray <$> mapM f a = Array.mapM f a.toArray

Tactic:
rcases a with ⟨a, rfl⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : Array α
⊢ toArray <$> mapM f { toArray := a, size_toArray := ⋯ } = Array.mapM f { toArray := a, size_toArray := ⋯ }.toArray

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : Array α
⊢ toArray <$> mapM f { toArray := a, size_toArray := ⋯ } = Array.mapM f { toArray := a, size_toArray := ⋯ }.toArray

Tactic:
unfold mapM

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : Array α
⊢ toArray <$> mapM.go f { toArray := a, size_toArray := ⋯ } 0 ⋯ { toArray := #[], size_toArray := ⋯ } =
    Array.mapM f { toArray := a, size_toArray := ⋯ }.toArray

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : Array α
⊢ toArray <$> mapM.go f { toArray := a, size_toArray := ⋯ } 0 ⋯ { toArray := #[], size_toArray := ⋯ } =
    Array.mapM f { toArray := a, size_toArray := ⋯ }.toArray

Tactic:
rw [toArray_mapM_go]

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : Array α
⊢ Array.mapM.map f { toArray := a, size_toArray := ⋯ }.toArray 0 { toArray := #[], size_toArray := ⋯ }.toArray =
    Array.mapM f { toArray := a, size_toArray := ⋯ }.toArray

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : Array α
⊢ Array.mapM.map f { toArray := a, size_toArray := ⋯ }.toArray 0 { toArray := #[], size_toArray := ⋯ }.toArray =
    Array.mapM f { toArray := a, size_toArray := ⋯ }.toArray

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval_mul_X_pow {k : ℕ} : (p * X ^ k).eval x = p.eval x * x ^ k

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
k : ℕ
ih : eval x (p * X ^ k) = eval x p * x ^ k
⊢ eval x (p * X ^ (k + 1)) = eval x p * x ^ (k + 1)

Tactic:
simp [pow_succ, ← mul_assoc, ih]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
k : ℕ
⊢ eval x (p * X ^ k) = eval x p * x ^ k

Tactic:
induction k with
| zero => simp
| succ k ih => simp [pow_succ, ← mul_assoc, ih]

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ eval x (p * X ^ 0) = eval x p * x ^ 0

Tactic:
simp

Result:
no goals
-- Mathlib/ModelTheory/Satisfiability.lean
theorem models_not_iff (h : T.IsComplete) (φ : L.Sentence) : T ⊨ᵇ φ.not ↔ ¬T ⊨ᵇ φ

Proof state:
case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : T ⊨ᵇ Formula.not φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ

Tactic:
simp only [hφn, true_iff]

Result:
case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : T ⊨ᵇ Formula.not φ
⊢ ¬T ⊨ᵇ φ

Proof state:
case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ

Tactic:
simp only [hφ, not_true, iff_false]

Result:
case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ ¬T ⊨ᵇ Formula.not φ

Proof state:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ

Tactic:
rcases h.2 φ with hφ | hφn

Result:
case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ

case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : T ⊨ᵇ Formula.not φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ

Proof state:
case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : ∀ (M : T.ModelType), ↑M ⊨ Formula.not φ
hφ : ∀ (M : T.ModelType), ↑M ⊨ φ
⊢ False

Tactic:
exact hφn h.1.some (hφ _)

Result:
no goals

Proof state:
case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : T ⊨ᵇ Formula.not φ
⊢ ¬T ⊨ᵇ φ

Tactic:
intro hφ

Result:
case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : T ⊨ᵇ Formula.not φ
hφ : T ⊨ᵇ φ
⊢ False

Proof state:
case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : T ⊨ᵇ Formula.not φ
hφ : T ⊨ᵇ φ
⊢ False

Tactic:
rw [models_sentence_iff] at *

Result:
case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : ∀ (M : T.ModelType), ↑M ⊨ Formula.not φ
hφ : ∀ (M : T.ModelType), ↑M ⊨ φ
⊢ False

Proof state:
case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ ∃ x, ¬↑x ⊨ Formula.not φ

Tactic:
refine ⟨h.1.some, ?_⟩

Result:
case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ ¬↑(Nonempty.some ⋯) ⊨ Formula.not φ

Proof state:
case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ ↑(Nonempty.some ⋯) ⊨ φ

Tactic:
exact models_sentence_iff.1 hφ _

Result:
no goals

Proof state:
case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ ¬T ⊨ᵇ Formula.not φ

Tactic:
rw [models_sentence_iff, not_forall]

Result:
case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ ∃ x, ¬↑x ⊨ Formula.not φ

Proof state:
case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ ¬↑(Nonempty.some ⋯) ⊨ Formula.not φ

Tactic:
simp only [Sentence.realize_not, Classical.not_not]

Result:
case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ ↑(Nonempty.some ⋯) ⊨ φ
-- Mathlib/Order/UpperLower/Basic.lean
theorem map_map (g : β ≃o γ) (f : α ≃o β) : map g (map f s) = map (f.trans g) s

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : LowerSet α
g : β ≃o γ
f : α ≃o β
⊢ (map g) ((map f) s) = (map (f.trans g)) s

Tactic:
ext

Result:
case a.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : LowerSet α
g : β ≃o γ
f : α ≃o β
x✝ : γ
⊢ x✝ ∈ ↑((map g) ((map f) s)) ↔ x✝ ∈ ↑((map (f.trans g)) s)

Proof state:
case a.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : LowerSet α
g : β ≃o γ
f : α ≃o β
x✝ : γ
⊢ x✝ ∈ ↑((map g) ((map f) s)) ↔ x✝ ∈ ↑((map (f.trans g)) s)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem Icc_mul_Ico_subset' (a b c d : α) : Icc a b * Ico c d ⊆ Ico (a * c) (b * d)

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

Tactic:
have := mulRightMono_of_mulRightStrictMono α

Result:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
⊢ Icc a b * Ico c d ⊆ Ico (a * c) (b * d)

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
⊢ Icc a b * Ico c d ⊆ Ico (a * c) (b * d)

Tactic:
have := mulLeftMono_of_mulLeftStrictMono α

Result:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this : MulLeftMono α
⊢ Icc a b * Ico c d ⊆ Ico (a * c) (b * d)

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
y : α
hya : a ≤ y
hyb : y ≤ b
z : α
hzc : c ≤ z
hzd : z < d
⊢ (fun x1 x2 => x1 * x2) y z ∈ Ico (a * c) (b * d)

Tactic:
exact ⟨mul_le_mul' hya hzc, mul_lt_mul_of_le_of_lt hyb hzd⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
⊢ Icc a b * Ico c d ⊆ Ico (a * c) (b * d)

Tactic:
rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
y : α
hya : a ≤ y
hyb : y ≤ b
z : α
hzc : c ≤ z
hzd : z < d
⊢ (fun x1 x2 => x1 * x2) y z ∈ Ico (a * c) (b * d)
-- Mathlib/RingTheory/Adjoin/FG.lean
theorem FG.map {S : Subalgebra R A} (f : A →ₐ[R] B) (hs : S.FG) : (S.map f).FG

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs✝ : S.FG
s : Finset A
hs : Algebra.adjoin R ↑s = S
⊢ (Subalgebra.map f S).FG

Tactic:
exact ⟨s.image f, by rw [Finset.coe_image, Algebra.adjoin_image, hs]⟩

Result:
no goals

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs✝ : S.FG
s : Finset A
hs : Algebra.adjoin R ↑s = S
⊢ (Subalgebra.map f S).FG

Tactic:
classical
exact ⟨s.image f, by rw [Finset.coe_image, Algebra.adjoin_image, hs]⟩

Result:
no goals

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs✝ : S.FG
s : Finset A
hs : Algebra.adjoin R ↑s = S
⊢ Algebra.adjoin R ↑(Finset.image (⇑f) s) = Subalgebra.map f S

Tactic:
rw [Finset.coe_image, Algebra.adjoin_image, hs]

Result:
no goals

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs : S.FG
⊢ (Subalgebra.map f S).FG

Tactic:
let ⟨s, hs⟩ := hs

Result:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs✝ : S.FG
s : Finset A
hs : Algebra.adjoin R ↑s = S
⊢ (Subalgebra.map f S).FG
-- Mathlib/Order/DirectedInverseSystem.lean
theorem lift₂_def (i x y) : DirectLimit.lift₂ f₁ f₂ ih compat ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ = ih i x y

Proof state:
ι : Type u_1
inst✝⁵ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst✝⁴ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)
inst✝³ : DirectedSystem F₁ fun x1 x2 x3 => ⇑(f₁ x1 x2 x3)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)
inst✝¹ : DirectedSystem F₂ fun x1 x2 x3 => ⇑(f₂ x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
C : Sort u_9
ih : (i : ι) → F₁ i → F₂ i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)
i : ι
x : F₁ i
y : F₂ i
⊢ DirectLimit.lift₂ f₁ f₂ ih compat ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ = ih i x y

Tactic:
rw [lift₂_def₂ _ _ _ _ _ _ i le_rfl le_rfl, map_self', map_self']

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem IsSeparable.image {β : Type*} [TopologicalSpace β] {s : Set α} (hs : IsSeparable s)
    {f : α → β} (hf : Continuous f) : IsSeparable (f '' s)

Proof state:
case intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous f
c : Set α
c_count : c.Countable
hc : s ⊆ closure c
⊢ IsSeparable (f '' s)

Tactic:
refine ⟨f '' c, c_count.image _, ?_⟩

Result:
case intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous f
c : Set α
c_count : c.Countable
hc : s ⊆ closure c
⊢ f '' s ⊆ closure (f '' c)

Proof state:
α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
hs : IsSeparable s
f : α → β
hf : Continuous f
⊢ IsSeparable (f '' s)

Tactic:
rcases hs with ⟨c, c_count, hc⟩

Result:
case intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous f
c : Set α
c_count : c.Countable
hc : s ⊆ closure c
⊢ IsSeparable (f '' s)

Proof state:
case intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous f
c : Set α
c_count : c.Countable
hc : s ⊆ closure c
⊢ f '' s ⊆ closure (f '' c)

Tactic:
rw [image_subset_iff]

Result:
case intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous f
c : Set α
c_count : c.Countable
hc : s ⊆ closure c
⊢ s ⊆ f ⁻¹' closure (f '' c)

Proof state:
case intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous f
c : Set α
c_count : c.Countable
hc : s ⊆ closure c
⊢ s ⊆ f ⁻¹' closure (f '' c)

Tactic:
exact hc.trans (closure_subset_preimage_closure_image hf)

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem wbtw_or_wbtw_smul_vadd_of_nonneg (x : P) (v : V) {r₁ r₂ : R} (hr₁ : 0 ≤ r₁) (hr₂ : 0 ≤ r₂) :
    Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Proof state:
case inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
h : r₂ ≤ r₁
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
exact Or.inr (wbtw_smul_vadd_smul_vadd_of_nonneg_of_le x v hr₂ h)

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
rcases le_total r₁ r₂ with (h | h)

Result:
case inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
h : r₁ ≤ r₂
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

case inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
h : r₂ ≤ r₁
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Proof state:
case inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
h : r₁ ≤ r₂
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
exact Or.inl (wbtw_smul_vadd_smul_vadd_of_nonneg_of_le x v hr₁ h)

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean
@[simp] lemma smul_apply {f : E →WOT[𝕜] F} (c : 𝕜) (x : E) : (c • f) x = c • (f x)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
f : E →WOT[𝕜] F
c : 𝕜
x : E
⊢ (↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm (c • f))).toFun x =
    c • (↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm f)).toFun x

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
f : E →WOT[𝕜] F
c : 𝕜
x : E
⊢ (c • f) x = c • f x

Tactic:
simp only [DFunLike.coe]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
f : E →WOT[𝕜] F
c : 𝕜
x : E
⊢ (↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm (c • f))).toFun x =
    c • (↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm f)).toFun x