mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Antisymm r
a b : α
h₁ : Decidable.decide (r a b) = true
h₂ : Decidable.decide (r b a) = true
⊢ r b a

Tactic:
by simpa using h₂

Goal state after:
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Nontrivial α
x : α
⊢ ∃ y, y ≠ x

Tactic:
by
  classical
  exact Decidable.exists_ne x

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

Goal state before:
pp: α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f₁ f₂ : α → β
hf : f₁ = f₂
a'₁ a'₂ : α
ha' : a'₁ = a'₂
v₁ v₂ : β
hv : v₁ = v₂
a₁ a₂ : α
ha : a₁ = a₂
⊢ update f₁ a'₁ v₁ a₁ = update f₂ a'₂ v₂ a₂

Tactic:
subst hf; subst ha'; subst hv; subst ha; rfl

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ (r ∘r p ∘r q) a d → ((r ∘r p) ∘r q) a d

Tactic:
exact fun ⟨b, hab, c, hbc, hcd⟩ ↦ ⟨c, ⟨b, hab, hbc⟩, hcd⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r✝ : α → β → Prop
f✝ : α → γ
g : β → δ
c : γ
d : δ
r : α → α → Prop
inst✝ : Std.Symm r
f : α → β
x✝¹ x✝ : β
⊢ Relation.Map r f f x✝¹ x✝ → Relation.Map r f f x✝ x✝¹

Tactic:
by
    rintro ⟨x, y, hxy, rfl, rfl⟩
    exact ⟨y, x, symm hxy, rfl, rfl⟩

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
intro a _ hab
  induction hab with
  | single hac => exact TransGen.single (h a _ hac)
  | tail _ hcd hac => exact TransGen.tail hac (h _ _ hcd)

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_2.inr
α : Type u_1
r : α → α → Prop
a b : α
h : TransGen r a b
⊢ ReflTransGen r a b

Tactic:
· exact h.to_reflTransGen

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (ReflTransGen p on f)
i✝¹ i✝ : α
hab : ReflTransGen r i✝¹ i✝
⊢ (ReflTransGen p on f) i✝¹ i✝

Tactic:
simpa [reflTransGen_eq_self] using hab.lift f h

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
⊢ ReflGen (TransGen r) = ReflGen r

Tactic:
transGen_eq_self

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
⊢ ReflGen r = ReflGen r
Module: Mathlib.Logic.Function.Conjugate

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga ga' : α → α
gb gb' : β → β
h : Semiconj f ga gb
ha : RightInverse ga' ga
hb : LeftInverse gb' gb
x : α
⊢ f (ga' x) = gb' (f x)

Tactic:
by
  rw [← hb (f (ga' x)), ← h.eq, ha x]

Goal state after:
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.succ]

Tactic:
iterate_succ

Goal state after:
α : Type u
f g : α → α
hg : LeftInverse g f
n✝ n : ℕ
ihn : LeftInverse g^[n] f^[n]
⊢ LeftInverse (g ∘ g^[n]) (f^[n] ∘ f)
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^[n.succ] f^[n.succ]

Tactic:
rw [iterate_succ', iterate_succ]
    exact ihn.comp hg

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

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : SMul M α
inst✝³ : SMul N α
inst✝² : SMul M β
inst✝¹ : SMul N β
inst✝ : SMulCommClass M N β
f : α → β
hf : Injective f
h₁ : ∀ (c : M) (x : α), f (c • x) = c • f x
h₂ : ∀ (c : N) (x : α), f (c • x) = c • f x
c₁ : M
c₂ : N
x : α
⊢ f (c₁ • c₂ • x) = f (c₂ • c₁ • x)

Tactic:
by simp only [h₁, h₂, smul_comm c₁ c₂ (f x)]

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

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : a = g • b
⊢ g⁻¹ • g • b = b

Tactic:
inv_smul_smul

Goal state after:
G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : a = g • b
⊢ b = b
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : g • a = b
⊢ a = g⁻¹ • g • a

Tactic:
inv_smul_smul

Goal state after:
G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : g • a = b
⊢ a = a
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
G✝ : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
G : Type u_9
P : Type u_10
inst✝¹ : Group G
inst✝ : MulAction G P
a : G
b c : P
h : a • b = a • c
⊢ a⁻¹ • a • c = c

Tactic:
inv_smul_smul

Goal state after:
M : Type u_1
N : Type u_2
G✝ : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
G : Type u_9
P : Type u_10
inst✝¹ : Group G
inst✝ : MulAction G P
a : G
b c : P
h : a • b = a • c
⊢ c = c
Module: Mathlib.Logic.IsEmpty.Basic

Goal state before:
pp: α : Sort u_1
π : α → Sort u_4
⊢ IsEmpty ((a : α) → π a) ↔ ∃ a, IsEmpty (π a)

Tactic:
simp only [← not_nonempty_iff, Classical.nonempty_pi, not_forall]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
b : β
⊢ Function.Injective fun a ↦ (a, b)

Tactic:
intro b₁ b₂ h
  simpa only [and_true, eq_self_iff_true, mk_inj] using h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
b₁ b₂ : β
hb : g b₁ = g b₂
⊢ b₁ = b₂

Tactic:
by
      inhabit α
      injection @h (default, b₁) (default, b₂) (congr_arg (Prod.mk (f default)) hb :)

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Nonempty β
a b : α
⊢ const β a < const β b ↔ a < b

Tactic:
by simpa [Pi.lt_def] using le_of_lt

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

Goal state before:
pp: case false
f : Bool → Bool
x : Bool
h₁ : f true = false
⊢ f (f (f x)) = f x

Tactic:
cases h₂ : f false

Goal state after:
case false.false
f : Bool → Bool
x : Bool
h₁ : f true = false
h₂ : f false = false
⊢ f (f (f x)) = f x

case false.true
f : Bool → Bool
x : Bool
h₁ : f true = false
h₂ : f false = true
⊢ f (f (f x)) = f x
Module: Mathlib.Data.Bool.Basic

Goal state before:
pp: case true
f : Bool → Bool
x : Bool
h₁ : f true = true
⊢ f (f (f x)) = f x

Tactic:
cases h₂ : f false

Goal state after:
case true.false
f : Bool → Bool
x : Bool
h₁ : f true = true
h₂ : f false = false
⊢ f (f (f x)) = f x

case true.true
f : Bool → Bool
x : Bool
h₁ : f true = true
h₂ : f false = true
⊢ f (f (f x)) = f x
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ x ⊓ y ⊓ y' ⊔ x' ⊓ (y ⊓ y') = ⊥

Tactic:
h.inf_eq_bot,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ ⊥ ⊓ y' ⊔ x' ⊓ (y ⊓ y') = ⊥
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ ↑(a ⊓ b) = ↑⊥ ↔ a ⊓ b = ⊥

Tactic:
coe_inj

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ a ⊓ b = ⊥ ↔ a ⊓ b = ⊥
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ ↑(a ⊔ b) = ↑⊤ ↔ a ⊔ b = ⊤

Tactic:
coe_inj

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ a ⊔ b = ⊤ ↔ a ⊔ b = ⊤
Module: Mathlib.Order.Lattice

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

Tactic:
by
  rw [sup_assoc, sup_left_comm b, ← sup_assoc]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
⊢ f (max x y) = f x ⊔ f y

Tactic:
by simp only [h, hf h, sup_of_le_right]

Goal state after:
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 c : α
ha : f a ≤ f c
hb : f b ≤ f c
⊢ f (a ⊔ b) ≤ f c

Tactic:
rw [map_sup]

Goal state after:
α : 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 c : α
ha : f a ≤ f c
hb : f b ≤ f c
⊢ f a ⊔ f b ≤ f c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⇨ b = ⊤ ↔ a ≤ b

Tactic:
by rw [← top_le_iff, le_himp_iff, top_inf_eq]

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ (a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c

Tactic:
rw [le_himp_iff, inf_right_comm, ← le_himp_iff]
  exact himp_inf_le.trans le_himp_himp

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

Goal state before:
pp: α : Type u_1
t s s' : Set α
⊢ t.ite s s' ∩ tᶜ = s' ∩ tᶜ

Tactic:
rw [← ite_compl, ite_inter_self]

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

Goal state before:
pp: α : Type u_7
β : Type u_8
⊢ Injective toSigma

Tactic:
rintro ⟨a, b⟩ ⟨c, d⟩ h

Goal state after:
α : Type u_7
β : Type u_8
a : α
b : β
c : α
d : β
h : (a, b).toSigma = (c, d).toSigma
⊢ (a, b) = (c, d)
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
by
  rw [sup_comm, inf_comm, ← inf_assoc, sup_inf_inf_sdiff]
  apply sdiff_unique
  · calc
      x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y)) := by
          rw [sup_inf_right]
      _ = (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) := by ac_rfl
      _ = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y) := by
          rw [sup_inf_self, sup_sdiff_left, ← sup_assoc, sup_inf_left, sdiff_sup_self',
            inf_sup_right, sup_comm y, inf_sdiff_sup_right, inf_sup_left x z y]
      _ = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ (x ⊓ y ⊔ x \ y))) := by ac_rfl
      _ = x := by simp
  · calc
      x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y := by rw [inf_sup_left]
      _ = x ⊓ (y \ z ⊓ z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y := by ac_rfl
      _ = x ⊓ y \ z ⊓ x \ y := by rw [inf_sdiff_self_left, bot_inf_eq, inf_bot_eq, bot_sup_eq]
      _ = x ⊓ (y \ z ⊓ y) ⊓ x \ y := by conv_lhs => rw [← inf_sdiff_left]
      _ = x ⊓ (y \ z ⊓ (y ⊓ x \ y)) := by ac_rfl
      _ = ⊥ := by rw [inf_sdiff_self_right, inf_bot_eq, inf_bot_eq]

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

pp: case neg
α : 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 = x a

Tactic:
· rw [← hx]; rfl

Goal state after:
case neg
α : 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 = x a
Module: Mathlib.Order.SymmDiff

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

Tactic:
by
  rw [symmDiff_eq_sup_sdiff_inf, inf_sdiff_distrib_left, inf_sup_left, inf_inf_distrib_left,
    symmDiff_eq_sup_sdiff_inf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' s = univ ↔ range f ⊆ s

Tactic:
← univ_subset_iff,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ univ ⊆ f ⁻¹' s ↔ range f ⊆ s
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
⊢ s.piecewise f₁ f₂ ≤ s.piecewise g₁ g₂

Tactic:
by
  apply piecewise_le <;> intros <;> simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ range Sum.inl ⊓ range Sum.inr ⊆ ⊥

Tactic:
rintro y ⟨⟨x₁, rfl⟩, ⟨x₂, h⟩⟩
      exact Sum.noConfusion rfl rfl (heq_of_eq h)

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi t₁ ⊆ s.pi t₂
hne : (s.pi t₁).Nonempty
i : ι
⊢ i ∈ s → t₁ i ⊆ t₂ i

Tactic:
hi

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi t₁ ⊆ s.pi t₂
hne : (s.pi t₁).Nonempty
i : ι
hi : i ∈ s
⊢ t₁ i ⊆ t₂ i
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' (s ∩ t) = f '' s ∩ f '' t

Tactic:
by
  apply Subset.antisymm (image_inter_subset _ _ _)
  intro x ⟨⟨y, ys, hy⟩, ⟨z, zt, hz⟩⟩
  have : y = z := by
    apply hf (hs ys) (ht zt)
    rwa [← hz] at hy
  rw [← this] at zt
  exact ⟨y, ⟨ys, zt⟩, hy⟩

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

Goal state before:
pp: R : Type u_10
S : Type u_11
F : Type u_12
inst✝³ : One R
inst✝² : One S
inst✝¹ : FunLike F R S
inst✝ : OneHomClass F R S
f : F
x : R
hx : f x ≠ 1
⊢ f x ≠ f 1

Tactic:
by rwa [(map_one f)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
p : Set γ
f : α → β
g : β → γ
h : SurjOn (g ∘ f) s p
hr : MapsTo f s t
x : α
hx : x ∈ s
hz : (g ∘ f) x ∈ p
⊢ (g ∘ f) x ∈ g '' t

Tactic:
exact ⟨f x, hr hx, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : Semigroup α
x y : α
⊢ ((fun x_1 ↦ x * x_1) ∘ fun x ↦ y * x) = fun x_1 ↦ x * y * x_1

Tactic:
ext z

Goal state after:
α : Type u_1
inst✝ : Semigroup α
x y z : α
⊢ ((fun x_1 ↦ x * x_1) ∘ fun x ↦ y * x) z = x * y * z
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Semigroup α
x y : α
⊢ ((fun x_1 ↦ x_1 * x) ∘ fun x ↦ x * y) = fun x_1 ↦ x_1 * (y * x)

Tactic:
ext z

Goal state after:
α : Type u_1
inst✝ : Semigroup α
x y z : α
⊢ ((fun x_1 ↦ x_1 * x) ∘ fun x ↦ x * y) z = z * (y * x)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
m n : ℕ
h : n ≤ m
⊢ a ^ (m - n) * a ^ n = a ^ m

Tactic:
by rw [← pow_add, Nat.sub_add_cancel h]

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

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

Tactic:
exact ⟨u.inv, u.val_inv, u.inv_val⟩

Goal state after:
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✝¹ : CommMagma M
inst✝ : CommMagma N
x✝¹ x✝ : M × N
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
by ext <;> apply mul_comm

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

Goal state before:
pp: M : Type u_3
N : Type u_4
P : Type u_5
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
f : M →ₙ* N × P
x : M
⊢ (((fst N P).comp f).prod ((snd N P).comp f)) x = f x

Tactic:
simp only [prod_apply, coe_fst, coe_snd, comp_apply]

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

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a✝ b x a : G₀
⊢ a⁻¹⁻¹ = a

Tactic:
by_cases h : a = 0
    · simp [h]
    · exact left_inv_eq_right_inv (inv_mul_cancel₀ <| inv_ne_zero h) (inv_mul_cancel₀ h)

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

Goal state before:
pp: case succ
A : Type u_3
F : Type u_4
inst✝² : MulZeroOneClass A
inst✝¹ : FunLike F ℕ A
inst✝ : ZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → f n = g n
n : ℕ
⊢ f (n + 1) = g (n + 1)

Tactic:
exact h_pos n.succ_pos

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
⊢ Commute (a * b⁻¹) c

Tactic:
exact hac.mul_left hbc.inv_left₀

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
u : Mˣ
a : M
⊢ Commute (↑u) a ↔ ↑u * (a * ↑u⁻¹) = a

Tactic:
u.commute_iff_mul_inv_cancel,

Goal state after:
M : Type u_1
inst✝ : Monoid M
u : Mˣ
a : M
⊢ ↑u * a * ↑u⁻¹ = a ↔ ↑u * (a * ↑u⁻¹) = a
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hc : c ≠ 0
hd : d ≠ 0
h : a / b = c / d
⊢ b ≠ 0

Tactic:
intro hb

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hc : c ≠ 0
hd : d ≠ 0
h : a / b = c / d
hb : b = 0
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a : G₀
ha : a ≠ 0
b c : G₀
⊢ a / b * (c / a) = c / b

Tactic:
rw [mul_comm, div_mul_div_cancel₀ ha]

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

Goal state before:
pp: α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ a /ₚ u + -b /ₚ u = (a + -b) /ₚ u

Tactic:
divp_add_divp_same

Goal state after:
α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ (a + -b) /ₚ u = (a + -b) /ₚ u
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
⊢ Even n → ∀ (a : α), (-a) ^ n = a ^ n

Tactic:
rintro ⟨c, rfl⟩ a

Goal state after:
α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
c : ℕ
a : α
⊢ (-a) ^ (c + c) = a ^ (c + c)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
⊢ Odd n → ∀ (a : α), (-a) ^ n = -a ^ n

Tactic:
rintro ⟨c, rfl⟩ a

Goal state after:
α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
c : ℕ
a : α
⊢ (-a) ^ (2 * c + 1) = -a ^ (2 * c + 1)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
⊢ Even n → ∀ (a : α), (-a) ^ n = a ^ n

Tactic:
rintro ⟨c, rfl⟩ a

Goal state after:
α : Type u_2
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
c : ℤ
a : α
⊢ (-a) ^ (c + c) = a ^ (c + c)
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
hb : AddLECancellable b
⊢ a ≤ a + b - b

Tactic:
rw [add_comm]

Goal state after:
α : Type u_1
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
hb : AddLECancellable b
⊢ a ≤ b + a - b
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a - (b + c) = a - c - b

Tactic:
rw [add_comm]

Goal state after:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a - (c + b) = a - c - b
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
hb : AddLECancellable b
⊢ a + b = a + b

Tactic:
rw [add_comm]

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hca : c < a
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

Tactic:
obtain hbd | rfl | hdb := lt_trichotomy b d

Goal state after:
case inr.inr.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hca : c < a
hbd : b < d
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

case inr.inr.inr.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
hca : c < a
h : a * b = c * b
⊢ a = c ∧ b = b ∨ a < c ∨ b < b

case inr.inr.inr.inr
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hca : c < a
hdb : d < b
⊢ a = c ∧ b = d ∨ a < c ∨ b < d
Module: Mathlib.Algebra.Order.Monoid.Defs

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
h : a ≤ 1
⊢ a * a ≤ 1

Tactic:
exact mul_le_one' h h

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c d : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
hab : a ≤ b
hcd : c ≤ d
⊢ a * d + b * c ≤ a * c + b * d

Tactic:
obtain ⟨d, hd, rfl⟩ := exists_nonneg_add_of_le hcd

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
hab : a ≤ b
d : R
hd : 0 ≤ d
hcd : c ≤ c + d
⊢ a * (c + d) + b * c ≤ a * c + b * (c + d)
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (f a' = b)
⊢ (f.setValue a b) a = b

Tactic:
simp [setValue]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α ↪ β
a c : α
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (f a' = f c)
⊢ (f.setValue a (f c)) c = f a

Tactic:
simp [setValue]

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₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ * b ≤ 1 ↔ b ≤ a

Tactic:
by rw [inv_mul_le_iff₀ ha, mul_one]

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✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ a = 0 ∧ b * b = 0 ↔ a = 0 ∧ b = 0

pp: case ha
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ a * a

pp: case hb
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ b * b

Tactic:
mul_self_eq_zero (M₀ := R)

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ a = 0 ∧ b = 0 ↔ a = 0 ∧ b = 0

case ha
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ a * a

case hb
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ b * b
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 c : G₀
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
⊢ a / b ≤ a / c

Tactic:
by
  rw [div_eq_mul_inv, div_eq_mul_inv]
  gcongr
  exacts [ha, hc]

Goal state after: