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

Goal state before:
pp: 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✝ }

Tactic:
grind [→ Array.sizeOf_lt_of_mem]

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

Goal state before:
pp: 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✝ }

Tactic:
grind [→ Array.sizeOf_lt_of_mem]

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

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
ih : motive n
h : ¬(n = 0 → b = true)
⊢ n = 0 ∧ b = false

Tactic:
cases n <;> cases b <;> simp at h ⊢

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : α → Prop
⊢ (∃ a, P a) ∨ ∀ (a : α), ¬P a

Tactic:
← not_exists

Goal state after:
α : Sort u_1
P : α → Prop
⊢ (∃ a, P a) ∨ ¬∃ x, P x
Module: Mathlib.Logic.Function.Conjugate

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : Std.IdempotentOp gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x : α
⊢ f (ga x x) = f x

Tactic:
by rw [h.eq, Std.IdempotentOp.idempotent (op := gb)]

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

Goal state before:
pp: R : Type u_4
S : Type u_5
T : Type u_6
inst✝⁸ : Monoid S
inst✝⁷ : MulOneClass T
inst✝⁶ : SMul R S
inst✝⁵ : SMul R T
inst✝⁴ : MulAction S T
inst✝³ : IsScalarTower R S S
inst✝² : IsScalarTower R T T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul R T
⊢ Injective ((fun x ↦ x • 1) ∘ fun r ↦ r • 1)

Tactic:
simpa [Function.comp_def, one_smul, ← faithfulSMul_iff_injective_smul_one]

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

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝¹ : (i : I) → Mul (f i)
inst✝ : ∀ (i : I), IsMulCommutative (f i)
x✝¹ x✝ : (i : I) → f i
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
by ext; apply mul_comm'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mul γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
⊢ extend f (g₁ * g₂) (e₁ * e₂) = extend f g₁ e₁ * extend f g₂ e₂

Tactic:
funext x
  simp [Function.extend_def, apply_dite₂]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Div γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
⊢ extend f (g₁ / g₂) (e₁ / e₂) = extend f g₁ e₁ / extend f g₂ e₂

Tactic:
funext x
  simp [Function.extend_def, apply_dite₂]

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder α
x✝ : α × β
a : α
b : β
⊢ ∃ b_1, b_1 < (a, b)

Tactic:
obtain ⟨c, h⟩ := exists_lt a
    exact ⟨(c, b), Prod.mk_lt_mk_iff_left.2 h⟩

Goal state after:
Module: Mathlib.Tactic.CongrExclamation

Goal state before:
pp: x y : Prop
p : x = y → Prop
h : ∀ (he : x ↔ y), p ⋯
he : x = y
⊢ p he

Tactic:
by
  cases he
  exact h Iff.rfl

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
p : α → Prop
ha : a ≤ b → p a
hb : b ≤ a → p b
⊢ p (min a b)

Tactic:
by
  obtain hab | hba := le_total a b <;> simp [min_eq_left, min_eq_right, *]

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

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

Tactic:
Int.natCast_mul,

Goal state after:
n m : ℕ
⊢ ↑m * ↑2 ≤ ↑n ↔ ↑m * 2 ≤ ↑n
Module: Mathlib.Order.Compare

Goal state before:
pp: o o' : Ordering
⊢ o.swap = o' ↔ o = o'.swap

Tactic:
← swap_inj,

Goal state after:
o o' : Ordering
⊢ o.swap.swap = o'.swap ↔ o = o'.swap
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ ¬s ⊆ t ↔ ∃ x, x ∈ s ∧ ¬x ∈ t

Tactic:
by simp [subset_def]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case mpr
α : Type u
inst✝ : SemilatticeSup α
a c : α
⊢ a ≤ a ⊔ c

Tactic:
exact le_sup_left

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case mk.mk
α : Type u_1
toSemilatticeSup✝¹ : SemilatticeSup α
inf✝¹ : α → α → α
inf_le_left✝¹ : ∀ (a b : α), inf✝¹ a b ≤ a
inf_le_right✝¹ : ∀ (a b : α), inf✝¹ a b ≤ b
le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝¹ b c
toSemilatticeSup✝ : SemilatticeSup α
inf✝ : α → α → α
inf_le_left✝ : ∀ (a b : α), inf✝ a b ≤ a
inf_le_right✝ : ∀ (a b : α), inf✝ a b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝ b c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ { toSemilatticeSup := toSemilatticeSup✝¹, inf := inf✝¹, inf_le_left := inf_le_left✝¹, inf_le_right := inf_le_right✝¹,
      le_inf := le_inf✝¹ } =
    { toSemilatticeSup := toSemilatticeSup✝, inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝,
      le_inf := le_inf✝ }

Tactic:
cases SemilatticeSup.ext H

Goal state after:
case mk.mk.refl
α : Type u_1
toSemilatticeSup✝ : SemilatticeSup α
inf✝¹ : α → α → α
inf_le_left✝¹ : ∀ (a b : α), inf✝¹ a b ≤ a
inf_le_right✝¹ : ∀ (a b : α), inf✝¹ a b ≤ b
le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝¹ b c
inf✝ : α → α → α
inf_le_left✝ : ∀ (a b : α), inf✝ a b ≤ a
inf_le_right✝ : ∀ (a b : α), inf✝ a b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf✝ b c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ { toSemilatticeSup := toSemilatticeSup✝, inf := inf✝¹, inf_le_left := inf_le_left✝¹, inf_le_right := inf_le_right✝¹,
      le_inf := le_inf✝¹ } =
    {
      toSemilatticeSup :=
        { toSemilatticeSup := toSemilatticeSup✝, inf := inf✝¹, inf_le_left := inf_le_left✝¹,
            inf_le_right := inf_le_right✝¹, le_inf := le_inf✝¹ }.toSemilatticeSup,
      inf := inf✝, inf_le_left := inf_le_left✝, inf_le_right := inf_le_right✝, le_inf := le_inf✝ }
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Max α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
a b : α
⊢ f a ≤ f a ⊔ f b

Tactic:
exact le_sup_left

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

Goal state before:
pp: ⊢ (fun x1 x2 ↦ max x1 x2) = or

Tactic:
dsimp

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

Goal state before:
pp: ⊢ (fun x1 x2 ↦ min x1 x2) = and

Tactic:
dsimp

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

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

Tactic:
exact le_sup_left

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

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a : α
⊢ a ≤ ⊤ᶜ ↔ a ≤ ⊥

Tactic:
by rw [le_compl_iff_disjoint_right, disjoint_top, le_bot_iff]

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

Goal state before:
pp: 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_9
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : p x
⊢ (fun a ↦ if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩) (Sum.elim Subtype.val Subtype.val (Sum.inl ⟨x, hx⟩)) =
    Sum.inl ⟨x, hx⟩

Tactic:
dsimp

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_9
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : p x
⊢ (if h : p x then Sum.inl ⟨x, h⟩ else Sum.inr ⟨x, h⟩) = Sum.inl ⟨x, hx⟩
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: 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_9
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : ¬p x
⊢ (fun a ↦ if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩) (Sum.elim Subtype.val Subtype.val (Sum.inr ⟨x, hx⟩)) =
    Sum.inr ⟨x, hx⟩

Tactic:
dsimp

Goal state after:
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_9
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : ¬p x
⊢ (if h : p x then Sum.inl ⟨x, h⟩ else Sum.inr ⟨x, h⟩) = Sum.inr ⟨x, hx⟩
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_9
p : α → Prop
inst✝ : DecidablePred p
a : α
⊢ Sum.elim Subtype.val Subtype.val ((fun a ↦ if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩) a) = a

Tactic:
dsimp

Goal state after:
α✝ : 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_9
p : α → Prop
inst✝ : DecidablePred p
a : α
⊢ Sum.elim Subtype.val Subtype.val (if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩) = a
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
r a : α
⊢ swapCore a a r = r

Tactic:
unfold swapCore

Goal state after:
α : Sort u_1
inst✝ : DecidableEq α
r a : α
⊢ (if r = a then a else if r = a then a else r) = r
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ swapCore a b (swapCore a b r) = r

Tactic:
unfold swapCore

Goal state after:
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ (if (if r = a then b else if r = b then a else r) = a then b
    else if (if r = a then b else if r = b then a else r) = b then a else if r = a then b else if r = b then a else r) =
    r
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ swapCore a b r = swapCore b a r

Tactic:
unfold swapCore

Goal state after:
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ (if r = a then b else if r = b then a else r) = if r = b then a else if r = a then b else r
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
W : Set γ
f : α × β → γ
⊢ s ×ˢ t ⊆ f ⁻¹' W ↔ ∀ (a : α) (b : β), a ∈ s → b ∈ t → f (a, b) ∈ W

Tactic:
by simp [subset_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ t ⊆ f '' s ↔ ∃ u, u ⊆ s ∧ f '' u = t

Tactic:
by
  refine ⟨fun h ↦ ⟨f ⁻¹' t ∩ s, inter_subset_right, ?_⟩,
    fun ⟨u, hu, hu'⟩ ↦ hu'.symm ▸ image_mono hu⟩
  rwa [image_preimage_inter, inter_eq_left]

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
⊢ s ×ˢ t = s₁ ×ˢ t₁ → s = s₁ ∧ t = t₁

pp: case mpr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s = s₁ ∧ t = t₁ → s ×ˢ t = s₁ ×ˢ t₁

Tactic:
· intro heq
    have h₁ : (s₁ ×ˢ t₁ : Set _).Nonempty := by rwa [← heq]
    rw [prod_nonempty_iff] at h h₁
    rw [← fst_image_prod s h.2, ← fst_image_prod s₁ h₁.2, heq, eq_self_iff_true, true_and, ←
      snd_image_prod h.1 t, ← snd_image_prod h₁.1 t₁, heq]

Goal state after:
case mpr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s = s₁ ∧ t = t₁ → s ×ˢ t = s₁ ×ˢ t₁
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set (α ⊕ β)
⊢ id ⁻¹' s = s

Tactic:
preimage_id

Goal state after:
α : Type u_1
β : Type u_2
s : Set (α ⊕ β)
⊢ s = s
Module: Mathlib.Data.Set.Image

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

Tactic:
preimage_id

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
⊢ s = s
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : IsMulTorsionFree N
f : M →* N
hf : Injective ⇑f
n : ℕ
hn : n ≠ 0
x y : M
hxy : (fun a ↦ a ^ n) x = (fun a ↦ a ^ n) y
⊢ (fun a ↦ a ^ n) (f x) = (fun a ↦ a ^ n) (f y)

Tactic:
by
    simpa using congrArg f hxy

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

Goal state before:
pp: case mp.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
ht : t.Nonempty
⊢ SurjOn f s t → ∃ s', s' ⊆ s ∧ BijOn f s' t

Tactic:
intro h
      have : Nonempty α := ⟨Classical.choose (h.comap_nonempty ht)⟩
      exact ⟨_, h.mapsTo_invFunOn.image_subset, h.bijOn_subset⟩

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

Goal state before:
pp: F : Type u_7
G : Type u_8
H : Type u_9
inst✝³ : Group G
inst✝² : MulOneClass H
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : ∀ (a : G), f a = 1 → a = 1
x y : G
hxy : f x = f y
⊢ f (x * y⁻¹) = 1

Tactic:
by rw [map_mul, hxy, ← map_mul, mul_inv_cancel, map_one]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommSemigroup G
a b c d : G
⊢ a * b * (c * d) = a * c * (b * d)

Tactic:
by
  simp only [mul_left_comm, mul_assoc]

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

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₂
inst✝¹ : One M₂
inst✝ : MulOneClass M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ 1 * f x = f x

Tactic:
← one,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₂
inst✝¹ : One M₂
inst✝ : MulOneClass M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ f 1 * f x = f x
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₂
inst✝¹ : One M₂
inst✝ : MulOneClass M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ f x * 1 = f x

Tactic:
← one,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₂
inst✝¹ : One M₂
inst✝ : MulOneClass M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ f x * f 1 = f x
Module: Mathlib.Algebra.Group.Units.Defs

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

Tactic:
rw [← a.commute_inv_coe.mul_pow]; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
⊢ f a c = f a b * f b c

Tactic:
have hmul' : ∀ {b c}, r b c → p a b → p b c → p a c → f a c = f a b * f b c := by
    intro b c rbc pab pbc pac
    obtain rab | rba := total_of r a b
    · exact hmul rab rbc pab pbc pac
    rw [← one_mul (f a c), ← hf_swap pab, mul_assoc]
    obtain rac | rca := total_of r a c
    · rw [hmul rba rac (symm pab) pac pbc]
    · rw [hmul rbc rca pbc (symm pac) (symm pab), mul_assoc, hf_swap (symm pac), mul_one]
  obtain rbc | rcb := total_of r b c
  · exact hmul' rbc pab pbc pac
  · rw [hmul' rcb pac (symm pbc) pab, mul_assoc, hf_swap (symm pbc), mul_one]

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:
← inv_mul_eq_one,

Goal state after:
α : Type u
inst✝ : Monoid α
u : αˣ
a : α
⊢ ↑u * a = 1 ↔ ↑u⁻¹⁻¹ * a = 1
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝⁵ : MulZeroOneClass α
inst✝⁴ : MulZeroOneClass β✝
inst✝³ : MulZeroOneClass γ
inst✝² : MulZeroOneClass δ
inst✝¹ : FunLike F α β✝
β : Type ?u.21
inst✝ : CommMonoidWithZero β
f g : α →*₀ β
⊢ (↑(↑f * ↑g)).toFun 0 = 0

Tactic:
dsimp

Goal state after:
F : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝⁵ : MulZeroOneClass α
inst✝⁴ : MulZeroOneClass β✝
inst✝³ : MulZeroOneClass γ
inst✝² : MulZeroOneClass δ
inst✝¹ : FunLike F α β✝
β : Type ?u.21
inst✝ : CommMonoidWithZero β
f g : α →*₀ β
⊢ f 0 * g 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x y : β
⊢ g • (x / y) = g • x / g • y

Tactic:
by
  rw [div_eq_mul_inv, div_eq_mul_inv, smul_mul', smul_inv₀']

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

Goal state before:
pp: n a : ℕ
⊢ a = n.sqrt ↔ a ^ 2 ≤ n ∧ n < (a + 1) ^ 2

Tactic:
by
  simpa only [Nat.pow_two] using eq_sqrt

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

Goal state before:
pp: case inr
a b c : ℕ
h : a = b * c
cb : c ≤ b
⊢ b ≤ a.sqrt ∨ c ≤ a.sqrt

Tactic:
exact Or.inr <| le_sqrt.mpr <| h ▸ mul_le_mul_right c cb

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

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
a : α
n : ℕ
⊢ n • a = a * ↑n

Tactic:
induction n with
  | zero => rw [zero_nsmul, Nat.cast_zero, mul_zero]
  | succ n ih => rw [succ_nsmul, ih, Nat.cast_succ, mul_add, mul_one]

Goal state after:
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: α : Type u_3
inst✝ : Group α
f : Multiplicative ℤ →* α
n : Multiplicative ℤ
⊢ f n = f (ofAdd 1) ^ toAdd n

Tactic:
← zpowersHom_symm_apply,

Goal state after:
α : Type u_3
inst✝ : Group α
f : Multiplicative ℤ →* α
n : Multiplicative ℤ
⊢ f n = (zpowersHom α).symm f ^ toAdd n
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: β : Type u_4
inst✝ : AddGroup β
f : ℤ →+ β
n : ℤ
⊢ f n = n • (zmultiplesHom β).symm f

Tactic:
← zmultiplesHom_apply,

Goal state after:
β : Type u_4
inst✝ : AddGroup β
f : ℤ →+ β
n : ℤ
⊢ f n = ((zmultiplesHom β) ((zmultiplesHom β).symm f)) n
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : M
⊢ SMul.smul 0 a = 0

Tactic:
SMul.smul,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : M
⊢ ↑0 • a = 0
Module: Mathlib.Order.MinMax

Goal state before:
pp: case inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hf : Monotone f
h : a ≤ b
⊢ f (max a b) = max (f a) (f b)

Tactic:
simp [h, hf h]

Goal state after:
Module: Mathlib.Order.MinMax

Goal state before:
pp: case inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hf : Monotone f
h : b ≤ a
⊢ f (max a b) = max (f a) (f b)

Tactic:
simp [h, hf h]

Goal state after:
Module: Mathlib.Order.MinMax

Goal state before:
pp: case inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hf : Antitone f
h : a ≤ b
⊢ f (max a b) = min (f a) (f b)

Tactic:
simp [h, hf h]

Goal state after:
Module: Mathlib.Order.MinMax

Goal state before:
pp: case inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hf : Antitone f
h : b ≤ a
⊢ f (max a b) = min (f a) (f b)

Tactic:
simp [h, hf h]

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

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : IsMulCommutative α
inst✝ : PartialOrder α
a : α
ha : MulLECancellable a
b c : α
h : (fun x ↦ x * a) b = (fun x ↦ x * a) c
⊢ (fun x ↦ a * x) b = (fun x ↦ a * x) c

Tactic:
dsimp

Goal state after:
α : Type u_1
inst✝² : Mul α
inst✝¹ : IsMulCommutative α
inst✝ : PartialOrder α
a : α
ha : MulLECancellable a
b c : α
h : (fun x ↦ x * a) b = (fun x ↦ x * a) c
⊢ a * b = a * c
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
⊢ c * a ≤ c * b

Tactic:
obtain ⟨d, hcd⟩ := exists_add_of_le hc
  refine le_of_add_le_add_right (a := d * b + d * a) ?_
  calc
    _ = d * b := by rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
    _ ≤ d * a := by gcongr; exact hcd.trans_le <| add_le_of_nonpos_left hc
    _ = _ := by rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]

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

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

Tactic:
obtain ha | ha := hab.1.lt_or_gt <;> 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

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: case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b c : G₀
h : 0 ≤ a / b
hc : c ≠ 0
⊢ a * c / (b * c) ≤ a / b

Tactic:
· rw [mul_div_mul_right _ _ hc]

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

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b c : G₀
h : a / b ≤ 0
hc : c ≠ 0
⊢ a / b ≤ a * c / (b * c)

Tactic:
· rw [mul_div_mul_right _ _ hc]

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ a⁻¹ < b⁻¹ ↔ b < a

Tactic:
inv_lt_iff_one_lt_mul₀' ha,

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ 1 < a * b⁻¹ ↔ b < a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hb : 0 < b
hc : 0 < c
⊢ a ≤ c * b ↔ a / c ≤ b

Tactic:
div_le_iff₀' hc

Goal state after:
G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hb : 0 < b
hc : 0 < c
⊢ a ≤ c * b ↔ a ≤ c * b
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inr.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
have : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔
    (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1) := by
    simp [ha.le, ha.not_ge, hb, mabs_of_le_one, mabs_of_one_le]

Goal state after:
case inr.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
⊢ |a|ₘ = |a / b * b|ₘ

Tactic:
by rw [div_mul_cancel]

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
ha : 1 < a
⊢ 1 < |a|ₘ ↔ a ≠ 1

Tactic:
· simp [mabs_of_one_lt ha, ha, ha.ne']

Goal state after: