mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case inl
M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
S : Submonoid M := { carrier := {1, a}, mul_mem' := ⋯, one_mem' := ⋯ }
⊢ 1 ∈ powers a

pp: case inr
M : Type u_1
inst✝ : Monoid M
x✝ : M
ha : IsIdempotentElem x✝
S : Submonoid M := { carrier := {1, x✝}, mul_mem' := ⋯, one_mem' := ⋯ }
⊢ x✝ ∈ powers x✝

Tactic:
;

Goal state after:
case inl
M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
S : Submonoid M := { carrier := {1, a}, mul_mem' := ⋯, one_mem' := ⋯ }
⊢ 1 ∈ powers a

case inr
M : Type u_1
inst✝ : Monoid M
x✝ : M
ha : IsIdempotentElem x✝
S : Submonoid M := { carrier := {1, x✝}, mul_mem' := ⋯, one_mem' := ⋯ }
⊢ x✝ ∈ powers x✝
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * (↑(m + 1) * ↑(n - 1) % ↑n).toNat) = x ^ (k * ((↑m.succ % ↑n).toNat * (n - 1)))

Tactic:
;

Goal state after:
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * (↑(m + 1) * ↑(n - 1) % ↑n).toNat) = x ^ (k * ((↑m.succ % ↑n).toNat * (n - 1)))
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
⊢ ∀ x ∈ s,
    ∀ (y : M),
      (∀ (y_1 : N) (z : α), (y • y_1) • z = y • y_1 • z) → ∀ (y_1 : N) (z : α), ((x * y) • y_1) • z = (x * y) • y_1 • z

Tactic:
intro x hx x' hx' y z

Goal state after:
case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
hx : x ∈ s
x' : M
hx' : ∀ (y : N) (z : α), (x' • y) • z = x' • y • z
y : N
z : α
⊢ ((x * x') • y) • z = (x * x') • y • z
Module: Mathlib.Data.Nat.Order.Lemmas

Goal state before:
pp: ⊢ 0 ∈ Set.univ ∧ ∀ (k : ℕ), k ∈ Set.univ → k + 1 ∈ Set.univ

Tactic:
;

Goal state after:
⊢ 0 ∈ Set.univ ∧ ∀ (k : ℕ), k ∈ Set.univ → k + 1 ∈ Set.univ
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
⊢ ∀ x ∈ s, ∀ (y : M), (∀ (n : N) (a : α), y • n • a = n • y • a) → ∀ (n : N) (a : α), (x * y) • n • a = n • (x * y) • a

Tactic:
intro x hx x' hx' y z

Goal state after:
case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
hx : x ∈ s
x' : M
hx' : ∀ (n : N) (a : α), x' • n • a = n • x' • a
y : N
z : α
⊢ (x * x') • y • z = y • (x * x') • z
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
⊢ ∀ x ∈ s, ∀ (y : M), (∀ (n : N) (a : α), y • n • a = n • y • a) → ∀ (n : N) (a : α), (x * y) • n • a = n • (x * y) • a

Tactic:
· clear x
    intro x hx x' hx' y z
    rw [mul_smul, mul_smul, hx', hs x hx]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: A : Type u_2
inst✝ : AddMonoid A
x y : A
⊢ (∃ x_1, ((multiplesHom A) x) x_1 = y) ↔ ∃ n, n • x = y

Tactic:
;

Goal state after:
A : Type u_2
inst✝ : AddMonoid A
x y : A
⊢ (∃ x_1, ((multiplesHom A) x) x_1 = y) ↔ ∃ n, n • x = y
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
a : α
l : List α
⊢ foldl (argAux fun b c ↦ f c < f b) none (l ++ [a]) =
    Option.casesOn (foldl (argAux fun b c ↦ f c < f b) none l) (some a) fun c ↦ if f c < f a then some a else some c

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
a : α
l : List α
⊢ foldl (argAux fun b c ↦ f c < f b) none (l ++ [a]) =
    Option.casesOn (foldl (argAux fun b c ↦ f c < f b) none l) (some a) fun c ↦ if f c < f a then some a else some c
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
inst✝¹ : Denumerable α
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ ((decode (unpair n).1).bind fun a ↦ Option.map (Sigma.mk a) (decode (unpair n).2)) =
    some ⟨ofNat α (unpair n).1, ofNat (γ (ofNat α (unpair n).1)) (unpair n).2⟩

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : Denumerable α
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ ((decode (unpair n).1).bind fun a ↦ Option.map (Sigma.mk a) (decode (unpair n).2)) =
    some ⟨ofNat α (unpair n).1, ofNat (γ (ofNat α (unpair n).1)) (unpair n).2⟩
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: x✝ : ℕ
⊢ ofNat (ℕ × ℕ) x✝ = unpair x✝

Tactic:
;

Goal state after:
x✝ : ℕ
⊢ ofNat (ℕ × ℕ) x✝ = unpair x✝
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
⊢ ∃ n, ↑x + n + 1 ∈ s

Tactic:
by_contra h
  have (a : ℕ) (ha : a ∈ s) : a < x + 1 :=
    lt_of_not_ge fun hax => h ⟨a - (x + 1), by rwa [Nat.add_right_comm, Nat.add_sub_cancel' hax]⟩
  classical
  exact Fintype.false
    ⟨(((Multiset.range (succ x)).filter (· ∈ s)).pmap
      (fun (y : ℕ) (hy : y ∈ s) => Subtype.mk y hy) (by simp [-Multiset.range_succ])).toFinset,
      by simpa [Subtype.ext_iff, Multiset.mem_filter, -Multiset.range_succ] ⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a : α
b : β
u : Finset (α ⊕ β)
⊢ ∀ (a a' : α ⊕ β), ∀ b ∈ Sum.elim some (fun x ↦ none) a, b ∈ Sum.elim some (fun x ↦ none) a' → a = a'

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a : α
b : β
u : Finset (α ⊕ β)
⊢ ∀ (a a' : α ⊕ β), ∀ b ∈ Sum.elim some (fun x ↦ none) a, b ∈ Sum.elim some (fun x ↦ none) a' → a = a'
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a : α
b : β
u : Finset (α ⊕ β)
⊢ ∀ (a a' : α ⊕ β), ∀ b ∈ Sum.elim (fun x ↦ none) some a, b ∈ Sum.elim (fun x ↦ none) some a' → a = a'

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a : α
b : β
u : Finset (α ⊕ β)
⊢ ∀ (a a' : α ⊕ β), ∀ b ∈ Sum.elim (fun x ↦ none) some a, b ∈ Sum.elim (fun x ↦ none) some a' → a = a'
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
a : ℕ
ha : a ∈ List.filter (fun y ↦ decide (y ∈ s)) (List.range x)
⊢ a ∈ s

Tactic:
;

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
a : ℕ
ha : a ∈ List.filter (fun y ↦ decide (y ∈ s)) (List.range x)
⊢ a ∈ s
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
x : α
⊢ x ∈ (s.disjSum t).toLeft ↔ x ∈ s

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
x : α
⊢ x ∈ (s.disjSum t).toLeft ↔ x ∈ s
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
x : β
⊢ x ∈ (s.disjSum t).toRight ↔ x ∈ t

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
x : β
⊢ x ∈ (s.disjSum t).toRight ↔ x ∈ t
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : β
⊢ x ∈ (map (Equiv.sumComm α β).toEmbedding u).toLeft ↔ x ∈ u.toRight

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : β
⊢ x ∈ (map (Equiv.sumComm α β).toEmbedding u).toLeft ↔ x ∈ u.toRight
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : α
⊢ x ∈ (map (Equiv.sumComm α β).toEmbedding u).toRight ↔ x ∈ u.toLeft

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : α
⊢ x ∈ (map (Equiv.sumComm α β).toEmbedding u).toRight ↔ x ∈ u.toLeft
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
ha : inl a ∉ u
y : α
⊢ y ∈ (cons (inl a) u ha).toLeft ↔ y ∈ cons a u.toLeft ⋯

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
ha : inl a ∉ u
y : α
⊢ y ∈ (cons (inl a) u ha).toLeft ↔ y ∈ cons a u.toLeft ⋯
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
hb : inr b ∉ u
y : α
⊢ y ∈ (cons (inr b) u hb).toLeft ↔ y ∈ u.toLeft

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
hb : inr b ∉ u
y : α
⊢ y ∈ (cons (inr b) u hb).toLeft ↔ y ∈ u.toLeft
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
ha : inl a ∉ u
y : β
⊢ y ∈ (cons (inl a) u ha).toRight ↔ y ∈ u.toRight

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
ha : inl a ∉ u
y : β
⊢ y ∈ (cons (inl a) u ha).toRight ↔ y ∈ u.toRight
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
hb : inr b ∉ u
y : β
⊢ y ∈ (cons (inr b) u hb).toRight ↔ y ∈ cons b u.toRight ⋯

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
hb : inr b ∉ u
y : β
⊢ y ∈ (cons (inr b) u hb).toRight ↔ y ∈ cons b u.toRight ⋯
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : β
⊢ x ∈ (image Sum.swap u).toLeft ↔ x ∈ u.toRight

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : β
⊢ x ∈ (image Sum.swap u).toLeft ↔ x ∈ u.toRight
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (image Sum.swap u).toRight ↔ x ∈ u.toLeft

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (image Sum.swap u).toRight ↔ x ∈ u.toLeft
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : α
⊢ y ∈ (insert (inl a) u).toLeft ↔ y ∈ insert a u.toLeft

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : α
⊢ y ∈ (insert (inl a) u).toLeft ↔ y ∈ insert a u.toLeft
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : α
⊢ y ∈ (insert (inr b) u).toLeft ↔ y ∈ u.toLeft

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : α
⊢ y ∈ (insert (inr b) u).toLeft ↔ y ∈ u.toLeft
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : β
⊢ y ∈ (insert (inl a) u).toRight ↔ y ∈ u.toRight

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : β
⊢ y ∈ (insert (inl a) u).toRight ↔ y ∈ u.toRight
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : β
⊢ y ∈ (insert (inr b) u).toRight ↔ y ∈ insert b u.toRight

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : β
⊢ y ∈ (insert (inr b) u).toRight ↔ y ∈ insert b u.toRight
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (u ∩ v).toLeft ↔ x ∈ u.toLeft ∩ v.toLeft

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (u ∩ v).toLeft ↔ x ∈ u.toLeft ∩ v.toLeft
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : β
⊢ x ∈ (u ∩ v).toRight ↔ x ∈ u.toRight ∩ v.toRight

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : β
⊢ x ∈ (u ∩ v).toRight ↔ x ∈ u.toRight ∩ v.toRight
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (u ∪ v).toLeft ↔ x ∈ u.toLeft ∪ v.toLeft

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (u ∪ v).toLeft ↔ x ∈ u.toLeft ∪ v.toLeft
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : β
⊢ x ∈ (u ∪ v).toRight ↔ x ∈ u.toRight ∪ v.toRight

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : β
⊢ x ∈ (u ∪ v).toRight ↔ x ∈ u.toRight ∪ v.toRight
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (u \ v).toLeft ↔ x ∈ u.toLeft \ v.toLeft

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (u \ v).toLeft ↔ x ∈ u.toLeft \ v.toLeft
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : β
⊢ x ∈ (u \ v).toRight ↔ x ∈ u.toRight \ v.toRight

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : β
⊢ x ∈ (u \ v).toRight ↔ x ∈ u.toRight \ v.toRight
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
g : TopHom α β
toFun✝ : α → β
map_top'✝ : toFun✝ ⊤ = ⊤
h : { toFun := toFun✝, map_top' := map_top'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_top' := map_top'✝ } = g

Tactic:
;

Goal state after:
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
g : TopHom α β
toFun✝ : α → β
map_top'✝ : toFun✝ ⊤ = ⊤
h : { toFun := toFun✝, map_top' := map_top'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_top' := map_top'✝ } = g
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
toFun✝¹ : α → β
map_top'✝¹ : toFun✝¹ ⊤ = ⊤
toFun✝ : α → β
map_top'✝ : toFun✝ ⊤ = ⊤
h : { toFun := toFun✝¹, map_top' := map_top'✝¹ }.toFun = { toFun := toFun✝, map_top' := map_top'✝ }.toFun
⊢ { toFun := toFun✝¹, map_top' := map_top'✝¹ } = { toFun := toFun✝, map_top' := map_top'✝ }

Tactic:
;

Goal state after:
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
toFun✝¹ : α → β
map_top'✝¹ : toFun✝¹ ⊤ = ⊤
toFun✝ : α → β
map_top'✝ : toFun✝ ⊤ = ⊤
h : { toFun := toFun✝¹, map_top' := map_top'✝¹ }.toFun = { toFun := toFun✝, map_top' := map_top'✝ }.toFun
⊢ { toFun := toFun✝¹, map_top' := map_top'✝¹ } = { toFun := toFun✝, map_top' := map_top'✝ }
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Top α
inst✝¹ : Top β
inst✝ : Top γ
g : TopHom β γ
f₁ f₂ : TopHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₂) a = g (f₂ a)

Tactic:
TopHom.comp_apply

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Top α
inst✝¹ : Top β
inst✝ : Top γ
g : TopHom β γ
f₁ f₂ : TopHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₂ a) = g (f₂ a)
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
g : BoundedOrderHom α β
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
map_top'✝ : { toFun := toFun✝, monotone' := monotone'✝ }.toFun ⊤ = ⊤
map_bot'✝ : { toFun := toFun✝, monotone' := monotone'✝ }.toFun ⊥ = ⊥
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, monotone' := monotone'✝, map_top' := map_top'✝, map_bot' := map_bot'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, monotone' := monotone'✝, map_top' := map_top'✝, map_bot' := map_bot'✝ } = g

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
g : BoundedOrderHom α β
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
map_top'✝ : { toFun := toFun✝, monotone' := monotone'✝ }.toFun ⊤ = ⊤
map_bot'✝ : { toFun := toFun✝, monotone' := monotone'✝ }.toFun ⊥ = ⊥
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, monotone' := monotone'✝, map_top' := map_top'✝, map_bot' := map_bot'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, monotone' := monotone'✝, map_top' := map_top'✝, map_bot' := map_bot'✝ } = g
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
map_top'✝¹ : { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun ⊤ = ⊤
map_bot'✝¹ : { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun ⊥ = ⊥
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
map_top'✝ : { toFun := toFun✝, monotone' := monotone'✝ }.toFun ⊤ = ⊤
map_bot'✝ : { toFun := toFun✝, monotone' := monotone'✝ }.toFun ⊥ = ⊥
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, monotone' := monotone'✝¹, map_top' := map_top'✝¹, map_bot' := map_bot'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, monotone' := monotone'✝, map_top' := map_top'✝, map_bot' := map_bot'✝ }
⊢ { toFun := toFun✝¹, monotone' := monotone'✝¹, map_top' := map_top'✝¹, map_bot' := map_bot'✝¹ } =
    { toFun := toFun✝, monotone' := monotone'✝, map_top' := map_top'✝, map_bot' := map_bot'✝ }

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
map_top'✝¹ : { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun ⊤ = ⊤
map_bot'✝¹ : { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun ⊥ = ⊥
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
map_top'✝ : { toFun := toFun✝, monotone' := monotone'✝ }.toFun ⊤ = ⊤
map_bot'✝ : { toFun := toFun✝, monotone' := monotone'✝ }.toFun ⊥ = ⊥
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, monotone' := monotone'✝¹, map_top' := map_top'✝¹, map_bot' := map_bot'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, monotone' := monotone'✝, map_top' := map_top'✝, map_bot' := map_bot'✝ }
⊢ { toFun := toFun✝¹, monotone' := monotone'✝¹, map_top' := map_top'✝¹, map_bot' := map_bot'✝¹ } =
    { toFun := toFun✝, monotone' := monotone'✝, map_top' := map_top'✝, map_bot' := map_bot'✝ }
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
g : SupHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
h : { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_sup' := map_sup'✝ } = g

Tactic:
;

Goal state after:
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
g : SupHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
h : { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_sup' := map_sup'✝ } = g
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
h : { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun = { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun
⊢ { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } = { toFun := toFun✝, map_sup' := map_sup'✝ }

Tactic:
;

Goal state after:
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
h : { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun = { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun
⊢ { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } = { toFun := toFun✝, map_sup' := map_sup'✝ }
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
f : SupHom β γ
g : SupHom α β
a b : α
⊢ f (g a) ⊔ f (g b) = (⇑f ∘ ⇑g) a ⊔ (⇑f ∘ ⇑g) b

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
f : SupHom β γ
g : SupHom α β
a b : α
⊢ f (g a) ⊔ f (g b) = (⇑f ∘ ⇑g) a ⊔ (⇑f ∘ ⇑g) b