internlm/Lean-Github huggingface dataset:
Theorem: local_preconnected_nhdsSet
Proof state before:
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : s ∈ 𝓝ˢ t
⊢ ∃ c, IsOpen c ∧ t ⊆ c ∧ c ⊆ s ∧ IsPreconnected c
Tactic:
rw [← subset_interior_iff_mem_nhdsSet] at st
Proof state after:
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
⊢ ∃ c, IsOpen c ∧ t ⊆ c ∧ c ⊆ s ∧ IsPreconnected c
Theorem: local_preconnected_nhdsSet
Proof state before:
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
⊢ ∃ c, IsOpen c ∧ t ⊆ c ∧ c ⊆ s ∧ IsPreconnected c
Tactic:
have hsub : t ⊆ ⋃ x : t, connectedComponentIn (interior s) x := fun x hx ↦
  mem_iUnion.2 ⟨⟨x, hx⟩, mem_connectedComponentIn (st hx)⟩
Proof state after:
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
hsub : t ⊆ ⋃ x, connectedComponentIn (interior s) ↑x
⊢ ∃ c, IsOpen c ∧ t ⊆ c ∧ c ⊆ s ∧ IsPreconnected c
Theorem: local_preconnected_nhdsSet
Proof state before:
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
hsub : t ⊆ ⋃ x, connectedComponentIn (interior s) ↑x
⊢ ∃ c, IsOpen c ∧ t ⊆ c ∧ c ⊆ s ∧ IsPreconnected c
Tactic:
refine ⟨_, isOpen_iUnion fun _ ↦ isOpen_interior.connectedComponentIn, hsub,
  iUnion_subset fun x ↦ ?_, ?_⟩
Proof state after:
case refine_1
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
hsub : t ⊆ ⋃ x, connectedComponentIn (interior s) ↑x
x : ↑t
⊢ connectedComponentIn (interior s) ↑x ⊆ s

case refine_2
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
hsub : t ⊆ ⋃ x, connectedComponentIn (interior s) ↑x
⊢ IsPreconnected (⋃ i, connectedComponentIn (interior s) ↑i)
Theorem: local_preconnected_nhdsSet
Proof state before:
case refine_1
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
hsub : t ⊆ ⋃ x, connectedComponentIn (interior s) ↑x
x : ↑t
⊢ connectedComponentIn (interior s) ↑x ⊆ s
Tactic:
exact (connectedComponentIn_subset _ _).trans interior_subset
Proof state after:
no goals
Theorem: local_preconnected_nhdsSet
Proof state before:
case refine_2
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
hsub : t ⊆ ⋃ x, connectedComponentIn (interior s) ↑x
⊢ IsPreconnected (⋃ i, connectedComponentIn (interior s) ↑i)
Tactic:
apply IsPreconnected.iUnion_of_pairwise_exists_isPreconnected
Proof state after:
case refine_2.hsc
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
hsub : t ⊆ ⋃ x, connectedComponentIn (interior s) ↑x
⊢ ∀ (i : ↑t), IsPreconnected (connectedComponentIn (interior s) ↑i)

case refine_2.h
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
hsub : t ⊆ ⋃ x, connectedComponentIn (interior s) ↑x
⊢ Pairwise fun i j =>
    (connectedComponentIn (interior s) ↑i).Nonempty →
      (connectedComponentIn (interior s) ↑j).Nonempty →
        ∃ u ⊆ ⋃ i, connectedComponentIn (interior s) ↑i,
          (connectedComponentIn (interior s) ↑i ∩ u).Nonempty ∧
            (u ∩ connectedComponentIn (interior s) ↑j).Nonempty ∧ IsPreconnected u
Theorem: local_preconnected_nhdsSet
Proof state before:
case refine_2.hsc
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
hsub : t ⊆ ⋃ x, connectedComponentIn (interior s) ↑x
⊢ ∀ (i : ↑t), IsPreconnected (connectedComponentIn (interior s) ↑i)
Tactic:
exact fun _ ↦ isPreconnected_connectedComponentIn
Proof state after:
no goals
Theorem: local_preconnected_nhdsSet
Proof state before:
case refine_2.h
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
hsub : t ⊆ ⋃ x, connectedComponentIn (interior s) ↑x
⊢ Pairwise fun i j =>
    (connectedComponentIn (interior s) ↑i).Nonempty →
      (connectedComponentIn (interior s) ↑j).Nonempty →
        ∃ u ⊆ ⋃ i, connectedComponentIn (interior s) ↑i,
          (connectedComponentIn (interior s) ↑i ∩ u).Nonempty ∧
            (u ∩ connectedComponentIn (interior s) ↑j).Nonempty ∧ IsPreconnected u
Tactic:
exact fun x y _ _ _ ↦ ⟨t, hsub, ⟨x, mem_connectedComponentIn (st x.2), x.2⟩,
  ⟨y, y.2, mem_connectedComponentIn (st y.2)⟩, tc⟩
Proof state after:
no goals
Theorem: Prod.frequently
Proof state before:
A B : Type
f : Filter A
g : Filter B
p : A → Prop
q : B → Prop
⊢ (∃ᶠ (x : A × B) in f ×ˢ g, p x.1 ∧ q x.2) ↔ (∃ᶠ (a : A) in f, p a) ∧ ∃ᶠ (b : B) in g, q b
Tactic:
simp only [frequently_iff_neBot, ← prod_neBot, ← prod_inf_prod, prod_principal_principal]
Proof state after:
A B : Type
f : Filter A
g : Filter B
p : A → Prop
q : B → Prop
⊢ (f ×ˢ g ⊓ 𝓟 {x | p x.1 ∧ q x.2}).NeBot ↔ (f ×ˢ g ⊓ 𝓟 ({a | p a} ×ˢ {b | q b})).NeBot
Theorem: Prod.frequently
Proof state before:
A B : Type
f : Filter A
g : Filter B
p : A → Prop
q : B → Prop
⊢ (f ×ˢ g ⊓ 𝓟 {x | p x.1 ∧ q x.2}).NeBot ↔ (f ×ˢ g ⊓ 𝓟 ({a | p a} ×ˢ {b | q b})).NeBot
Tactic:
rfl
Proof state after:
no goals
Theorem: MapClusterPt.prod
Proof state before:
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : MapClusterPt b a f
ga : Tendsto g a (𝓝 c)
⊢ MapClusterPt (b, c) a fun x => (f x, g x)
Tactic:
rw [mapClusterPt_iff] at fa ⊢
Proof state after:
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : ∀ s ∈ 𝓝 b, ∃ᶠ (a : A) in a, f a ∈ s
ga : Tendsto g a (𝓝 c)
⊢ ∀ s ∈ 𝓝 (b, c), ∃ᶠ (a : A) in a, (f a, g a) ∈ s
Theorem: MapClusterPt.prod
Proof state before:
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : ∀ s ∈ 𝓝 b, ∃ᶠ (a : A) in a, f a ∈ s
ga : Tendsto g a (𝓝 c)
⊢ ∀ s ∈ 𝓝 (b, c), ∃ᶠ (a : A) in a, (f a, g a) ∈ s
Tactic:
intro s n
Proof state after:
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : ∀ s ∈ 𝓝 b, ∃ᶠ (a : A) in a, f a ∈ s
ga : Tendsto g a (𝓝 c)
s : Set (B × C)
n : s ∈ 𝓝 (b, c)
⊢ ∃ᶠ (a : A) in a, (f a, g a) ∈ s
Theorem: MapClusterPt.prod
Proof state before:
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : ∀ s ∈ 𝓝 b, ∃ᶠ (a : A) in a, f a ∈ s
ga : Tendsto g a (𝓝 c)
s : Set (B × C)
n : s ∈ 𝓝 (b, c)
⊢ ∃ᶠ (a : A) in a, (f a, g a) ∈ s
Tactic:
rcases mem_nhds_prod_iff.mp n with ⟨u, un, v, vn, sub⟩
Proof state after:
case intro.intro.intro.intro
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : ∀ s ∈ 𝓝 b, ∃ᶠ (a : A) in a, f a ∈ s
ga : Tendsto g a (𝓝 c)
s : Set (B × C)
n : s ∈ 𝓝 (b, c)
u : Set B
un : u ∈ 𝓝 b
v : Set C
vn : v ∈ 𝓝 c
sub : u ×ˢ v ⊆ s
⊢ ∃ᶠ (a : A) in a, (f a, g a) ∈ s
Theorem: MapClusterPt.prod
Proof state before:
case intro.intro.intro.intro
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : ∀ s ∈ 𝓝 b, ∃ᶠ (a : A) in a, f a ∈ s
ga : Tendsto g a (𝓝 c)
s : Set (B × C)
n : s ∈ 𝓝 (b, c)
u : Set B
un : u ∈ 𝓝 b
v : Set C
vn : v ∈ 𝓝 c
sub : u ×ˢ v ⊆ s
⊢ ∃ᶠ (a : A) in a, (f a, g a) ∈ s
Tactic:
apply (fa _ un).mp
Proof state after:
case intro.intro.intro.intro
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : ∀ s ∈ 𝓝 b, ∃ᶠ (a : A) in a, f a ∈ s
ga : Tendsto g a (𝓝 c)
s : Set (B × C)
n : s ∈ 𝓝 (b, c)
u : Set B
un : u ∈ 𝓝 b
v : Set C
vn : v ∈ 𝓝 c
sub : u ×ˢ v ⊆ s
⊢ ∀ᶠ (x : A) in a, f x ∈ u → (f x, g x) ∈ s
Theorem: MapClusterPt.prod
Proof state before:
case intro.intro.intro.intro
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : ∀ s ∈ 𝓝 b, ∃ᶠ (a : A) in a, f a ∈ s
ga : Tendsto g a (𝓝 c)
s : Set (B × C)
n : s ∈ 𝓝 (b, c)
u : Set B
un : u ∈ 𝓝 b
v : Set C
vn : v ∈ 𝓝 c
sub : u ×ˢ v ⊆ s
⊢ ∀ᶠ (x : A) in a, f x ∈ u → (f x, g x) ∈ s
Tactic:
apply (Filter.tendsto_iff_forall_eventually_mem.mp ga v vn).mp
Proof state after:
case intro.intro.intro.intro
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : ∀ s ∈ 𝓝 b, ∃ᶠ (a : A) in a, f a ∈ s
ga : Tendsto g a (𝓝 c)
s : Set (B × C)
n : s ∈ 𝓝 (b, c)
u : Set B
un : u ∈ 𝓝 b
v : Set C
vn : v ∈ 𝓝 c
sub : u ×ˢ v ⊆ s
⊢ ∀ᶠ (x : A) in a, g x ∈ v → f x ∈ u → (f x, g x) ∈ s
Theorem: MapClusterPt.prod
Proof state before:
case intro.intro.intro.intro
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : ∀ s ∈ 𝓝 b, ∃ᶠ (a : A) in a, f a ∈ s
ga : Tendsto g a (𝓝 c)
s : Set (B × C)
n : s ∈ 𝓝 (b, c)
u : Set B
un : u ∈ 𝓝 b
v : Set C
vn : v ∈ 𝓝 c
sub : u ×ˢ v ⊆ s
⊢ ∀ᶠ (x : A) in a, g x ∈ v → f x ∈ u → (f x, g x) ∈ s
Tactic:
exact eventually_of_forall fun x gv fu ↦ sub (mk_mem_prod fu gv)
Proof state after:
no goals
Theorem: Option.bind_const_none
Proof state before:
α : Type u_1
β : Type u_2
x : Option α
⊢ (Option.bind x fun x => none) = none
Tactic:
cases x <;> simp
Proof state after:
no goals
Theorem: Option.isNone_false_iff_isSome
Proof state before:
α : Type u_1
x : Option α
⊢ isNone x = false ↔ isSome x = true
Tactic:
cases x <;> simp
Proof state after:
no goals
Theorem: Fin.tuple_sequence₁
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Fin 1 → Type u
x : (i : Fin 1) → m (α i)
⊢ tupleSequence x = do
    let r₀ ← x 0
    pure (cons r₀ default)
Tactic:
simp [Fin.tupleSequence, functor_norm]
Proof state after:
no goals
Theorem: Fin.tuple_sequence₂
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Fin 2 → Type u
x : (i : Fin 2) → m (α i)
⊢ tupleSequence x = do
    let r₀ ← x 0
    let r₁ ← x 1
    pure (cons r₀ (cons r₁ default))
Tactic:
simp [Fin.tupleSequence, functor_norm]
Proof state after:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Fin 2 → Type u
x : (i : Fin 2) → m (α i)
⊢ (do
      let r ← x 0
      let x ← tail x 0
      pure (cons r (cons x default))) =
    do
    let r₀ ← x 0
    let r₁ ← x 1
    pure (cons r₀ (cons r₁ default))
Theorem: Fin.tuple_sequence₂
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Fin 2 → Type u
x : (i : Fin 2) → m (α i)
⊢ (do
      let r ← x 0
      let x ← tail x 0
      pure (cons r (cons x default))) =
    do
    let r₀ ← x 0
    let r₁ ← x 1
    pure (cons r₀ (cons r₁ default))
Tactic:
rfl
Proof state after:
no goals
Theorem: Option.bind_isSome
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
β : Type u_2
x : Option α
y : α → Option β
⊢ isSome (Option.bind x y) = true ↔ ∃ (h : isSome x = true), isSome (y (get x h)) = true
Tactic:
cases x <;> simp
Proof state after:
no goals
Theorem: Option.map_isSome
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α β : Type u_1
x : Option α
y : α → β
⊢ isSome (y <$> x) = isSome x
Tactic:
cases x <;> simp
Proof state after:
no goals
Theorem: Option.not_isSome'
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
x : Option α
⊢ (!decide (isSome x = isNone x)) = true
Tactic:
cases x <;> simp
Proof state after:
no goals
Theorem: Option.guardProp_isSome
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
p : Prop
inst✝ : Decidable p
x : α
⊢ isSome (guardProp p x) = true ↔ p
Tactic:
dsimp only [Option.guardProp]
Proof state after:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
p : Prop
inst✝ : Decidable p
x : α
⊢ isSome (if p then some x else none) = true ↔ p
Theorem: Option.guardProp_isSome
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
p : Prop
inst✝ : Decidable p
x : α
⊢ isSome (if p then some x else none) = true ↔ p
Tactic:
split_ifs <;> simpa
Proof state after:
no goals
Theorem: Option.coe_part_dom
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
x : Option α
⊢ (↑x).Dom ↔ isSome x = true
Tactic:
cases x <;> simp
Proof state after:
no goals
Theorem: Option.coe_part_eq_some
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
x : Option α
y : α
⊢ ↑x = Part.some y ↔ x = some y
Tactic:
simp [Part.eq_some_iff]
Proof state after:
no goals
Theorem: List.get?_isSome_iff
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
x : List α
n : ℕ
⊢ Option.isSome (get? x n) = true ↔ n < length x
Tactic:
rw [← not_iff_not]
Proof state after:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
x : List α
n : ℕ
⊢ ¬Option.isSome (get? x n) = true ↔ ¬n < length x
Theorem: List.get?_isSome_iff
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
x : List α
n : ℕ
⊢ ¬Option.isSome (get? x n) = true ↔ ¬n < length x
Tactic:
simp [Option.isNone_iff_eq_none]
Proof state after:
no goals
Theorem: Option.map_is_some'
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
β : Type u_2
x : Option α
f : α → β
⊢ isSome (Option.map f x) = isSome x
Tactic:
cases x <;> simp
Proof state after:
no goals
Theorem: List.zipWith_fst
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
hl : length l₁ ≤ length l₂
⊢ zipWith (fun a b => a) l₁ l₂ = l₁
Tactic:
erw [← List.map_uncurry_zip_eq_zipWith, List.map_fst_zip]
Proof state after:
case a
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
hl : length l₁ ≤ length l₂
⊢ length l₁ ≤ length l₂
Theorem: List.zipWith_fst
Proof state before:
case a
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
hl : length l₁ ≤ length l₂
⊢ length l₁ ≤ length l₂
Tactic:
exact hl
Proof state after:
no goals
Theorem: List.zipWith_snd
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
hl : length l₂ ≤ length l₁
⊢ zipWith (fun a b => b) l₁ l₂ = l₂
Tactic:
erw [← List.map_uncurry_zip_eq_zipWith, List.map_snd_zip]
Proof state after:
case a
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
hl : length l₂ ≤ length l₁
⊢ length l₂ ≤ length l₁
Theorem: List.zipWith_snd
Proof state before:
case a
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
hl : length l₂ ≤ length l₁
⊢ length l₂ ≤ length l₁
Tactic:
exact hl
Proof state after:
no goals
Theorem: Multiset.map_get
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
l : List α
⊢ map (List.get l) Finset.univ.val = ↑l
Tactic:
simp [Finset.univ, Fintype.elems]
Proof state after:
no goals
Theorem: Multiset.get_zero
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
⊢ get 0 = none
Tactic:
simp [Multiset.get]
Proof state after:
no goals
Theorem: Multiset.get_singleton
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
a : α
⊢ get {a} = some a
Tactic:
simp [Multiset.get]
Proof state after:
no goals
Theorem: le_false_iff
Proof state before:
m : Type u → Type v
inst✝ : Monad m
⊢ ∀ {b : Bool}, b ≤ false ↔ b = false
Tactic:
decide
Proof state after:
no goals
Theorem: lt_true_iff
Proof state before:
m : Type u → Type v
inst✝ : Monad m
⊢ ∀ {b : Bool}, b < true ↔ b = false
Tactic:
decide
Proof state after:
no goals
Theorem: false_lt_iff
Proof state before:
m : Type u → Type v
inst✝ : Monad m
⊢ ∀ {b : Bool}, false < b ↔ b = true
Tactic:
decide
Proof state after:
no goals
Theorem: ne_min_of_ne_and_ne
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a x y : ι
hx : a ≠ x
hy : a ≠ y
⊢ a ≠ min x y
Tactic:
rcases min_choice x y with h | h <;> rw [h] <;> assumption
Proof state after:
no goals
Theorem: max_ne_self_iff
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a b : ι
⊢ ¬a = max a b ↔ a < b
Tactic:
rw [max_def]
Proof state after:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a b : ι
⊢ (¬a = if a ≤ b then b else a) ↔ a < b
Theorem: max_ne_self_iff
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a b : ι
⊢ (¬a = if a ≤ b then b else a) ↔ a < b
Tactic:
split_ifs with h
Proof state after:
case pos
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a b : ι
h : a ≤ b
⊢ ¬a = b ↔ a < b

case neg
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a b : ι
h : ¬a ≤ b
⊢ ¬a = a ↔ a < b
Theorem: max_ne_self_iff
Proof state before:
case pos
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a b : ι
h : a ≤ b
⊢ ¬a = b ↔ a < b
Tactic:
simpa using h
Proof state after:
no goals
Theorem: max_ne_self_iff
Proof state before:
case neg
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a b : ι
h : ¬a ≤ b
⊢ ¬a = a ↔ a < b
Tactic:
simpa using le_of_not_ge h
Proof state after:
no goals
Theorem: max_ne_self_iff'
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a b : ι
⊢ ¬b = max a b ↔ b < a
Tactic:
rw [max_comm]
Proof state after:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a b : ι
⊢ ¬b = max b a ↔ b < a
Theorem: max_ne_self_iff'
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a b : ι
⊢ ¬b = max b a ↔ b < a
Tactic:
simp
Proof state after:
no goals
Theorem: WithTop.isSome_iff_lt_top
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type
inst✝ : PartialOrder ι
x : WithTop ι
⊢ Option.isSome x = true ↔ x < ⊤
Tactic:
rw [← not_iff_not, Bool.eq_false_eq_not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none,
  lt_top_iff_ne_top, Ne, Classical.not_not]
Proof state after:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type
inst✝ : PartialOrder ι
x : WithTop ι
⊢ x = none ↔ x = ⊤
Theorem: WithTop.isSome_iff_lt_top
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type
inst✝ : PartialOrder ι
x : WithTop ι
⊢ x = none ↔ x = ⊤
Tactic:
rfl
Proof state after:
no goals
Theorem: Prod.Lex.le_iff''
Proof state before:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : Lex (α × β)
⊢ x ≤ y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 ≤ y.2)
Tactic:
rw [Prod.Lex.le_iff', le_iff_lt_or_eq]
Proof state after:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : Lex (α × β)
⊢ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 ≤ y.2 ↔ (x.1 < y.1 ∨ x.1 = y.1) ∧ (x.1 = y.1 → x.2 ≤ y.2)
Theorem: Prod.Lex.le_iff''
Proof state before:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : Lex (α × β)
⊢ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 ≤ y.2 ↔ (x.1 < y.1 ∨ x.1 = y.1) ∧ (x.1 = y.1 → x.2 ≤ y.2)
Tactic:
have := @ne_of_lt _ _ x.1 y.1
Proof state after:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : Lex (α × β)
this : x.1 < y.1 → x.1 ≠ y.1
⊢ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 ≤ y.2 ↔ (x.1 < y.1 ∨ x.1 = y.1) ∧ (x.1 = y.1 → x.2 ≤ y.2)
Theorem: Prod.Lex.le_iff''
Proof state before:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : Lex (α × β)
this : x.1 < y.1 → x.1 ≠ y.1
⊢ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 ≤ y.2 ↔ (x.1 < y.1 ∨ x.1 = y.1) ∧ (x.1 = y.1 → x.2 ≤ y.2)
Tactic:
tauto
Proof state after:
no goals
Theorem: Prod.Lex.lt_iff''
Proof state before:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : Lex (α × β)
⊢ x < y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2)
Tactic:
rw [lt_iff', le_iff_lt_or_eq]
Proof state after:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : Lex (α × β)
⊢ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2 ↔ (x.1 < y.1 ∨ x.1 = y.1) ∧ (x.1 = y.1 → x.2 < y.2)
Theorem: Prod.Lex.lt_iff''
Proof state before:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : Lex (α × β)
⊢ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2 ↔ (x.1 < y.1 ∨ x.1 = y.1) ∧ (x.1 = y.1 → x.2 < y.2)
Tactic:
have : x.1 < y.1 → ¬x.1 = y.1 := ne_of_lt
Proof state after:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : Lex (α × β)
this : x.1 < y.1 → ¬x.1 = y.1
⊢ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2 ↔ (x.1 < y.1 ∨ x.1 = y.1) ∧ (x.1 = y.1 → x.2 < y.2)
Theorem: Prod.Lex.lt_iff''
Proof state before:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : Lex (α × β)
this : x.1 < y.1 → ¬x.1 = y.1
⊢ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2 ↔ (x.1 < y.1 ∨ x.1 = y.1) ∧ (x.1 = y.1 → x.2 < y.2)
Tactic:
tauto
Proof state after:
no goals
Theorem: Prod.Lex.fst_le_of_le
Proof state before:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : Lex (α × β)
h : x ≤ y
⊢ x.1 ≤ y.1
Tactic:
rw [Prod.Lex.le_iff'] at h
Proof state after:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : Lex (α × β)
h : x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 ≤ y.2
⊢ x.1 ≤ y.1
Theorem: Prod.Lex.fst_le_of_le
Proof state before:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : Lex (α × β)
h : x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 ≤ y.2
⊢ x.1 ≤ y.1
Tactic:
cases h with
| inl h => exact h.le
| inr h => exact h.1.le
Proof state after:
no goals
Theorem: Prod.Lex.fst_le_of_le
Proof state before:
case inl
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : Lex (α × β)
h : x.1 < y.1
⊢ x.1 ≤ y.1
Tactic:
exact h.le
Proof state after:
no goals
Theorem: Prod.Lex.fst_le_of_le
Proof state before:
case inr
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : Lex (α × β)
h : x.1 = y.1 ∧ x.2 ≤ y.2
⊢ x.1 ≤ y.1
Tactic:
exact h.1.le
Proof state after:
no goals
Theorem: Prod.Lex.fst_lt_of_lt_of_le
Proof state before:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : Preorder α
inst✝ : PartialOrder β
x y : Lex (α × β)
h : x < y
h' : y.2 ≤ x.2
⊢ x.1 < y.1
Tactic:
rw [Prod.Lex.lt_iff'] at h
Proof state after:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : Preorder α
inst✝ : PartialOrder β
x y : Lex (α × β)
h : x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2
h' : y.2 ≤ x.2
⊢ x.1 < y.1
Theorem: Prod.Lex.fst_lt_of_lt_of_le
Proof state before:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : Preorder α
inst✝ : PartialOrder β
x y : Lex (α × β)
h : x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2
h' : y.2 ≤ x.2
⊢ x.1 < y.1
Tactic:
cases h with
| inl h => exact h
| inr h => cases h.2.not_le h'
Proof state after:
no goals
Theorem: Prod.Lex.fst_lt_of_lt_of_le
Proof state before:
case inl
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : Preorder α
inst✝ : PartialOrder β
x y : Lex (α × β)
h' : y.2 ≤ x.2
h : x.1 < y.1
⊢ x.1 < y.1
Tactic:
exact h
Proof state after:
no goals
Theorem: Prod.Lex.fst_lt_of_lt_of_le
Proof state before:
case inr
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : Preorder α
inst✝ : PartialOrder β
x y : Lex (α × β)
h' : y.2 ≤ x.2
h : x.1 = y.1 ∧ x.2 < y.2
⊢ x.1 < y.1
Tactic:
cases h.2.not_le h'
Proof state after:
no goals