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

Goal state before:
pp: case refine_1
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst✝⁷ : Group G
inst✝⁶ : Group H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
f : F
inst✝³ : SetLike S G
inst✝² : OneMemClass S G
inst✝¹ : MulMemClass S G
inst✝ : InvMemClass S G
s : S
h : ∀ (a : G), a ∈ s → f a = 1 → a = 1
x : G
hx : x ∈ ↑s
y : G
hy : y ∈ ↑s
hxy : f x = f y
⊢ x ∈ s

pp: case refine_2
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst✝⁷ : Group G
inst✝⁶ : Group H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
f : F
inst✝³ : SetLike S G
inst✝² : OneMemClass S G
inst✝¹ : MulMemClass S G
inst✝ : InvMemClass S G
s : S
h : ∀ (a : G), a ∈ s → f a = 1 → a = 1
x : G
hx : x ∈ ↑s
y : G
hy : y ∈ ↑s
hxy : f x = f y
⊢ y ∈ s

pp: case refine_3
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst✝⁷ : Group G
inst✝⁶ : Group H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
f : F
inst✝³ : SetLike S G
inst✝² : OneMemClass S G
inst✝¹ : MulMemClass S G
inst✝ : InvMemClass S G
s : S
h : ∀ (a : G), a ∈ s → f a = 1 → a = 1
x : G
hx : x ∈ ↑s
y : G
hy : y ∈ ↑s
hxy : f x = f y
⊢ f (x * y⁻¹) = 1

Tactic:
<;>

Goal state after:
case refine_1
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst✝⁷ : Group G
inst✝⁶ : Group H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
f : F
inst✝³ : SetLike S G
inst✝² : OneMemClass S G
inst✝¹ : MulMemClass S G
inst✝ : InvMemClass S G
s : S
h : ∀ (a : G), a ∈ s → f a = 1 → a = 1
x : G
hx : x ∈ ↑s
y : G
hy : y ∈ ↑s
hxy : f x = f y
⊢ x ∈ s

case refine_2
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst✝⁷ : Group G
inst✝⁶ : Group H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
f : F
inst✝³ : SetLike S G
inst✝² : OneMemClass S G
inst✝¹ : MulMemClass S G
inst✝ : InvMemClass S G
s : S
h : ∀ (a : G), a ∈ s → f a = 1 → a = 1
x : G
hx : x ∈ ↑s
y : G
hy : y ∈ ↑s
hxy : f x = f y
⊢ y ∈ s

case refine_3
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst✝⁷ : Group G
inst✝⁶ : Group H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
f : F
inst✝³ : SetLike S G
inst✝² : OneMemClass S G
inst✝¹ : MulMemClass S G
inst✝ : InvMemClass S G
s : S
h : ∀ (a : G), a ∈ s → f a = 1 → a = 1
x : G
hx : x ∈ ↑s
y : G
hy : y ∈ ↑s
hxy : f x = f y
⊢ f (x * y⁻¹) = 1
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑e.symm) H = K → map (↑e) K = H

pp: case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑e) K = H → map (↑e.symm) H = K

Tactic:
<;>

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑e.symm) H = K → map (↑e) K = H

case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑e) K = H → map (↑e.symm) H = K
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ K : Subgroup G
⊢ H₁.subgroupOf K = H₂.subgroupOf K ↔ H₁ ⊓ K = H₂ ⊓ K

Tactic:
simpa only [SetLike.ext_iff, mem_inf, mem_subgroupOf, and_congr_left_iff] using Subtype.forall

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

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ x / y ∈ f.ker → f x = f y

pp: case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ f x = f y → x / y ∈ f.ker

Tactic:
<;>

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ x / y ∈ f.ker → f x = f y

case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ f x = f y → x / y ∈ f.ker
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ x / y ∈ f.ker

Tactic:
· rw [mem_ker, div_eq_mul_inv, map_mul, h, ← map_mul, mul_inv_cancel, map_one]

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

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ f x = f y → y⁻¹ * x ∈ f.ker

pp: case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ y⁻¹ * x ∈ f.ker → f x = f y

Tactic:
<;>

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ f x = f y → y⁻¹ * x ∈ f.ker

case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ y⁻¹ * x ∈ f.ker → f x = f y
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
p : Prop
K : p → Subgroup G
x : G
h : p
⊢ x ∈ ⨆ (h : p), K h ↔ x = 1 ∨ ∃ (h : p), x ∈ K h

pp: case neg
G : Type u_1
inst✝ : Group G
p : Prop
K : p → Subgroup G
x : G
h : ¬p
⊢ x ∈ ⨆ (h : p), K h ↔ x = 1 ∨ ∃ (h : p), x ∈ K h

Tactic:
<;>

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
p : Prop
K : p → Subgroup G
x : G
h : p
⊢ x ∈ ⨆ (h : p), K h ↔ x = 1 ∨ ∃ (h : p), x ∈ K h

case neg
G : Type u_1
inst✝ : Group G
p : Prop
K : p → Subgroup G
x : G
h : ¬p
⊢ x ∈ ⨆ (h : p), K h ↔ x = 1 ∨ ∃ (h : p), x ∈ K h
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
f : G →* N
g : N →* P
hg : Injective ⇑g
⊢ (g.comp f).ker = f.ker

Tactic:
rw [← comap_ker, g.ker_eq_bot hg, comap_bot]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup N
hH : H ≤ f.range
hK : K ≤ f.range
⊢ H ⊔ K = f.range ⊓ (H ⊔ K)

Tactic:
inf_eq_right.mpr (sup_le hH hK)

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup N
hH : H ≤ f.range
hK : K ≤ f.range
⊢ H ⊔ K = H ⊔ K
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
f : F
S : Submonoid N
⊢ 1 ∈ S

Tactic:
exact S.one_mem

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
⊢ mrange (id M) = ⊤

Tactic:
by
  simp [mrange_eq_map]

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

Goal state before:
pp: case inl
x : ℕ
⊢ natSumNatEquivNat (Sum.inl x) = Sum.elim (fun x ↦ 2 * x) (fun x ↦ 2 * x + 1) (Sum.inl x)

pp: case inr
x : ℕ
⊢ natSumNatEquivNat (Sum.inr x) = Sum.elim (fun x ↦ 2 * x) (fun x ↦ 2 * x + 1) (Sum.inr x)

Tactic:
<;>

Goal state after:
case inl
x : ℕ
⊢ natSumNatEquivNat (Sum.inl x) = Sum.elim (fun x ↦ 2 * x) (fun x ↦ 2 * x + 1) (Sum.inl x)

case inr
x : ℕ
⊢ natSumNatEquivNat (Sum.inr x) = Sum.elim (fun x ↦ 2 * x) (fun x ↦ 2 * x + 1) (Sum.inr x)
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case succ.false
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (false && n.bodd ^^ false) = (false && !n.bodd)

pp: case succ.true
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (true && n.bodd ^^ true) = (true && !n.bodd)

Tactic:
<;>

Goal state after:
case succ.false
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (false && n.bodd ^^ false) = (false && !n.bodd)

case succ.true
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (true && n.bodd ^^ true) = (true && !n.bodd)
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case succ
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (m.bodd && n.bodd ^^ m.bodd) = (m.bodd && !n.bodd)

Tactic:
cases bodd m <;> cases bodd n

Goal state after:
case succ.false.false
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (false && false ^^ false) = (false && !false)

case succ.false.true
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (false && true ^^ false) = (false && !true)

case succ.true.false
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (true && false ^^ true) = (true && !false)

case succ.true.true
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (true && true ^^ true) = (true && !true)
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case succ.false.false
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (false && false ^^ false) = (false && !false)

pp: case succ.false.true
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (false && true ^^ false) = (false && !true)

pp: case succ.true.false
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (true && false ^^ true) = (true && !false)

pp: case succ.true.true
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (true && true ^^ true) = (true && !true)

Tactic:
<;>

Goal state after:
case succ.false.false
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (false && false ^^ false) = (false && !false)

case succ.false.true
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (false && true ^^ false) = (false && !true)

case succ.true.false
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (true && false ^^ true) = (true && !false)

case succ.true.true
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (true && true ^^ true) = (true && !true)
Module: Mathlib.Data.Nat.Bits

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

pp: case true
n : ℕ
⊢ (bit true n).bodd = true

Tactic:
<;>

Goal state after:
case false
n : ℕ
⊢ (bit false n).bodd = false

case true
n : ℕ
⊢ (bit true n).bodd = true
Module: Mathlib.Data.Nat.Bits

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

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

Tactic:
<;>

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

case bit.true
n : ℕ
⊢ bit true n % 2 = (bit true n).bodd.toNat
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case bit.false
n : ℕ
⊢ (bit false n + 1).div2 = bif (bit false n).bodd then (bit false n).div2.succ else (bit false n).div2

pp: case bit.true
n : ℕ
⊢ (bit true n + 1).div2 = bif (bit true n).bodd then (bit true n).div2.succ else (bit true n).div2

Tactic:
<;>

Goal state after:
case bit.false
n : ℕ
⊢ (bit false n + 1).div2 = bif (bit false n).bodd then (bit false n).div2.succ else (bit false n).div2

case bit.true
n : ℕ
⊢ (bit true n + 1).div2 = bif (bit true n).bodd then (bit true n).div2.succ else (bit true n).div2
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case pos
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : n - s * s < s
⊢ (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 < n

pp: case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : ¬n - s * s < s
⊢ (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 < n

Tactic:
<;>

Goal state after:
case pos
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : n - s * s < s
⊢ (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 < n

case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : ¬n - s * s < s
⊢ (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 < n
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case succ.false
n : ℕ
ih : n.boddDiv2 = (n.bodd, n.div2)
hn : n.bodd = false
⊢ (match (false, n.div2) with
    | (false, m) => (true, m)
    | (true, m) => (false, m.succ)) =
    ((n + 1).bodd, (n + 1).div2)

pp: case succ.true
n : ℕ
ih : n.boddDiv2 = (n.bodd, n.div2)
hn : n.bodd = true
⊢ (match (true, n.div2) with
    | (false, m) => (true, m)
    | (true, m) => (false, m.succ)) =
    ((n + 1).bodd, (n + 1).div2)

Tactic:
<;>

Goal state after:
case succ.false
n : ℕ
ih : n.boddDiv2 = (n.bodd, n.div2)
hn : n.bodd = false
⊢ (match (false, n.div2) with
    | (false, m) => (true, m)
    | (true, m) => (false, m.succ)) =
    ((n + 1).bodd, (n + 1).div2)

case succ.true
n : ℕ
ih : n.boddDiv2 = (n.bodd, n.div2)
hn : n.bodd = true
⊢ (match (true, n.div2) with
    | (false, m) => (true, m)
    | (true, m) => (false, m.succ)) =
    ((n + 1).bodd, (n + 1).div2)
Module: Mathlib.Data.Nat.Pairing

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

pp: case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ pair a₁ b < pair a₂ b

Tactic:
<;>

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

case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ pair a₁ b < pair a₂ b
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case false
n : ℕ
h : n ≠ 0
⊢ bit false n ≠ 0

pp: case true
n : ℕ
h : n ≠ 0
⊢ bit true n ≠ 0

Tactic:
<;>

Goal state after:
case false
n : ℕ
h : n ≠ 0
⊢ bit false n ≠ 0

case true
n : ℕ
h : n ≠ 0
⊢ bit true n ≠ 0
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case false
n : ℕ
h : n ≠ 0
⊢ ¬2 * n = 0

pp: case true
n : ℕ
h : n ≠ 0
⊢ ¬2 * n + 1 = 0

Tactic:
<;>

Goal state after:
case false
n : ℕ
h : n ≠ 0
⊢ ¬2 * n = 0

case true
n : ℕ
h : n ≠ 0
⊢ ¬2 * n + 1 = 0
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case false
m n : ℕ
b : Bool
h : m < n
⊢ bit false m < 2 * n

pp: case true
m n : ℕ
b : Bool
h : m < n
⊢ bit true m < 2 * n

Tactic:
<;>

Goal state after:
case false
m n : ℕ
b : Bool
h : m < n
⊢ bit false m < 2 * n

case true
m n : ℕ
b : Bool
h : m < n
⊢ bit true m < 2 * n
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case false
m n : ℕ
b : Bool
h : m < n
⊢ 2 * m < 2 * n

pp: case true
m n : ℕ
b : Bool
h : m < n
⊢ 2 * m + 1 < 2 * n

Tactic:
<;>

Goal state after:
case false
m n : ℕ
b : Bool
h : m < n
⊢ 2 * m < 2 * n

case true
m n : ℕ
b : Bool
h : m < n
⊢ 2 * m + 1 < 2 * n
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case false
m n : ℕ
a : Bool
h : m < n
⊢ 2 * n ≤ bit false n

pp: case true
m n : ℕ
a : Bool
h : m < n
⊢ 2 * n ≤ bit true n

Tactic:
<;>

Goal state after:
case false
m n : ℕ
a : Bool
h : m < n
⊢ 2 * n ≤ bit false n

case true
m n : ℕ
a : Bool
h : m < n
⊢ 2 * n ≤ bit true n
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case false
m n : ℕ
a : Bool
h : m < n
⊢ 2 * n ≤ 2 * n

pp: case true
m n : ℕ
a : Bool
h : m < n
⊢ 2 * n ≤ 2 * n + 1

Tactic:
<;>

Goal state after:
case false
m n : ℕ
a : Bool
h : m < n
⊢ 2 * n ≤ 2 * n

case true
m n : ℕ
a : Bool
h : m < n
⊢ 2 * n ≤ 2 * n + 1
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: case none
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Encodable α
⊢ (Nat.casesOn (Option.casesOn none zero fun a ↦ (encode a).succ) (some none) fun m ↦ Option.map some (decode m)) =
    some none

pp: case some
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Encodable α
val✝ : α
⊢ (Nat.casesOn (Option.casesOn (some val✝) zero fun a ↦ (encode a).succ) (some none) fun m ↦
      Option.map some (decode m)) =
    some (some val✝)

Tactic:
<;>

Goal state after:
case none
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Encodable α
⊢ (Nat.casesOn (Option.casesOn none zero fun a ↦ (encode a).succ) (some none) fun m ↦ Option.map some (decode m)) =
    some none

case some
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Encodable α
val✝ : α
⊢ (Nat.casesOn (Option.casesOn (some val✝) zero fun a ↦ (encode a).succ) (some none) fun m ↦
      Option.map some (decode m)) =
    some (some val✝)
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case pos
m n : ℕ
h✝ : m < n
⊢ n * n + m < max m n * max m n + (max m n + (max m n + 1))

pp: case neg
m n : ℕ
h✝ : ¬m < n
⊢ m * m + (m + n) < max m n * max m n + (max m n + (max m n + 1))

Tactic:
<;>

Goal state after:
case pos
m n : ℕ
h✝ : m < n
⊢ n * n + m < max m n * max m n + (max m n + (max m n + 1))

case neg
m n : ℕ
h✝ : ¬m < n
⊢ m * m + (m + n) < max m n * max m n + (max m n + (max m n + 1))
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case pos
m n : ℕ
h✝ : m < n
⊢ m < n + (n + 1)

pp: case neg
m n : ℕ
h✝ : ¬m < n
⊢ n < m + 1

Tactic:
<;>

Goal state after:
case pos
m n : ℕ
h✝ : m < n
⊢ m < n + (n + 1)

case neg
m n : ℕ
h✝ : ¬m < n
⊢ n < m + 1
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
val✝ : α
⊢ decodeSum (encodeSum (Sum.inl val✝)) = some (Sum.inl val✝)

pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
val✝ : β
⊢ decodeSum (encodeSum (Sum.inr val✝)) = some (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
val✝ : α
⊢ decodeSum (encodeSum (Sum.inl val✝)) = some (Sum.inl val✝)

case inr
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
val✝ : β
⊢ decodeSum (encodeSum (Sum.inr val✝)) = some (Sum.inr val✝)
Module: Mathlib.Logic.Encodable.Basic

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

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

Tactic:
<;>

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

case true
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = m.succ
⊢ (match true, n / 2 with
    | false, m => Option.map Sum.inl (decode m)
    | x, m => Option.map Sum.inr (decode m)) =
    none
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) (none.bind fun a ↦ Option.map (Sigma.mk a) (decode (unpair n).2)) =
    none.bind fun a ↦ Option.map (Prod.mk a) (decode (unpair n).2)

pp: case some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
val✝ : α
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) ((some val✝).bind fun a ↦ Option.map (Sigma.mk a) (decode (unpair n).2)) =
    (some val✝).bind fun a ↦ Option.map (Prod.mk a) (decode (unpair n).2)

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) (none.bind fun a ↦ Option.map (Sigma.mk a) (decode (unpair n).2)) =
    none.bind fun a ↦ Option.map (Prod.mk a) (decode (unpair n).2)

case some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
val✝ : α
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) ((some val✝).bind fun a ↦ Option.map (Sigma.mk a) (decode (unpair n).2)) =
    (some val✝).bind fun a ↦ Option.map (Prod.mk a) (decode (unpair n).2)
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: case none.none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) (none.bind fun a ↦ Option.map (Sigma.mk a) none) =
    none.bind fun a ↦ Option.map (Prod.mk a) none

pp: case none.some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
val✝ : β
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) (none.bind fun a ↦ Option.map (Sigma.mk a) (some val✝)) =
    none.bind fun a ↦ Option.map (Prod.mk a) (some val✝)

pp: case some.none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
val✝ : α
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) ((some val✝).bind fun a ↦ Option.map (Sigma.mk a) none) =
    (some val✝).bind fun a ↦ Option.map (Prod.mk a) none

pp: case some.some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
val✝¹ : α
val✝ : β
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) ((some val✝¹).bind fun a ↦ Option.map (Sigma.mk a) (some val✝)) =
    (some val✝¹).bind fun a ↦ Option.map (Prod.mk a) (some val✝)

Tactic:
<;>

Goal state after:
case none.none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) (none.bind fun a ↦ Option.map (Sigma.mk a) none) =
    none.bind fun a ↦ Option.map (Prod.mk a) none

case none.some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
val✝ : β
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) (none.bind fun a ↦ Option.map (Sigma.mk a) (some val✝)) =
    none.bind fun a ↦ Option.map (Prod.mk a) (some val✝)

case some.none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
val✝ : α
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) ((some val✝).bind fun a ↦ Option.map (Sigma.mk a) none) =
    (some val✝).bind fun a ↦ Option.map (Prod.mk a) none

case some.some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
val✝¹ : α
val✝ : β
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) ((some val✝¹).bind fun a ↦ Option.map (Sigma.mk a) (some val✝)) =
    (some val✝¹).bind fun a ↦ Option.map (Prod.mk a) (some val✝)
Module: Mathlib.Logic.Encodable.Basic

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

Tactic:
rintro ⟨l⟩; dsimp; rw [encodek]; exact congr_arg some ⟦l⟧.rep_spec

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ comap ϕ.symm.toMonoidHom H

Tactic:
exact characteristic_iff_le_comap.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

Goal state after:
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: S : Type u_3
inst✝ : Semigroup S
a b : S
hab : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ a * a * (b * b) = a * b

Tactic:
ha.eq,

Goal state after:
S : Type u_3
inst✝ : Semigroup S
a b : S
hab : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ a * (b * b) = a * b
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

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

Tactic:
ext; simp [mem_smul_set_iff_inv_smul_mem]

Goal state after:
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; simp [mem_smul_set_iff_inv_smul_mem]

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

Goal state before:
pp: case nil
α : Type u_1
⊢ toList [].prod = (List.map ⇑toList []).flatten

pp: case cons
α : Type u_1
head✝ : FreeMonoid α
tail✝ : List (FreeMonoid α)
tail_ih✝ : toList tail✝.prod = (List.map (⇑toList) tail✝).flatten
⊢ toList (head✝ :: tail✝).prod = (List.map (⇑toList) (head✝ :: tail✝)).flatten

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
⊢ toList [].prod = (List.map ⇑toList []).flatten

case cons
α : Type u_1
head✝ : FreeMonoid α
tail✝ : List (FreeMonoid α)
tail_ih✝ : toList tail✝.prod = (List.map (⇑toList) tail✝).flatten
⊢ toList (head✝ :: tail✝).prod = (List.map (⇑toList) (head✝ :: tail✝)).flatten
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

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

pp: case h₂
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ b • t ⊆ z • t⁻¹ * t

Tactic:
<;>

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ a • s ⊆ z • s⁻¹ * s

case h₂
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ b • t ⊆ z • t⁻¹ * t
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: case h₁
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ a ∈ z • s⁻¹

pp: case h₂
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ b ∈ z • t⁻¹

Tactic:
<;>

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ a ∈ z • s⁻¹

case h₂
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ b ∈ z • t⁻¹