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

Goal state before:
pp: case mpr
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ ↑s
h2 : (x1, x2).2 ∈ ↑t
h1' : (inl M N) x1 ∈ u
h2' : (inr M N) x2 ∈ u
⊢ (x1, x2) ∈ u

Tactic:
simpa using

Goal state after:
case mpr
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ ↑s
h2 : (x1, x2).2 ∈ ↑t
h1' : (inl M N) x1 ∈ u
h2' : (inr M N) x2 ∈ u
⊢ (x1, x2) ∈ u
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: case mpr
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u → s.prod t ≤ u

Tactic:
rintro ⟨hH, hK⟩ ⟨x1, x2⟩ ⟨h1, h2⟩
    have h1' : inl M N x1 ∈ u := by
      apply hH
      simpa using h1
    have h2' : inr M N x2 ∈ u := by
      apply hK
      simpa using h2
    simpa using Submonoid.mul_mem _ h1' h2'

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
g : N →* P
f : M →* N
⊢ map g (mrange f) = mrange (g.comp f)

Tactic:
simpa using

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
g : N →* P
f : M →* N
⊢ map g (map f ⊤) = map (g.comp f) ⊤
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
inst✝³ : MulOneClass M
N : Type u_5
S : Type u_6
inst✝² : MulOneClass N
f : M →* N
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
s : S
⊢ f.domRestrict s = 1 ↔ ∀ x ∈ s, f x = 1

Tactic:
simp [MonoidHom.ext_iff]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mrange (inl M N) = ⊤.prod ⊥

Tactic:
simpa using

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ map (inl M N) ⊤ = ⊤.prod ⊥
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mrange (inr M N) = ⊥.prod ⊤

Tactic:
simpa using

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ map (inr M N) ⊤ = ⊥.prod ⊤
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
S : Submonoid M
inst✝ : Subsingleton ↥S
y : M
hy : y ∈ S
⊢ y = 1

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝¹ : MulOneClass M
S : Submonoid M
inst✝ : Subsingleton ↥S
y : M
hy : y ∈ S
⊢ y = 1
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
h : S ≤ MonoidHom.mrange f
⊢ map f (comap f S) = S

Tactic:
simpa using

Goal state after:
M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
h : S ≤ MonoidHom.mrange f
⊢ map f (comap f S) = S
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case bit
b : Bool
n : ℕ
⊢ (bit b n).bodd.toNat + 2 * (bit b n).div2 = bit b n

Tactic:
simpa using

Goal state after:
case bit
b : Bool
n : ℕ
⊢ b.toNat + n * 2 = bit b n
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: n a b : ℕ
H : unpair n = (a, b)
⊢ pair a b = n

Tactic:
simpa using

Goal state after:
n a b : ℕ
H : unpair n = (a, b)
⊢ pair a b = n
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
⊢ (n + 2).bodd = (1 &&& n + 2 != 0)

Tactic:
simpa using

Goal state after:
n : ℕ
⊢ n.bodd = (n % 2 == 1)
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: a b : ℕ
⊢ a ≤ pair a b

Tactic:
simpa using

Goal state after:
a b : ℕ
⊢ a ≤ pair a b
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case pos
a b : ℕ
h : a < b
⊢ b ≤ pair a b

Tactic:
simpa using

Goal state after:
case pos
a b : ℕ
h : a < b
⊢ b ≤ b * b + a
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: n : ℕ
⊢ (unpair n).2 ≤ n

Tactic:
simpa using

Goal state after:
n : ℕ
⊢ (unpair n).2 ≤ n
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: motive : ℕ → Sort u
H₁ H₂ : (b : Bool) → (n : ℕ) → motive (bit b n)
h : (fun H n ↦ bitCasesOn n H) H₁ = (fun H n ↦ bitCasesOn n H) H₂
b : Bool
n : ℕ
⊢ H₁ b n = H₂ b n

Tactic:
simpa using

Goal state after:
motive : ℕ → Sort u
H₁ H₂ : (b : Bool) → (n : ℕ) → motive (bit b n)
h : (fun H n ↦ bitCasesOn n H) H₁ = (fun H n ↦ bitCasesOn n H) H₂
b : Bool
n : ℕ
⊢ H₁ b n = H₂ b n
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : a < b₁
⊢ pair a b₁ < pair a b₂

Tactic:
simpa using

Goal state after:
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : a < b₁
⊢ b₁ * b₁ < b₂ * b₂
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: a : ℤ
⊢ AddSubgroup.zmultiples ↑a.natAbs = AddSubgroup.zmultiples a

Tactic:
by
  simp [le_antisymm_iff, Int.mem_zmultiples_iff, Int.dvd_natAbs, Int.natAbs_dvd]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ s
h : G
hh : h ∈ H
k : G
hk : h * k * h⁻¹ ∈ s
⊢ k ∈ s

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ s
h : G
hh : h ∈ H
k : G
hk : h * k * h⁻¹ ∈ s
⊢ k ∈ s
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K
h : G
hh : h ∈ H
k : G
hk : h * k * h⁻¹ ∈ ↑K
⊢ k ∈ ↑K

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K
h : G
hh : h ∈ H
k : G
hk : h * k * h⁻¹ ∈ ↑K
⊢ k ∈ K
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_5
inst✝ : Group G
s t : Set G
⊢ ⋃ a ∈ s ∪ t, conjugatesOf a = (⋃ a ∈ s, conjugatesOf a) ∪ ⋃ a ∈ t, conjugatesOf a

Tactic:
Set.biUnion_union

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
h : a ∈ H.normalCore
⊢ a ∈ H

Tactic:
← mul_one a,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
h : a ∈ H.normalCore
⊢ a * 1 ∈ H
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Set β
a : α
⊢ Disjoint (a • s) t ↔ Disjoint s (a⁻¹ • t)

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Set β
a : α
⊢ Disjoint (a • s) t ↔ Disjoint s (a⁻¹ • t)
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Set β
a : α
⊢ Disjoint s (a • t) ↔ Disjoint (a⁻¹ • s) t

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Set β
a : α
⊢ Disjoint s (a • t) ↔ Disjoint (a⁻¹ • s) t
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
h : ∀ ⦃i j : α⦄, ((j⁻¹ * i) • s ∩ s).Nonempty → i = j
a : α
⊢ (a • s ∩ s).Nonempty → a = 1

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
h : ∀ ⦃i j : α⦄, ((j⁻¹ * i) • s ∩ s).Nonempty → i = j
a : α
⊢ (a • s ∩ s).Nonempty → a = 1
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
h : ∀ (a : α), (a • s ∩ s).Nonempty → a = 1
i j : α
ne : ((j⁻¹ * i) • s ∩ s).Nonempty
⊢ i = j

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
h : ∀ (a : α), (a • s ∩ s).Nonempty → a = 1
i j : α
ne : ((j⁻¹ * i) • s ∩ s).Nonempty
⊢ i = j
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ : List M
a✝ b✝ : M
l₁✝ l₂✝ : List M
hab : a✝ ≤ b✝
ih : Forall₂ (fun x1 x2 ↦ x1 ≤ x2) l₁✝ l₂✝
ih' : l₁✝.prod ≤ l₂✝.prod
⊢ (a✝ :: l₁✝).prod ≤ (b✝ :: l₂✝).prod

Tactic:
simpa using

Goal state after:
case cons
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ : List M
a✝ b✝ : M
l₁✝ l₂✝ : List M
hab : a✝ ≤ b✝
ih : Forall₂ (fun x1 x2 ↦ x1 ≤ x2) l₁✝ l₂✝
ih' : l₁✝.prod ≤ l₂✝.prod
⊢ a✝ * l₁✝.prod ≤ b✝ * l₂✝.prod
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l : List M
n : M
h : ∀ (x : M), x ∈ l → x ≤ n
⊢ l.prod ≤ n ^ l.length

Tactic:
simpa using

Goal state after:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l : List M
n : M
h : ∀ (x : M), x ∈ l → x ≤ n
⊢ l.prod ≤ n ^ l.length
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
N : Type u_5
inst✝³ : Group N
M : Type u_6
inst✝² : AddGroup M
I : AddSubgroup M
G : Type u_7
inst✝¹ : Group G
inst✝ : MulAction G M
a b : G
ha : a ∈ {σ | ∀ (x : M), σ • x - x ∈ I}
hb : b ∈ {σ | ∀ (x : M), σ • x - x ∈ I}
x : M
⊢ (a * b) • x - x ∈ I

Tactic:
simpa using

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
N : Type u_5
inst✝³ : Group N
M : Type u_6
inst✝² : AddGroup M
I : AddSubgroup M
G : Type u_7
inst✝¹ : Group G
inst✝ : MulAction G M
a b : G
ha : a ∈ {σ | ∀ (x : M), σ • x - x ∈ I}
hb : b ∈ {σ | ∀ (x : M), σ • x - x ∈ I}
x : M
⊢ a • b • x - x ∈ I
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
N : Type u_5
inst✝³ : Group N
M : Type u_6
inst✝² : AddGroup M
I : AddSubgroup M
G : Type u_7
inst✝¹ : Group G
inst✝ : MulAction G M
a : G
ha : a ∈ {σ | ∀ (x : M), σ • x - x ∈ I}
x : M
⊢ a⁻¹ • x - x ∈ I

Tactic:
simpa using

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
N : Type u_5
inst✝³ : Group N
M : Type u_6
inst✝² : AddGroup M
I : AddSubgroup M
G : Type u_7
inst✝¹ : Group G
inst✝ : MulAction G M
a : G
ha : a ∈ {σ | ∀ (x : M), σ • x - x ∈ I}
x : M
⊢ a⁻¹ • x - x ∈ I
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
this : x ∈ closure (⋃ i, ↑(S i)) → ∃ i, x ∈ S i
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
this : x ∈ closure (⋃ i, ↑(S i)) → ∃ i, x ∈ S i
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
hx : x ∈ closure (⋃ i, ↑(S i))
⊢ ∀ (x y : M),
    x ∈ closure (⋃ i, ↑(S i)) → y ∈ closure (⋃ i, ↑(S i)) → (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S i

Tactic:
rintro x y _ _ ⟨i, hi⟩ ⟨j, hj⟩

Goal state after:
M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x✝ : M
hx : x✝ ∈ closure (⋃ i, ↑(S i))
x y : M
hx✝ : x ∈ closure (⋃ i, ↑(S i))
hy✝ : y ∈ closure (⋃ i, ↑(S i))
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
⊢ ∃ i, x * y ∈ S i
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case nil
M : Type u_3
N : Type u_4
inst✝² : AddZeroClass M
inst✝¹ : Zero N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
⊢ f [].sum ≤ foldr max 0 (map f [])

Tactic:
simpa using

Goal state after:
case nil
M : Type u_3
N : Type u_4
inst✝² : AddZeroClass M
inst✝¹ : Zero N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
⊢ f 0 ≤ 0
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
b : M
h : ∀ (x : M), x ∈ [b] → 1 < x
x✝ : [b] ≠ []
⊢ 1 < [b].prod

Tactic:
simpa using

Goal state after:
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
b : M
h : ∀ (x : M), x ∈ [b] → 1 < x
x✝ : [b] ≠ []
⊢ 1 < 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₁ : ∀ (x : M), x ∈ head✝ :: tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ head✝ :: tail✝ → x ≤ head✝ * tail✝.prod

Tactic:
forall_mem_cons

Goal state after:
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
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: case inr.hx
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ ¬p ↑((Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯) x)

Tactic:
suffices ¬p x by simpa

Goal state after:
case inr.hx
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ ¬p ↑x
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: case inr.hx
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
hp : p ↑x
⊢ False

Tactic:
simpa using

Goal state after:
case inr.hx
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
hp : p ↑x
⊢ False
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: case inl.inr
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ Sum.elim Subtype.val Subtype.val (Sum.inl ⟨a, ha⟩) = Sum.elim Subtype.val Subtype.val (Sum.inr ⟨b, hb⟩) →
    Sum.inl ⟨a, ha⟩ = Sum.inr ⟨b, hb⟩

Tactic:
simpa using

Goal state after:
case inl.inr
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ ¬a = b
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
S : Submonoid M
inst✝ : Fintype ↥S
h : card ↥S ≤ 1
x : M
hx : x ∈ S
⊢ x = 1

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
S : Submonoid M
inst✝ : Fintype ↥S
h : card ↥S ≤ 1
x : M
hx : x ∈ S
⊢ x = 1
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: case inr.inl
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ t
b : α
hb : b ∈ s
⊢ Sum.elim Subtype.val Subtype.val (Sum.inr ⟨a, ha⟩) = Sum.elim Subtype.val Subtype.val (Sum.inl ⟨b, hb⟩) →
    Sum.inr ⟨a, ha⟩ = Sum.inl ⟨b, hb⟩

Tactic:
simpa using

Goal state after:
case inr.inl
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ t
b : α
hb : b ∈ s
⊢ ¬a = b
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case inr.inl
M : Type u_1
inst✝ : Monoid M
a✝ : M
ha : IsIdempotentElem a✝
⊢ a✝ * 1 ∈ {1, a✝}

pp: case inr.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ b✝ * b✝ ∈ {1, b✝}

Tactic:
· rw [mul_one]; exact .inr rfl

Goal state after:
case inr.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ b✝ * b✝ ∈ {1, b✝}
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
hd : α
tl : List α
m : α
⊢ m ∈ argmax f (hd :: tl) → m ∈ hd :: tl

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
hd : α
tl : List α
m : α
⊢ foldl (argAux fun b c ↦ f c < f b) (some hd) tl = some m → m = hd ∨ m ∈ tl
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
n : ℕ
b : α
h : decode n = some b
⊢ ofNat α n = b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Denumerable α
n : ℕ
b : α
h : decode n = some b
⊢ ofNat α n = b
Module: Mathlib.Data.Finset.Sum

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

Tactic:
simp [toRight]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
h : u ⊆ v
x✝ : α
⊢ x✝ ∈ u.toLeft → x✝ ∈ v.toLeft

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
h : u ⊆ v
x✝ : α
⊢ inl x✝ ∈ u → inl x✝ ∈ v
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
h : u ⊆ v
x✝ : β
⊢ x✝ ∈ u.toRight → x✝ ∈ v.toRight

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
h : u ⊆ v
x✝ : β
⊢ inr x✝ ∈ u → inr x✝ ∈ v
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✝ : β
x : α ⊕ β
u v : Finset (α ⊕ β)
a : α
b : β
f : α ⊕ β ↪ γ
⊢ Disjoint (map (Embedding.inl.trans f) s) (map (Embedding.inr.trans f) t)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a✝ : α
b✝ : β
x : α ⊕ β
u v : Finset (α ⊕ β)
a : α
b : β
f : α ⊕ β ↪ γ
⊢ Disjoint (map f (map Embedding.inl s)) (map f (map Embedding.inr t))
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Tactic:
by
    set t : List s :=
      ((List.range x).filter fun y => y ∈ s).pmap
        (fun (y : ℕ) (hy : y ∈ s) => ⟨y, hy⟩)
        (by intro a ha; simpa using! (List.mem_filter.mp ha).2) with ht
    have hmt : ∀ {y : s}, y ∈ t ↔ y < ⟨x, hx⟩ := by
      simp [List.mem_filter, Subtype.ext_iff, ht]
    cases hmax : List.maximum t with
    | bot =>
      refine ⟨0, le_antisymm bot_le (le_of_not_gt fun h => List.not_mem_nil (a := (⊥ : s)) ?_)⟩
      rwa [← List.maximum_eq_bot.1 hmax, hmt]
    | coe m =>
      have wf : ↑m < x := by simpa using! hmt.mp (List.maximum_mem hmax)
      rcases ofNat_surjective m with ⟨a, rfl⟩
      refine ⟨a + 1, le_antisymm (succ_le_of_lt wf) ?_⟩
      exact le_succ_of_forall_lt_le fun z hz => List.le_maximum_of_mem (hmt.2 hz) hmax

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h✝ : hd :: tl ≠ []
h : ¬tl = []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) tl.maximum

Tactic:
simp [IH h]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a y : α
l : List α
IH : (∀ (x : α), x ∈ l → x ≤ a) → foldr max ⊥ l ≤ a
h : ∀ (x : α), x ∈ y :: l → x ≤ a
⊢ foldr max ⊥ (y :: l) ≤ a

Tactic:
simpa using

Goal state after:
case cons
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a y : α
l : List α
IH : (∀ (x : α), x ∈ l → x ≤ a) → foldr max ⊥ l ≤ a
h : ∀ (x : α), x ∈ y :: l → x ≤ a
⊢ foldr max ⊥ l ≤ a
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
r₁ r₂ : List (List α)
this : foldl (fun r l ↦ r ++ [a :: l]) r₂.toArray.toList r₁ = (foldl (fun r l ↦ r.push (a :: l)) r₂.toArray r₁).toList
⊢ Array.foldl (fun r l ↦ r ++ [a :: l]) r₂ { toList := r₁ } =
    (Array.foldl (fun r l ↦ r.push (a :: l)) r₂.toArray r₁.toArray).toList

Tactic:
simpa using

Goal state after:
α : Type u
a : α
r₁ r₂ : List (List α)
this : foldl (fun r l ↦ r ++ [a :: l]) r₂.toArray.toList r₁ = (foldl (fun r l ↦ r.push (a :: l)) r₂.toArray r₁).toList
⊢ (map (fun x2 ↦ [a :: x2]) r₁).flatten = map (cons a) r₁
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
r₁✝ r₁ : List (List α)
l : List α
ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
r₂ : List (List α)
⊢ sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ map (cons a) (r₁ ++ [l])

Tactic:
by
    rw [map_append, map_singleton, ← append_assoc, ← ih, sublists'Aux, foldl_append, foldl]
    simp [sublists'Aux]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
a : α
hat : a ∈ t
hxa : x < a
hay : a < y
b : α
hb : b ∈ {y_1 ∈ t | y < y_1}
⊢ y < b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
a : α
hat : a ∈ t
hxa : x < a
hay : a < y
b : α
hb : b ∈ {y_1 ∈ t | y < y_1}
⊢ y < b
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 ∈ (a :: t).sublists' ↔ s <+ a :: t

Tactic:
simp only [sublists'_cons, mem_append, IH, mem_map]

Goal state after:
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
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
r : List (List α)
this : foldl (fun r l ↦ r ++ [l, a :: l]) #[].toList r = (foldl (fun r l ↦ (r.push l).push (a :: l)) #[] r).toList
⊢ foldl (fun r l ↦ r ++ [l, a :: l]) [] r = (Array.foldl (fun r l ↦ (r.push l).push (a :: l)) #[] r.toArray).toList

Tactic:
simpa using

Goal state after:
α : Type u
a : α
r : List (List α)
this : foldl (fun r l ↦ r ++ [l, a :: l]) #[].toList r = (foldl (fun r l ↦ (r.push l).push (a :: l)) #[] r).toList
⊢ (map (fun x2 ↦ [x2, a :: x2]) r).flatten = (foldl (fun r l ↦ (r.push l).push (a :: l)) #[] r).toList
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
s : Multiset α
powerset : s.powerset = {0}
⊢ s = 0

Tactic:
simpa using

Goal state after:
α : Type u_1
s : Multiset α
powerset : s.powerset = {0}
⊢ s = 0
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
s t : Multiset α
h : (s, t) ∈ l'.revzip
⊢ (s, t) = (s, (s, t).1 + (s, t).2 - s)

Tactic:
add_tsub_cancel_left

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
s t : Multiset α
h : (s, t) ∈ l'.revzip
⊢ (s, t) = (s, (s, t).2)
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
this : Forall₂ (fun p s ↦ p = (s, ↑l - s)) l'.revzip (List.map Prod.fst l'.revzip)
⊢ Forall₂ (fun a c ↦ a = (c, ↑l - c)) l'.revzip l'

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
this : Forall₂ (fun p s ↦ p = (s, ↑l - s)) l'.revzip (List.map Prod.fst l'.revzip)
⊢ Forall₂ (fun a c ↦ a = (c, ↑l - c)) l'.revzip l'