mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Vector.Defs

Goal state before:
pp: case mk
α : Type u_1
n m : ℕ
val✝ : List α
property✝ : val✝.length = m
⊢ (take n ⟨val✝, property✝⟩).toList = List.take n (toList ⟨val✝, property✝⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∉ s
⊢ ∀ x ∈ s, (if h : x = a then b x h else 1) = 1

Tactic:
grind

Goal state after:
Module: Mathlib.Control.Traversable.Basic

Goal state before:
pp: F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
η η' : ApplicativeTransformation F G
h : ∀ (α : Type u) (x : F α), (fun {α} ↦ η.app α) x = (fun {α} ↦ η'.app α) x
⊢ (fun {α} ↦ η.app α) = fun {α} ↦ η'.app α

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
⊢ image (fun i ↦ b ↑i) univ ⊂ image b univ

Tactic:
grind

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ α✝ β✝ : Type v
x✝ : Comp F G α✝
y✝ : Comp F G β✝
⊢ x✝ <* y✝ = const β✝ <$> x✝ <*> y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ α✝ β✝ : Type v
x✝ : Comp F G α✝
y✝ : Comp F G β✝
⊢ x✝ *> y✝ = const α✝ id <$> x✝ <*> y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case h.inr.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ g' i ≠ ⟨f a, hfat⟩

pp: case h.inr.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ g' i ≠ g' a

Tactic:
· exact
        ne_of_apply_ne Subtype.val
          (ne_of_eq_of_ne (hg' _ hi) <|
            hfs.ne (subset_insert _ _ hi) (mem_insert_self _ _) <| ne_of_mem_of_not_mem hi has)

Goal state after:
case h.inr.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ g' i ≠ g' a
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case mk
α : Type u_1
n : ℕ
β : Type u_6
f : α → β
val✝ : List α
property✝ : val✝.length = n
⊢ (map f ⟨val✝, property✝⟩).toList = List.map f (toList ⟨val✝, property✝⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
val✝ : List α
property✝ : val✝.length = n
hp : ∀ (x : α), x ∈ toList ⟨val✝, property✝⟩ → p x
⊢ (pmap f ⟨val✝, property✝⟩ hp).toList = List.pmap f (toList ⟨val✝, property✝⟩) hp

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case mk
α : Type u_1
n : ℕ
a : α
val✝ : List α
property✝ : val✝.length = n
⊢ ofVector (a ::ᵥ ⟨val✝, property✝⟩) = a ::ₛ ofVector ⟨val✝, property✝⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case mk
α : Type u_1
n : ℕ
a : α
val✝ : List α
property✝ : val✝.length = n
⊢ ↑(a ::ₛ ofVector ⟨val✝, property✝⟩) = ↑(ofVector (a ::ᵥ ⟨val✝, property✝⟩))

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
n✝ n' m : ℕ
s : Sym α✝ n✝
a b : α✝
α : Type u_3
n : ℕ
x✝ : List α
⊢ x✝.length = n ↔ Multiset.card ⟦x✝⟧ = n

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
n✝ n' m : ℕ
s : Sym α✝ n✝
a b : α✝
α : Type u_3
n : ℕ
x✝¹ x✝ : { l // l.length = n }
⊢ (Vector.Perm.isSetoid α n) x✝¹ x✝ ↔ (List.isSetoid α) ↑x✝¹ ↑x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case mk
α : Type u_3
n : ℕ
a : α
val✝ : Multiset α
l : List α
property✝ : Multiset.card (Quot.mk (⇑(List.isSetoid α)) l) = n
⊢ (a :: symEquivSym' ⟨Quot.mk (⇑(List.isSetoid α)) l, property✝⟩) =
    symEquivSym' (a ::ₛ ⟨Quot.mk (⇑(List.isSetoid α)) l, property✝⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case nil
α : Type u_1
n i : ℕ
ih : i < n - 1
h : [].length = n
⊢ (tail ⟨[], h⟩).get ⟨i, ih⟩ = get ⟨[], h⟩ ⟨i + 1, ⋯⟩

Tactic:
rfl

Goal state after:
case nil
α : Type u_1
n i : ℕ
ih : i < n - 1
h : [].length = n
⊢ (tail ⟨[], h⟩).get ⟨i, ih⟩ = get ⟨[], h⟩ ⟨i + 1, ⋯⟩
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case cons
α : Type u_1
n i : ℕ
ih : i < n - 1
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝).length = n
⊢ (tail ⟨head✝ :: tail✝, h⟩).get ⟨i, ih⟩ = get ⟨head✝ :: tail✝, h⟩ ⟨i + 1, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
l : List α
e : (a :: l).length = n.succ
i : ℕ
h : i < n
⊢ (tail ⟨a :: l, e⟩).toList[i] = get ⟨a :: l, e⟩ ⟨i + 1, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n.succ → α
i : Fin (n.succ - 1)
⊢ f ⟨↑i + 1, ⋯⟩ = f i.succ

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
property✝ : [].length = n
⊢ (tail ⟨[], property✝⟩).toList = (toList ⟨[], property✝⟩).tail

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
head✝ : α
tail✝ : List α
property✝ : (head✝ :: tail✝).length = n
⊢ (tail ⟨head✝ :: tail✝, property✝⟩).toList = (toList ⟨head✝ :: tail✝, property✝⟩).tail

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α 1
l l' : { x // x.length = 1 }
⊢ (Subtype.instSetoid_mathlib fun x ↦ x.length = 1) l l' ↔ (List.isSetoid α) ↑l ↑l'

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a✝ b : α
val✝ : Multiset α
a : α
h : Multiset.card (Quot.mk ⇑(List.isSetoid α) [a]) = 1
⊢ (fun a ↦ ⟨{a}, ⋯⟩)
      ((fun s ↦
          ((Equiv.subtypeQuotientEquivQuotientSubtype (fun x ↦ x.length = 1) (fun x ↦ Multiset.card x = 1) ⋯ ⋯)
                s).liftOn
            (fun l ↦ (↑l).head ⋯) ⋯)
        ⟨Quot.mk ⇑(List.isSetoid α) [a], h⟩) =
    ⟨Quot.mk ⇑(List.isSetoid α) [a], h⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ Option.map (fun x1 x2 ↦ x1 :: x2) (decode v₁) <*> decodeList v₂ =
    Option.map (fun x1 x2 ↦ x1 :: x2) (decode v₁) <*> decode v₂

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case pos
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ((↑v).eraseIdx i).insertIdx j a =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      j a

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: case h
α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
x✝ : α
⊢ x✝ ∈ {x | p x} ↔ p x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case neg
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ ((↑v).eraseIdx i).insertIdx j a =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      j a

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: F : Type u → Type u
inst✝ : Applicative F
α β : Type u
f : α → F β
x : α
xs : List α
⊢ Vector.traverse f (x ::ᵥ ⟨xs, ⋯⟩) = cons <$> f x <*> Vector.traverse f ⟨xs, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case nil
α : Type u
⊢ traverseAux pure [] = pure ⟨[], ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case nil
n : ℕ
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
⊢ pure nil = Comp.mk (pure (pure nil))

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case nil
α β : Type u_6
f : α → β
⊢ pure nil = pure ⟨[], ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case cons
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
ih : (fun {α} ↦ η.app α) (Vector.traverse f w✝) = Vector.traverse ((fun {α} ↦ η.app α) ∘ f) w✝
⊢ cons <$> (fun {α} ↦ η.app α) (f x✝) <*> (fun {α} ↦ η.app α) (Vector.traverse f w✝) =
    cons <$> ((fun {α} ↦ η.app α) ∘ f) x✝ <*> (fun {α} ↦ η.app α) (Vector.traverse f w✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
p : Set β
f : r ≼i s
H : ∀ (a : α), f a ∈ p
a : α
x✝ : { x // x ∈ p }
a' : α
m : f a' ∈ p
h : Subrel s (fun x ↦ x ∈ p) ⟨f a', m⟩ ((RelEmbedding.codRestrict p f.toRelEmbedding H) a)
⊢ (RelEmbedding.codRestrict p f.toRelEmbedding H) a' = ⟨f a', m⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder γ t
e : r ≃r s
f : r ≺i t
g : s ≺i t
⊢ (relIsoTrans e g).top = g.top

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
f' : r ≃r s
⊢ g.toRelEmbedding (f' a) = g.toRelEmbedding (f a)

Tactic:
f.eq_relIso

Goal state after:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
f' : r ≃r s
⊢ g.toRelEmbedding (f a) = g.toRelEmbedding (f a)
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case h.inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a m : α
h : s (↑(collapseF f m)) ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a)
hm : m ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) ↑(collapseF f m)}
hm' : ∀ x ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) ↑(collapseF f m)}, ¬r x m
⊢ (ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) m = ↑(collapseF f m)

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
x : β
s : Set α
a✝³ : s ∈ D
a : α
h✝ : a ∈ s
a✝² : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a✝¹ : α
a✝ : IsLUB s a✝¹
⊢ ∀ ⦃a : β⦄, (∀ a_1 ∈ s, x ≤ a) → x ≤ a

Tactic:
grind

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun x ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : ∀ x ∈ d, ∀ y ∈ d, ∃ z ∈ d, x ≤ z ∧ y ≤ z
a : α
ha : IsLUB d a
this : (∀ (a b : α), a ≤ b → {a, b} ∈ D) → ∀ ⦃a b : α⦄, a ≤ b → f a ≤ f b
⊢ ∀ a ∈ d, ∀ a_2 ∈ d, ∃ a_4 ∈ d, f a ≤ f a_4 ∧ f a_2 ≤ f a_4

Tactic:
grind

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun x ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (f '' d)
⊢ f (Exists.choose hd₂) ∈ (fun x ↦ f '' x) d

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: case zero
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁✝ a₂✝ a₁ a₂ : α
⊢ (⇑f)^[0] (a₁ ⊔ a₂) ≤ (⇑f)^[0] a₁ ⊔ a₂

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : α → γ
hf : ScottContinuousOn univ f
hg : ScottContinuousOn univ g
⊢ ∀ (a b : α), a ≤ b → {a, b} ∈ univ

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ o.toOption = Option.some a ↔ a ∈ o

Tactic:
← Option.mem_def,

Goal state after:
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ a ∈ o.toOption ↔ a ∈ o
Module: Mathlib.Data.Part

Goal state before:
pp: case pos
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : a.Dom
⊢ (Option.some (a.get h)).elim b f = f (a.get h)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case neg
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
⊢ Option.none.elim b f = b

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case some
α : Type u_4
val✝ : α
h₁ : (↑(Option.some val✝)).Dom
h₂ : { Dom := (Option.some val✝).isSome = true, get := (Option.some val✝).get }.Dom
⊢ (↑(Option.some val✝)).get h₁ = { Dom := (Option.some val✝).isSome = true, get := (Option.some val✝).get }.get h₂

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case none
α : Type u_1
⊢ (↑Option.none).toOption = Option.none

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case some
α : Type u_1
val✝ : α
⊢ (↑(Option.some val✝)).toOption = Option.some val✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
h : o.Dom
⊢ (f (o.get h)).toOption = (Option.some (o.get h)).elim Option.none fun a ↦ (f a).toOption

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
γ : Type u_3
α✝ : Type u_4
Dom✝ : Prop
get✝ : Dom✝ → α✝
⊢ id <$> { Dom := Dom✝, get := get✝ } = { Dom := Dom✝, get := get✝ }

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case zero
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ ((pair a₁ a₂ ha).zip (pair b₁ b₂ hb)) 0 = (pair (a₁, b₁) (a₂, b₂) ⋯) 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case succ
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
n✝ : ℕ
⊢ ((pair a₁ a₂ ha).zip (pair b₁ b₂ hb)) (n✝ + 1) = (pair (a₁, b₁) (a₂, b₂) ⋯) (n✝ + 1)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Mul α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ (a * b).get ⋯ = a.get ⋯ * b.get ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case union
α : Type u_1
r : α → α → Prop
c : Set α
s✝ : Set (Set α)
hs : ∀ a ∈ s✝, ChainClosure r a
h : ∀ a ∈ s✝, IsChain r a
⊢ IsChain r (⋃₀ s✝)

Tactic:
exact fun c₁ ⟨t₁, ht₁, (hc₁ : c₁ ∈ t₁)⟩ c₂ ⟨t₂, ht₂, (hc₂ : c₂ ∈ t₂)⟩ hneq =>
      ((hs _ ht₁).total <| hs _ ht₂).elim (fun ht => h t₂ ht₂ (ht hc₁) hc₂ hneq) fun ht =>
        h t₁ ht₁ hc₁ (ht hc₂) hneq

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
a✝ : y ≠ z
left✝ : z ∈ bot x f
hz : z ≤ y
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z ∨ (fun x1 x2 ↦ x1 ≤ x2) z y

pp: case inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
a✝ : y ≠ z
left✝ : z ∈ bot x f
hz : f y ≤ z
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z ∨ (fun x1 x2 ↦ x1 ≤ x2) z y

Tactic:
· right; exact hz

Goal state after:
case inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
a✝ : y ≠ z
left✝ : z ∈ bot x f
hz : f y ≤ z
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z ∨ (fun x1 x2 ↦ x1 ≤ x2) z y
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsChain (fun x1 x2 ↦ x1 ≤ x2) (bot x f)

Tactic:
intro y hy z hz _
  rw [mem_bot_iff_isExtremePt le_map] at hy
  rw [← bot_eq_of_le_or_map_le le_map hy] at hz
  obtain ⟨_, (hz | hz)⟩ := hz
  · right; exact hz
  · left; exact le_trans (le_map y) hz

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type u_6
f : α → Part β
g : α → β → Part γ
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
⊢ ωSup (c.map ({ toFun := f, monotone' := ⋯ }.partBind { toFun := g, monotone' := ⋯ })) =
    ωSup (c.map { toFun := fun x ↦ f x >>= g x, monotone' := ⋯ })

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i : ℕ
⊢ g (c.toOrderHom i) ≤ (c.map { toFun := g, monotone' := ⋯ }) i

Tactic:
rfl

Goal state after:
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this✝ : Surjective h
this : Injective h
a : α
h✝ : a ∉ s
⊢ a ∈ g '' (f '' s)ᶜ

Tactic:
grind

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β✝
inst✝¹ : OmegaCompletePartialOrder γ✝
inst✝ : OmegaCompletePartialOrder δ
β γ : Type v
f : α →𝒄 Part β
g : α →𝒄 β → Part γ
c : Chain α
⊢ ((↑f).partBind ↑g).toFun (ωSup c) = f (ωSup c) >>= g (ωSup c)

Tactic:
rfl

Goal state after:
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case inr.isFalse
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this✝¹ : Surjective h
this✝ : Injective h
a : α
h✝ : a ∉ s
this : g (invFun g a) = a
⊢ R a (invFun g a)

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
h : IsSMulRegular M 0
a b : M
⊢ (fun x ↦ 0 • x) a = (fun x ↦ 0 • x) b

Tactic:
by dsimp only [Function.comp_def]; repeat' rw [MulActionWithZero.zero_smul]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: f : Cardinal.{u} → Cardinal.{max u v}
s : Set Cardinal.{u}
hs : BddAbove s
⊢ BddAbove (f '' s)

Tactic:
rw [bddAbove_iff_small] at hs ⊢
  exact small_lift _

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
h : ∀ (n : ℕ), ↑n ≤ c
hn : c < ℵ₀
⊢ False

Tactic:
rcases lt_aleph0.1 hn with ⟨n, rfl⟩

Goal state after:
n : ℕ
h : ∀ (n_1 : ℕ), ↑n_1 ≤ ↑n
hn : ↑n < ℵ₀
⊢ False
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑m * ↑n < ℵ₀

Tactic:
by rw [← Nat.cast_mul]; apply natCast_lt_aleph0

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
s : Finset ↑t
u : Finset α := Finset.image Subtype.val s
this : u.card = s.card
⊢ s.card ≤ n

Tactic:
grind

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x ↦ f ↑x
⊢ lift.{v, u} #↑{x | f ↑x ∈ t} = lift.{v, u} #↑((fun x ↦ f ↑x) ⁻¹' t)

Tactic:
rfl

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x ↦ f ↑x
⊢ #↑{x | f ↑x ∈ t} = #↑((fun x ↦ f ↑x) ⁻¹' t)

Tactic:
rfl

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u}
α : Type u
s : Set α
t : Set ↑s
⊢ #↑t = c ↔ #↑(Subtype.val '' t) = c

Tactic:
mk_image_eq

Goal state after:
c : Cardinal.{u}
α : Type u
s : Set α
t : Set ↑s
⊢ #↑t = c ↔ #↑t = c

c : Cardinal.{u}
α : Type u
s : Set α
t : Set ↑s
⊢ Injective Subtype.val
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
toSemigroupAction✝ : SemigroupAction (M × N) α
one_smul✝ : ∀ (b : α), 1 • b = b
m : M
n : N
a : α
⊢ (m, n) • a = SMul.smul (m, n) a

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m (1 • a)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_4.e_2.e_4.e_4.e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
x✝ : MulAction N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m (1 • a)

Tactic:
rfl

Goal state after: