mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝² : Group G
N : Type u_5
inst✝¹ : Group N
P : Type u_8
inst✝ : MulOneClass P
g : N →* P
iso : G ≃* N
⊢ (g.comp ↑iso).ker = map (↑iso.symm) g.ker

Tactic:
rw [← comap_ker, comap_equiv_eq_map_symm]

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

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑s
⊢ y * 1 = y

Tactic:
simp

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

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑t
⊢ 1 * y = y

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x✝ : G
hx✝ : x✝ ∈ closure (↑s ∪ ↑t)
x : G
hx : x ∈ ↑s
⊢ x * 1 = x

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x✝ : G
hx✝ : x✝ ∈ closure (↑s ∪ ↑t)
x : G
hx : x ∈ ↑t
⊢ 1 * x = x

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ closure (↑s ∪ ↑t)
⊢ 1 * 1 = 1

Tactic:
simp

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

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
H✝ : Subgroup G
f : G →* N
H : Subgroup G
⊢ ∀ {a b : Subgroup ↥H},
    { toFun := fun H' ↦ ⟨map H.subtype H', ⋯⟩, invFun := fun sH' ↦ (↑sH').subgroupOf H, left_inv := ⋯, right_inv := ⋯ }
          a ≤
        { toFun := fun H' ↦ ⟨map H.subtype H', ⋯⟩, invFun := fun sH' ↦ (↑sH').subgroupOf H, left_inv := ⋯,
            right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure (⇑(closure s).subtype ⁻¹' s) = ⊤

Tactic:
simp

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

Goal state before:
pp: M : Type u_5
N : Type u_6
inst✝¹ : CommGroup M
inst✝ : CommGroup N
e : M ≃* N
n : ℕ
x✝ : M
⊢ ((↑e).comp (powMonoidHom n)) x✝ = ((powMonoidHom n).comp ↑e) x✝

Tactic:
simp

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

Goal state before:
pp: P : Type u_3
inst✝ : MulOneClass P
S : Submonoid P
⊢ ∀ (x : P), x ∈ comap (MonoidHom.id P) S ↔ x ∈ S

Tactic:
simp

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

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Set M
⊢ map (inr M N) ⊥ ≤ closure (s ×ˢ {1})

Tactic:
simp

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

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
t : Set N
⊢ map (inl M N) ⊥ ≤ closure ({1} ×ˢ t)

Tactic:
simp

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
S✝ : Submonoid M
F : Type u_4
inst✝³ : FunLike F M N
mc : MonoidHomClass F M N
S : Type u_5
inst✝² : SetLike S M
inst✝¹ : SubmonoidClass S M
M' : S
A : Type u_6
inst✝ : CommMonoid A
x✝ : ↥M'
⊢ (domRestrict 1 M') x✝ = 1 x✝

Tactic:
simp

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
S✝ : Submonoid M
F : Type u_4
inst✝³ : FunLike F M N
mc : MonoidHomClass F M N
S : Type u_5
inst✝² : SetLike S M
inst✝¹ : SubmonoidClass S M
M' : S
A : Type u_6
inst✝ : CommMonoid A
x✝² x✝¹ : M →* A
x✝ : ↥M'
⊢ ((x✝² * x✝¹).domRestrict M') x✝ = (x✝².domRestrict M' * x✝¹.domRestrict M') x✝

Tactic:
simp

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
f : M →* N
x : M
⊢ ⟨f x, ⋯⟩ = ⟨1, ⋯⟩ ↔ f x = 1

Tactic:
simp

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
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
hf : Surjective ⇑f
H K : Submonoid M
h : Codisjoint H K
⊢ Codisjoint (map f H) (map f K)

Tactic:
by
  rw [codisjoint_iff, ← map_sup, codisjoint_iff.mp h, ← MonoidHom.mrange_eq_map,
    mrange_eq_top_of_surjective _ hf]

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

Goal state before:
pp: α : Type u_1
x✝ : Bool × ℕ
b : Bool
n : ℕ
⊢ (fun n ↦ (n.bodd, n.div2)) (uncurry bit (b, n)) = (b, n)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
n : ℕ
⊢ uncurry bit ((fun n ↦ (n.bodd, n.div2)) n) = n

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m : ℕ
⊢ (m + 0).bodd = (m.bodd ^^ bodd 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case zero
m : ℕ
⊢ (m * 0).bodd = (m.bodd && bodd 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case bit.false
n : ℕ
⊢ bit false n % 2 = (bit false n).bodd.toNat

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case bit.true
n : ℕ
⊢ bit true n % 2 = (bit true n).bodd.toNat

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m n : ℕ
⊢ m * 2 ^ n.succ = 2 ^ (n + 1) * m

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: ⊢ (if 0 - sqrt 0 * sqrt 0 < sqrt 0 then (0 - sqrt 0 * sqrt 0, sqrt 0) else (sqrt 0, 0 - sqrt 0 * sqrt 0 - sqrt 0)) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: ⊢ (unpair 0).1 ≤ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : PUnit.{?u.4 + 1}
⊢ (Nat.casesOn 0 (some PUnit.unit) fun x ↦ none) = some x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case zero
⊢ bodd 0 = (bits 0).headI

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case zero
⊢ (div2 0).bits = (bits 0).tail

Tactic:
simp

Goal state after:
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 ∈ ⊥, ∀ (g : G), g * n * g⁻¹ ∈ ⊥

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
y : G
hy : y ∈ normalizer ↑H
hx : f y ∈ map f (normalizer ↑H)
x✝ : G
⊢ ((↑(MulAut.conj (f y))).comp f) x✝ = (f.comp ↑(MulAut.conj y)) x✝

Tactic:
simp

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

Goal state before:
pp: case refine_2
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
s : Set G
n : G
h : n ∈ normalClosure s
g : G
⊢ g * 1 * g⁻¹ ∈ normalClosure s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
x b : α
hb : b ∈ s
h : x • b ∈ x • s
ha : x • b ∈ t
⊢ x • b * b⁻¹ = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
a b : α
ha : a ∈ t
hb : b ∈ s
⊢ (a * b⁻¹) • b = a

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
b : α
hb : b ∈ s
h : x • b ∈ x • s
ha : x • b ∈ t
⊢ b⁻¹ * x • b = unop x

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G ≃* N
x : N
a✝ : G
⊢ (a✝ ∈ H ↔ f.symm x * a✝ * (f.symm x)⁻¹ ∈ H) ↔ (f.symm (f.toEquiv a✝) ∈ H ↔ f.symm (x * f.toEquiv a✝ * x⁻¹) ∈ H)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: α : Type u_1
xs : List (List α)
⊢ toList (ofList xs.flatten) = toList (List.map (⇑ofList) xs).prod

Tactic:
simp

Goal state after:
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
x✝ : α
⊢ (g.comp (lift f)) (of x✝) = (lift (⇑g ∘ f)) (of x✝)

Tactic:
simp

Goal state after:
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₃
⊢ (fun g ↦ f.liftOfRightInverseAux f_inv hf ↑g ⋯) ((fun φ ↦ ⟨φ.comp f, ⋯⟩) φ) = φ

Tactic:
ext b

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₃
b : G₂
⊢ ((fun g ↦ f.liftOfRightInverseAux f_inv hf ↑g ⋯) ((fun φ ↦ ⟨φ.comp f, ⋯⟩) φ)) b = φ b
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: 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₁ →* G₃
hg : f.ker ≤ g.ker
h : G₂ →* G₃
hh : h.comp f = g
⊢ h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩

Tactic:
simp_rw [← hh]
  exact ((f.liftOfRightInverse f_inv hf).apply_symm_apply _).symm

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B' B : Subgroup G
hN : (B'.subgroupOf B).Normal
⊢ ((A ⊓ B').subgroupOf (A ⊓ B)).Normal

Tactic:
rw [normal_subgroupOf_iff_le_normalizer_inf] at hN ⊢

Goal state after:
G : Type u_1
inst✝ : Group G
A B' B : Subgroup G
hN : B ≤ normalizer ↑(B' ⊓ B)
⊢ A ⊓ B ≤ normalizer ↑(A ⊓ B' ⊓ (A ⊓ B))
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A' A B : Subgroup G
hN : (A'.subgroupOf A).Normal
⊢ ((A' ⊓ B).subgroupOf (A ⊓ B)).Normal

Tactic:
rw [normal_subgroupOf_iff_le_normalizer_inf] at hN ⊢

Goal state after:
G : Type u_1
inst✝ : Group G
A' A B : Subgroup G
hN : A ≤ normalizer ↑(A' ⊓ A)
⊢ A ⊓ B ≤ normalizer ↑(A' ⊓ B ⊓ (A ⊓ B))
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons.inl
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
x : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
⊢ x ≤ (x :: ys).prod

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
l : List α
⊢ ∀ (a b : α), True → True → True

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
l : List α
⊢ ∀ (a : α), a ∈ l → True

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h)
⊢ {⟨g, hg⟩} ⊆
    ↑(comap (((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h)
        (normalClosure {⟨c * g * c⁻¹, hg'⟩}))

Tactic:
rw [Set.singleton_subset_iff, SetLike.mem_coe]

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h)
⊢ ⟨g, hg⟩ ∈
    comap (((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h) (normalClosure {⟨c * g * c⁻¹, hg'⟩})
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 ∈ ⋃ i, ↑(S i), ∃ i, x ∈ S i

Tactic:
simp

Goal state after:
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))
⊢ ∃ i, 1 ∈ S i

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
l : List α
hs_nonempty : l ≠ ∅
⊢ ∀ (a b : α), True → True → True

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
l : List α
hs_nonempty : l ≠ ∅
⊢ ∀ (a : α), a ∈ l → True

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : Nonempty (Subtype p)
S : ι → Submonoid M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ (∃ i, x ∈ S ↑i) ↔ ∃ i, p i ∧ x ∈ S i

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case nil
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
hl₁ : ∀ (x : M), x ∈ [] → 1 ≤ x
⊢ ∀ (x : M), x ∈ [] → x ≤ [].prod

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Sort u_1
β : Type u_2
p : β → Prop
e : α ≃ Subtype p
x : β
hs : x ∈ ofPred p
⊢ e.asEmbedding (e.symm ⟨x, hs⟩) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: case none
α : Type ?u.8
β : Type ?u.9
f : Option α ↪ β
⊢ ((fun f ↦ f.fst.optionElim ↑f.snd ⋯) ((fun f ↦ ⟨Embedding.some.trans f, ⟨f none, ⋯⟩⟩) f)) none = f none

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: case some
α : Type ?u.8
β : Type ?u.9
f : Option α ↪ β
val✝ : α
⊢ ((fun f ↦ f.fst.optionElim ↑f.snd ⋯) ((fun f ↦ ⟨Embedding.some.trans f, ⟨f none, ⋯⟩⟩) f)) (some val✝) = f (some val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: 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✝

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: 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

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
ha : (a₁, b₁).1 < (a₂, b₂).1
⊢ toLex (a₁, b₁) < toLex (a₂, b₂)

Tactic:
· exact left _ _ ha

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : AddMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
l : List α
f : α → β
h_one : f 1 ≤ 0
h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b
hd : α
tl : List α
IH : f tl.prod ≤ (map f tl).sum
⊢ f hd + (map f tl).sum ≤ (map f (hd :: tl)).sum

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Embedding.Set

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelIso.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
⊢ Set.range ⇑e = Set.univ

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelIso.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
p : α → Prop
h : ∀ (x : α), p x
⊢ ∀ {a b : Subtype p}, r ((Equiv.subtypeUnivEquiv h) a) ((Equiv.subtypeUnivEquiv h) b) ↔ Subrel r p a b

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Embedding.Set

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

Tactic:
simp

Goal state after:
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 n✝ n : M
i : ℕ
⊢ (fun x ↦ n✝ ^ x) i = n ↔ ((powersHom M) n✝) i = n

Tactic:
simp

Goal state after:
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a n✝ n : M
i : ℕ
⊢ n✝ ^ i = n ↔ ((powersHom M) n✝) i = n
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
⊢ foldl (argAux r) o [] = none ↔ [] = [] ∧ o = none

Tactic:
simp

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

Goal state before:
pp: case none
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd : α
⊢ (none = none ↔ tl = [] ∧ o = none) →
    (Option.rec (some hd) (fun val ↦ if r hd val then some hd else some val) none = none ↔
      (tl = [] ∧ [hd] = []) ∧ o = none)

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd val✝ : α
h✝ : r hd val✝
⊢ (False ↔ tl = [] ∧ o = none) → (False ↔ (tl = [] ∧ False) ∧ o = none)

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd val✝ : α
h✝ : ¬r hd val✝
⊢ (False ↔ tl = [] ∧ o = none) → (False ↔ (tl = [] ∧ False) ∧ o = none)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Order.Lemmas

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

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
⊢ ∀ {a m : α} {o : Option α}, a ∈ [] → m ∈ foldl (argAux r) o [] → ¬r a m

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : AddMonoid A
x n : A
i : ℕ
⊢ (fun i ↦ i • x) i = n ↔ ((multiplesHom A) x) i = n

Tactic:
simp

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

Goal state before:
pp: case append_singleton
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ Option.casesOn (foldl (argAux r) o tl) (some a) fun c ↦ if r a c then some a else some c
⊢ ¬r b m

Tactic:
rcases hf : foldl (argAux r) o tl with - | c

Goal state after:
case append_singleton.none
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ Option.casesOn (foldl (argAux r) o tl) (some a) fun c ↦ if r a c then some a else some c
hf : foldl (argAux r) o tl = none
⊢ ¬r b m

case append_singleton.some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ Option.casesOn (foldl (argAux r) o tl) (some a) fun c ↦ if r a c then some a else some c
c : α
hf : foldl (argAux r) o tl = some c
⊢ ¬r b m
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case append_singleton.none
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ Option.casesOn (foldl (argAux r) o tl) (some a) fun c ↦ if r a c then some a else some c
hf : foldl (argAux r) o tl = none
⊢ ¬r b m

Tactic:
hf

Goal state after:
case append_singleton.none
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ Option.casesOn none (some a) fun c ↦ if r a c then some a else some c
hf : foldl (argAux r) o tl = none
⊢ ¬r b m
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
m : α
⊢ m ∈ argmax f [] → m ∈ []

Tactic:
simp

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

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c ↦ if f a < f c then some c else some a
h : argmax f hd = none
⊢ (Option.casesOn (Option.casesOn none (some a) fun c ↦ if f a < f c then some c else some a) (some tl) fun c ↦
      if f c < f tl then some tl else some c) =
    Option.casesOn (Option.casesOn none (some tl) fun c ↦ if f c < f tl then some tl else some c) (some a) fun c ↦
      if f a < f c then some c else some a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
m : α
x✝³ : m ∈ argmax f []
x✝² : α
x✝¹ : x✝² ∈ []
x✝ : f m ≤ f x✝²
⊢ idxOf m [] ≤ idxOf x✝² []

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ Option.map (⇑e.symm) (decode n) = some (e.symm (ofNat α n))

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Multiset α
a : α
⊢ sup 0 ≤ a ↔ ∀ (b : α), b ∈ 0 → b ≤ a

Tactic:
simp

Goal state after:
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:
simp

Goal state after:
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:
simp

Goal state after: