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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ a * (b * a⁻¹) = b

Tactic:
by
  rw [← mul_assoc, h.mul_inv_cancel]

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

Goal state before:
pp: G : Type u_1
inst✝ : DivInvMonoid G
x : G
⊢ x⁻¹ = 1 / x

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_1
inst✝ : DivInvMonoid G
x : G
⊢ x⁻¹ = 1 * x⁻¹
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_1
inst✝ : DivInvMonoid G
a b c : G
⊢ a * b * c⁻¹ = a * (b / c)
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_1
inst✝ : DivInvMonoid G
a b c : G
⊢ a * b * c⁻¹ = a * (b * c⁻¹)
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : G
⊢ a / a = 1

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_1
inst✝ : Group G
a : G
⊢ a * a⁻¹ = 1
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
⊢ a * b / b = a

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_1
inst✝ : Group G
a b : G
⊢ a * b * b⁻¹ = a
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
⊢ a / b * b = a

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_1
inst✝ : Group G
a b : G
⊢ a * b⁻¹ * b = a
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_inj : ¬Injective f
surj : Surjective fun g ↦ g ∘ f
c c' : γ
⊢ c = c'

Tactic:
simp only [Injective, not_forall] at not_inj

Goal state after:
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
surj : Surjective fun g ↦ g ∘ f
c c' : γ
not_inj : ∃ x x_1 x_2, ¬x = x_1
⊢ c = c'
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: p : Prop
α : Sort u_1
inst✝ : Nonempty α
P : α → Prop
f : p → α
a : p
h : P (f a)
⊢ P (sometimes f)

Tactic:
rwa [sometimes_eq]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
a c b✝ c✝ : α
a✝ : TransGen r a b✝
hbc : r b✝ c✝
IH : ∃ b, r a b ∧ ReflTransGen r b b✝
⊢ ∃ b, r a b ∧ ReflTransGen r b c✝

Tactic:
| tail _ hbc IH =>

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_1
s : Setoid α
x : Quotient s
y : α
⊢ x = ⟦y⟧ ↔ ⟦x.out⟧ = ⟦y⟧

Tactic:
Quotient.out_eq x

Goal state after:
α : Sort u_1
s : Setoid α
x : Quotient s
y : α
⊢ x = ⟦y⟧ ↔ x = ⟦y⟧
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
β : Type v
f : α → α
g : α → β
h : g ∘ f = g
n : ℕ
⊢ g ∘ f^[0] = g

Tactic:
iterate_zero,

Goal state after:
α : Type u
β : Type v
f : α → α
g : α → β
h : g ∘ f = g
n : ℕ
⊢ g ∘ id = g
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
β : Type v
f : α → α
a : α
l : List β
⊢ foldl (fun b x ↦ f b) a l = f^[l.length] a

Tactic:
induction l generalizing a with

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
f : α → α → α
comm : Std.Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f a (f b c) ≤ f (f a b) c

Tactic:
by
      rw [comm.comm, comm.comm b, comm.comm _ c, comm.comm a]
      exact assoc ..

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

Goal state before:
pp: case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} ↦ next)
x : C m✝.succ
⊢ ∃ a, leRecOn ⋯ (fun {k} ↦ next) a = x

Tactic:
obtain ⟨w, rfl⟩ := Hnext _ x

Goal state after:
case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} ↦ next)
w : C m✝
⊢ ∃ a, leRecOn ⋯ (fun {k} ↦ next) a = next w
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: C : ℕ → Sort u_1
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
⊢ Surjective (leRecOn hnm fun {k} ↦ next)

Tactic:
induction hnm with
  | refl =>
    intro x
    refine ⟨x, ?_⟩
    rw [leRecOn_self]
  | step hnm ih =>
    intro x
    obtain ⟨w, rfl⟩ := Hnext _ x
    obtain ⟨x, rfl⟩ := ih w
    refine ⟨x, ?_⟩
    rw [leRecOn_succ]

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

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

Tactic:
have ha1 : a > 1 := Nat.lt_of_le_of_ne ha0 ha.symm

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
M : α
⊢ ¬P M

Tactic:
induction M using WellFoundedGT.induction with

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t✝ : Set α
a b : α
inst✝ : DecidableEq α
t : Set α
x : α
h : ¬x ∈ t
⊢ RightInverse (fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩

Tactic:
rintro (_ | y)

Goal state after:
case none
α : Type u_1
β : Type u_2
s t✝ : Set α
a b : α
inst✝ : DecidableEq α
t : Set α
x : α
h : ¬x ∈ t
⊢ (fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩) ((fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) none) = none

case some
α : Type u_1
β : Type u_2
s t✝ : Set α
a b : α
inst✝ : DecidableEq α
t : Set α
x : α
h : ¬x ∈ t
y : { i // i ∈ t }
⊢ (fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩) ((fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) (some y)) = some y
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case zero
f : ℕ → ℕ
mono_f : Monotone f
hc : ∀ (n : ℕ), f n ≤ 0
⊢ ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b

Tactic:
use 0, 0, fun n _ ↦ Nat.eq_zero_of_le_zero (hc n)

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

Goal state before:
pp: α : Type u_1
l : List α
H : l.Nodup
a : α
⊢ {x | x ∈ l} = {a} ↔ l = [a]

Tactic:
constructor
  · rw [ofPred_mem_list_eq_replicate]
    rintro ⟨n, hn, rfl⟩
    simp only [List.nodup_replicate] at H
    simp [show n = 1 by lia]
  · rintro rfl
    simp

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : DistribLattice α
x y z : α
h₁ : x ⊓ z ≤ y ⊓ z
h₂ : x ⊔ z ≤ y ⊔ z
⊢ y ⊓ z ⊔ x = (y ⊔ x) ⊓ (x ⊔ z)

Tactic:
by rw [sup_inf_right, sup_comm x]

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

Goal state before:
pp: α : Type u
a : α
s : Set α
ha : a ∈ s
⊢ s = {a} ∨ s.Nontrivial

Tactic:
← subsingleton_iff_singleton ha

Goal state after:
α : Type u
a : α
s : Set α
ha : a ∈ s
⊢ s.Subsingleton ∨ s.Nontrivial
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case a
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ ((a ⇨ b) ⊓ a)ᶜᶜ ≤ bᶜᶜ

Tactic:
exact compl_anti (compl_anti himp_inf_le)

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

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

Tactic:
by
  simp [inter_union_distrib_right]

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

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

Tactic:
by
  simp [inter_union_distrib_right]

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

Goal state before:
pp: α : Type u_1
s₁ s₂ t : Set α
h : s₁ ⊆ s₂
⊢ s₁ \ t ⊆ s₂ \ t

Tactic:
by
  gcongr

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

Goal state before:
pp: α : Type u_1
s t u : Set α
h : t ⊆ u
⊢ s \ u ⊆ s \ t

Tactic:
by
  gcongr

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

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

Tactic:
rw [← sdiff_sup_cancel hyz]

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
⊢ x ⊔ y < z \ y ⊔ y
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
rw [← le_compl_iff_disjoint_right, compl_compl]

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

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
f : ℕ → Type u
⊢ LeftInverse (Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x ↦ id)) fun x ↦
    Sigma.casesOn x fun n ↦
      Nat.casesOn (motive := fun i ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x ↦ inl x) fun n x ↦ inr ⟨n, x⟩

Tactic:
by rintro ⟨n | n, x⟩ <;> rfl

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
sup_comm (c \ b),

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (h₁ a)
f : (a : α) → W a
a : α
⊢ (h₁.piCongr h₂) f (h₁ a) = (h₂ a) (f a)

Tactic:
by
  rw [piCongr, trans_apply, piCongrLeft_apply_apply, piCongrRight_apply, Pi.map_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Option α → β
⊢ Injective f ↔ Injective (f ∘ some) ∧ ¬f none ∈ range (f ∘ some)

Tactic:
simp only [mem_range, not_exists, (· ∘ ·)]

Goal state after:
α : Type u_1
β : Type u_2
f : Option α → β
⊢ Injective f ↔ Injective (f ∘ some) ∧ ∀ (x : α), ¬f (some x) = f none
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
⊢ (InjOn f s₁ ∧ InjOn f s₂ ∧ ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y) → InjOn f (s₁ ∪ s₂)

Tactic:
rintro ⟨h₁, h₂, h₁₂⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
h₁ : InjOn f s₁
h₂ : InjOn f s₂
h₁₂ : ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
⊢ InjOn f (s₁ ∪ s₂)
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
⊢ update f i ⁻¹' s.pi t = t i

Tactic:
by
  ext x
  refine ⟨fun h => ?_, fun hx j hj => ?_⟩
  · convert! h i hi
    simp
  · obtain rfl | h := eq_or_ne j i
    · simpa
    · rw [update_of_ne h]
      exact hf j hj h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
h : LeftInvOn f' f s
hf : SurjOn f s t
y : β
hy : y ∈ t
⊢ f' y ∈ s

Tactic:
by
  let ⟨x, hs, hx⟩ := hf hy
  rwa [← hx, h hs]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
h : range f = {b}
a : α
⊢ f a = b

Tactic:
by
  simpa only [h, mem_singleton_iff] using mem_range_self (f := f) a

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
a b : M
n : ℕ
⊢ (a * b) ^ (n + 1) = a ^ (n + 1) * b ^ (n + 1)

Tactic:
rw [pow_succ', pow_succ', pow_succ', mul_pow, mul_mul_mul_comm]

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

Goal state before:
pp: G : Type u_3
inst✝ : DivInvMonoid G
x y : G
⊢ x * (1 / y) = x / y

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_3
inst✝ : DivInvMonoid G
x y : G
⊢ x * (1 * y⁻¹) = x / y
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_3
inst✝ : DivInvMonoid G
a b : G
⊢ a * b⁻¹ = a * (1 / b)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : 1 / a = 1 / b
⊢ a = b

Tactic:
by
  rw [← one_div_one_div a, h, one_div_one_div]

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✝² : Pow M₁ ℕ
inst✝¹ : Inv M₁
inst✝ : InvOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
⊢ f 1⁻¹ = f 1

Tactic:
by rw [inv, one, inv_one]

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

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

Tactic:
by
    rw [zpow_negSucc, zpow_negSucc, Int.negSucc_mul_negSucc, inv_pow, inv_inv, ← pow_mul, ←
      zpow_natCast]
    rfl

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b : G
⊢ a / b = b⁻¹ ↔ a = 1

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_3
inst✝ : Group G
a b : G
⊢ a * b⁻¹ = b⁻¹ ↔ a = 1
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
⊢ b / a = c / a ↔ b = c

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_3
inst✝ : Group G
a b c : G
⊢ b * a⁻¹ = c / a ↔ b = c
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b : G
⊢ a / b = a ↔ b = 1

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_3
inst✝ : Group G
a b : G
⊢ a * b⁻¹ = a ↔ b = 1
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
⊢ a = b / c ↔ a * c = b

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_3
inst✝ : Group G
a b c : G
⊢ a = b * c⁻¹ ↔ a * c = b
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
⊢ a / b = c ↔ a = c * b

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_3
inst✝ : Group G
a b c : G
⊢ a * b⁻¹ = c ↔ a = c * b
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₁
inst✝⁵ : One M₁
inst✝⁴ : Pow M₁ ℕ
inst✝³ : Inv M₁
inst✝² : Div M₁
inst✝¹ : Pow M₁ ℤ
inst✝ : Group M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x : M₁
⊢ f (x⁻¹ * x) = f 1

Tactic:
by rw [mul, inv, inv_mul_cancel, one]

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✝¹ : Pow M₂ ℕ
inst✝ : Monoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
x : M₁
⊢ f x ^ 0 = 1

Tactic:
by rw [← npow, pow_zero, ← one]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c : G
h : a = b * c
⊢ b * c / b = c

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c : G
h : a = b * c
⊢ b * c * b⁻¹ = c
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c : G
h : b = c / a
⊢ a * (c / a) = c

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c : G
h : b = c / a
⊢ a * (c * a⁻¹) = c
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
⊢ f x / f y = f (x * y⁻¹)

Tactic:
← div,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
⊢ f (x / y) = f (x * y⁻¹)
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
u : Mˣ
⊢ ↑u = 1

Tactic:
simp [u.eq_one]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
h : IsUnit a
⊢ a / a = 1

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
a : α
h : IsUnit a
⊢ a * a⁻¹ = 1
Module: Mathlib.Algebra.Group.Units.Defs

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

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ b * (a * b)⁻¹ = a⁻¹
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
u : αˣ
⊢ a /ₚ u = a / ↑u

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
a : α
u : αˣ
⊢ a /ₚ u = a * (↑u)⁻¹
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ a / b * b = a

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ a * b⁻¹ * b = a
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ a * b / b = a

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ a * b * b⁻¹ = a
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit b
⊢ a / b = c ↔ a = c * b

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit b
⊢ a * b⁻¹ = c ↔ a = c * b
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a = b / c ↔ a * c = b

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a = b * c⁻¹ ↔ a * c = b
Module: Mathlib.Algebra.Group.Units.Basic

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

Tactic:
h.mul_div_cancel_right

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

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

Tactic:
div_eq_mul_inv,

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

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

Tactic:
div_eq_mul_inv,

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

Goal state before:
pp: G₀ : Type u
M₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ a b : G₀
hb : b ≠ 0
⊢ a * b / b = a

Tactic:
div_eq_mul_inv,

Goal state after:
G₀ : Type u
M₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ a b : G₀
hb : b ≠ 0
⊢ a * b * b⁻¹ = a
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
⊢ 0⁻¹ = 0

Tactic:
inv_zero

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
⊢ 0 = 0
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₀' ℤ
h01 : 0 ≠ 1
f : G₀ → G₀'
hf : Surjective 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
⊢ f 0⁻¹ = f 0

Tactic:
inv_zero

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₀' ℤ
h01 : 0 ≠ 1
f : G₀ → G₀'
hf : Surjective 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
⊢ f 0 = f 0
Module: Mathlib.Algebra.GroupWithZero.Basic

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

Tactic:
by_cases ha : a = 0
    · simp [ha]
    by_cases hb : b = 0
    · simp [hb]
    apply inv_eq_of_mul
    simp [mul_assoc, ha, hb]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ 0 / a = 0

Tactic:
div_eq_mul_inv,

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ 0 * a⁻¹ = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a / 0 = 0

Tactic:
div_eq_mul_inv,

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a * 0⁻¹ = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

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

Tactic:
div_eq_mul_inv,

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a * a * a⁻¹ = a
Module: Mathlib.Algebra.GroupWithZero.Basic

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

Tactic:
div_eq_mul_inv,

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a * a⁻¹ * a = a
Module: Mathlib.Algebra.GroupWithZero.Basic

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

Tactic:
inv_zero

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a = 0 ↔ a = 0
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: case pos
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x : β
hx : x = 0
⊢ 0 = 0⁻¹

Tactic:
inv_zero

Goal state after:
case pos
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x : β
hx : x = 0
⊢ 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
a b c : G₀
⊢ a / c * b = a * b / c

Tactic:
div_eq_mul_inv,

Goal state after:
G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
a b c : G₀
⊢ a * c⁻¹ * b = a * b * c⁻¹
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:
div_eq_mul_inv,

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