mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: R : Type u_2
inst✝ : Mul R
⊢ (∀ (x : R), IsLeftRegular x ∧ IsRightRegular x) ↔ ∀ (r : R), IsRegular r

Tactic:
exact forall_congr' fun _ ↦ isRegular_iff.symm

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

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
a : G
n : ℕ
⊢ a ^ Int.negSucc n = (a ^ (n + 1))⁻¹

Tactic:
rw [← zpow_natCast]

Goal state after:
G : Type u_1
inst✝ : DivInvMonoid G
a : G
n : ℕ
⊢ a ^ Int.negSucc n = (a ^ ↑(n + 1))⁻¹
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α' → β
a : α
a' : α'
b : β
⊢ uncurry (update f a (update (f a) a' b)) = update (uncurry f) (a, a') b

Tactic:
by
  apply curry_injective
  simp [curry_update]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : β → β → Prop
f : α → β
hsurj : Surjective f
x y : β
⊢ Relation.Map (r on f) f f x y ↔ r x y

Tactic:
have _ := hsurj x

Goal state after:
α : Type u_1
β : Type u_2
r : β → β → Prop
f : α → β
hsurj : Surjective f
x y : β
x✝ : ∃ a, f a = x
⊢ Relation.Map (r on f) f f x y ↔ r x y
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : β → β → Prop
f : α → β
hsurj : Surjective f
x y : β
x✝ : ∃ a, f a = x
⊢ Relation.Map (r on f) f f x y ↔ r x y

Tactic:
have _ := hsurj y

Goal state after:
α : Type u_1
β : Type u_2
r : β → β → Prop
f : α → β
hsurj : Surjective f
x y : β
x✝¹ : ∃ a, f a = x
x✝ : ∃ a, f a = y
⊢ Relation.Map (r on f) f f x y ↔ r x y
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) → DivInvMonoid (f i)
⊢ ∀ (n : ℕ) (a : (i : I) → f i), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹

Tactic:
intros; ext; exact DivInvMonoid.zpow_neg' _ _

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Trichotomous s
i : α
a : β
j : α
b : β
hij : r i j
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)

pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Trichotomous s
i : α
a b : β
⊢ Prod.Lex r s (i, a) (i, b) ∨ (i, a) = (i, b) ∨ Prod.Lex r s (i, b) (i, a)

pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Trichotomous s
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)

Tactic:
{ exact Or.inl (Lex.left _ _ hij) }

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Trichotomous s
i : α
a b : β
⊢ Prod.Lex r s (i, a) (i, b) ∨ (i, a) = (i, b) ∨ Prod.Lex r s (i, b) (i, a)

case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Trichotomous s
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
o : Ordering
⊢ compare a b = o ↔ o.Compares a b

Tactic:
cases o <;> simp only [Ordering.Compares]
  · exact compare_lt_iff_lt
  · exact compare_eq_iff_eq
  · exact compare_gt_iff_gt

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PartialOrder α
⊢ ∀ (a b : BoundedOrder α), a = b

Tactic:
by rintro ⟨⟩ ⟨⟩; congr <;> exact Subsingleton.elim _ _

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

Goal state before:
pp: case succ.inr
a : ℕ
ha : a ≠ 1
b : ℕ
ha0 : a > 0
ha1 : a > 1
⊢ a * (b + 1) ≤ a ^ (b + 1)

Tactic:
Nat.pow_succ'

Goal state after:
case succ.inr
a : ℕ
ha : a ≠ 1
b : ℕ
ha0 : a > 0
ha1 : a > 1
⊢ a * (b + 1) ≤ a * a ^ b
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ MonotoneOn (f ∘ ⇑ofDual) s ↔ AntitoneOn f s

Tactic:
monotoneOn_comp_ofDual_iff

Goal state after:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ AntitoneOn f s ↔ AntitoneOn f s
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b c : α
h : a ≤ c ⊔ b
hd : Disjoint a c
⊢ a ≤ b ⊔ c

Tactic:
sup_comm

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b c : α
h : a ≤ c ⊔ b
hd : Disjoint a c
⊢ a ≤ c ⊔ b
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') = ⊥

Tactic:
inf_left_comm,

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') = ⊥
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b : α
hab : a ⊔ b = b
hba : b ⊔ a = a
⊢ b ⊔ a = b

Tactic:
sup_comm

Goal state after:
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b : α
hab : a ⊔ b = b
hba : b ⊔ a = a
⊢ a ⊔ b = b
Module: Mathlib.Order.Lattice

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

Tactic:
sup_comm

Goal state after:
α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ b ⊔ c ⊔ a = b ⊔ c ⊔ a
Module: Mathlib.Order.Lattice

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

Tactic:
sup_comm

Goal state after:
α : Type u
inst✝ : DistribLattice α
a b c : α
⊢ (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c) = (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c)
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
sup_comm

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ≤ c ⊔ b ↔ a ≤ c ⊔ b
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d : α
a b c : αᵒᵈ
⊢ toDual (ofDual b ⇨ ofDual a) ≤ c ↔ a ≤ b ⊔ c

Tactic:
sup_comm

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d : α
a b c : αᵒᵈ
⊢ toDual (ofDual b ⇨ ofDual a) ≤ c ↔ a ≤ c ⊔ b
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x
i : x ⊓ y ⊓ z = ⊥
| x ⊓ y ⊔ x \ y

Tactic:
sup_comm

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x
i : x ⊓ y ⊓ z = ⊥
| x \ y ⊔ x ⊓ y
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
⊢ x \ y = z

Tactic:
sup_comm

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
⊢ x \ y = z
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ : α
a b c : αᵒᵈ
⊢ toDual (ofDual b ⇨ ofDual a) ≤ c ↔ a ≤ b ⊔ c

Tactic:
sup_comm

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ : α
a b c : αᵒᵈ
⊢ toDual (ofDual b ⇨ ofDual a) ≤ c ↔ a ≤ c ⊔ b
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (s ∪ t) ∩ sᶜ ⊆ t

Tactic:
simp [union_inter_distrib_right]

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (s ∪ t) ∩ tᶜ ⊆ s

Tactic:
simp [union_inter_distrib_right]

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

Goal state before:
pp: α : Type u
β : Type u_1
x✝ y✝ z✝ : α
inst✝ : GeneralizedBooleanAlgebra α
y x z : α
h : y \ x ≤ z
⊢ y ⊔ y \ x ≤ y \ x ⊔ x ⊔ z

Tactic:
by
            grind [sup_of_le_left, sdiff_le', le_sup_left, sdiff_sup_self']

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
⊢ HeytingAlgebra α

Tactic:
by
  let generalizedHeytingAlgebra := e.generalizedHeytingAlgebra
  let bot := e.bot
  let compl := e.compl
  apply e.injective.heytingAlgebra <;> intros <;> first | rfl | exact e.apply_symm_apply _

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

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

Tactic:
rw [eq_comm, compl_eq_iff_isCompl, eq_compl_iff_isCompl]

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

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

Tactic:
rw [eq_comm, compl_eq_iff_isCompl, eq_compl_iff_isCompl]

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

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

Tactic:
sup_comm

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ y ⊔ xᶜ = y ⊔ xᶜ
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ Disjoint xᶜ y ↔ y ≤ x

Tactic:
rw [← le_compl_iff_disjoint_left, compl_compl]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ (b \ a) = a ⊔ b

Tactic:
by
  rw [symmDiff, sdiff_idem]
  exact
    le_antisymm (sup_le_sup sdiff_le sdiff_le)
      (sup_le le_sdiff_sup <| le_sdiff_sup.trans <| sup_le le_sup_right le_sdiff_sup)

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b ⊔ a = a ⊔ b

Tactic:
sup_comm

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊔ b = a ⊔ b
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
a : α
⊢ Injective fun x ↦ swap x a

Tactic:
simp_rw [swap_comm _ a]

Goal state after:
α : Sort u_1
inst✝ : DecidableEq α
a : α
⊢ Injective fun x ↦ swap a x
Module: Mathlib.Data.Set.Image

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

Tactic:
induction n with
  | zero => simp
  | succ n ih => rw [iterate_succ', iterate_succ', ← ih, image_comp_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
b : β
s : Set α
h₁ : LeftInverse g f
h₂ : RightInverse g f
⊢ b ∈ f '' s ↔ g b ∈ s

Tactic:
by
  rw [image_eq_preimage_of_inverse h₁ h₂, mem_preimage]

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

Goal state before:
pp: case inr.refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
⊢ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅ → s ×ˢ t ⊆ s₁ ×ˢ t₁

Tactic:
intro H
    simp only [st.1.ne_empty, st.2.ne_empty, or_false] at H
    exact prod_mono H.1 H.2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
⊢ x ∈ s.piecewise f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t)

Tactic:
by by_cases x ∈ s <;> simp [*, Set.ite]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
α : ι → Type u_4
inst✝² : (i : ι) → SMul M (α i)
inst✝¹ : ∀ (i : ι), Nonempty (α i)
i : ι
inst✝ : FaithfulSMul M (α i)
m₁✝ m₂✝ : M
h : ∀ (a : (i : ι) → α i), m₁✝ • a = m₂✝ • a
a : α i
⊢ m₁✝ • a = m₂✝ • a

Tactic:
classical
    simpa using
      congr_fun (h <| Function.update (fun j => Classical.choice (‹∀ i, Nonempty (α i)› j)) i a) i

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ val ⁻¹' s = univ

Tactic:
← preimage_range,

Goal state after:
α : Type u_1
s : Set α
⊢ val ⁻¹' s = ?m.9 ⁻¹' range ?m.9

α : Type u_1
s : Set α
⊢ { x // x ∈ s } → ?m.8

α : Type u_1
s : Set α
⊢ Type ?u.14
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
β : ι → Type u_4
i : ι
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ (univ.pi fun j ↦ t j (update f i a j)) = {x | x i ∈ t i a} ∩ {i}ᶜ.pi fun j ↦ t j (f j)

Tactic:
by
  rw [compl_eq_univ_sdiff, ← pi_update_of_mem (mem_univ _)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
h' : f '' s₁ ⊆ f '' s₂
⊢ f ⁻¹' f '' s₁ ∩ s ⊆ f ⁻¹' f '' s₂ ∩ s

Tactic:
exact inter_subset_inter_left _ (preimage_mono h')

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
⊢ ∃ f', range f = graphOn f' univ

Tactic:
refine ⟨fun h ↦ (f (hf₁ h).choose).snd, ?_⟩
  ext x
  simp only [mem_range, comp_apply, mem_graphOn, mem_univ, true_and]
  refine ⟨?_, fun hi ↦ ⟨(hf₁ x.1).choose, Prod.ext (hf₁ x.1).choose_spec hi⟩⟩
  rintro ⟨g, rfl⟩
  exact hf _ _ (hf₁ (f g).1).choose_spec

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
htt' : t ⊆ t'
ht' : t' ⊆ range f
⊢ SurjOn f univ t'

Tactic:
by simpa [SurjOn]

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

Goal state before:
pp: M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
val inv : M
val_inv : val * inv = 1
inv_val : inv * val = 1
⊢ f inv * f val = 1

Tactic:
by simp [← map_mul, 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✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Subsingleton Mˣ
inst✝ : Subsingleton Nˣ
⊢ ∀ (a : M × N), IsUnit a → a = 1

Tactic:
by simp [Prod.isUnit_iff, Prod.ext_iff]

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

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝² : MulZeroClass M₀
inst✝¹ : Mul M₀'
inst✝ : Zero M₀'
f : M₀ → M₀'
hf : Surjective f
zero : f 0 = 0
mul : ∀ (a b : M₀), f (a * b) = f a * f b
x : M₀
⊢ f x * 0 = 0

Tactic:
by simp only [← zero, ← mul, mul_zero]

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

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
f : G₀' → G₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀'), f (x * y) = f x * f y
inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀'), f (x / y) = f x / f y
npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n
x : G₀'
hx : x ≠ 0
⊢ f x * (f x)⁻¹ = 1

Tactic:
mul_inv_cancel₀ ((hf.ne_iff' zero).2 hx)

Goal state after:
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
f : G₀' → G₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀'), f (x * y) = f x * f y
inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀'), f (x / y) = f x / f y
npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n
x : G₀'
hx : x ≠ 0
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Hom.Instances

Goal state before:
pp: M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
mM : MulOneClass M
mN : MulOneClass N
mP : CommMonoid P
f : M →* N →* P
y : N
⊢ (f 1) y = 1

Tactic:
simp [f.map_one, one_apply]

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

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

Tactic:
SemiconjBy

Goal state after:
M : Type u_1
inst✝ : Monoid M
u : Mˣ
a : M
⊢ ↑u * a = a * ↑u ↔ ↑u * a = a * ↑u
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case h
α : Type u_2
inst✝² : Add α
inst✝¹ : Mul α
inst✝ : RightDistribClass α
b k : α
⊢ (k + k) * b = k * b + k * b

Tactic:
rw [add_mul]

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

Goal state before:
pp: α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hn : Even n
⊢ f^[n] = id

Tactic:
by
  obtain ⟨m, rfl⟩ := hn
  rw [← two_mul, hf.iterate_two_mul]

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 : α
inst✝ : AddLeftMono α
⊢ a + b ≤ a - c + (b + c)

Tactic:
by
  rw [add_comm a, add_comm (a - c)]
  exact add_le_add_add_tsub

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

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

Tactic:
by
  rw [add_comm a b, add_comm a c, add_tsub_add_eq_tsub_right]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬a * c = a * b

Tactic:
· exact mul_lt_mul_right (h.lt_of_ne h') a |>.ne

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

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

Tactic:
ha.mul_le_mul_iff_left

Goal state after:
α : Type u_1
inst✝³ : LE α
inst✝² : Mul α
inst✝¹ : IsMulCommutative α
inst✝ : MulLeftMono α
a b c : α
ha : MulLECancellable a
⊢ b ≤ c ↔ b ≤ c
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 c : G₀
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ b * c
⊢ b⁻¹ * a ≤ c

Tactic:
obtain rfl | hb := hb.eq_or_lt

Goal state after:
case inl
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a c : G₀
hc : 0 ≤ c
hb : 0 ≤ 0
h : a ≤ 0 * c
⊢ 0⁻¹ * a ≤ c

case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hb✝ : 0 ≤ b
hc : 0 ≤ c
h : a ≤ b * c
hb : 0 < b
⊢ b⁻¹ * a ≤ c
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 : G₀
ha : a ≤ 0
hb : 0 ≤ b
⊢ a / b ≤ 0

Tactic:
by
  rw [div_eq_mul_inv]; exact mul_nonpos_of_nonpos_of_nonneg ha (Right.inv_nonneg.2 hb)

Goal state after:
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₀
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
⊢ a * b⁻¹ ≤ c

Tactic:
obtain rfl | hb := hb.eq_or_lt

Goal state after:
case inl
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a c : G₀
hc : 0 ≤ c
hb : 0 ≤ 0
h : a ≤ c * 0
⊢ a * 0⁻¹ ≤ c

case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hb✝ : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
hb : 0 < b
⊢ a * b⁻¹ ≤ c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

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

Tactic:
by
  obtain rfl | hc := eq_or_ne c 0
  · simpa
  · rw [mul_div_mul_left _ _ hc]

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

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

Tactic:
by
  obtain rfl | hc := eq_or_ne c 0
  · simpa
  · rw [mul_div_mul_left _ _ hc]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Lattice

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

Tactic:
sup_comm

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) * (a * b * (a⁻¹ ⊔ b⁻¹)) = (a ⊓ b) * (a * b * (a⁻¹ ⊔ b⁻¹))
Module: Mathlib.Data.Nat.Cast.NeZero

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
h : NeZero ↑n
⊢ n ≠ 0

Tactic:
by rintro rfl; exact h.out Nat.cast_zero

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 c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a) * c / ((b ⊓ a) * c) = (b ⊔ a) / (b ⊓ a)

Tactic:
by
        rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← div_eq_mul_inv]

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

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

Tactic:
simp [cast_add_one_pos]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n✝ : ℕ
⊢ 0 < ↑(n✝ + 1) ↔ 0 < n✝ + 1

Tactic:
simp [cast_add_one_pos]

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

Goal state before:
pp: case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, x.P y (b % a, s, t) → x.P y (a, s', t') → x.P y ((b % a).xgcdAux s t a s' t')
s t s' t' : ℤ
p : x.P y (a, s, t)
p' : x.P y (b, s', t')
⊢ x.P y (a.xgcdAux s t b s' t')

Tactic:
rw [xgcdAux_rec h]

Goal state after:
case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, x.P y (b % a, s, t) → x.P y (a, s', t') → x.P y ((b % a).xgcdAux s t a s' t')
s t s' t' : ℤ
p : x.P y (a, s, t)
p' : x.P y (b, s', t')
⊢ x.P y ((b % a).xgcdAux (s' - ↑b / ↑a * s) (t' - ↑b / ↑a * t) a s t)
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h : a ≤ c
h2 : b ≤ c - a
⊢ a + (c - a) ≤ c

Tactic:
add_tsub_cancel_of_le h

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h : a ≤ c
h2 : b ≤ c - a
⊢ c ≤ c
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

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

Tactic:
add_tsub_cancel_of_le h

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h : c ≤ b
⊢ a - b = a - b
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ a
h2 : a < b
⊢ c + (a - c) < b

Tactic:
add_tsub_cancel_of_le h

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ a
h2 : a < b
⊢ a < b