mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.Translate.Reorder

Goal state before:
pp: r : ArgReorder
x : Nat × ArgReorder
h✝ : x ∈ r.argReorders
⊢ sizeOf x.snd < sizeOf r

Tactic:
cases r; grind [→ Array.sizeOf_lt_of_mem]

Goal state after:
Module: Mathlib.Tactic.Translate.Reorder

Goal state before:
pp: r : ArgReorder
perm : List String :=
  List.map
    (fun x ↦
      match x with
      | ⟨x, h⟩ =>
        " ".intercalate
          (List.map
            (fun x_1 ↦
              match x_1 with
              | ⟨x_2, h⟩ => ToString.toString (x_2 + 1))
            x.val.attach))
    (List.attach r.perm)
x : Nat × ArgReorder
h✝ : x ∈ r.argReorders
⊢ sizeOf x.snd < sizeOf r

Tactic:
cases r; grind [→ Array.sizeOf_lt_of_mem]

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_5
β : α → Type u_4
f : (x : α) → β x
p : α → Prop
x : Subtype p
⊢ restrict p f x = f ↑x

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_4
β : Sort u_5
f : α → β
p : β → Prop
h : ∀ (a : α), p (f a)
hf : Injective f
x y : α
hxy : coind f h x = coind f h y
⊢ f x = f y

Tactic:
by apply congr_arg Subtype.val hxy

Goal state after:
Module: Mathlib.Algebra.Opposites

Goal state before:
pp: α : Type u_1
inst✝ : Add α
⊢ IsCancelAdd αᵐᵒᵖ ↔ IsCancelAdd α

Tactic:
by
  simp_rw [isCancelAdd_iff, isLeftCancelAdd_iff, isRightCancelAdd_iff]

Goal state after:
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
n : ℕ
hn : 0 < n
⊢ f ∘ f^[n.pred] = f^[n]

Tactic:
← iterate_succ',

Goal state after:
α : Type u
f : α → α
n : ℕ
hn : 0 < n
⊢ f^[n.pred.succ] = f^[n]
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : M
⊢ (fun x ↦ a • x)^[0] = fun x ↦ a ^ 0 • x

Tactic:
simp [funext_iff]

Goal state after:
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Bot γ
x : α → β
⊢ ⊥ ∘ x = ⊥

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case step
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℕ → β
a : ℕ
h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))
b c : ℕ
hab : a ≤ b
m✝ : ℕ
b_lt_k : b.succ.le m✝
r_b_k : r (f b) (f m✝)
⊢ r (f b) (f m✝.succ)

Tactic:
| step b_lt_k r_b_k =>

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

Goal state before:
pp: case refine_1
α : Type u
s : Set α
⊢ (∃ a, s = {a}) → s.Nonempty ∧ s.Subsingleton

pp: case refine_2
α : Type u
s : Set α
h : s.Nonempty ∧ s.Subsingleton
⊢ ∃ a, s = {a}

Tactic:
· rintro ⟨a, rfl⟩
    exact ⟨singleton_nonempty a, subsingleton_singleton⟩

Goal state after:
case refine_2
α : Type u
s : Set α
h : s.Nonempty ∧ s.Subsingleton
⊢ ∃ a, s = {a}
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ b ≤ c ↔ a ≤ c ⊔ b

Tactic:
by
  rw [sdiff_le_iff, sup_comm]

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ a ⇨ b ⇨ ⊥ = b ⇨ a ⇨ ⊥

Tactic:
himp_left_comm

Goal state after:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ a ⊓ b ≤ ⊥ ↔ Disjoint a b

Tactic:
disjoint_iff_inf_le

Goal state after:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ a ⊓ b ≤ ⊥ ↔ a ⊓ b ≤ ⊥
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : y ≤ x ⊔ z
⊢ y ⊓ x ⊓ z = ⊥

Tactic:
rw [inf_assoc, hd.eq_bot, inf_bot_eq]

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊓ (y ⊓ x \ y)) = ⊥

Tactic:
inf_sdiff_self_right,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊓ ⊥) = ⊥
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ (z ⊓ x \ z) ⊓ y \ z = ⊥

Tactic:
inf_sdiff_self_right,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ ⊥ ⊓ y \ z = ⊥
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case none
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.12
p : Option α → Type v
h : ∀ (a : p none), False
⊢ ∀ (a : p none), none.isSome = true

pp: case some
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.12
p : Option α → Type v
h : ∀ (a : p none), False
val✝ : α
⊢ ∀ (a : p (some val✝)), (some val✝).isSome = true

Tactic:
· intro n
      exfalso
      exact h n

Goal state after:
case some
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.12
p : Option α → Type v
h : ∀ (a : p none), False
val✝ : α
⊢ ∀ (a : p (some val✝)), (some val✝).isSome = true
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ b \ a ∆ b = a ⊓ b

Tactic:
by
  rw [symmDiff_comm, inf_comm, sdiff_symmDiff_left]

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

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ : Sort u_8
α : Type ?u.18
β : Type ?u.17
γ : Type ?u.15
⊢ RightInverse (fun s ↦ Sum.elim (Prod.map inl id) (Prod.map inr id) s) fun p ↦
    Sum.map (fun x ↦ (x, p.snd)) (fun x ↦ (x, p.snd)) p.fst

Tactic:
by rintro (⟨_, _⟩ | ⟨_, _⟩) <;> rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : BooleanAlgebra α
s : Set α
⊢ compl '' compl '' s = s

Tactic:
← image_comp,

Goal state after:
α : Type u_1
inst✝ : BooleanAlgebra α
s : Set α
⊢ compl ∘ compl '' s = s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Set α
f : α → β
hf : Injective f
eq : f '' s = f '' t
⊢ f ⁻¹' f '' s = t

Tactic:
← preimage_image_eq t hf,

Goal state after:
α : Type u_1
β : Type u_2
s t : Set α
f : α → β
hf : Injective f
eq : f '' s = f '' t
⊢ f ⁻¹' f '' s = f ⁻¹' f '' t
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
⊢ range (codRestrict f s h) = Subtype.val ⁻¹' range f

Tactic:
by
  ext; simp [Subtype.ext_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ (fun a ↦ ↑a) '' MapsTo.restrict f (f ⁻¹' t) t ⋯ '' Subtype.val ⁻¹' s = (fun a ↦ ↑a) '' Subtype.val ⁻¹' f '' s

Tactic:
← image_comp,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ (fun a ↦ ↑a) ∘ MapsTo.restrict f (f ⁻¹' t) t ⋯ '' Subtype.val ⁻¹' s = (fun a ↦ ↑a) '' Subtype.val ⁻¹' f '' s
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
⊢ Injective (restrict f s t h) ↔ InjOn f s

Tactic:
rw [h.restrict_eq_codRestrict, injective_codRestrict, injOn_iff_injective]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
x : α
⊢ range f ⊆ {x} ↔ f = const ι x

Tactic:
simp [funext_iff]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = f₁ '' f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s

Tactic:
← image_comp,

Goal state after:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s

Tactic:
← image_comp,

Goal state after:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
h : f '' s = f '' t
⊢ f ⁻¹' f '' s = t

Tactic:
← preimage_image_eq t hf,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
h : f '' s = f '' t
⊢ f ⁻¹' f '' s = f ⁻¹' f '' t
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f g : (i : ι) → α i
⊢ (g ∈ univ.pi fun i ↦ {f i}) ↔ g ∈ {f}

Tactic:
simp [funext_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
⊢ g '' f '' s = s

Tactic:
← image_comp,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
⊢ g ∘ f '' s = s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s : Set α
t : Set ↑s
x : α
x✝ : x ∈ val '' t
y : { x // x ∈ s }
left✝ : y ∈ t
yvaleq : ↑y = x
⊢ x ∈ s

Tactic:
by
  rw [← yvaleq]; exact y.property

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : α → β
a : α
⊢ EqOn f₁ f₂ {a} ↔ f₁ a = f₂ a

Tactic:
simp [Set.EqOn]

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

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : ¬i ∈ s
xᵢ : α i
⊢ (∃ x, ∀ (i : ι), i ∈ s → x i ∈ t i) → ∃ x, (∀ (i : ι), i ∈ s → x i ∈ t i) ∧ x i = xᵢ

Tactic:
· rintro ⟨x, hx⟩
    refine ⟨Function.update x i xᵢ, ?_⟩
    simpa +contextual [(ne_of_mem_of_not_mem · hi)]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
⊢ ⇑(piCongrLeft α f) ⁻¹' (⇑f '' s).pi t = s.pi fun i ↦ t (f i)

Tactic:
apply Set.ext
  rw [← (f.piCongrLeft α).symm.forall_congr_right]
  simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f g : M →* G
a b : M
⊢ f (a * b) / g (a * b) = f a / g a * (f b / g b)

Tactic:
simp [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm]

Goal state after:
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : αˣ
⊢ ↑a = 1 ↔ a = 1

Tactic:
← Units.val_one,

Goal state after:
α : Type u
inst✝ : Monoid α
a : αˣ
⊢ ↑a = ↑1 ↔ a = 1
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
x✝¹ x✝ : M × N
m₁ : M
n₁ : N
fst✝ : M
snd✝ : N
⊢ (m₁ * fst✝, n₁ * snd✝) = (fst✝ * m₁, snd✝ * n₁)

Tactic:
mul_comm m₁,

Goal state after:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
x✝¹ x✝ : M × N
m₁ : M
n₁ : N
fst✝ : M
snd✝ : N
⊢ (fst✝ * m₁, n₁ * snd✝) = (fst✝ * m₁, snd✝ * n₁)
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
⊢ (∀ {a b : M₀}, a * b = 0 → ¬b = 0 → a = 0) ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), y * x = 0 → y = 0

Tactic:
exact ⟨fun h b hb a eq ↦ h eq hb, fun h a b eq hb ↦ h b hb a eq⟩

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

Goal state before:
pp: case succ
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p (f x) ↔ p x
n : ℕ
ih : f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯
⊢ f.subtypePerm hf ^ (n + 1) = (f ^ (n + 1)).subtypePerm ⋯

Tactic:
simp_rw [pow_succ', ih, subtypePerm_mul]

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

Goal state before:
pp: R : Type u_3
inst✝ : MonoidWithZero R
x : R
m : ℕ
h✝ : IsNilpotent (x ^ m)
n : ℕ
h : (x ^ m) ^ n = 0
⊢ x ^ (m * n) = (x ^ m) ^ n

Tactic:
pow_mul x m n

Goal state after:
R : Type u_3
inst✝ : MonoidWithZero R
x : R
m : ℕ
h✝ : IsNilpotent (x ^ m)
n : ℕ
h : (x ^ m) ^ n = 0
⊢ (x ^ m) ^ n = (x ^ m) ^ n
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 3 + 1 = 4

Tactic:
by
  rw [← two_add_one_eq_three, ← one_add_one_eq_two, ← Nat.cast_one,
    ← Nat.cast_add, ← Nat.cast_add, ← Nat.cast_add]
  apply congrArg
  decide

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
i : ℤ
⊢ a ^ (1 + i) = a * a ^ i

Tactic:
rw [zpow_add₀ h, zpow_one]

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m n : ℕ
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
rcases mod_two_eq_zero_or_one m with h₁ | h₁ <;> rcases mod_two_eq_zero_or_one n with h₂ | h₂ <;>
    simp [even_iff, h₁, h₂, Nat.mul_mod]

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

Goal state before:
pp: a b : Prop
l : List Prop
h_chain : IsChain (fun x1 x2 ↦ x1 → x2) (a :: b :: l)
h_last : l.getLastD b → a
⊢ (a :: b :: l).TFAE

Tactic:
induction l generalizing a b with

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

Goal state before:
pp: a b : Prop
l : List Prop
h_chain : IsChain (fun x1 x2 ↦ x1 → x2) (a :: b :: l)
h_last : l.getLastD b → a
⊢ (a :: b :: l).TFAE

Tactic:
by
  induction l generalizing a b with
  | nil => simp_all [tfae_cons_cons, iff_def]
  | cons c l IH =>
    simp only [tfae_cons_cons, getLastD_cons, isChain_cons_cons] at *
    rcases h_chain with ⟨ab, ⟨bc, ch⟩⟩
    have := IH ⟨bc, ch⟩ (ab ∘ h_last)
    exact ⟨⟨ab, h_last ∘ (this.2 c (.head _) _ getLastD_mem_cons).1 ∘ bc⟩, this⟩

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

Goal state before:
pp: α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
p₁ : α → Prop
hp₁ : p₁ ∈ l
⊢ ∀ (j : α → Prop), j ∈ l → ((∀ (a : α), p₁ a) ↔ ∀ (a : α), j a)

Tactic:
p₂

Goal state after:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
p₁ : α → Prop
hp₁ : p₁ ∈ l
p₂ : α → Prop
⊢ p₂ ∈ l → ((∀ (a : α), p₁ a) ↔ ∀ (a : α), p₂ a)
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
p₁ : α → Prop
hp₁ : p₁ ∈ l
⊢ ∀ (j : α → Prop), j ∈ l → ((∃ a, p₁ a) ↔ ∃ a, j a)

Tactic:
p₂

Goal state after:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
p₁ : α → Prop
hp₁ : p₁ ∈ l
p₂ : α → Prop
⊢ p₂ ∈ l → ((∃ a, p₁ a) ↔ ∃ a, p₂ a)
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
⊢ ⇑f.toMonoidWithZeroHom = ⇑f

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: case negSucc
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : M
a✝ : ℕ
⊢ ↑-[a✝+1] • b = -[a✝+1] • b

Tactic:
simp [add_smul, Nat.cast_smul_eq_nsmul]

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
⊢ ↑n = 0 ∨ ↑n = 1

Tactic:
obtain hn | hn := Nat.even_or_odd n
  · exact Or.inl <| natCast_eq_zero_of_even_of_two_eq_zero hn h
  · exact Or.inr <| natCast_eq_one_of_odd_of_two_eq_zero hn h

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : LE α
inst✝² : Mul α
inst✝¹ : IsMulCommutative α
inst✝ : MulLeftMono α
a b c : α
ha : MulLECancellable a
⊢ b * a ≤ c * a ↔ b ≤ c

Tactic:
mul_comm' b,

Goal state after:
α : Type u_1
inst✝³ : LE α
inst✝² : Mul α
inst✝¹ : IsMulCommutative α
inst✝ : MulLeftMono α
a b c : α
ha : MulLECancellable a
⊢ a * b ≤ c * a ↔ b ≤ c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
hb : 0 ≤ b
h : a ≤ 1
⊢ a * b ≤ b

Tactic:
simpa only [one_mul] using mul_le_mul_of_nonneg_right h hb

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : Zero α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
hb : 0 ≤ b
h : 1 ≤ a
⊢ b ≤ a * b

Tactic:
simpa only [one_mul] using mul_le_mul_of_nonneg_right h hb

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
a b : R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (¬a ≤ 0 → 0 ≤ b) ∧ (¬b ≤ 0 → 0 ≤ a)

Tactic:
← or_iff_not_imp_left

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
a b : R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
a b : α
h : s ({ toFun := f, inj' := ⋯ } a) ({ toFun := f, inj' := ⋯ } b)
⊢ ¬a = b

Tactic:
exact (irrefl _ <| · ▸ h)

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a b : ℤ
H1 : 0 ≤ a
H2✝ : a < |b|
n : ℕ
H2 : a < ↑-[n+1].natAbs
⊢ -(a / -[n+1]) = -0

Tactic:
by rw [← Int.ediv_neg]; exact ediv_eq_zero_of_lt H1 H2

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

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsRightRegular a
h : b * a = a
⊢ b = 1

Tactic:
rwa [← ha.eq_iff, one_mul]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ ((StrictMono fun a ↦ map f ↑a) ∧ ∀ (x : α), map f ⊥ < map f ↑x) ↔ StrictMono f

Tactic:
simp [StrictMono, bot_lt_coe]

Goal state after:
Module: Mathlib.Data.Int.LeastGreatest

Goal state before:
pp: P : ℤ → Prop
Hbdd : ∃ b, ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
⊢ ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub

Tactic:
let ⟨b, Hb⟩ := Hbdd
  let ⟨lb, H⟩ := greatestOfBdd b Hb Hinh
  exact ⟨lb, H⟩

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

Goal state before:
pp: case inr.inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ d + (a + b) < c + (a + b)

Tactic:
add_rotate',

Goal state after:
case inr.inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ a + (b + d) < c + (a + b)
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
wf : WellFounded r
inst✝ : Nonempty α
⊢ ¬Relator.RightTotal r

Tactic:
intro h
  obtain ⟨a, -, ha⟩ := wf.has_min Set.univ Set.univ_nonempty
  obtain ⟨b, hba⟩ := h a
  specialize ha b (Set.mem_univ b)
  contradiction

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

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
f : α → β
s : Set ↑(range f)
y : ↑(range f)
m : y ∈ s
⊢ ⟨f ↑⟨rangeSplitting f y, ⋯⟩, ⋯⟩ ∈ s

Tactic:
simpa [apply_rangeSplitting f] using m

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : ¬a < b
⊢ Ioo a b = Ioc a b

Tactic:
by rw [Ioo_eq_empty h, Ioc_eq_empty h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α × Set β
⊢ (fun s ↦ (Sum.inl ⁻¹' s, Sum.inr ⁻¹' s)) ((fun s ↦ Sum.inl '' s.1 ∪ Sum.inr '' s.2) s) = s

Tactic:
simp [preimage_image_eq _ Sum.inl_injective, preimage_image_eq _ Sum.inr_injective]

Goal state after:
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: ι : Sort u_4
α : Type u_5
inst✝ : SemilatticeSup α
f g : ι → α
h : BddAbove (range fun x ↦ f x ⊔ g x)
⊢ BddAbove (range f)

Tactic:
by
  have ⟨b, hb⟩ := h
  exact ⟨b, fun a ⟨i, ha⟩ ↦ ha ▸ le_sup_left.trans (hb ⟨i, rfl⟩)⟩

Goal state after:
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝² : Ring A
inst✝¹ : PartialOrder A
inst✝ : IsStrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ ¬↑n = 0

Tactic:
apply ne_of_gt

Goal state after:
A : Type u_1
e : A
n : ℕ
inst✝² : Ring A
inst✝¹ : PartialOrder A
inst✝ : IsStrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ 0 < ↑n
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ 1 / a ≤ 1 / b ↔ b ≤ a

Tactic:
simpa [one_div] using inv_le_inv_of_neg ha hb

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b

Tactic:
by
  rcases lt_trichotomy b 0 with (hb | rfl | hb)
  · simp [hb, hb.not_gt, one_le_div_of_neg]
  · simp [zero_lt_one.not_ge]
  · simp [hb, hb.not_gt, one_le_div]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
⊢ SublistForall₂ R l₁ l₂

Tactic:
obtain ⟨l, hl1, hl2⟩ := h

Goal state after:
case mpr
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ l : List β
hl1 : Forall₂ R l₁ l
hl2 : l <+ l₂
⊢ SublistForall₂ R l₁ l₂
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
⊢ n ≤ l.length - 1

Tactic:
exact Nat.le_sub_one_of_lt h

Goal state after:
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case inl.intro
α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m < l₁.length
hn : n < l₂.length
hnm : l₂[n] = l₁[m]
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
rw [← perm_cons l₁[m], rel_congr_left (getElem_cons_eraseIdx_perm ..), ← hnm,
        rel_congr_right (getElem_cons_eraseIdx_perm ..)]

Goal state after:
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
o₁ o₂ : Option α
p : o₁.toList ~ o₂.toList
⊢ o₁ = o₂

Tactic:
rcases o₁ with - | a <;> rcases o₂ with - | b

Goal state after:
case none.none
α : Type u_1
p : none.toList ~ none.toList
⊢ none = none

case none.some
α : Type u_1
b : α
p : none.toList ~ (some b).toList
⊢ none = some b

case some.none
α : Type u_1
a : α
p : (some a).toList ~ none.toList
⊢ some a = none

case some.some
α : Type u_1
a b : α
p : (some a).toList ~ (some b).toList
⊢ some a = some b
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f : α → M
l : List α
⊢ (map f (filter (fun b ↦ decide (p b)) l)).prod * (map f (filter (fun x ↦ decide ¬p x) l)).prod = (map f l).prod

Tactic:
rw [← prod_map_ite]
  simp only [ite_self]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Injective f
x : α
xs : List α
y : α
ys : List α
hxy : map f (x :: xs) = map f (y :: ys)
⊢ x :: xs = y :: ys

Tactic:
injection hxy with hxy hxys
    rw [h hxy, h.list_map hxys]

Goal state after: