mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ ⁅z, ⁅x, y⁆⁆ = x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹

pp: G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹ = 1

Tactic:
· simp [commutatorElement_def, mul_assoc]

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹ = 1
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅⊤, H⁆ = ⊥ ↔ H ≤ center G

Tactic:
by
  rw [commutator_comm, commutator_top_right_eq_bot_iff_le_center]

Goal state after:
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
base : Set G := {x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
⊢ ⁅H₁, H₂⁆.Normal

Tactic:
change (closure base).Normal

Goal state after:
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
base : Set G := {x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
⊢ (closure base).Normal
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x : FreeAbelianGroup α
L3 L2 : α
ih : x * of L2 * of L3 = x * (of L2 * of L3)
⊢ x * -of L2 * of L3 = x * (-of L2 * of L3)

Tactic:
rw [neg_mul, mul_neg, mul_neg, neg_mul, ih]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ 1 * x = x

Tactic:
simp_rw [mul_def, one_def, lift_apply_of]
    induction x using FreeAbelianGroup.induction_on with
    | zero => rfl
    | of L => rw [lift_apply_of, one_mul]
    | neg L ih => rw [map_neg, ih]
    | add x1 x2 ih1 ih2 => rw [map_add, ih1, ih2]

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → X → ↥S → C
hP :
  ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S),
    P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩
r₁ : X
t₁ : R
s₁ : ↥S
ht₁ : t₁ * ↑s₁ ∈ S
x : OreLocalization S X
⊢ liftExpand (P r₁ s₁) ⋯ x = liftExpand (P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩) ⋯ x

Tactic:
cases x with | _ r₂ s₂

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → X → ↥S → C
hP :
  ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S),
    P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩
r₁ : X
t₁ : R
s₁ : ↥S
ht₁ : t₁ * ↑s₁ ∈ S
r₂ : X
s₂ : ↥S
⊢ liftExpand (P r₁ s₁) ⋯ (r₂ /ₒ s₂) = liftExpand (P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩) ⋯ (r₂ /ₒ s₂)
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
⊢ (f.lift hg).comp f.toMonoidHom = g

Tactic:
by ext; exact f.lift_eq hg _

Goal state after:
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
a b : WithZero G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun a ≤ (MulEquiv.withZero e.toMulEquiv).toFun b ↔ a ≤ b

Tactic:
cases a <;> cases b

Goal state after:
case zero.zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
⊢ (MulEquiv.withZero e.toMulEquiv).toFun 0 ≤ (MulEquiv.withZero e.toMulEquiv).toFun 0 ↔ 0 ≤ 0

case zero.coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
a✝ : G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun 0 ≤ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝ ↔ 0 ≤ ↑a✝

case coe.zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
a✝ : G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝ ≤ (MulEquiv.withZero e.toMulEquiv).toFun 0 ↔ ↑a✝ ≤ 0

case coe.coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
a✝¹ a✝ : G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝¹ ≤ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝ ↔ ↑a✝¹ ≤ ↑a✝
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
x✝ : WithZero G ≃*o WithZero H
⊢ (fun e ↦ { toMulEquiv := MulEquiv.withZero e.toMulEquiv, map_le_map_iff' := ⋯ })
      ((fun e ↦ { toMulEquiv := MulEquiv.withZero.symm ↑e, map_le_map_iff' := ⋯ }) x✝) =
    x✝

Tactic:
ext x; cases x <;> simp

Goal state after:
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
a b : WithZero αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun a ≤ WithZero.withZeroUnitsEquiv.toFun b ↔ a ≤ b

Tactic:
cases a <;> cases b

Goal state after:
case zero.zero
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
⊢ WithZero.withZeroUnitsEquiv.toFun 0 ≤ WithZero.withZeroUnitsEquiv.toFun 0 ↔ 0 ≤ 0

case zero.coe
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
a✝ : αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun 0 ≤ WithZero.withZeroUnitsEquiv.toFun ↑a✝ ↔ 0 ≤ ↑a✝

case coe.zero
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
a✝ : αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun ↑a✝ ≤ WithZero.withZeroUnitsEquiv.toFun 0 ↔ ↑a✝ ≤ 0

case coe.coe
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
a✝¹ a✝ : αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun ↑a✝¹ ≤ WithZero.withZeroUnitsEquiv.toFun ↑a✝ ↔ ↑a✝¹ ≤ ↑a✝
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case e_s
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this✝ : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₁') = ↑s₄' * (r₃' * r₂' * r₂)
this : ↑s₄' * r₃' * (↑s₂' * ↑s) ∈ S
⊢ ↑(s₄' * (s₃' * (s₁' * s))) = ↑⟨↑s₄' * (r₃' * (↑s₂' * ↑s)), ⋯⟩

Tactic:
simp only [Submonoid.coe_mul, ← mul_assoc]

Goal state after:
case e_s
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this✝ : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₁') = ↑s₄' * (r₃' * r₂' * r₂)
this : ↑s₄' * r₃' * (↑s₂' * ↑s) ∈ S
⊢ ↑s₄' * ↑s₃' * ↑s₁' * ↑s = ↑s₄' * r₃' * ↑s₂' * ↑s
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case e_s
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this✝ : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
this : ↑s₄' * r₃' * (↑s₁' * ↑s) ∈ S
⊢ ↑⟨↑s₄' * (r₃' * (↑s₁' * ↑s)), ⋯⟩ = ↑(s₄' * (s₃' * (s₂' * ⟨r₂ * ↑s, hs⟩)))

Tactic:
simp only [Submonoid.coe_mul, ← mul_assoc]

Goal state after:
case e_s
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this✝ : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
this : ↑s₄' * r₃' * (↑s₁' * ↑s) ∈ S
⊢ ↑s₄' * r₃' * ↑s₁' * ↑s = ↑s₄' * ↑s₃' * ↑s₂' * r₂ * ↑s
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ : ↥S
r' : R
s' : ↥S
huv : ↑s' * r₁ = r' * ↑s₂
⊢ (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = r' • r₂ /ₒ (s' * s₁)

Tactic:
exact smul'_char r₁ r₂ s₁ s₂ s' r' huv

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
r' : R
s' : ↥S
huv : ↑s' * r₁ = r' * ↑s₂
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁)

Tactic:
exact smul'_char r₁ r₂ s₁ s₂ s' r' huv

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
⊢ a * b = if a = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) a b

Tactic:
cases a <;> cases b

Goal state after:
case top.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
⊢ ⊤ * ⊤ = if ⊤ = 0 ∨ ⊤ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ⊤ ⊤

case top.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
⊢ ⊤ * ↑a✝ = if ⊤ = 0 ∨ ↑a✝ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ⊤ ↑a✝

case coe.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
⊢ ↑a✝ * ⊤ = if ↑a✝ = 0 ∨ ⊤ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ↑a✝ ⊤

case coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ a✝ : α
⊢ ↑a✝¹ * ↑a✝ = if ↑a✝¹ = 0 ∨ ↑a✝ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ↑a✝¹ ↑a✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : ¬c = 0
⊢ (Option.bind (a + b) fun b ↦ Option.some (c * b)) =
    (Option.bind a fun b ↦ Option.some (c * b)) + Option.bind b fun b ↦ Option.some (c * b)

Tactic:
cases a <;> cases b

Goal state after:
case neg.top.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
⊢ (Option.bind (⊤ + ⊤) fun b ↦ Option.some (c * b)) =
    (Option.bind ⊤ fun b ↦ Option.some (c * b)) + Option.bind ⊤ fun b ↦ Option.some (c * b)

case neg.top.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝ : α
⊢ (Option.bind (⊤ + ↑a✝) fun b ↦ Option.some (c * b)) =
    (Option.bind ⊤ fun b ↦ Option.some (c * b)) + Option.bind ↑a✝ fun b ↦ Option.some (c * b)

case neg.coe.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝ : α
⊢ (Option.bind (↑a✝ + ⊤) fun b ↦ Option.some (c * b)) =
    (Option.bind ↑a✝ fun b ↦ Option.some (c * b)) + Option.bind ⊤ fun b ↦ Option.some (c * b)

case neg.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝¹ a✝ : α
⊢ (Option.bind (↑a✝¹ + ↑a✝) fun b ↦ Option.some (c * b)) =
    (Option.bind ↑a✝¹ fun b ↦ Option.some (c * b)) + Option.bind ↑a✝ fun b ↦ Option.some (c * b)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : ¬c = 0
⊢ (Option.bind (a + b) fun a ↦ Option.some (a * c)) =
    (Option.bind a fun a ↦ Option.some (a * c)) + Option.bind b fun a ↦ Option.some (a * c)

Tactic:
cases a <;> cases b

Goal state after:
case neg.top.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
⊢ (Option.bind (⊤ + ⊤) fun a ↦ Option.some (a * c)) =
    (Option.bind ⊤ fun a ↦ Option.some (a * c)) + Option.bind ⊤ fun a ↦ Option.some (a * c)

case neg.top.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝ : α
⊢ (Option.bind (⊤ + ↑a✝) fun a ↦ Option.some (a * c)) =
    (Option.bind ⊤ fun a ↦ Option.some (a * c)) + Option.bind ↑a✝ fun a ↦ Option.some (a * c)

case neg.coe.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝ : α
⊢ (Option.bind (↑a✝ + ⊤) fun a ↦ Option.some (a * c)) =
    (Option.bind ↑a✝ fun a ↦ Option.some (a * c)) + Option.bind ⊤ fun a ↦ Option.some (a * c)

case neg.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝¹ a✝ : α
⊢ (Option.bind (↑a✝¹ + ↑a✝) fun a ↦ Option.some (a * c)) =
    (Option.bind ↑a✝¹ fun a ↦ Option.some (a * c)) + Option.bind ↑a✝ fun a ↦ Option.some (a * c)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
ha₂ : a₂ ≠ ⊤
hb : ↑b₁ < ⊤
⊢ ↑a₁ * ↑b₁ < a₂ * ⊤

Tactic:
rw [mul_top (by simpa [bot_eq_zero] using ha.bot_lt.ne')]

Goal state after:
case inr.inl
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
ha₂ : a₂ ≠ ⊤
hb : ↑b₁ < ⊤
⊢ ↑a₁ * ↑b₁ < ⊤
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
⊢ a * b = if a = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) a b

Tactic:
cases a <;> cases b

Goal state after:
case bot.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
⊢ ⊥ * ⊥ = if ⊥ = 0 ∨ ⊥ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ⊥ ⊥

case bot.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
⊢ ⊥ * ↑a✝ = if ⊥ = 0 ∨ ↑a✝ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ⊥ ↑a✝

case coe.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
⊢ ↑a✝ * ⊥ = if ↑a✝ = 0 ∨ ⊥ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ↑a✝ ⊥

case coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ a✝ : α
⊢ ↑a✝¹ * ↑a✝ = if ↑a✝¹ = 0 ∨ ↑a✝ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ↑a✝¹ ↑a✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
⊢ Contravariant { x // 0 ≤ x } (WithBot α) (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 < x2

Tactic:
intro ⟨x, x0⟩

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : WithBot α
x0 : 0 ≤ x
⊢ ∀ {n₁ n₂ : WithBot α},
    (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ n₁) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ n₂) → (fun x1 x2 ↦ x1 < x2) n₁ n₂
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
⊢ Contravariant { x // 0 ≤ x } (WithBot α) (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 < x2

Tactic:
intro ⟨x, x0⟩

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : WithBot α
x0 : 0 ≤ x
⊢ ∀ {n₁ n₂ : WithBot α},
    (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ n₁) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ n₂) → (fun x1 x2 ↦ x1 < x2) n₁ n₂
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
⊢ Contravariant { x // 0 < x } (WithBot α) (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 ≤ x2

Tactic:
intro ⟨x, x0⟩

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
x : WithBot α
x0 : 0 < x
⊢ ∀ {n₁ n₂ : WithBot α},
    (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ n₁) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ n₂) → (fun x1 x2 ↦ x1 ≤ x2) n₁ n₂
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
⊢ Contravariant { x // 0 < x } (WithBot α) (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 ≤ x2

Tactic:
intro ⟨x, x0⟩

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : WithBot α
x0 : 0 < x
⊢ ∀ {n₁ n₂ : WithBot α},
    (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ n₁) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ n₂) → (fun x1 x2 ↦ x1 ≤ x2) n₁ n₂
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α✝ : Type u_1
inst✝³ : Preorder α✝
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n k : ℕ
h : n ≤ n + k
⊢ succ^[n] r ≤ (succ^[k] ∘ succ^[n]) r

Tactic:
Function.comp_apply

Goal state after:
α✝ : Type u_1
inst✝³ : Preorder α✝
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n k : ℕ
h : n ≤ n + k
⊢ succ^[n] r ≤ succ^[k] (succ^[n] r)
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case inl
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
h : v₁ ≤ v₂
⊢ v₁ < v₂

pp: case inr
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
h : v₂ ≤ v₁
⊢ v₁ < v₂

Tactic:
· apply lt_of_le_of_ne h (ne_of_not_le nh).symm

Goal state after:
case inr
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
h : v₂ ≤ v₁
⊢ v₁ < v₂
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
ha :
  (match ↑a✝ with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    ↑a✝
⊢ IsMax ↑a✝

Tactic:
dsimp only at ha

Goal state after:
case coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
ha : (if succ a✝ = a✝ then ⊤ else ↑(succ a✝)) ≤ ↑a✝
⊢ IsMax ↑a✝
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝¹ a✝ : α
h : a✝ < a✝¹
ha : succ a✝ = a✝
⊢ ⊤ ≤ ↑a✝¹

Tactic:
rw [succ_eq_iff_isMax] at ha
      exact (ha.not_lt h).elim

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) < f a
⊢ StrictAnti f

Tactic:
by
  simpa using strictAntiOn_of_succ_lt Set.ordConnected_univ (by simpa using hf)

Goal state after:
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: a b : ℕ∞
⊢ (a * b).toNat = a.toNat * b.toNat

Tactic:
cases a <;> cases b

Goal state after:
case top.top
⊢ (⊤ * ⊤).toNat = ⊤.toNat * ⊤.toNat

case top.coe
a✝ : ℕ
⊢ (⊤ * ↑a✝).toNat = ⊤.toNat * (↑a✝).toNat

case coe.top
a✝ : ℕ
⊢ (↑a✝ * ⊤).toNat = (↑a✝).toNat * ⊤.toNat

case coe.coe
a✝¹ a✝ : ℕ
⊢ (↑a✝¹ * ↑a✝).toNat = (↑a✝¹).toNat * (↑a✝).toNat
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℕ
⊢ (↑a✝¹ * ↑a✝).toNat = a✝¹ * a✝

Tactic:
← natCast_mul,

Goal state after:
case coe.coe
a✝¹ a✝ : ℕ
⊢ (↑(a✝¹ * a✝)).toNat = a✝¹ * a✝
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: a b c d m n : ℕ∞
x : ℕ∞ˣ
x_top : ↑x ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y z : ℕ
this : ↑y * ↑z = 1
x_z : ↑z = x.inv
x_y : ↑x = ↑y
⊢ x = default

Tactic:
← natCast_mul,

Goal state after:
a b c d m n : ℕ∞
x : ℕ∞ˣ
x_top : ↑x ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y z : ℕ
this : ↑(y * z) = 1
x_z : ↑z = x.inv
x_y : ↑x = ↑y
⊢ x = default
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

Tactic:
by
  by_cases hs : i ∈ s
  · convert! (s.prod_inter_mul_prod_sdiff { i } f).symm
    simp [hs]
  · simp_all only [not_false_eq_true, forall_const, one_mul]
    apply Finset.prod_congr <;> aesop

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
v : Vector α n
f : α → β
⊢ (map f v).toList = List.map f v.toList

Tactic:
by cases v; rfl

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α n
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ (pmap f v hp).toList = List.pmap f v.toList hp

Tactic:
by cases v; rfl

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: case mpr.inl
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
hSc : ∅.Countable
hps : ∀ s ∈ ∅, p s
hS : sSup ∅ = ⊤
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤

Tactic:
rw [sSup_empty] at hS
      have := subsingleton_of_bot_eq_top hS
      rcases h with ⟨x, hx⟩
      exact ⟨fun _ => x, fun _ => hx, Subsingleton.elim _ _⟩

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a b : α
h : inl b < inl a
⊢ ∃ b, b < a

Tactic:
exact ⟨b, inl_lt_inl_iff.1 h⟩

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a b : α
h : inl a < inl b
⊢ ∃ b, a < b

Tactic:
exact ⟨b, inl_lt_inl_iff.1 h⟩

Goal state after: