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

Goal state before:
pp: S : Type u_1
inst✝ : Semigroup S
a x y x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ a * x * x' = y * y' * a

Tactic:
h.eq,

Goal state after:
S : Type u_1
inst✝ : Semigroup S
a x y x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ y * a * x' = y * y' * a
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: S : Type u_1
inst✝ : Semigroup S
a x y x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x * x') (y * y')

Tactic:
by
  unfold SemiconjBy
  -- TODO this could be done using `assoc_rw` if/when this is ported to mathlib4
  rw [← mul_assoc, h.eq, mul_assoc, h'.eq, ← mul_assoc]

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

Goal state before:
pp: S : Type u_3
inst✝ : Semigroup S
b c : S
h : Commute b c
a : S
⊢ a * b * c = a * c * b

Tactic:
simp only [mul_assoc, h.eq]

Goal state after:
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:
h.eq,

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, y * z = 1
x y : M
h : x * y = 1
⊢ y * x = 1

Tactic:
have ⟨z, hz⟩ := ex x y h

Goal state after:
M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, y * z = 1
x y : M
h : x * y = 1
z : M
hz : y * z = 1
⊢ y * x = 1
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, z * x = 1
x y : M
h : x * y = 1
⊢ y * x = 1

Tactic:
have ⟨z, hz⟩ := ex x y h

Goal state after:
M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, z * x = 1
x y : M
h : x * y = 1
z : M
hz : z * x = 1
⊢ y * x = 1
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
apply inv_eq_of_mul

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

Goal state before:
pp: α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
⊢ x = y

Tactic:
rcases em (p x) with (hx | hx) <;> rcases em (p y) with (hy | hy)

Goal state after:
case inl.inl
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : p x
hy : p y
⊢ x = y

case inl.inr
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : p x
hy : ¬p y
⊢ x = y

case inr.inl
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : ¬p x
hy : p y
⊢ x = y

case inr.inr
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : ¬p x
hy : ¬p y
⊢ x = y
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ : α → γ
⊢ ∀ ⦃a₂ : α → γ⦄, (fun g ↦ extend f g e') g₁ = (fun g ↦ extend f g e') a₂ → g₁ = a₂

Tactic:
g₂

Goal state after:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
⊢ (fun g ↦ extend f g e') g₁ = (fun g ↦ extend f g e') g₂ → g₁ = g₂
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single
α : Type u_1
r : α → α → Prop
a i✝ b✝ : α
h : r a b✝
⊢ ReflTransGen r a b✝

Tactic:
| single h =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single
α : Type u_1
r : α → α → Prop
b a b✝ : α
h : r a b✝
motive : (a : α) → TransGen r a b✝ → Prop
single : ∀ {a : α} (h : r a b✝), motive a ⋯
head : ∀ {a c : α} (h' : r a c) (h : TransGen r c b✝), motive c h → motive a ⋯
⊢ motive a ⋯

Tactic:
| single h =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single
α : Type u_1
r : α → α → Prop
motive : {a b : α} → TransGen r a b → Prop
a b : α
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), motive h₁ → motive h₂ → motive ⋯
b✝ : α
h : r a b✝
⊢ motive ⋯

Tactic:
| single h =>

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
intro _

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (TransGen p on f)
i✝ : α
⊢ TransGen r i✝ ≤ (TransGen p on f) i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Function.swap (TransGen r) ≤ TransGen (Function.swap r)

Tactic:
intro _

Goal state after:
α : Type u_1
r : α → α → Prop
i✝ : α
⊢ Function.swap (TransGen r) i✝ ≤ TransGen (Function.swap r) i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single
α : Type u_1
r : α → α → Prop
i✝¹ i✝ b✝ : α
h : r i✝ b✝
⊢ TransGen (Function.swap r) b✝ i✝

Tactic:
| single h =>

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)
⊢ ReflTransGen r ≤ (ReflTransGen p on f)

Tactic:
intro _

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (ReflTransGen p on f)
i✝ : α
⊢ ReflTransGen r i✝ ≤ (ReflTransGen p on f) i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Function.swap (ReflTransGen r) ≤ ReflTransGen (Function.swap r)

Tactic:
intro _

Goal state after:
α : Type u_1
r : α → α → Prop
i✝ : α
⊢ Function.swap (ReflTransGen r) i✝ ≤ ReflTransGen (Function.swap r) i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r p : α → α → Prop
hrp : r ≤ p
⊢ EqvGen r ≤ EqvGen p

Tactic:
intro _

Goal state after:
α : Type u_1
r p : α → α → Prop
hrp : r ≤ p
i✝ : α
⊢ EqvGen r i✝ ≤ EqvGen p i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ TransGen r ≤ EqvGen r

Tactic:
intro _

Goal state after:
α : Type u_1
r : α → α → Prop
i✝ : α
⊢ TransGen r i✝ ≤ EqvGen r i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single
α : Type u_1
r : α → α → Prop
i✝¹ i✝ a✝ b✝ : α
h : r a✝ b✝
⊢ EqvGen r a✝ b✝

Tactic:
| single h =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ ReflTransGen r ≤ EqvGen r

Tactic:
intro _

Goal state after:
α : Type u_1
r : α → α → Prop
i✝ : α
⊢ ReflTransGen r i✝ ≤ EqvGen r i✝
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:
h.eq,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : Std.IdempotentOp gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x : α
⊢ gb (f x) (f x) = f x
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) → DivisionMonoid (f i)
⊢ ∀ (a b : (i : I) → f i), a * b = 1 → a⁻¹ = b

Tactic:
intro _

Goal state after:
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) → DivisionMonoid (f i)
a✝ : (i : I) → f i
⊢ ∀ (b : (i : I) → f i), a✝ * b = 1 → a✝⁻¹ = b
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ ¬IsMin a ↔ ∃ b, b < a

Tactic:
simp [lt_iff_le_not_ge, IsMin, not_forall]

Goal state after:
Module: Mathlib.Order.Lattice

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

Tactic:
rw [sup_comm, sup_comm a, sup_assoc]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
⊢ SemilatticeInf α

Tactic:
apply e.injective.semilatticeInf <;> intros <;> first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β γ : Type u₀
ab : α ≃ β
bc : β ≃ γ
x : f α
⊢ ((mapEquiv f ab).trans (mapEquiv f bc)) x = (mapEquiv f (ab.trans bc)) x

Tactic:
simp [mapEquiv, map_trans']

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

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

Tactic:
inf_inf_sdiff

Goal state after:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
x y : α
⊢ ⊥ = ⊥
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
h : b ≤ c
⊢ a ≤ ⊤ ↔ min a b ≤ c

Tactic:
exact iff_of_true le_top (inf_le_of_right_le h)

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

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

Tactic:
by
  rw [Set.ite, Set.ite, sdiff_compl, union_comm, sdiff_eq]

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

Goal state before:
pp: α : Type u_1
t s₁ s₂ s : Set α
h : s₁ ∩ s = s₂ ∩ s
⊢ t.ite s₁ s₂ ∩ s = s₁ ∩ s

Tactic:
by rw [← ite_inter, ← h, ite_same]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Max α
inst✝⁷ : Min α
inst✝⁶ : LE α
inst✝⁵ : LT α
inst✝⁴ : Top α
inst✝³ : Bot α
inst✝² : Compl α
inst✝¹ : HImp α
inst✝ : HeytingAlgebra β
f : α → β
hf : 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
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ f (a ⇨ ⊥) = f aᶜ

Tactic:
by rw [map_himp, map_compl, map_bot, himp_bot]

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

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

Tactic:
inf_inf_sdiff

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y \ x = y \ z
⊢ ⊥ = ⊥
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case some
α✝ : 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.12
p : Option α → Type v
h : ∀ (a : p none), False
val✝ : α
⊢ ∀ (a : p (some val✝)), (some val✝).isSome = true

Tactic:
intro _

Goal state after:
case some
α✝ : 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.12
p : Option α → Type v
h : ∀ (a : p none), False
val✝ : α
a✝ : p (some val✝)
⊢ (some val✝).isSome = true
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_4
P : α → Sort u_9
e : α ≃ β
g : (b : β) → P (e.symm b)
b : β
⊢ (piCongrLeft' P e).symm g (e.symm b) = g b

Tactic:
piCongrLeft'_symm_apply,

Goal state after:
α : Sort u_1
β : Sort u_4
P : α → Sort u_9
e : α ≃ β
g : (b : β) → P (e.symm b)
b : β
⊢ ⋯ ▸ g (e (e.symm b)) = g b
Module: Mathlib.Logic.Equiv.Prod

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
β : Type u_10
γ : Type u_11
f : α ⊕ β → γ
⊢ (fun p ↦ Sum.elim p.fst p.snd) ((fun f ↦ (f ∘ inl, f ∘ inr)) f) = f

Tactic:
ext ⟨⟩ <;> rfl

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
⊢ range f = ∅ ↔ ¬(range ?m.11).Nonempty

pp: α : Type u_1
ι : Sort u_4
f : ι → α
⊢ Type ?u.23

pp: α : Type u_1
ι : Sort u_4
f : ι → α
⊢ ι → ?m.9

Tactic:
not_nonempty_iff_eq_empty

Goal state after:
α : Type u_1
ι : Sort u_4
f : ι → α
⊢ range f = ∅ ↔ range ?m.11 = ∅

α : Type u_1
ι : Sort u_4
f : ι → α
⊢ Type ?u.24

α : Type u_1
ι : Sort u_4
f : ι → α
⊢ ι → ?m.13
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i
hf : f ∈ s.pi t
⊢ t i ⊆ eval i '' s.pi t

Tactic:
refine fun y hy => ⟨update f i y, fun j hj => ?_, update_self ..⟩

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i
hf : f ∈ s.pi t
y : α i
hy : y ∈ t i
j : ι
hj : j ∈ s
⊢ update f i y j ∈ t j
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
x✝ : ∃ f t, s = graphOn f t
f : α → β
t : Set α
hs : s = graphOn f t
⊢ s = graphOn f (Prod.fst '' s)

Tactic:
by rw [hs, image_fst_graphOn]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ f '' s = t ↔ SurjOn f s t ∧ MapsTo f s t

Tactic:
refine ⟨?_, fun h => h.1.image_eq_of_mapsTo h.2⟩
  rintro rfl
  exact ⟨s.surjOn_image f, s.mapsTo_image f⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
this : f (fa x) = f (fa y)
⊢ x = y

Tactic:
h.eq,

Goal state after:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
this : fb (f x) = f (fa y)
⊢ x = y
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ (1 / a) ^ n = 1 / a ^ n

Tactic:
by simp only [one_div, inv_zpow]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop (x✝ ^ ↑x✝¹.succ) = unop (x✝ ^ ↑x✝¹ * x✝)

Tactic:
simp_rw [HPow.hPow, Pow.pow]

Goal state after:
α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop (op (unop x✝ ^ ↑x✝¹.succ)) = unop (op (unop x✝ ^ ↑x✝¹) * x✝)
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : Mul α
a x y : α
⊢ SemiconjBy (op a) (op y) (op x) ↔ SemiconjBy a x y

Tactic:
simp only [SemiconjBy, ← op_mul, op_inj, eq_comm]

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

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

Tactic:
by rw [div_eq_iff_eq_mul', div_eq_iff_eq_mul]

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

Goal state before:
pp: case inr.inl
α : 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✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
rac : r a c
⊢ f a b * (f b a * f a c) = f a b * f b c

pp: case inr.inr
α : 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✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
rca : r c a
⊢ f a b * (f b a * f a c) = f a b * f b c

Tactic:
· rw [hmul rba rac (symm pab) pac pbc]

Goal state after:
case inr.inr
α : 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✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
rca : r c a
⊢ f a b * (f b a * f a c) = f a b * f b c
Module: Mathlib.Algebra.GroupWithZero.Basic

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

Tactic:
obtain _ | _ := subsingleton_or_nontrivial α
  · exact ⟨a, Subsingleton.elim _ _⟩
  obtain ⟨b, hb⟩ := h a ha
  obtain ⟨c, hc⟩ := h b (left_ne_zero_of_mul <| hb.trans_ne one_ne_zero)
  refine ⟨b, ?_⟩
  conv_lhs => rw [← one_mul (a * b), ← hc, mul_assoc, ← mul_assoc b, hb, one_mul, hc]

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

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

Tactic:
apply inv_eq_of_mul

Goal state after:
case neg
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a✝ b✝ x a b : G₀
ha : ¬a = 0
hb : ¬b = 0
⊢ a * b * (b⁻¹ * a⁻¹) = 1
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝³ : AddZeroClass A
inst✝² : DistribSMul M A
inst✝¹ : AddZeroClass B
inst✝ : SMul M B
f : A →+ B
hf : Surjective ⇑f
smul : ∀ (c : M) (x : A), f (c • x) = c • f x
c : M
x y : B
⊢ c • (x + y) = c • x + c • y

Tactic:
rcases hf x with ⟨x, rfl⟩

Goal state after:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝³ : AddZeroClass A
inst✝² : DistribSMul M A
inst✝¹ : AddZeroClass B
inst✝ : SMul M B
f : A →+ B
hf : Surjective ⇑f
smul : ∀ (c : M) (x : A), f (c • x) = c • f x
c : M
y : B
x : A
⊢ c • (f x + y) = c • f x + c • y
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
⊢ ¬g • 0 * (g • 0)⁻¹ = 1

Tactic:
← smul_one g,

Goal state after:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
⊢ ¬g • 0 * (g • 0)⁻¹ = g • 1
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M →+ M₂
hf : Surjective ⇑f
smul : ∀ (c : R) (x : M), f (c • x) = c • f x
c₁ c₂ : R
x : M₂
⊢ (c₁ + c₂) • x = c₁ • x + c₂ • x

Tactic:
rcases hf x with ⟨x, rfl⟩

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M →+ M₂
hf : Surjective ⇑f
smul : ∀ (c : R) (x : M), f (c • x) = c • f x
c₁ c₂ : R
x : M
⊢ (c₁ + c₂) • f x = c₁ • f x + c₂ • f x
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M →+ M₂
hf : Surjective ⇑f
smul : ∀ (c : R) (x : M), f (c • x) = c • f x
x : M₂
⊢ 0 • x = 0

Tactic:
rcases hf x with ⟨x, rfl⟩

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M →+ M₂
hf : Surjective ⇑f
smul : ∀ (c : R) (x : M), f (c • x) = c • f x
x : M
⊢ 0 • f x = 0
Module: Mathlib.Algebra.GroupWithZero.Semiconj

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

Tactic:
h.eq,

Goal state after:
case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
this : y * a ≠ 0
⊢ SemiconjBy a x⁻¹ y⁻¹
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
⊢ a / b * b = a

Tactic:
obtain rfl | hb := eq_or_ne b 0

Goal state after:
case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : 0 = 0 → a = 0
⊢ a / 0 * 0 = a

case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
hb : b ≠ 0
⊢ a / b * b = a
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
⊢ a * b / b = a

Tactic:
obtain rfl | hb := eq_or_ne b 0

Goal state after:
case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : 0 = 0 → a = 0
⊢ a * 0 / 0 = a

case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
hb : b ≠ 0
⊢ a * b / b = a
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = a * a - a * b + (b * a - b * b)

Tactic:
h.eq,

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = a * a - b * a + (b * a - b * b)
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = a * a - b * a + (a * b - b * b)

Tactic:
h.eq,

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = a * a - b * a + (b * a - b * b)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
c : ℕ
a : α
⊢ ((-a) ^ 2) ^ c = (a ^ 2) ^ c

Tactic:
neg_sq

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

Goal state before:
pp: case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r b c
⊢ r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)

Tactic:
· rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a] at bc
    exact h a⁻¹ bc

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h : CovariantClass α>0 α (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 ≤ x2
a : α
ha : 0 ≤ a
b c : α
hbc : b ≤ c
⊢ a * b ≤ a * c

Tactic:
obtain ha | ha := ha.eq_or_lt
        · simp [← ha]
        · exact @CovariantClass.elim α>0 α (fun x y => x * y) (· ≤ ·) _ ⟨_, ha⟩ _ _ hbc

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

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

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ one_le_pow₀ h⟩
  contrapose! h
  exact pow_lt_one₀ ha h hn

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

Goal state before:
pp: G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
ha : 0 ≤ a
⊢ a * b * b⁻¹ ≤ a

Tactic:
obtain rfl | hb := eq_or_ne b 0

Goal state after:
case inl
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a : G₀
ha : 0 ≤ a
⊢ a * 0 * 0⁻¹ ≤ a

case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
ha : 0 ≤ a
hb : b ≠ 0
⊢ a * b * b⁻¹ ≤ a