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

Goal state after:
case mk
x : Nat × ArgReorder
perm✝ : Permutation
argReorders✝ : Array (Nat × ArgReorder)
h✝ : x ∈ { perm := perm✝, argReorders := argReorders✝ }.argReorders
⊢ sizeOf x.snd < sizeOf { perm := perm✝, argReorders := argReorders✝ }
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

Goal state after:
case mk
x : Nat × ArgReorder
perm✝ : Permutation
argReorders✝ : Array (Nat × 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 { perm := perm✝, argReorders := argReorders✝ }.perm)
h✝ : x ∈ { perm := perm✝, argReorders := argReorders✝ }.argReorders
⊢ sizeOf x.snd < sizeOf { perm := perm✝, argReorders := argReorders✝ }
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: case succ
M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
ih : SemiconjBy a (x ^ n) (y ^ n)
⊢ SemiconjBy a (x ^ (n + 1)) (y ^ (n + 1))

Tactic:
| succ n ih =>

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

Goal state before:
pp: case succ.succ
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
ih : n + 1 ≠ 0 → npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a
hn : n + 1 + 1 ≠ 0
⊢ npowRec (m + (n + 1 + 1)) a = npowRec m a * npowRec (n + 1 + 1) a

Tactic:
| succ n ih =>

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

Goal state before:
pp: case succ
M : Type u_2
inst✝ : Monoid M
a b : M
n : ℕ
ih : (a * b) ^ n * a = a * (b * a) ^ n
⊢ (a * b) ^ (n + 1) * a = a * (b * a) ^ (n + 1)

Tactic:
| succ n ih =>

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

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
a b c : G
⊢ a * b / c = a * (b / c)

Tactic:
by
  rw [div_eq_mul_inv, div_eq_mul_inv, mul_assoc]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α₁ α₂ : Sort u
β₁ : α₁ → Sort v
β₂ : α₂ → Sort v
f₁ : (a : α₁) → β₁ a
f₂ : (a : α₂) → β₂ a
a₁ : α₁
a₂ : α₂
hargs : a₁ ≍ a₂
ht : ∀ (t₁ : α₁) (t₂ : α₂), t₁ ≍ t₂ → β₁ t₁ = β₂ t₂
hf : α₁ = α₂ → β₁ ≍ β₂ → f₁ ≍ f₂
⊢ f₁ a₁ ≍ f₂ a₂

Tactic:
by
  cases hargs
  cases funext fun v => ht v v .rfl
  cases hf rfl .rfl
  rfl

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

Goal state before:
pp: α : Sort u
f : α → α
h : Involutive f
P : Prop
inst✝ : Decidable P
x : α
⊢ f (if P then x else f x) = if ¬P then x else f x

Tactic:
apply_ite f,

Goal state after:
α : Sort u
f : α → α
h : Involutive f
P : Prop
inst✝ : Decidable P
x : α
⊢ (if P then f x else f (f x)) = if ¬P then x else f x
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
⊢ ReflTransGen r a b ↔ a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b

Tactic:
use cases_head
  rintro (rfl | ⟨c, hac, hcb⟩)
  · rfl
  · exact head hac hcb

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.single
α : Type u_1
r : α → α → Prop
a✝² b✝¹ c : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a✝² c
d e : α
a✝¹ : ReflTransGen r a✝² d
hde : r d e
b✝ f b : α
a✝ : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : r f a
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a

Tactic:
rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩

Goal state after:
case tail.single
α : Type u_1
r : α → α → Prop
a✝² b✝¹ c✝ : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac✝ : ReflTransGen r a✝² c✝
d e : α
a✝¹ : ReflTransGen r a✝² d
hde : r d e
b✝ f b : α
a✝ : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : r f a
c : α
hbc : ReflGen r b c
hac : ReflTransGen r a c
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f g : α → α
hg : LeftInverse g f
n✝ n : ℕ
ihn : LeftInverse g^[n] f^[n]
⊢ LeftInverse (g ∘ g^[n]) (f^[n] ∘ f)

Tactic:
exact ihn.comp hg

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁸ : LinearOrder β
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Max α
inst✝⁴ : Min α
inst✝³ : Ord α
inst✝² : DecidableEq α
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x✝¹ x✝ : α
⊢ f (x✝¹ ⊓ x✝) = f (if f x✝¹ ≤ f x✝ then x✝¹ else x✝)

Tactic:
apply_ite f,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁸ : LinearOrder β
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Max α
inst✝⁴ : Min α
inst✝³ : Ord α
inst✝² : DecidableEq α
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x✝¹ x✝ : α
⊢ f (x✝¹ ⊓ x✝) = if f x✝¹ ≤ f x✝ then f x✝¹ else f x✝
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁸ : LinearOrder β
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Max α
inst✝⁴ : Min α
inst✝³ : Ord α
inst✝² : DecidableEq α
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x✝¹ x✝ : α
⊢ f (x✝¹ ⊔ x✝) = f (if f x✝¹ ≤ f x✝ then x✝ else x✝¹)

Tactic:
apply_ite f,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁸ : LinearOrder β
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Max α
inst✝⁴ : Min α
inst✝³ : Ord α
inst✝² : DecidableEq α
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x✝¹ x✝ : α
⊢ f (x✝¹ ⊔ x✝) = if f x✝¹ ≤ f x✝ then f x✝ else f x✝¹
Module: Mathlib.Order.RelClasses

Goal state before:
pp: case inl
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
hac : r a c
⊢ r a c

Tactic:
exact hac

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: case ind.ind
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α), a' ≤ a → Acc (fun x1 x2 ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
⊢ Acc (fun x1 x2 ↦ x1 < x2) (a', b)

Tactic:
| ind b ihb
     => 

Goal state after:
case ind.ind
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α), a' ≤ a → Acc (fun x1 x2 ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
⊢ Acc (fun x1 x2 ↦ x1 < x2) (a', b)
Module: Mathlib.Tactic.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
coeβα : β → α
condβα : α → Prop
coeδγ : δ → γ
condδγ : γ → Prop
inst✝¹ : CanLift α β coeβα condβα
inst✝ : CanLift γ δ coeδγ condδγ
⊢ ∀ (x : α × γ), condβα x.fst ∧ condδγ x.snd → ∃ y, map coeβα coeδγ y = x

Tactic:
rintro ⟨x, y⟩ ⟨hx, hy⟩
    rcases CanLift.prf (β := β) x hx with ⟨x, rfl⟩
    rcases CanLift.prf (β := δ) y hy with ⟨y, rfl⟩
    exact ⟨(x, y), by simp⟩

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

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℤ → α
hf : Antitone f
n a : ℤ
h1 : f (n + 1) < f a
h2 : f a < f n
⊢ False

Tactic:
exact (hf.reflect_lt h2).not_ge (Int.le_of_lt_add_one <| hf.reflect_lt h1)

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ≤ b ↔ ∃ c, b = a ⊔ c

Tactic:
by
  constructor
  · intro h
    exact ⟨b, (sup_eq_right.mpr h).symm⟩
  · rintro ⟨c, rfl : _ = _ ⊔ _⟩
    exact le_sup_left

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B

Tactic:
by
  cases A
  cases B
  cases PartialOrder.ext H
  congr
  ext; apply SemilatticeSup.ext_sup H

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ insert a (s \ insert a t) = insert a (s \ t)

Tactic:
by
  rw [← union_singleton (s := t), ← sdiff_sdiff, insert_sdiff_singleton]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
⊢ (fun e ↦
        ⟨{ toFun := fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e),
            invFun := fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩), left_inv := ⋯, right_inv := ⋯ },
          ⋯⟩)
      ((fun e ↦
          { toFun := fun a ↦ ⟨↑e (some a), ⋯⟩, invFun := fun b ↦ ((↑e).symm ↑b).get ⋯, left_inv := ⋯, right_inv := ⋯ })
        e) =
    e

Tactic:
by
    ext a
    cases a
    · simpa using e.property.symm
    · simp

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

Goal state before:
pp: α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
i : (a : α) × β a
f : (i : (a : α) × β a) → γ i.fst i.snd
x : γ i.fst i.snd
⊢ curry (update f i x) = update (curry f) i.fst (update (curry f i.fst) i.snd x)

Tactic:
obtain ⟨ia, ib⟩ := i
  ext ja jb
  unfold Sigma.curry
  obtain rfl | ha := eq_or_ne ia ja
  · simp
    grind
  · rw [Function.update_of_ne (ne_of_apply_ne Sigma.fst _), Function.update_of_ne]
    · exact ha.symm
    · exact ha.symm

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

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

Tactic:
sdiff_sup

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

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

Tactic:
by
        rw [sdiff_sup, sdiff_sdiff_right, sdiff_sdiff_right, sup_inf_left, sup_comm, sup_inf_sdiff,
          sup_inf_left, sup_comm (z \ y), sup_inf_sdiff]

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

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.14
β : Type ?u.13
t : α ⊕ β → Type u_9
⊢ RightInverse (Sum.elim (fun a ↦ ⟨inl a.fst, a.snd⟩) fun b ↦ ⟨inr b.fst, b.snd⟩) fun x ↦
    match x with
    | ⟨inl x, y⟩ => inl ⟨x, y⟩
    | ⟨inr x, y⟩ => inr ⟨x, y⟩

Tactic:
rintro (⟨x,y⟩|⟨x,y⟩)

Goal state after:
case inl
α✝ : 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.14
β : Type ?u.13
t : α ⊕ β → Type u_9
x : α
y : t (inl x)
⊢ (fun x ↦
        match x with
        | ⟨inl x, y⟩ => inl ⟨x, y⟩
        | ⟨inr x, y⟩ => inr ⟨x, y⟩)
      (Sum.elim (fun a ↦ ⟨inl a.fst, a.snd⟩) (fun b ↦ ⟨inr b.fst, b.snd⟩) (inl ⟨x, y⟩)) =
    inl ⟨x, y⟩

case inr
α✝ : 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.14
β : Type ?u.13
t : α ⊕ β → Type u_9
x : β
y : t (inr x)
⊢ (fun x ↦
        match x with
        | ⟨inl x, y⟩ => inl ⟨x, y⟩
        | ⟨inr x, y⟩ => inr ⟨x, y⟩)
      (Sum.elim (fun a ↦ ⟨inl a.fst, a.snd⟩) (fun b ↦ ⟨inr b.fst, b.snd⟩) (inr ⟨x, y⟩)) =
    inr ⟨x, y⟩
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : xᶜ = y
⊢ IsCompl x xᶜ

Tactic:
exact isCompl_compl

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

Goal state before:
pp: α' : Type u_9
β' : Type u_10
e : Perm α'
p : β' → Prop
inst✝ : DecidablePred p
f : α' ≃ Subtype p
a : α'
⊢ (e.extendDomain f) ↑(f a) = ↑(f (e a))

Tactic:
simp [Perm.extendDomain]

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

Goal state before:
pp: α' : Type u_9
β' : Type u_10
p : β' → Prop
inst✝ : DecidablePred p
f : α' ≃ Subtype p
⊢ extendDomain (Equiv.refl α') f = Equiv.refl β'

Tactic:
simp [Perm.extendDomain]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)

Tactic:
sdiff_sup

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b = c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a ≤ a ∆ b ↔ Disjoint a b

Tactic:
refine ⟨fun h => ?_, fun h => h.symmDiff_eq_sup.symm ▸ le_sup_left⟩
  rw [symmDiff_eq_sup_sdiff_inf] at h
  exact disjoint_iff_inf_le.mpr (le_sdiff_right.1 <| inf_le_of_left_le h).le

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

Goal state before:
pp: case succ
α : Type u_1
f : α → α
n : ℕ
ih : preimage f^[n] = (preimage f)^[n]
⊢ preimage f^[n + 1] = (preimage f)^[n + 1]

Tactic:
| succ n ih =>

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

Goal state before:
pp: case succ
α : Type u_1
f : α → α
n : ℕ
ih : image f^[n] = (image f)^[n]
⊢ image f^[n + 1] = (image f)^[n + 1]

Tactic:
| succ n ih =>

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

Goal state before:
pp: case succ
α : Type u_1
s : Set α
f : α → α
h : MapsTo f s s
x : ↑s
k : ℕ
ih : ↑((restrict f s s h)^[k] x) = f^[k] ↑x
⊢ ↑((restrict f s s h)^[k + 1] x) = f^[k + 1] ↑x

Tactic:
simp only [iterate_succ', comp_apply, val_restrict_apply, ih]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
hy : ¬y = x
⊢ {x}.piecewise f g y = update g x (f x) y

Tactic:
· simp [hy]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : (s₁ ×ˢ t₁).Nonempty
⊢ s = s₁ ∧ t = t₁

Tactic:
rw [prod_nonempty_iff] at h h₁

Goal state after:
case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
⊢ s = s₁ ∧ t = t₁
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : SurjOn f s t
u : β
⊢ u ∈ t → u ∈ f '' f ⁻¹' t

Tactic:
hu

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : SurjOn f s t
u : β
hu : u ∈ t
⊢ u ∈ f '' f ⁻¹' t
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a : ℤ
⊢ (-a.pred).pred = -a

Tactic:
rw [neg_pred, pred_succ]

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

Goal state before:
pp: case negSucc.succ
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive ↑i → motive (↑i + 1)
pred : ∀ (i : ℕ), motive (-↑i) → motive (-↑i - 1)
i n : ℕ
ih : motive (-↑n)
⊢ motive (-↑(n + 1))

Tactic:
| succ n ih =>

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

Goal state before:
pp: a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n + 1
⊢ -[m+1].ediv (↑n + 1) = -((- -[m+1] - 1) / (↑n + 1) + 1)

Tactic:
rw [show (- -[m+1] : ℤ) = (m + 1 : ℤ) by rfl]

Goal state after:
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n + 1
⊢ -[m+1].ediv (↑n + 1) = -((↑m + 1 - 1) / (↑n + 1) + 1)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (Int.negSucc m * ↑n) = a⁻¹ ^ ((m + 1) * n)

Tactic:
Int.negSucc_mul_ofNat,

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (-↑(m.succ * n)) = a⁻¹ ^ ((m + 1) * n)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case succ
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (g ^ ↑n)
⊢ P (g ^ (↑n + 1))

Tactic:
| succ n ih =>

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

Goal state before:
pp: case succ
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (g ^ ↑n)
⊢ P (g ^ (↑n + 1))

Tactic:
| succ n ih =>

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

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

Tactic:
by rw [← inv_mul_eq_one, inv_inv]

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 * (f ^ n).subtypePerm ⋯ = (f * f ^ n).subtypePerm ⋯

Tactic:
subtypePerm_mul

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:
| succ n ih =>

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

Goal state before:
pp: case succ
M₀ : Type u_1
G₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
a✝ : M₀
n✝ : ℕ
inst✝ : NoZeroDivisors M₀
a : M₀
x✝ : IsNilpotent a
n : ℕ
ih : a ^ n = 0 → a = 0
ha : a ^ (n + 1) = 0
⊢ a = 0

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case succ
R : Type u_1
inst✝ : AddMonoidWithOne R
m n : ℕ
ih : ↑(m + n) = ↑m + ↑n
⊢ ↑(m + (n + 1)) = ↑m + ↑(n + 1)

Tactic:
| succ n ih =>

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

Goal state before:
pp: case succ
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + ↑n) = a ^ m * a ^ ↑n
⊢ a ^ (m + (↑n + 1)) = a ^ m * a ^ (↑n + 1)

Tactic:
simp only [← Int.add_assoc, zpow_add_one₀ ha, ihn, mul_assoc]

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

Goal state before:
pp: n : ℕ
x : ℤ
⊢ (↑n + 1) * x = ↑n * x + x

Tactic:
Int.add_mul,

Goal state after:
n : ℕ
x : ℤ
⊢ ↑n * x + 1 * x = ↑n * x + x
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(subNatNat m n) = ↑m - ↑n

Tactic:
unfold subNatNat

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(match n - m with
      | 0 => ofNat (m - n)
      | k.succ => -[k+1]) =
    ↑m - ↑n
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: case succ
α : Type u
inst✝ : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = ↑n * a
⊢ (n + 1) • a = ↑(n + 1) * a

Tactic:
| succ n ih =>

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

Goal state before:
pp: m n : ℤ
| (m % n + n * (m / n)).gcd n

Tactic:
gcd_add_mul_left_left

Goal state after:
m n : ℤ
| (m % n).gcd n
Module: Mathlib.Data.Nat.Cast.Basic

Goal state before:
pp: case succ
α : Type u_1
inst✝ : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = a * ↑n
⊢ (n + 1) • a = a * ↑(n + 1)

Tactic:
| succ n ih =>

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Ring α
F : Type u_1
inst✝² : Ring β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
u : αˣ
⊢ ↑((map ↑f) (-u)) = ↑(-(map ↑f) u)

Tactic:
by simp only [coe_map, Units.val_neg, MonoidHom.coe_coe, map_neg]

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

Goal state before:
pp: case succ
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
n : ℕ
ih : ↑n • b = n • b
⊢ ↑(n + 1) • b = (n + 1) • b

Tactic:
| succ n ih =>

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

Goal state before:
pp: case succ
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : R
y : M
n : ℕ
ih : (n • x) • y = n • x • y
⊢ ((n + 1) • x) • y = (n + 1) • x • y

Tactic:
| succ n ih =>

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ a * (a + b) = 0

Tactic:
hab,

Goal state after:
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ a * 0 = 0
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ 0 = (a + b) * b

Tactic:
hab,

Goal state after:
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ 0 = 0 * b
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a : α
⊢ Odd (a - 2) ↔ Odd a

Tactic:
by
  rw [← odd_add_two (a := a - 2), add_comm_sub, sub_self, add_zero]

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c d : α
⊢ a / b < c / d ↔ a * d < c * b

Tactic:
simpa only [div_eq_mul_inv] using mul_inv_lt_mul_inv_iff'

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

Goal state before:
pp: case inl
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : a < 0
⊢ a * b ≠ 0

Tactic:
obtain hb | hb := hab.2.lt_or_gt

Goal state after:
case inl.inl
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : a < 0
hb : b < 0
⊢ a * b ≠ 0

case inl.inr
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : a < 0
hb : 0 < b
⊢ a * b ≠ 0
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: case inr
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : 0 < a
⊢ a * b ≠ 0

Tactic:
obtain hb | hb := hab.2.lt_or_gt

Goal state after:
case inr.inl
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : 0 < a
hb : b < 0
⊢ a * b ≠ 0

case inr.inr
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : 0 < a
hb : 0 < b
⊢ a * b ≠ 0
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b * c⁻¹ ≤ a ↔ b ≤ a * c

Tactic:
mul_inv_le_iff₀ hc

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b ≤ a * c ↔ b ≤ a * c