mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : x = y
⊢ ∃ y, y ≠ x

Tactic:
← hx

Goal state after:
case pos
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : x ≠ y'
hx : x = y
⊢ ∃ y, y ≠ x
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
r p q : α → Prop
⊢ (∃ x x_1, r x) ↔ (∃ x x_1, r x) ∨ ∃ x x_1, r x

Tactic:
simp only [exists_prop]

Goal state after:
α : Sort u_1
r p q : α → Prop
⊢ (∃ x, (p x ∨ q x) ∧ r x) ↔ (∃ x, p x ∧ r x) ∨ ∃ x, q x ∧ r x
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
⊢ f (invFun f b) = f (g b)

Tactic:
by
        rw [hg b]
        exact invFun_eq ⟨g b, hg b⟩

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

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (∀ (x : α), p x (update f a b x)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)

Tactic:
rw [← and_forall_ne a, update_self]
  simp +contextual

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
hf : FactorsThrough g f
e' : β → γ
a : α
⊢ extend f g e' (f a) = g a

Tactic:
classical
  simp only [extend_def, dif_pos, exists_apply_eq_apply]
  exact hf (Classical.choose_spec (exists_apply_eq_apply f a))

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (TransGen p on f)
⊢ TransGen r ≤ (TransGen p on f)

Tactic:
intro _ _ hab
  simpa [transGen_eq_self] using hab.lift f h

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

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
h : ∀ (x : M) (y : N), x • 1 * y = x • y
x : M
y z : N
⊢ x • (y * z) = x • y • z

Tactic:
smul_eq_mul

Goal state after:
M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
h : ∀ (x : M) (y : N), x • 1 * y = x • y
x : M
y z : N
⊢ x • (y * z) = x • (y * z)
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : One γ
f : α → β
x✝ : β
⊢ extend f 1 1 x✝ = 1 x✝

Tactic:
apply ite_self

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a b : α
⊢ ¬a < b ↔ a ≤ b → b ≤ a

Tactic:
by
  simp [not_lt_iff_not_le_or_ge, or_iff_not_imp_left]

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

Goal state before:
pp: n m : ℕ
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

Tactic:
rcases le_or_gt n m with h | h

Goal state after:
case inl
n m : ℕ
h : n ≤ m
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

case inr
n m : ℕ
h : m < n
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: n m : ℕ
⊢ ↑m * ↑2 ≤ ↑n ↔ ↑m * 2 ≤ ↑n

Tactic:
Int.ofNat_two

Goal state after:
n m : ℕ
⊢ ↑m * 2 ≤ ↑n ↔ ↑m * 2 ≤ ↑n
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case step
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
m✝ : ℕ
hmk : m.le m✝
ih : leRec refl le_succ_of_le ⋯ = leRec (leRec refl (fun x h ↦ le_succ_of_le h) hnm) (fun x h ↦ le_succ_of_le ⋯) hmk
⊢ le_succ_of_le ⋯ (leRec (leRec refl (fun x h ↦ le_succ_of_le h) hnm) (fun x h ↦ le_succ_of_le ⋯) hmk) =
    leRec (leRec refl (fun x h ↦ le_succ_of_le h) hnm) (fun x h ↦ le_succ_of_le ⋯) ⋯

Tactic:
leRec_succ

Goal state after:
case step
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
m✝ : ℕ
hmk : m.le m✝
ih : leRec refl le_succ_of_le ⋯ = leRec (leRec refl (fun x h ↦ le_succ_of_le h) hnm) (fun x h ↦ le_succ_of_le ⋯) hmk
⊢ le_succ_of_le ⋯ (leRec (leRec refl (fun x h ↦ le_succ_of_le h) hnm) (fun x h ↦ le_succ_of_le ⋯) hmk) =
    le_succ_of_le ⋯ (leRec (leRec refl (fun x h ↦ le_succ_of_le h) hnm) (fun x h ↦ le_succ_of_le ⋯) ?step.h1)

case step.h1
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
m✝ : ℕ
hmk : m.le m✝
ih : leRec refl le_succ_of_le ⋯ = leRec (leRec refl (fun x h ↦ le_succ_of_le h) hnm) (fun x h ↦ le_succ_of_le ⋯) hmk
⊢ m ≤ m✝
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: m n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
mn : m ≤ n
msn : m ≤ n + 1
⊢ leRec (motive := fun {n} mn ↦
      {motive : (m : ℕ) → m ≤ n → Sort u_1} →
        ((k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → motive n ⋯ → motive m mn)
      (fun {motive} of_succ self ↦ self)
      (fun ⦃k⦄ h ih {motive} of_succ self ↦ ih (fun i hi ↦ of_succ i ⋯) (of_succ k ⋯ self)) msn of_succ self =
    leRec (motive := fun {n} mn ↦
      {motive : (m : ℕ) → m ≤ n → Sort u_1} →
        ((k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → motive n ⋯ → motive m mn)
      (fun {motive} of_succ self ↦ self)
      (fun ⦃k⦄ h ih {motive} of_succ self ↦ ih (fun i hi ↦ of_succ i ⋯) (of_succ k ⋯ self)) mn (fun x x_1 ↦ of_succ x ⋯)
      (of_succ n ⋯ self)

Tactic:
leRec_succ

Goal state after:
m n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
mn : m ≤ n
msn : m ≤ n + 1
⊢ leRec (motive := fun {n} mn ↦
      {motive : (m : ℕ) → m ≤ n → Sort u_1} →
        ((k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → motive n ⋯ → motive m mn)
      (fun {motive} of_succ self ↦ self)
      (fun ⦃k⦄ h ih {motive} of_succ self ↦ ih (fun i hi ↦ of_succ i ⋯) (of_succ k ⋯ self)) ?h1 (fun i hi ↦ of_succ i ⋯)
      (of_succ n ⋯ self) =
    leRec (motive := fun {n} mn ↦
      {motive : (m : ℕ) → m ≤ n → Sort u_1} →
        ((k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → motive n ⋯ → motive m mn)
      (fun {motive} of_succ self ↦ self)
      (fun ⦃k⦄ h ih {motive} of_succ self ↦ ih (fun i hi ↦ of_succ i ⋯) (of_succ k ⋯ self)) mn (fun x x_1 ↦ of_succ x ⋯)
      (of_succ n ⋯ self)

case h1
m n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
mn : m ≤ n
msn : m ≤ n + 1
⊢ m ≤ n
Module: Mathlib.Order.Monotone.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
⊢ Injective f

Tactic:
grind [Injective]

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
y : α
⊢ y ∈ s

Tactic:
Subsingleton.elim y x

Goal state after:
α : Type u
s : Set α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
y : α
⊢ x ∈ s
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
hs : s.Nonempty
⊢ s = ∅ ∨ s = {a} ∨ s = {b} ∨ s = {a, b} ↔ s = {a} ∨ s = {b} ∨ s = {a, b}

Tactic:
or_iff_right

Goal state after:
α : Type u_1
s : Set α
a b : α
hs : s.Nonempty
⊢ s = {a} ∨ s = {b} ∨ s = {a, b} ↔ s = {a} ∨ s = {b} ∨ s = {a, b}

α : Type u_1
s : Set α
a b : α
hs : s.Nonempty
⊢ ¬s = ∅
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
b : α
⊢ b ⊔ b ⊓ (b ⊔ b) = b

Tactic:
rw [sup_inf_self]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
b : α
⊢ b ⊓ b = b ⊓ (b ⊔ b ⊓ b)

Tactic:
rw [sup_inf_self]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : DistribLattice α
a b c : α
⊢ a ⊓ (a ⊓ b ⊔ c) = (a ⊔ a ⊓ b) ⊓ (a ⊓ b ⊔ c)

Tactic:
rw [sup_inf_self]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
⊢ LinearOrder α

Tactic:
let min := e.min

Goal state after:
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
⊢ LinearOrder α
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
⊢ SemilatticeSup α

Tactic:
apply e.injective.semilatticeSup

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
⊢ SemilatticeInf α

Tactic:
let min := e.min

Goal state after:
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
⊢ SemilatticeInf α
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
rw [sup_inf_self]

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
p : α ⊕ β → Prop
⊢ RightInverse
    (fun x ↦
      match x with
      | inl a => ⟨inl ↑a, ⋯⟩
      | inr b => ⟨inr ↑b, ⋯⟩)
    fun x ↦
    match x with
    | ⟨inl a, h⟩ => inl ⟨a, h⟩
    | ⟨inr b, h⟩ => inr ⟨b, h⟩

Tactic:
by rintro (a | b) <;> rfl

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

Goal state before:
pp: case pos
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x✝ : { x // x ∘ Subtype.val = x₀ }
x : α → β
hx : x ∘ Subtype.val = x₀
a : α
h✝ : p a
⊢ x₀ ⟨a, h✝⟩ = x a

Tactic:
← hx

Goal state after:
case pos
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x✝ : { x // x ∘ Subtype.val = x₀ }
x : α → β
hx : x ∘ Subtype.val = x₀
a : α
h✝ : p a
⊢ (x ∘ Subtype.val) ⟨a, h✝⟩ = x a
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
a c d : α
h : swap a c = swap a d
⊢ (swap a d) a = d

Tactic:
Equiv.swap_apply_left

Goal state after:
α : Sort u_1
inst✝ : DecidableEq α
a c d : α
h : swap a c = swap a d
⊢ d = d
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case mp.inl
α : Type u_9
inst✝ : DecidableEq α
s : Set α
j : α
hj : ¬j ∈ s
a : α
ha hi : a ∈ s
⊢ j ∈ insert j s \ {a}

Tactic:
exact ⟨.inl rfl, (ne_of_mem_of_not_mem hi hj).symm⟩

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by rw [symmDiff_right_inj]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f ∘ Subtype.val '' Subtype.val ⁻¹' t = f '' (t ∩ s)

Tactic:
image_comp,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' Subtype.val '' Subtype.val ⁻¹' t = f '' (t ∩ s)
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ f ∘ Subtype.val '' 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 : α → β
⊢ f '' Subtype.val '' Subtype.val ⁻¹' s = (fun a ↦ ↑a) '' Subtype.val ⁻¹' f '' s
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
⊢ s.piecewise f g x ∈ f '' s ∪ g '' sᶜ

Tactic:
by_cases h : x ∈ s <;> [left; right]

Goal state after:
case pos
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : x ∈ s
⊢ s.piecewise f g x ∈ f '' s

case neg
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : ¬x ∈ s
⊢ s.piecewise f g x ∈ g '' sᶜ
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : f ∈ {f | ∀ (x y : α), f x = f y}
a : α
⊢ ∃ a, const α a = f

Tactic:
exact ⟨f a, funext fun x ↦ hf _ _⟩

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 = h ∘ f '' f ⁻¹' s ∪ h ∘ 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 = h '' f '' f ⁻¹' s ∪ h ∘ 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 = h '' f '' f ⁻¹' s ∪ h ∘ 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 = h '' f '' f ⁻¹' s ∪ h '' g '' g ⁻¹' s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ BijOn f univ univ ↔ Bijective f

Tactic:
by simp [Bijective, BijOn]

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

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
h✝ : t₂.Nonempty
x✝ : β₁
h : x✝ ∈ t₁
⊢ x✝ ∈ Prod.fst '' t₁ ×ˢ t₂

Tactic:
by simpa [h]

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

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
h✝ : t₁.Nonempty
x✝ : β₂
h : x✝ ∈ t₂
⊢ x✝ ∈ Prod.snd '' t₁ ×ˢ t₂

Tactic:
by simpa [h]

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

Goal state before:
pp: case inl.inl
α : Type u_1
s : Set α
inst✝ : DecidableEq α
x : α
ha hb : x ∈ s
⊢ (swap x x) x ∈ s ↔ x ∈ s

Tactic:
simp [*, swap_apply_of_ne_of_ne]

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

Goal state before:
pp: case inl.inr
α : Type u_1
s : Set α
inst✝ : DecidableEq α
b : α
hb : b ∈ s
x : α
ha : x ∈ s
hxb : x ≠ b
⊢ (swap x b) x ∈ s ↔ x ∈ s

Tactic:
simp [*, swap_apply_of_ne_of_ne]

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

Goal state before:
pp: case inr.inl
α : Type u_1
s : Set α
inst✝ : DecidableEq α
a : α
ha : a ∈ s
x : α
hxa : x ≠ a
hb : x ∈ s
⊢ (swap a x) x ∈ s ↔ x ∈ s

Tactic:
simp [*, swap_apply_of_ne_of_ne]

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

Goal state before:
pp: case inr.inr
α : Type u_1
s : Set α
inst✝ : DecidableEq α
a b : α
ha : a ∈ s
hb : b ∈ s
x : α
hxa : x ≠ a
hxb : x ≠ b
⊢ (swap a b) x ∈ s ↔ x ∈ s

Tactic:
simp [*, swap_apply_of_ne_of_ne]

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

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
P : Prop
inst✝ : Decidable P
a : M
⊢ (a ^ if P then 1 else 0) = if P then a else 1

Tactic:
simp only [pow_ite, pow_one, pow_zero]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ b⁻¹ * a = d⁻¹ * c ↔ a * d = c * b

Tactic:
rw [← div_eq_inv_mul, ← div_eq_inv_mul, div_eq_div_iff_mul_eq_mul]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x : M
x✝ : IsUnit x
u : Mˣ
hu : ↑u = x
⊢ ∃ b, x * b = 1 ∧ b * x = 1

Tactic:
subst x

Goal state after:
M : Type u_1
inst✝ : Monoid M
u : Mˣ
x✝ : IsUnit ↑u
⊢ ∃ b, ↑u * b = 1 ∧ b * ↑u = 1
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
⊢ c (f ^ 0) = (c f)^[0]

Tactic:
rw [pow_zero, h1]

Goal state after:
M : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
⊢ id = (c f)^[0]
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a / (b * a) = b⁻¹

Tactic:
h.div_mul_cancel_right

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ b⁻¹ = b⁻¹
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
| c * b

Tactic:
hc

Goal state after:
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
| 1
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
a b : M₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : IsLeftCancelMulZero M₀
ha : a ≠ 0
⊢ a * b = a ↔ b = 1

Tactic:
by
  rw [Iff.comm, ← mul_right_inj' ha, mul_one]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a * a * a⁻¹ = a

Tactic:
by_cases h : a = 0
  · rw [h, inv_zero, mul_zero]
  · rw [mul_assoc, mul_inv_cancel₀ h, mul_one]

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

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

Tactic:
by
  induction n with
  | zero => simp
  | succ n ihn => simp only [← Int.add_assoc, zpow_add_one₀ ha, ihn, mul_assoc]
  | pred n ihn => rw [zpow_sub_one₀ ha, ← mul_assoc, ← ihn, ← zpow_sub_one₀ ha, Int.add_sub_assoc]

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

Goal state before:
pp: case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : ¬n = 0
ha : a = 0
⊢ a ^ (m + n) = a ^ m * a ^ n

pp: case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : ¬n = 0
ha : ¬a = 0
⊢ a ^ (m + n) = a ^ m * a ^ n

Tactic:
· subst a
    simp only [false_or, not_true, Ne, hm, hn, false_and, or_false] at h
    rw [zero_zpow _ h, zero_zpow _ hm, zero_mul]

Goal state after:
case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : ¬n = 0
ha : ¬a = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
Module: Mathlib.Algebra.GroupWithZero.Semiconj

Goal state before:
pp: case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : x = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
subst x

Goal state after:
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a y : G₀
ha : ¬a = 0
h : SemiconjBy a 0 y
⊢ SemiconjBy a 0⁻¹ y⁻¹
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case refine_3
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : (Contravariant M N μ fun x1 x2 ↦ x1 < x2) ∧ Contravariant M N μ fun x1 x2 ↦ x1 = x2
a : M
b c : N
bc : (fun x1 x2 ↦ x1 ≤ x2) (μ a b) (μ a c)
⊢ (fun x1 x2 ↦ x1 ≤ x2) b c

Tactic:
· exact bc.lt_or_eq.elim (fun bc ↦ (h.1 a bc).le) (fun bc ↦ (h.2 a bc).le)

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftMono α
⊢ a + b - (c + d) ≤ a - c + (b - d)

Tactic:
by
  rw [add_comm c, tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]
  refine (tsub_le_tsub_right add_tsub_le_assoc c).trans ?_
  rw [add_comm a, add_comm (a - c)]
  exact add_tsub_le_assoc

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.NatCast

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 3

Tactic:
rw [← two_add_one_eq_three]

Goal state after:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 2 + 1
Module: Mathlib.Algebra.Order.Monoid.NatCast

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftMono α
⊢ 0 < 3

Tactic:
rw [← two_add_one_eq_three]

Goal state after:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftMono α
⊢ 0 < 2 + 1
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : LinearOrder M₀
inst✝¹ : PosMulStrictMono M₀
a : M₀
n : ℕ
inst✝ : ZeroLEOneClass M₀
ha : 0 ≤ a
hn : n ≠ 0
h : a < 1
⊢ a ^ n < 1

Tactic:
exact pow_lt_one₀ ha h hn

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

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
a d : R
inst✝¹ : PosMulMono R
inst✝ : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
⊢ b * a ≤ max d b * max c a

Tactic:
by
    gcongr
    exacts [ha, hd.trans <| le_max_left d b, le_max_right d b, le_max_right c a]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
⊢ Injective f

Tactic:
intro x y hxy
  rcases trichotomous_of r x y with (h | h | h)
  · have := hf h
    rw [hxy] at this
    exfalso
    exact irrefl_of s (f y) this
  · exact h
  · have := hf h
    rw [hxy] at this
    exfalso
    exact irrefl_of s (f y) this

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

Goal state before:
pp: β : Type u_1
M : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
f : β → M
hf : Monotone f
n : ℕ
⊢ Monotone fun a ↦ f a ^ (n + 1)

Tactic:
simp_rw [pow_succ]
    exact (Monotone.pow_const hf _).mul' hf

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ |a * b|ₘ ≤ |a|ₘ * |b|ₘ

Tactic:
apply sup_le

Goal state after:
case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a * b ≤ |a|ₘ * |b|ₘ

case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a * b)⁻¹ ≤ |a|ₘ * |b|ₘ
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊔ b) ^ 2 = (a ⊓ b) * (a ⊔ b) * |b / a|ₘ

Tactic:
← sup_div_inf_eq_mabs_div,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊔ b) ^ 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) / (a ⊓ b))