mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: n : ℕ
⊢ pair
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt)
        else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).2 =
    n

Tactic:
;

Goal state after:
n : ℕ
⊢ pair
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt)
        else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).2 =
    n
Module: Mathlib.Data.Nat.Bits

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

Tactic:
;

Goal state after:
m n : ℕ
⊢ m * 2 ^ n.succ = 2 ^ (n + 1) * m
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : ¬n - n.sqrt * n.sqrt < n.sqrt
⊢ n ≤ s * s + s + s

Tactic:
;

Goal state after:
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : ¬n - n.sqrt * n.sqrt < n.sqrt
⊢ n ≤ s * s + s + s
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: a b : ℕ
⊢ unpair (if a < b then b * b + a else a * a + a + b) = (a, b)

Tactic:
;

Goal state after:
a b : ℕ
⊢ unpair (if a < b then b * b + a else a * a + a + b) = (a, b)
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝¹ x✝ : ℕ
⊢ 2 * (x✝¹ + x✝) + 1 = 2 * x✝¹ + (2 * x✝ + 1)

Tactic:
;

Goal state after:
x✝¹ x✝ : ℕ
⊢ 2 * (x✝¹ + x✝) + 1 = 2 * x✝¹ + (2 * x✝ + 1)
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝¹ x✝ : ℕ
⊢ 2 * (x✝¹ + x✝) = 2 * x✝¹ + 2 * x✝

Tactic:
;

Goal state after:
x✝¹ x✝ : ℕ
⊢ 2 * (x✝¹ + x✝) = 2 * x✝¹ + 2 * x✝
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝¹ x✝ : ℕ
⊢ 2 * (x✝¹ + x✝) + 1 = 2 * x✝¹ + 1 + 2 * x✝

Tactic:
;

Goal state after:
x✝¹ x✝ : ℕ
⊢ 2 * (x✝¹ + x✝) + 1 = 2 * x✝¹ + 1 + 2 * x✝
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_3
inst✝ : Encodable α
d x : α
⊢ (some x).getD d = x

Tactic:
;

Goal state after:
α : Type u_3
inst✝ : Encodable α
d x : α
⊢ (some x).getD d = x
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝¹ x✝ : ℕ
h : x✝¹ ≤ x✝
⊢ 2 * x✝¹ + 1 ≤ 2 * x✝ + 1

Tactic:
;

Goal state after:
x✝¹ x✝ : ℕ
h : x✝¹ ≤ x✝
⊢ 2 * x✝¹ + 1 ≤ 2 * x✝ + 1
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝¹ x✝ : ℕ
h : x✝¹ ≤ x✝
⊢ 2 * x✝¹ ≤ 2 * x✝

Tactic:
;

Goal state after:
x✝¹ x✝ : ℕ
h : x✝¹ ≤ x✝
⊢ 2 * x✝¹ ≤ 2 * x✝
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ < a₂

Tactic:
;

Goal state after:
case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ < a₂
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)

pp: case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : ¬a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)

Tactic:
;

Goal state after:
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)

case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : ¬a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : ¬a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)

pp: case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)

Tactic:
;

Goal state after:
case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : ¬a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)

case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x : ℕ
x✝ : (fun x ↦ x ∈ Set.range encode) x
n : α
hn : encode n = x
⊢ (some n).isSome = true

Tactic:
;

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x : ℕ
x✝ : (fun x ↦ x ∈ Set.range encode) x
n : α
hn : encode n = x
⊢ (some n).isSome = true
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
n : ↑(Set.range encode)
x : α
hx : encode x = ↑n
⊢ (decode₂ α ↑n).isSome = true

Tactic:
;

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
n : ↑(Set.range encode)
x : α
hx : encode x = ↑n
⊢ (decode₂ α ↑n).isSome = true
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
n : ↑(Set.range encode)
x : α
hx : encode x = ↑n
⊢ (some x).isSome = true

Tactic:
;

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
n : ↑(Set.range encode)
x : α
hx : encode x = ↑n
⊢ (some x).isSome = true
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x✝ : α
⊢ (decode₂ α (encode x✝)).get ⋯ = x✝

Tactic:
;

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x✝ : α
⊢ (decode₂ α (encode x✝)).get ⋯ = x✝
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = m.succ
⊢ (match n.bodd, n / 2 with
    | false, m => Option.map Sum.inl (decode m)
    | x, m => Option.map Sum.inr (decode m)) =
    none

Tactic:
;

Goal state after:
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = m.succ
⊢ (match n.bodd, n / 2 with
    | false, m => Option.map Sum.inl (decode m)
    | x, m => Option.map Sum.inr (decode m)) =
    none
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
g : G
a b : ℤ
⊢ (fun x ↦ g ^ x) a * (fun x ↦ g ^ x) b ∈ Set.range fun x ↦ g ^ x

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
g : G
a b : ℤ
⊢ (fun x ↦ g ^ x) a * (fun x ↦ g ^ x) b ∈ Set.range fun x ↦ g ^ x
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
g : G
a : ℤ
⊢ ((fun x ↦ g ^ x) a)⁻¹ ∈ Set.range fun x ↦ g ^ x

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
g : G
a : ℤ
⊢ ((fun x ↦ g ^ x) a)⁻¹ ∈ Set.range fun x ↦ g ^ x
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: case mk
α : Type u_1
P : α → Prop
encA : Encodable α
decP : DecidablePred P
val✝ : α
property✝ : P val✝
⊢ encode ⟨val✝, property✝⟩ = encode ↑⟨val✝, property✝⟩

Tactic:
;

Goal state after:
case mk
α : Type u_1
P : α → Prop
encA : Encodable α
decP : DecidablePred P
val✝ : α
property✝ : P val✝
⊢ encode ⟨val✝, property✝⟩ = encode ↑⟨val✝, property✝⟩
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: ⊢ Countable { n // 0 < n }

Tactic:
;

Goal state after:
⊢ Countable { n // 0 < n }
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
⊢ DecidableEq ↑(Set.range Encodable.encode)

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Encodable α
⊢ DecidableEq ↑(Set.range Encodable.encode)
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
⊢ Encodable ↑(Set.range Encodable.encode)

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Encodable α
⊢ Encodable ↑(Set.range Encodable.encode)
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: case mk
α : Type u_1
s : Setoid α
inst✝¹ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
inst✝ : Encodable α
a✝ : Quotient s
l : α
⊢ Quotient.mk'' <$> decode (encode (rep (Quot.mk (⇑s) l))) = some (Quot.mk (⇑s) l)

Tactic:
;

Goal state after:
case mk
α : Type u_1
s : Setoid α
inst✝¹ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
inst✝ : Encodable α
a✝ : Quotient s
l : α
⊢ Quotient.mk'' <$> decode (encode (rep (Quot.mk (⇑s) l))) = some (Quot.mk (⇑s) l)
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: case mk
α : Type u_1
s : Setoid α
inst✝¹ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
inst✝ : Encodable α
a✝ : Quotient s
l : α
⊢ Option.map Quotient.mk'' (decode (encode (rep (Quot.mk (⇑s) l)))) = some (Quot.mk (⇑s) l)

Tactic:
;

Goal state after:
case mk
α : Type u_1
s : Setoid α
inst✝¹ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
inst✝ : Encodable α
a✝ : Quotient s
l : α
⊢ Option.map Quotient.mk'' (decode (encode (rep (Quot.mk (⇑s) l)))) = some (Quot.mk (⇑s) l)
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: case mk
α : Type u_1
s : Setoid α
inst✝¹ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
inst✝ : Encodable α
a✝ : Quotient s
l : α
⊢ Option.map Quotient.mk'' (some (rep (Quot.mk (⇑s) l))) = some (Quot.mk (⇑s) l)

Tactic:
;

Goal state after:
case mk
α : Type u_1
s : Setoid α
inst✝¹ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
inst✝ : Encodable α
a✝ : Quotient s
l : α
⊢ Option.map Quotient.mk'' (some (rep (Quot.mk (⇑s) l))) = some (Quot.mk (⇑s) l)
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:
;

Goal state after:
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✝
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ∀ (a : Subgroup G), a < ⊤ → a < normalizer ↑a ↔ normalizer ↑a = a → a = ⊤

Tactic:
;

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ ∀ (a : Subgroup G), a < ⊤ → a < normalizer ↑a ↔ normalizer ↑a = a → a = ⊤
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
a b : α
s : Set α
⊢ (fun x ↦ a * x) '' s ∪ (fun x ↦ b * x) '' s = a • s ∪ b • s

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : Mul α
a b : α
s : Set α
⊢ (fun x ↦ a * x) '' s ∪ (fun x ↦ b * x) '' s = a • s ∪ b • s
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
s : Set α
a b : α
⊢ (fun x ↦ x * a) '' s ∪ (fun x ↦ x * b) '' s = s <• a ∪ s <• b

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : Mul α
s : Set α
a b : α
⊢ (fun x ↦ x * a) '' s ∪ (fun x ↦ x * b) '' s = s <• a ∪ s <• b
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
s : Set G
H : Subgroup G
a : G
⊢ 1 ∈ H

Tactic:
;

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
s : Set G
H : Subgroup G
a : G
⊢ 1 ∈ H
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
s : Set G
H : Subgroup G
a : G
h : a ∈ H.normalCore
b c : G
⊢ c * b * a * (c * b)⁻¹ ∈ H

Tactic:
;

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
s : Set G
H : Subgroup G
a : G
h : a ∈ H.normalCore
b c : G
⊢ c * b * a * (c * b)⁻¹ ∈ H
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
h : IsUnit 1
⊢ IsIdempotentElem 1

Tactic:
;

Goal state after:
M : Type u_1
inst✝ : Monoid M
h : IsUnit 1
⊢ IsIdempotentElem 1
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
A B : Set β
a : α
⊢ A ⊆ (fun x ↦ a⁻¹ • x) ⁻¹' B ↔ A ⊆ a • B

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
A B : Set β
a : α
⊢ A ⊆ (fun x ↦ a⁻¹ • x) ⁻¹' B ↔ A ⊆ a • B
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
A B : Set β
a : α
⊢ (fun x ↦ a⁻¹ • x) ⁻¹' B = a • B

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
A B : Set β
a : α
⊢ (fun x ↦ a⁻¹ • x) ⁻¹' B = a • B
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

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

Tactic:
;

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

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

Tactic:
;

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

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

Tactic:
← mul_smul,

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
⊢ (map f) 1 = 1

Tactic:
;

Goal state after:
case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
⊢ (map f) 1 = 1
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: case inr
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
calc
    a • s ∩ b • t ⊆ (z • s⁻¹) * s ∩ ((z • t⁻¹) * t) := by
      gcongr <;> apply smul_set_subset_mul <;> simpa
    _ = z • ((s⁻¹ * s) ∩ (t⁻¹ * t)) := by simp_rw [Set.smul_set_inter, smul_mul_assoc]

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✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : List α
ih : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpl : ∀ (a_1 : α), a_1 ∈ a :: s → p a_1
hpla : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f (a :: s).prod ≤ (map f (a :: s)).prod

Tactic:
prod_cons,

Goal state after:
case cons
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : List α
ih : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpl : ∀ (a_1 : α), a_1 ∈ a :: s → p a_1
hpla : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f (a * s.prod) ≤ (map f (a :: s)).prod
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : List α
ih : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpl : ∀ (a_1 : α), a_1 ∈ a :: s → p a_1
hpla : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f (a * s.prod) ≤ (f a :: map f s).prod

Tactic:
prod_cons,

Goal state after:
case cons
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : List α
ih : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpl : ∀ (a_1 : α), a_1 ∈ a :: s → p a_1
hpla : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f (a * s.prod) ≤ f a * (map f s).prod
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
⊢ normalClosure {⟨c * g * c⁻¹, hg'⟩} = ⊤

Tactic:
have hs : Function.Surjective (((MulAut.conj c).toMonoidHom.domRestrict N).codRestrict _ h) := by
    rintro ⟨x, hx⟩
    refine ⟨⟨c⁻¹ * x * c, ?_⟩, ?_⟩
    · have h := hn.conj_mem _ hx c⁻¹
      rwa [inv_inv] at h
    simp only [MonoidHom.codRestrict_apply, MulEquiv.coe_toMonoidHom, MulAut.conj_apply,
      MonoidHom.domRestrict_apply, Subtype.mk_eq_mk, ← mul_assoc, mul_inv_cancel, one_mul]
    rw [mul_assoc, mul_inv_cancel, mul_one]

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)
⊢ normalClosure {⟨c * g * c⁻¹, hg'⟩} = ⊤
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ f (a :: l).prod ≤ (map f (a :: l)).prod

Tactic:
prod_cons,

Goal state after:
case cons
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ f (a * l.prod) ≤ (map f (a :: l)).prod
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:
prod_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₁ : ∀ (x : M), x ∈ head✝ :: tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ head✝ :: tail✝ → x ≤ head✝ * tail✝.prod
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 : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ a ∈ ⨆ i, S i, ∀ b ∈ ⨆ i, S i, a * b = b * a

Tactic:
simp_rw [← SetLike.mem_coe, coe_iSup_of_directed dir, Set.mem_iUnion,
    SetLike.mem_coe, forall_exists_index]

Goal state after:
M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ (a : M) (x : ι), a ∈ S x → ∀ (b : M) (x : ι), b ∈ S x → a * b = b * a
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 :: tl).prod ≤ (map f (hd :: tl)).sum

Tactic:
prod_cons,

Goal state after:
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 * tl.prod) ≤ (map f (hd :: tl)).sum
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:
;

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : Std.Trichotomous r
p : α → Prop
x y : Subtype p
⊢ ¬Subrel r p x y → ¬Subrel r p y x → ↑x = ↑y

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : Std.Trichotomous r
p : α → Prop
x y : Subtype p
⊢ ¬Subrel r p x y → ¬Subrel r p y x → ↑x = ↑y
Module: Mathlib.Order.RelIso.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
t : Set β
⊢ ⇑e ⁻¹' t = ⇑e.symm.symm ⁻¹' t

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
t : Set β
⊢ ⇑e ⁻¹' t = ⇑e.symm.symm ⁻¹' t
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x y : M
⊢ (∃ x_1, ((powersHom M) x) x_1 = y) ↔ ∃ n, x ^ n = y

Tactic:
;

Goal state after:
M : Type u_1
inst✝ : Monoid M
x y : M
⊢ (∃ x_1, ((powersHom M) x) x_1 = y) ↔ ∃ n, x ^ n = y
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Fintype ↥⊥
⊢ card ↥⊥ = 1

Tactic:
;

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Fintype ↥⊥
⊢ card ↥⊥ = 1
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 : ℕ
⊢ n✝ ^ i = n ↔ ((powersHom M) n✝) i = n

Tactic:
;

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.Algebra.Group.Submonoid.Membership

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

Tactic:
;

Goal state after:
case inl.inl
M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
⊢ 1 ∈ {1, a}
Module: Mathlib.Algebra.Group.Submonoid.Membership

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

Tactic:
;

Goal state after:
case inl.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ b✝ ∈ {1, 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, a✝}

Tactic:
;

Goal state after:
case inr.inl
M : Type u_1
inst✝ : Monoid M
a✝ : M
ha : IsIdempotentElem a✝
⊢ a✝ ∈ {1, a✝}
Module: Mathlib.Algebra.Group.Submonoid.Membership

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

Tactic:
;

Goal state after:
case inr.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ b✝ ∈ {1, b✝}