mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a : α
s : Set α
⊢ (op a • s)⁻¹ = a⁻¹ • s⁻¹

Tactic:
ext

Goal state after:
α : Type u_2
inst✝ : Group α
a : α
s : Set α
x✝ : α
⊢ x✝ ∈ (op a • s)⁻¹ ↔ x✝ ∈ a⁻¹ • s⁻¹
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
g : M →* N
f : α → M
⊢ g.comp (lift f) = lift (⇑g ∘ f)

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
g : M →* N
f : α → M
x✝ : α
⊢ (g.comp (lift f)) (of x✝) = (lift (⇑g ∘ f)) (of x✝)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : { g // f.ker ≤ g.ker }
⊢ (fun φ ↦ ⟨φ.comp f, ⋯⟩) ((fun g ↦ f.liftOfRightInverseAux f_inv hf ↑g ⋯) g) = g

Tactic:
ext

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : { g // f.ker ≤ g.ker }
x✝ : G₁
⊢ ↑((fun φ ↦ ⟨φ.comp f, ⋯⟩) ((fun g ↦ f.liftOfRightInverseAux f_inv hf ↑g ⋯) g)) x✝ = ↑g x✝
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ Function.Surjective ⇑(map f) ↔ Function.Surjective f

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
⊢ Function.Surjective ⇑(map f) → Function.Surjective f

case mpr
α : Type u_1
β : Type u_2
f : α → β
⊢ Function.Surjective f → Function.Surjective ⇑(map f)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
⊢ (iInf a).Normal

Tactic:
constructor

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
⊢ ∀ n ∈ iInf a, ∀ (g : G), g * n * g⁻¹ ∈ iInf a
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ (map f l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod ∧ (map g l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod

Tactic:
constructor

Goal state after:
case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ (map f l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod

case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ (map g l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ H₁ ⊓ H₂

Tactic:
constructor

Goal state after:
case left
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ ↑H₁.toSubmonoid

case right
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ ↑H₂.toSubmonoid
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ (map (fun i ↦ min (f i) (g i)) l).prod ≤ (map f l).prod ∧ (map (fun i ↦ min (f i) (g i)) l).prod ≤ (map g l).prod

Tactic:
constructor

Goal state after:
case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ (map (fun i ↦ min (f i) (g i)) l).prod ≤ (map f l).prod

case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ (map (fun i ↦ min (f i) (g i)) l).prod ≤ (map g l).prod
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex r s a b ↔ r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex r s a b → r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd

case mpr
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ (r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd) → Lex r s a b
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex (Function.swap r) s a b ↔ Lex r (fun i ↦ Function.swap (s i)) b a

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex (Function.swap r) s a b → Lex r (fun i ↦ Function.swap (s i)) b a

case mpr
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex r (fun i ↦ Function.swap (s i)) b a → Lex (Function.swap r) s a b
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ head✝ ≤ head✝ * tail✝.prod ∧ ∀ (x : M), x ∈ tail✝ → x ≤ head✝ * tail✝.prod

Tactic:
constructor

Goal state after:
case cons.left
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ head✝ ≤ head✝ * tail✝.prod

case cons.right
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ tail✝ → x ≤ head✝ * tail✝.prod
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ Lex r s a b ↔ r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd

Tactic:
constructor

Goal state after:
case mp
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ Lex r s a b → r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd

case mpr
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ (r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd) → Lex r s a b
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Type ?u.8
β : Type ?u.9
x✝ : (f : α ↪ β) × ↑(range ⇑f)ᶜ
f : α ↪ β
y : β
hy : y ∈ (range ⇑f)ᶜ
⊢ (fun f ↦ ⟨Embedding.some.trans f, ⟨f none, ⋯⟩⟩) ((fun f ↦ f.fst.optionElim ↑f.snd ⋯) ⟨f, ⟨y, hy⟩⟩) = ⟨f, ⟨y, hy⟩⟩

Tactic:
ext

Goal state after:
case a
α : Type ?u.8
β : Type ?u.9
x✝¹ : (f : α ↪ β) × ↑(range ⇑f)ᶜ
f : α ↪ β
y : β
hy : y ∈ (range ⇑f)ᶜ
x✝ : α
⊢ ((fun f ↦ ⟨Embedding.some.trans f, ⟨f none, ⋯⟩⟩) ((fun f ↦ f.fst.optionElim ↑f.snd ⋯) ⟨f, ⟨y, hy⟩⟩)).fst x✝ =
    ⟨f, ⟨y, hy⟩⟩.fst x✝

case a
α : Type ?u.8
β : Type ?u.9
x✝ : (f : α ↪ β) × ↑(range ⇑f)ᶜ
f : α ↪ β
y : β
hy : y ∈ (range ⇑f)ᶜ
⊢ ↑((fun f ↦ ⟨Embedding.some.trans f, ⟨f none, ⋯⟩⟩) ((fun f ↦ f.fst.optionElim ↑f.snd ⋯) ⟨f, ⟨y, hy⟩⟩)).snd =
    ↑⟨f, ⟨y, hy⟩⟩.snd
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
n : M
⊢ powers n = closure {n}

Tactic:
ext

Goal state after:
M : Type u_1
inst✝ : Monoid M
n x✝ : M
⊢ x✝ ∈ powers n ↔ x✝ ∈ closure {n}
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 : ℕ
x : ↥(powers x✝)
⊢ x ^ (Int.negSucc m).natMod ↑n = (x ^ (↑m.succ).natMod ↑n) ^ (n - 1)

Tactic:
ext

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 : ℕ
x : ↥(powers x✝)
⊢ ↑(x ^ (Int.negSucc m).natMod ↑n) = ↑((x ^ (↑m.succ).natMod ↑n) ^ (n - 1))
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x : M
⊢ ⇑Additive.ofMul '' ↑(Submonoid.powers x) = ↑(AddSubmonoid.multiples (Additive.ofMul x))

Tactic:
ext

Goal state after:
M : Type u_1
inst✝ : Monoid M
x : M
x✝ : Additive M
⊢ x✝ ∈ ⇑Additive.ofMul '' ↑(Submonoid.powers x) ↔ x✝ ∈ ↑(AddSubmonoid.multiples (Additive.ofMul x))
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: ⊢ AddSubmonoid.closure {1} = ⊤

Tactic:
ext

Goal state after:
x✝ : ℕ
⊢ x✝ ∈ AddSubmonoid.closure {1} ↔ x✝ ∈ ⊤
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ Disjoint (map Embedding.inl s) (map Embedding.inr t)

Tactic:
disjoint_left,

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ ∀ ⦃a : α ⊕ β⦄, a ∈ map Embedding.inl s → a ∉ map Embedding.inr t
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
u : Finset (α ⊕ β)
⊢ map Embedding.inl s ⊆ u ↔ s ⊆ u.toLeft

Tactic:
by
  simp [← disjSum_empty, disjSum_subset]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Union

Goal state before:
pp: α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
t : α → Finset β
⊢ s.sup t = s.biUnion t

Tactic:
ext

Goal state after:
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
t : α → Finset β
a✝ : β
⊢ a✝ ∈ s.sup t ↔ a✝ ∈ s.biUnion t
Module: Mathlib.Data.List.Zip

Goal state before:
pp: α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ (init, tail) ∈ ([], hd :: tl) :: (map (fun t ↦ hd :: t) tl.inits).zip tl.tails ↔ init ++ tail = hd :: tl

Tactic:
constructor

Goal state after:
case mp
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ (init, tail) ∈ ([], hd :: tl) :: (map (fun t ↦ hd :: t) tl.inits).zip tl.tails → init ++ tail = hd :: tl

case mpr
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ init ++ tail = hd :: tl → (init, tail) ∈ ([], hd :: tl) :: (map (fun t ↦ hd :: t) tl.inits).zip tl.tails
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsLeast (↑(insert a s)) (min a (s.min' H))

Tactic:
by
    rw [coe_insert]
    exact (isLeast_min' _ _).insert _

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
⊢ (s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) ↔ s <+ a :: t

Tactic:
constructor

Goal state after:
case cons.mp
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
⊢ (s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) → s <+ a :: t

case cons.mpr
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
⊢ s <+ a :: t → s <+ t ∨ ∃ a_2, a_2 <+ t ∧ a :: a_2 = s
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case nil
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
l₂ : List α
a✝ : l₂ <+ l
sl₁ : [] <+ l
⊢ Lex (Function.swap R) [] (a :: l₂)

Tactic:
constructor

Goal state after:
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case h
α : Type u_2
a✝ : List α
⊢ ↑(flatMap (fun a ↦ List.map ofList (sublistsLen a a✝)) (List.range ((↑a✝).card + 1))) =
    ↑(List.map ofList a✝.sublists')

Tactic:
← List.map_flatMap,

Goal state after:
case h
α : Type u_2
a✝ : List α
⊢ ↑(List.map ofList (flatMap (fun a ↦ sublistsLen a a✝) (List.range ((↑a✝).card + 1)))) =
    ↑(List.map ofList a✝.sublists')
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
⊢ (⋃ n, f n).Pairwise r ↔ ∀ (n : κ), (f n).Pairwise r

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
⊢ (⋃ n, f n).Pairwise r → ∀ (n : κ), (f n).Pairwise r

case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
⊢ (∀ (n : κ), (f n).Pairwise r) → (⋃ n, f n).Pairwise r
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
f : β → α
a : α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
h : (s✝.sup fun b ↦ f b \ a) = s✝.sup f \ a
⊢ ((cons a✝ s✝ h✝).sup fun b ↦ f b \ a) = (cons a✝ s✝ h✝).sup f \ a

Tactic:
rw [sup_cons, sup_cons, h, sup_sdiff]

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
r : α → α → Prop
h : ∀ a ∈ s, a.Pairwise r
x : α
S : Set α
hS : S ∈ s
hx : x ∈ S
y : α
T : Set α
⊢ T ∈ s → y ∈ T → x ≠ y → r x y

Tactic:
hT

Goal state after:
α : Type u_1
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
r : α → α → Prop
h : ∀ a ∈ s, a.Pairwise r
x : α
S : Set α
hS : S ∈ s
hx : x ∈ S
y : α
T : Set α
hT : T ∈ s
⊢ y ∈ T → x ≠ y → r x y
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ [] ::
      (flatMap (fun a ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)) ++
        flatMap (fun a ↦ map (cons h) (sublistsLen a tl)) (range (tl.length + 1))) ~
    tl.sublists' ++ map (cons h) tl.sublists'

Tactic:
← List.map_flatMap,

Goal state after:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ [] ::
      (flatMap (fun a ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)) ++
        map (cons h) (flatMap (fun a ↦ sublistsLen a tl) (range (tl.length + 1)))) ~
    tl.sublists' ++ map (cons h) tl.sublists'
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case inl
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ g c
d : ι'
hd : d ∈ s
hb : b ∈ g d
hcd : g c = g d
⊢ (Disjoint on f) a b

pp: case inr
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ g c
d : ι'
hd : d ∈ s
hb : b ∈ g d
hcd : g c ≠ g d
⊢ (Disjoint on f) a b

Tactic:
· exact hg d hd (hcd ▸ ha) hb hab

Goal state after:
case inr
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ g c
d : ι'
hd : d ∈ s
hb : b ∈ g d
hcd : g c ≠ g d
⊢ (Disjoint on f) a b
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ ↑s.powerset = SetLike.coe ⁻¹' 𝒫 ↑s

Tactic:
ext

Goal state after:
α : Type u_1
s x✝ : Finset α
⊢ x✝ ∈ ↑s.powerset ↔ x✝ ∈ SetLike.coe ⁻¹' 𝒫 ↑s
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
x : Finset α
⊢ (x ⊆ t ∧ #x = n) ∧ s ⊆ x ↔ ∃ a, (a ⊆ t \ s ∧ #a = n - #s) ∧ a ∪ s = x

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
x : Finset α
⊢ (x ⊆ t ∧ #x = n) ∧ s ⊆ x → ∃ a, (a ⊆ t \ s ∧ #a = n - #s) ∧ a ∪ s = x

case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
x : Finset α
⊢ (∃ a, (a ⊆ t \ s ∧ #a = n - #s) ∧ a ∪ s = x) → (x ⊆ t ∧ #x = n) ∧ s ⊆ x
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
⊢ powersetCard n s = {x ∈ s.powerset | #x = n}

Tactic:
ext

Goal state after:
α : Type u_1
n : ℕ
s a✝ : Finset α
⊢ a✝ ∈ powersetCard n s ↔ a✝ ∈ {x ∈ s.powerset | #x = n}
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset (Option α)
⊢ eraseNone s = s.biUnion Option.toFinset

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset (Option α)
a✝ : α
⊢ a✝ ∈ eraseNone s ↔ a✝ ∈ s.biUnion Option.toFinset
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ eraseNone (map Embedding.some s) = s

Tactic:
ext

Goal state after:
α : Type u_1
s : Finset α
a✝ : α
⊢ a✝ ∈ eraseNone (map Embedding.some s) ↔ a✝ ∈ s
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
⊢ eraseNone (s ∪ t) = eraseNone s ∪ eraseNone t

Tactic:
ext

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
a✝ : α
⊢ a✝ ∈ eraseNone (s ∪ t) ↔ a✝ ∈ eraseNone s ∪ eraseNone t
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
⊢ eraseNone (s ∩ t) = eraseNone s ∩ eraseNone t

Tactic:
ext

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
a✝ : α
⊢ a✝ ∈ eraseNone (s ∩ t) ↔ a✝ ∈ eraseNone s ∩ eraseNone t
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
⊢ eraseNone ∅ = ∅

Tactic:
ext

Goal state after:
α : Type u_1
a✝ : α
⊢ a✝ ∈ eraseNone ∅ ↔ a✝ ∈ ∅
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
⊢ eraseNone {none} = ∅

Tactic:
ext

Goal state after:
α : Type u_1
a✝ : α
⊢ a✝ ∈ eraseNone {none} ↔ a✝ ∈ ∅
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ powersetCard (#s) s = {s}

Tactic:
ext

Goal state after:
α : Type u_1
s a✝ : Finset α
⊢ a✝ ∈ powersetCard (#s) s ↔ a✝ ∈ {s}
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s a✝ : Finset α
⊢ a✝ ⊆ s ∧ #a✝ = #s ↔ a✝ = s

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
s a✝ : Finset α
⊢ a✝ ⊆ s ∧ #a✝ = #s → a✝ = s

case mpr
α : Type u_1
s a✝ : Finset α
⊢ a✝ = s → a✝ ⊆ s ∧ #a✝ = #s
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ eraseNone (insertNone s) = s

Tactic:
ext

Goal state after:
α : Type u_1
s : Finset α
a✝ : α
⊢ a✝ ∈ eraseNone (insertNone s) ↔ a✝ ∈ s
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ #t = n ↔ ∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ #t = n → ∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t

case mpr
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ (∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t) → t ⊆ map f s ∧ #t = n
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Nonempty ι
f : ι → α
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hf : BddAbove (range f)
⊢ Ici (⨆ i, f i) = ⋂ i, Ici (f i)

Tactic:
ext

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Nonempty ι
f : ι → α
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hf : BddAbove (range f)
x✝ : α
⊢ x✝ ∈ Ici (⨆ i, f i) ↔ x✝ ∈ ⋂ i, Ici (f i)
Module: Mathlib.Algebra.Group.Embedding

Goal state before:
pp: G : Type u_1
inst✝¹ : CommMagma G
inst✝ : IsCancelMul G
g : G
⊢ mulLeftEmbedding g = mulRightEmbedding g

Tactic:
ext

Goal state after:
G : Type u_1
inst✝¹ : CommMagma G
inst✝ : IsCancelMul G
g x✝ : G
⊢ (mulLeftEmbedding g) x✝ = (mulRightEmbedding g) x✝
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j ↦ Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i ↦ ⟨Exists.choose ⋯, ⋯⟩
i : ι
hi : i ∈ {i | (s i).Nonempty}
j : ι
hj : j ∈ {i | (s i).Nonempty}
hij : u ⟨i, hi⟩ = u ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Tactic:
ext

Goal state after:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j ↦ Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := ⋯
i : ι
hi : i ∈ {i | (s i).Nonempty}
j : ι
hj : j ∈ {i | (s i).Nonempty}
hij : u ⟨i, hi⟩ = u ⟨j, hj⟩
⊢ ↑⟨i, hi⟩ = ↑⟨j, hj⟩
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
⊢ x ∈ t ↔ ∃ i, x ∈ s ↑i ∩ t

Tactic:
constructor

Goal state after:
case mp
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
⊢ x ∈ t → ∃ i, x ∈ s ↑i ∩ t

case mpr
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
⊢ (∃ i, x ∈ s ↑i ∩ t) → x ∈ t
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ s, f i < a ↔ ∀ x ∈ s, f x < a

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ s, f i < a → ∀ x ∈ s, f x < a

case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ (∀ x ∈ s, f x < a) → ⨆ i ∈ s, f i < a
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ a < ⨅ i ∈ s, f i ↔ ∀ x ∈ s, a < f x

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ a < ⨅ i ∈ s, f i → ∀ x ∈ s, a < f x

case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ (∀ x ∈ s, a < f x) → a < ⨅ i ∈ s, f i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
hf : BddBelow (range f)
⊢ Iic (⨅ i, f i) = ⋂ i, Iic (f i)

Tactic:
ext

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
hf : BddBelow (range f)
x✝ : α
⊢ x✝ ∈ Iic (⨅ i, f i) ↔ x✝ ∈ ⋂ i, Iic (f i)