mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a : α
⊢ (∀ (y : Quot r), mk r a = y) ↔ ∀ (i : α), ⊤ ≤ Relation.EqvGen r a i

Tactic:
refine Quot.mk_surjective.forall.trans (forall_congr' fun b => ?_)

Goal state after:
α : Type u_1
r : α → α → Prop
a b : α
⊢ mk r a = mk r b ↔ ⊤ ≤ Relation.EqvGen r a b
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
x' : κ
hx : x' ∈ ↑t
y' : κ
hy : y' ∈ ↑t
⊢ x' ≠ y' → (Disjoint on fun j ↦ {i ∈ s | g i = j}) x' y'

Tactic:
hne

Goal state after:
case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
x' : κ
hx : x' ∈ ↑t
y' : κ
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ (Disjoint on fun j ↦ {i ∈ s | g i = j}) x' y'
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
s : Finset ι
t : Finset κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → M
x' : κ
hx : x' ∈ ↑t
y' : κ
hy : y' ∈ ↑t
⊢ x' ≠ y' → (Disjoint on fun j ↦ {i ∈ s | g i = j}) x' y'

Tactic:
hne

Goal state after:
case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
s : Finset ι
t : Finset κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → M
x' : κ
hx : x' ∈ ↑t
y' : κ
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ (Disjoint on fun j ↦ {i ∈ s | g i = j}) x' y'
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:

Tactic:
∏ x ∈ s, f x = ∏ x ∈ {a}, f x := by
      { refine (prod_subset ?_ ?_).symm
        · intro _ H
          rwa [mem_singleton.1 H]
        · simpa only [mem_singleton] }
    _ = f a := prod_singleton _ _

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
h : ∀ (x x_1 : G), x_1⁻¹ * x ∈ N
⊢ N = ⊤

Tactic:
by ext; simpa using h _ 1

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
h : ∀ (x x_1 : G), x * x_1⁻¹ ∈ N
⊢ N = ⊤

Tactic:
by ext; simpa using h _ 1

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure.pure
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
q : β✝
⊢ pure (p, q) = (pure fun a ↦ (a, q)) <*> pure p

Tactic:
pure_seq,

Goal state after:
case pure.pure
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
q : β✝
⊢ pure (p, q) = (fun a ↦ (a, q)) <$> pure p
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case a.left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
rw [map_commutator]

Goal state after:
case a.left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅map (MonoidHom.inl G G') H₁, map (MonoidHom.inl G G') H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case a.right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
rw [map_commutator]

Goal state after:
case a.right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅map (MonoidHom.inr G G') K₁, map (MonoidHom.inr G G') K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
y : FreeAbelianGroup α
s : α
ih : of s * y = y * of s
⊢ -(y * of s) = y * -of s

Tactic:
neg_mul_eq_mul_neg

Goal state after:
case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
y : FreeAbelianGroup α
s : α
ih : of s * y = y * of s
⊢ y * -of s = y * -of s
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α✝ : Type u
G : Type u_1
β✝ : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup α
⊢ (map ⇑f.symm) ((map ⇑f) x) = x

Tactic:
← map_comp_apply,

Goal state after:
α✝ : Type u
G : Type u_1
β✝ : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup α
⊢ (map (⇑f.symm ∘ ⇑f)) x = x
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α✝ : Type u
G : Type u_1
β✝ : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup β
⊢ (map ⇑f) ((map ⇑f.symm) x) = x

Tactic:
← map_comp_apply,

Goal state after:
α✝ : Type u
G : Type u_1
β✝ : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup β
⊢ (map (⇑f ∘ ⇑f.symm)) x = x
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case h
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)
H : ∀ (v : P), ∃ x, v * g ↑x.2 = g x.1
v : P
x : M × ↥S
hx : v * g ↑x.2 = g x.1
⊢ (f.lift hg) (f.mk' x.1 x.2) = v

Tactic:
rw [lift_mk', mul_inv_left hg, mul_comm, ← hx]

Goal state after:
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)
⊢ Surjective ⇑(f.lift hg) ↔ ∀ (v : P), ∃ x, v * g ↑x.2 = g x.1

Tactic:
by
  constructor
  · intro H v
    obtain ⟨z, hz⟩ := H v
    obtain ⟨x, hx⟩ := f.surj z
    use x
    rw [← hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2),
      ← MonoidHom.domRestrict_apply, IsUnit.mul_liftRight_inv (g.domRestrict S) hg, mul_one]
  · intro H v
    obtain ⟨x, hx⟩ := H v
    use f.mk' x.1 x.2
    rw [lift_mk', mul_inv_left hg, mul_comm, ← hx]

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

Goal state before:
pp: case refine_1
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f ↑a.2 = f a.1
b : M × ↥S
hb : w * f ↑b.2 = f b.1
⊢ z * f ↑(a.2 * b.2) = f (a.1 * ↑b.2)

pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f ↑a.2 = f a.1
b : M × ↥S
hb : w * f ↑b.2 = f b.1
⊢ w * f ↑(a.2 * b.2) = f (↑a.2 * b.1)

Tactic:
· simp_rw [mul_def, map_mul, ← ha]
    exact (mul_assoc z _ _).symm

Goal state after:
case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f ↑a.2 = f a.1
b : M × ↥S
hb : w * f ↑b.2 = f b.1
⊢ w * f ↑(a.2 * b.2) = f (↑a.2 * b.1)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x : OreLocalization S R
⊢ x * 1 = x

Tactic:
cases x with | _ r s
  simp [OreLocalization.one_def, oreDiv_mul_char r (1 : R) s (1 : S) r 1 (by simp)]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
a : M
b c : ↥S
⊢ a * ↑(b * c) = a * ↑c * ↑b

Tactic:
rw [Submonoid.coe_mul, mul_comm (b : M), mul_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : α
h₀ : 0 < ↑a
b c : WithTop α
hbc : b < c
⊢ (fun x ↦ ↑a * x) b < (fun x ↦ ↑a * x) c

Tactic:
lift b to α using hbc.ne_top

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : α
h₀ : 0 < ↑a
c : WithTop α
b : α
hbc : ↑b < c
⊢ (fun x ↦ ↑a * x) ↑b < (fun x ↦ ↑a * x) c
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
a : α
h₀ : 0 < ↑a
b c : WithTop α
hbc : b < c
⊢ (fun x ↦ x * ↑a) b < (fun x ↦ x * ↑a) c

Tactic:
lift b to α using hbc.ne_top

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
a : α
h₀ : 0 < ↑a
c : WithTop α
b : α
hbc : ↑b < c
⊢ (fun x ↦ x * ↑a) ↑b < (fun x ↦ x * ↑a) c
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
⊢ φ = universalMulHom f fS hf

Tactic:
ext x; cases x with | _ r s
  rw [universalMulHom_apply, ← huniv r, numeratorHom_apply, ← one_mul (φ (r /ₒ s)), ←
    Units.val_one, ← inv_mul_cancel (fS s), Units.val_mul, mul_assoc, ← hf, ← huniv, ← φ.map_mul,
    numeratorHom_apply, OreLocalization.mul_cancel]

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

Goal state before:
pp: case c.c
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹³ : Monoid M
S : Submonoid M
inst✝¹² : OreSet S
inst✝¹¹ : MulAction M X
inst✝¹⁰ : SMul R X
inst✝⁹ : SMul R M
inst✝⁸ : IsScalarTower R M M
inst✝⁷ : IsScalarTower R M X
inst✝⁶ : SMul R' X
inst✝⁵ : SMul R' M
inst✝⁴ : IsScalarTower R' M M
inst✝³ : IsScalarTower R' M X
inst✝² : SMul R R'
inst✝¹ : IsScalarTower R R' M
inst✝ : SMulCommClass R M M
r : R
r₁ : M
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ (r • 1 /ₒ 1 * (r₁ /ₒ s₁)) • (r₂ /ₒ s₂) = (r₁ /ₒ s₁ * (r • 1 /ₒ 1)) • (r₂ /ₒ s₂)

Tactic:
mul_div_one,

Goal state after:
case c.c
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹³ : Monoid M
S : Submonoid M
inst✝¹² : OreSet S
inst✝¹¹ : MulAction M X
inst✝¹⁰ : SMul R X
inst✝⁹ : SMul R M
inst✝⁸ : IsScalarTower R M M
inst✝⁷ : IsScalarTower R M X
inst✝⁶ : SMul R' X
inst✝⁵ : SMul R' M
inst✝⁴ : IsScalarTower R' M M
inst✝³ : IsScalarTower R' M X
inst✝² : SMul R R'
inst✝¹ : IsScalarTower R R' M
inst✝ : SMulCommClass R M M
r : R
r₁ : M
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ (r • 1 /ₒ 1 * (r₁ /ₒ s₁)) • (r₂ /ₒ s₂) = (r₁ * r • 1 /ₒ s₁) • (r₂ /ₒ s₂)
Module: Mathlib.Order.Iterate

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : f x = g x
⊢ f^[n] x < g^[n] x ↔ f x < g x

pp: case inr.inr
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : g x < f x
⊢ f^[n] x < g^[n] x ↔ f x < g x

Tactic:
· simp only [*, h.iterate_eq_of_map_eq, lt_irrefl]

Goal state after:
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : g x < f x
⊢ f^[n] x < g^[n] x ↔ f x < g x
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝¹ a✝ : α
h : a✝¹ ≤ a✝
⊢ x * a✝¹ ≤ x * a✝

Tactic:
norm_cast at x0

Goal state after:
case inr.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
x : α
x0' : ↑x ≠ 0
a✝¹ a✝ : α
h : a✝¹ ≤ a✝
x0 : 0 ≤ x
⊢ x * a✝¹ ≤ x * a✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝¹ a✝ : α
h : a✝¹ ≤ a✝
⊢ a✝¹ * x ≤ a✝ * x

Tactic:
norm_cast at x0

Goal state after:
case inr.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
x : α
x0' : ↑x ≠ 0
a✝¹ a✝ : α
h : a✝¹ ≤ a✝
x0 : 0 ≤ x
⊢ a✝¹ * x ≤ a✝ * x
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
x : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : a✝ < a✝¹
⊢ x * a✝ < x * a✝¹

Tactic:
norm_cast at x0

Goal state after:
case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
x a✝¹ a✝ : α
h : a✝ < a✝¹
x0 : 0 < x
⊢ x * a✝ < x * a✝¹
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
x : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : a✝ < a✝¹
⊢ a✝ * x < a✝¹ * x

Tactic:
norm_cast at x0

Goal state after:
case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
x a✝¹ a✝ : α
h : a✝ < a✝¹
x0 : 0 < x
⊢ a✝ * x < a✝¹ * x
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝¹ a✝ : α
h : x * a✝ < x * a✝¹
⊢ a✝ < a✝¹

Tactic:
norm_cast at x0

Goal state after:
case inr.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : α
x0' : ↑x ≠ 0
a✝¹ a✝ : α
h : x * a✝ < x * a✝¹
x0 : 0 ≤ x
⊢ a✝ < a✝¹
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝¹ a✝ : α
h : a✝ * x < a✝¹ * x
⊢ a✝ < a✝¹

Tactic:
norm_cast at x0

Goal state after:
case inr.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : α
x0' : ↑x ≠ 0
a✝¹ a✝ : α
h : a✝ * x < a✝¹ * x
x0 : 0 ≤ x
⊢ a✝ < a✝¹
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
x : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : x * a✝¹ ≤ x * a✝
⊢ a✝¹ ≤ a✝

Tactic:
norm_cast at x0

Goal state after:
case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
x a✝¹ a✝ : α
h : x * a✝¹ ≤ x * a✝
x0 : 0 < x
⊢ a✝¹ ≤ a✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : α
x0 : 0 < ↑x
a✝ : α
h : ↑a✝ * ↑x ≤ ⊥ * ↑x
⊢ ↑a✝ ≤ ⊥

pp: case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : ↑a✝¹ * ↑x ≤ ↑a✝ * ↑x
⊢ ↑a✝¹ ≤ ↑a✝

Tactic:
· rw [bot_mul x0.ne.symm, ← coe_mul] at h
      exact absurd h (bot_lt_coe _).not_ge

Goal state after:
case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : ↑a✝¹ * ↑x ≤ ↑a✝ * ↑x
⊢ ↑a✝¹ ≤ ↑a✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : a✝¹ * x ≤ a✝ * x
⊢ a✝¹ ≤ a✝

Tactic:
norm_cast at x0

Goal state after:
case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x a✝¹ a✝ : α
h : a✝¹ * x ≤ a✝ * x
x0 : 0 < x
⊢ a✝¹ ≤ a✝
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case _a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
⊢ a < succ a

Tactic:
exact lt_succ_of_not_isMax ha

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b : α
⊢ a ≤ b → ∃ n, pred^[n] b = a

Tactic:
refine WellFounded.fix (C := fun b => a ≤ b → ∃ n, Nat.iterate pred n b = a)
      h.wf ?_ b

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b : α
⊢ ∀ (x : α), (∀ y < x, a ≤ y → ∃ n, pred^[n] y = a) → a ≤ x → ∃ n, pred^[n] x = a
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LinearOrder α
ha : IsSuccPrelimit a
b : α
hb : b ∈ upperBounds (Iio a)
c : α
hc : c < a
⊢ c < b

Tactic:
obtain ⟨d, hd, hd'⟩ := ha.lt_iff_exists_lt.1 hc

Goal state after:
α : Type u_1
a : α
inst✝ : LinearOrder α
ha : IsSuccPrelimit a
b : α
hb : b ∈ upperBounds (Iio a)
c : α
hc : c < a
d : α
hd : d < a
hd' : c < d
⊢ c < b
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case h.succ
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
⊢ pred^[n] (pred ⟨c, hc⟩) = ⟨b, hb⟩

Tactic:
change Order.pred^[n] (dite ..) = _

Goal state after:
case h.succ
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
⊢ pred^[n] (if h : pred ↑⟨c, hc⟩ ∈ s then ⟨pred ↑⟨c, hc⟩, h⟩ else ⟨c, hc⟩) = ⟨b, hb⟩
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case succ.succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : succ^[n + 1] a ∈ s → f a < f (succ^[n + 1] a)
hb : succ (succ^[n + 1] a) ∈ s
this : succ^[n + 1] a ∈ s
⊢ f a < f (succ (succ^[n + 1] a))

Tactic:
by_cases hb' : IsMax (succ^[n + 1] a)

Goal state after:
case pos
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : succ^[n + 1] a ∈ s → f a < f (succ^[n + 1] a)
hb : succ (succ^[n + 1] a) ∈ s
this : succ^[n + 1] a ∈ s
hb' : IsMax (succ^[n + 1] a)
⊢ f a < f (succ (succ^[n + 1] a))

case neg
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : succ^[n + 1] a ∈ s → f a < f (succ^[n + 1] a)
hb : succ (succ^[n + 1] a) ∈ s
this : succ^[n + 1] a ∈ s
hb' : ¬IsMax (succ^[n + 1] a)
⊢ f a < f (succ (succ^[n + 1] a))
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
f g : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
⊢ (insert i ∅).piecewise f g = update g i (f i)

Tactic:
piecewise_insert,

Goal state after:
ι : Type u_1
π : ι → Sort u_2
f g : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
⊢ update (∅.piecewise f g) i (f i) = update g i (f i)
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f ↑∅
e : α ≃ ↥t
⊢ ∃ g, ∀ i ∈ ∅, ↑(g i) = f i

Tactic:
use e

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f ↑∅
e : α ≃ ↥t
⊢ ∀ i ∈ ∅, ↑(e i) = f i
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
n : ℕ
g : β → γ
f : α → β
s : Sym α n
⊢ ↑(map g (map f s)) = ↑(map (g ∘ f) s)

Tactic:
dsimp only [Sym.map]

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
n : ℕ
g : β → γ
f : α → β
s : Sym α n
⊢ Multiset.map g (Multiset.map f ↑s) = Multiset.map (g ∘ f) ↑s
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: m : Type u_6 → Type u_7
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_6
n : ℕ
f : Fin (n + 1) → α
⊢ (do
      let a ← pure (f 0)
      let v ← mOfFn fun i ↦ pure (f i.succ)
      pure (a ::ᵥ v)) =
    pure (ofFn f)

Tactic:
@mOfFn_pure m _ _ _ n _,

Goal state after:
m : Type u_6 → Type u_7
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_6
n : ℕ
f : Fin (n + 1) → α
⊢ (do
      let a ← pure (f 0)
      let v ← pure (ofFn fun i ↦ f i.succ)
      pure (a ::ᵥ v)) =
    pure (ofFn f)
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
⊢ RightInverse
    (fun s ↦
      ((Equiv.subtypeQuotientEquivQuotientSubtype (fun x ↦ x.length = 1) (fun x ↦ Multiset.card x = 1) ⋯ ⋯) s).liftOn
        (fun l ↦ (↑l).head ⋯) ⋯)
    fun a ↦ ⟨{a}, ⋯⟩

Tactic:
rintro ⟨⟨l⟩, h⟩; obtain ⟨a, rfl⟩ := List.length_eq_one_iff.mp h; rfl

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun x ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
⊢ ScottContinuousOn D (g ∘ f)

Tactic:
intro d

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun x ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
⊢ d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → IsLUB (g ∘ f '' d) ((g ∘ f) a)
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set (α × β))
⊢ ScottContinuousOn D Prod.fst

Tactic:
intro d

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set (α × β))
d : Set (α × β)
⊢ d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α × β⦄, IsLUB d a → IsLUB (Prod.fst '' d) a.1
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set (α × β))
⊢ ScottContinuousOn D Prod.snd

Tactic:
intro d

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set (α × β))
d : Set (α × β)
⊢ d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α × β⦄, IsLUB d a → IsLUB (Prod.snd '' d) a.2
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case succ
α : Type u_1
r : α → α → Prop
c₂ s✝ : Set α
a✝ : ChainClosure r s✝
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ s✝ → s✝ = c₁ ∨ SuccChain r c₁ ⊆ s✝
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r s✝
h₁ : c₁ ⊆ s✝
⊢ SuccChain r c₁ ⊆ SuccChain r s✝

Tactic:
obtain rfl | h₂ := ih hc₁ h₁

Goal state after:
case succ.inl
α : Type u_1
r : α → α → Prop
c₂ s✝ : Set α
a✝ : ChainClosure r s✝
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ s✝ → s✝ = c₁ ∨ SuccChain r c₁ ⊆ s✝
hc₁ : ChainClosure r s✝
h : s✝ ⊆ SuccChain r s✝
h₁ : s✝ ⊆ s✝
⊢ SuccChain r s✝ ⊆ SuccChain r s✝

case succ.inr
α : Type u_1
r : α → α → Prop
c₂ s✝ : Set α
a✝ : ChainClosure r s✝
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ s✝ → s✝ = c₁ ∨ SuccChain r c₁ ⊆ s✝
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r s✝
h₁ : c₁ ⊆ s✝
h₂ : SuccChain r c₁ ⊆ s✝
⊢ SuccChain r c₁ ⊆ SuccChain r s✝
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a b : Cardinal.{u_1}
h : a < b
⊢ a + 1 ≤ b

Tactic:
by
  induction a, b using Cardinal.inductionOn₂ with | mk α β
  obtain ⟨f⟩ := h.le
  have hf : ¬Surjective f := fun hn ↦ h.not_ge (mk_le_of_surjective hn)
  rw [Surjective, not_forall] at hf
  obtain ⟨b, hb⟩ := hf
  rw [← mk_option]
  exact (f.optionElim b hb).cardinal_le

Goal state after: