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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : α
b : P → α
c : ¬P → α
⊢ (a * if h : P then b h else c h) = if h : P then a * b h else a * c h

Tactic:
split <;> rfl

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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : α
⊢ (if h : P then a h else b h) * c = if h : P then a h * c else b h * c

Tactic:
split <;> rfl

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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
⊢ ((if h : P then a h else b h) * if h : P then c h else d h) = if h : P then a h * c h else b h * d h

Tactic:
split <;> rfl

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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a b c d : α
⊢ ((if P then a else b) * if P then c else d) = if P then a * c else b * d

Tactic:
split <;> rfl

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

Goal state before:
pp: α : Type u_3
P : Prop
inst✝¹ : Decidable P
inst✝ : Neg α
b c : α
⊢ (-if P then b else c) = if P then -b else -c

Tactic:
split <;> rfl

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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : α
b : P → α
c : ¬P → α
⊢ (a / if h : P then b h else c h) = if h : P then a / b h else a / c h

Tactic:
split <;> rfl

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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : α
⊢ (if h : P then a h else b h) / c = if h : P then a h / c else b h / c

Tactic:
split <;> rfl

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

Goal state before:
pp: α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
⊢ ((if h : P then a h else b h) / if h : P then c h else d h) = if h : P then a h / c h else b h / d h

Tactic:
split <;> rfl

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

Goal state before:
pp: M : Type u_2
inst✝ : CancelCommMonoid M
a x y : M
h : x = y
⊢ a * y = y * a

Tactic:
mul_comm

Goal state after:
M : Type u_2
inst✝ : CancelCommMonoid M
a x y : M
h : x = y
⊢ y * a = y * a
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
⊢ IsMulCommutative M ↔ ∀ (a b : M), a * b = b * a

Tactic:
by
  grind [IsMulCommutative, Std.Commutative]

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m : M
⊢ npowRec' (2 * k) m = npowRec' k (m * m)

Tactic:
induction k using Nat.strongRecOn with
  | ind k' ih =>
    match k' with
    | 0 => rfl
    | 1 => simp [npowRec']
    | k + 2 =>
      simp [npowRec', ← mul_assoc, ← ih, Nat.mul_succ]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: p : Prop
⊢ Decidable p

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
p : α → Prop
⊢ DecidablePred p

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
p : α → α → Prop
⊢ DecidableRel p

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α✝ : Sort u_1
α : Sort u_2
⊢ DecidableEq α

Tactic:
infer_instance

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

Goal state before:
pp: α : Sort u
β : Sort v
h : Nonempty α
inst✝ : IsEmpty β
⊢ IsEmpty (α → β)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Std.Refl r ↔ Eq ≤ r

Tactic:
unfold Pi.hasLe Prop.le
  grind [Std.Refl]

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
exact ⟨fun ⟨x', y', hr, hx, hy⟩ ↦ hinj hx ▸ hinj hy ▸ hr, fun h ↦ ⟨x, y, h, rfl, rfl⟩⟩

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α✝ : Sort u_1
β : Sort u_2
ι : Type u_3
α : ι → Sort u_4
S : (i : ι) → Setoid (α i)
⊢ Setoid ((i : ι) → α i)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α✝ : Sort u_1
β : Sort u_2
ι : Type u_3
α : ι → Type u_4
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
⊢ Setoid ((i : ι) → α i)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
a b✝ c : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
this : ∃ a, ReflTransGen r e a ∧ ReflGen r b a
⊢ Join (ReflTransGen r) e c

Tactic:
rcases this with ⟨a, hea, hba⟩

Goal state after:
case tail
α : Type u_1
r : α → α → Prop
a✝¹ b✝ c : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a✝¹ c
d e : α
a✝ : ReflTransGen r a✝¹ d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
a : α
hea : ReflTransGen r e a
hba : ReflGen r b a
⊢ Join (ReflTransGen r) e c
Module: Mathlib.Order.Compare

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a < b
⊢ o.Compares a b

pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a = b
⊢ o.Compares a b

pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : b < a
⊢ o.Compares a b

Tactic:
· have hab : Compares Ordering.lt a b := hab
    rwa [ho.inj (h hab)]

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a = b
⊢ o.Compares a b

case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : b < a
⊢ o.Compares a b
Module: Mathlib.Order.Monotone.Basic

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

Tactic:
rw [strictMonoOn_toDual_comp_iff, strictAntiOn_comp_ofDual_iff]

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ Disjoint x y ↔ x ≤ z

Tactic:
by
  rw [disjoint_iff]
  exact h.inf_left_eq_bot_iff

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

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ s ⊂ {x} ↔ s = ∅

Tactic:
ssubset_iff_subset_ne,

Goal state after:
α : Type u_1
s : Set α
x : α
⊢ s ⊆ {x} ∧ s ≠ {x} ↔ s = ∅
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
f : α → β
h : ∀ (x y : α), f x ≤ f (x ⊔ y)
⊢ Monotone f

Tactic:
intro x y hxy
  rw [← sup_eq_right.2 hxy]
  apply h

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

Goal state before:
pp: case refine_2
α : Type u
s : Set α
h : s.Nonempty ∧ s.Subsingleton
⊢ ∃ a, s = {a}

Tactic:
exact h.2.eq_empty_or_singleton.resolve_left h.1.ne_empty

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

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

Tactic:
by
  rw [le_himp_iff, le_himp_iff, inf_assoc, himp_inf_self, ← inf_assoc, himp_inf_self, inf_assoc]
  exact inf_le_left

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
⊢ HeytingAlgebra α

Tactic:
let compl := e.compl

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
⊢ HeytingAlgebra α
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.14
β : Type ?u.13
p : α ⊕ β → Prop
⊢ RightInverse
    (fun x ↦
      match x with
      | inl a => ⟨inl ↑a, ⋯⟩
      | inr b => ⟨inr ↑b, ⋯⟩)
    fun x ↦
    match x with
    | ⟨inl a, h⟩ => inl ⟨a, h⟩
    | ⟨inr b, h⟩ => inr ⟨b, h⟩

Tactic:
rintro (a | b)

Goal state after:
case inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.14
β : Type ?u.13
p : α ⊕ β → Prop
a : { a // p (inl a) }
⊢ (fun x ↦
        match x with
        | ⟨inl a, h⟩ => inl ⟨a, h⟩
        | ⟨inr b, h⟩ => inr ⟨b, h⟩)
      ((fun x ↦
          match x with
          | inl a => ⟨inl ↑a, ⋯⟩
          | inr b => ⟨inr ↑b, ⋯⟩)
        (inl a)) =
    inl a

case inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.14
β : Type ?u.13
p : α ⊕ β → Prop
b : { b // p (inr b) }
⊢ (fun x ↦
        match x with
        | ⟨inl a, h⟩ => inl ⟨a, h⟩
        | ⟨inr b, h⟩ => inr ⟨b, h⟩)
      ((fun x ↦
          match x with
          | inl a => ⟨inl ↑a, ⋯⟩
          | inr b => ⟨inr ↑b, ⋯⟩)
        (inr b)) =
    inr b
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.14
β : Type ?u.13
t : α ⊕ β → Type u_9
⊢ RightInverse (Sum.elim (fun a ↦ ⟨inl a.fst, a.snd⟩) fun b ↦ ⟨inr b.fst, b.snd⟩) fun x ↦
    match x with
    | ⟨inl x, y⟩ => inl ⟨x, y⟩
    | ⟨inr x, y⟩ => inr ⟨x, y⟩

Tactic:
rintro (⟨x,y⟩|⟨x,y⟩) <;> simp

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a : α
⊢ ⊥ ∆ a = a

Tactic:
rw [symmDiff_comm, symmDiff_bot]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
{ rw [sdiff_symmDiff', sup_comm (c ⊓ a ⊓ b), symmDiff_sdiff] }

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
⊢ BooleanAlgebra α

Tactic:
let compl := e.compl

Goal state after:
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
⊢ BooleanAlgebra α
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ f '' s ∪ g '' sᶜ → y ∈ range (s.piecewise f g)

Tactic:
· rintro (⟨x, hx, rfl⟩ | ⟨x, hx, rfl⟩) <;> use x <;> simp_all

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 ⊆ s₂

Tactic:
← h.preimage_image_inter h₂

Goal state after:
α : 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
Module: Mathlib.Algebra.Group.Torsion

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
a : G
⊢ a = a⁻¹ ↔ a = 1

Tactic:
rw [← sq_eq_one, sq, mul_eq_one_iff_eq_inv]

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

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
a : G
⊢ a = a⁻¹ ↔ a = 1

Tactic:
by rw [← sq_eq_one, sq, mul_eq_one_iff_eq_inv]

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

Goal state before:
pp: m n : ℕ
h : n.succ ≤ m
⊢ ofNat m + -[n+1] = ofNat (m - n.succ)

Tactic:
negSucc_eq,

Goal state after:
m n : ℕ
h : n.succ ≤ m
⊢ ofNat m + -(↑n + 1) = ofNat (m - n.succ)
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Mul M₁
inst✝ : CommMagma M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y : M₁
⊢ f x * f y = f y * f x

Tactic:
mul_comm

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Mul M₁
inst✝ : CommMagma M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y : M₁
⊢ f y * f x = f y * f x
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
rw [h, inv_mul_cancel]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
m n : ℤ
⊢ a ^ m * a ^ n = a ^ n * a ^ m

Tactic:
rw [← zpow_add, Int.add_comm, zpow_add]

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

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

Tactic:
mul_comm

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

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

Tactic:
mul_comm

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

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

Tactic:
mul_comm

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ a = b * c ↔ a = b * c
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:
div_eq_iff_eq_mul',

Goal state after:
G : Type u_3
inst✝ : CommGroup 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✝ : CommGroup G
a b c : G
⊢ b * a = a * b

Tactic:
mul_comm

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ a * b = a * b
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:
mul_comm

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

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

Tactic:
div_eq_iff_eq_mul',

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a = c * b / d ↔ a = c * (b / d)
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
⊢ IsUnit a → IsUnit b → IsUnit (a * b)

Tactic:
rintro ⟨x, rfl⟩ ⟨y, rfl⟩; exact ⟨x * y, rfl⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
⊢ IsUnit a → IsUnit b → IsUnit (a * b)

Tactic:
by
  rintro ⟨x, rfl⟩ ⟨y, rfl⟩; exact ⟨x * y, rfl⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
this : IsUnit (a * ↑u * ↑u⁻¹)
⊢ IsUnit a

Tactic:
rwa [mul_assoc, Units.mul_inv, mul_one] at this

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

Goal state before:
pp: α : Type u
inst✝ : CommMonoid α
a c : α
b d : αˣ
⊢ ↑d * a = c * ↑b ↔ a * ↑d = c * ↑b

Tactic:
mul_comm

Goal state after:
α : Type u
inst✝ : CommMonoid α
a c : α
b d : αˣ
⊢ a * ↑d = c * ↑b ↔ a * ↑d = c * ↑b
Module: Mathlib.Algebra.Group.Units.Hom

Goal state before:
pp: M : Type u_3
N : Type u_4
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit (f x)
x : M
⊢ ∀ (x : M), ↑⋯.unit = f x

Tactic:
intro

Goal state after:
M : Type u_3
N : Type u_4
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit (f x)
x x✝ : M
⊢ ↑⋯.unit = f x✝
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b * a = 1

Tactic:
mul_comm

Goal state after:
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ a * b = 1
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
b d : α
hb : IsUnit b
hd : IsUnit d
a c : α
h : a / b = c / d
⊢ a * (b / b) * d = c * b

Tactic:
← mul_comm_div,

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
b d : α
hb : IsUnit b
hd : IsUnit d
a c : α
h : a / b = c / d
⊢ a / b * b * d = c * b
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case neg
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
hx : ¬p x
⊢ (ofSubtype (f.subtypePerm h₁)) x = f x

Tactic:
rw [ofSubtype, MonoidHom.coe_mk, OneHom.coe_mk,
        Equiv.Perm.extendDomain_apply_not_subtype _ _ hx]

Goal state after:
case neg
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
hx : ¬p x
⊢ x = f x
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : (k + 1) % 2 = 0
⊢ ((k + 1) / 2).binCast + ((k + 1) / 2).binCast = ↑((k + 1) % 2 + 2 * ((k + 1) / 2))

Tactic:
hk _ <| Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2),

Goal state after:
case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : (k + 1) % 2 = 0
⊢ ↑((k + 1) / 2) + ↑((k + 1) / 2) = ↑((k + 1) % 2 + 2 * ((k + 1) / 2))
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b x✝ x : G₀
hx : x ≠ 0
y z : G₀
h : (fun x_1 ↦ x_1 * x) y = (fun x_1 ↦ x_1 * x) z
⊢ y = z

Tactic:
dsimp only at h; rw [← mul_inv_cancel_right₀ hx y, h, mul_inv_cancel_right₀ hx z]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
⊢ ((k + 1) / 2).binCast + ((k + 1) / 2).binCast + 1 = ↑((k + 1) % 2 + 2 * ((k + 1) / 2))

Tactic:
hk _ <| Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2),

Goal state after:
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
⊢ ↑((k + 1) / 2) + ↑((k + 1) / 2) + 1 = ↑((k + 1) % 2 + 2 * ((k + 1) / 2))
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then ((k + 1) / 2).binCast + ((k + 1) / 2).binCast
    else ((k + 1) / 2).binCast + ((k + 1) / 2).binCast + 1) =
    ↑(k + 1)

Tactic:
· conv => rhs; rw [← Nat.mod_add_div (k + 1) 2]
        rw [if_neg h, hk _ <| Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
        have h1 := Or.resolve_left (Nat.mod_two_eq_zero_or_one (succ k)) h
        rw [h1, Nat.add_comm 1, Nat.succ_mul, Nat.one_mul]
        simp only [Nat.cast_add, Nat.cast_one]

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

Goal state before:
pp: ⊢ AddCommMonoid ℤ

Tactic:
infer_instance

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

Goal state before:
pp: ⊢ AddMonoid ℤ

Tactic:
infer_instance

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

Goal state before:
pp: ⊢ Monoid ℤ

Tactic:
infer_instance

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

Goal state before:
pp: ⊢ CommSemigroup ℤ

Tactic:
infer_instance

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

Goal state before:
pp: ⊢ Semigroup ℤ

Tactic:
infer_instance

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

Goal state before:
pp: ⊢ AddGroup ℤ

Tactic:
infer_instance

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

Goal state before:
pp: ⊢ AddCommSemigroup ℤ

Tactic:
infer_instance

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

Goal state before:
pp: ⊢ AddSemigroup ℤ

Tactic:
infer_instance

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

Goal state before:
pp: ⊢ AddCommMonoid ℕ

Tactic:
infer_instance

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

Goal state before:
pp: ⊢ AddMonoid ℕ

Tactic:
infer_instance

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

Goal state before:
pp: ⊢ Monoid ℕ

Tactic:
infer_instance

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

Goal state before:
pp: ⊢ CommSemigroup ℕ

Tactic:
infer_instance

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

Goal state before:
pp: ⊢ Semigroup ℕ

Tactic:
infer_instance

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

Goal state before:
pp: ⊢ AddCommSemigroup ℕ

Tactic:
infer_instance

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

Goal state before:
pp: ⊢ AddSemigroup ℕ

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a b c : α
h : c * a = b
⊢ a * c = b

Tactic:
mul_comm

Goal state after:
α : Type u_1
inst✝ : CommSemigroup α
a b c : α
h : a * c = b
⊢ a * c = b
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a b : α
h : a ∣ b
c : α
⊢ a ∣ c * b

Tactic:
mul_comm

Goal state after:
α : Type u_1
inst✝ : CommSemigroup α
a b : α
h : a ∣ b
c : α
⊢ a ∣ b * c
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a b c : α
⊢ b = c * a ↔ b = a * c

Tactic:
mul_comm

Goal state after:
α : Type u_1
inst✝ : CommSemigroup α
a b c : α
⊢ b = a * c ↔ b = a * c
Module: Mathlib.Algebra.Group.Hom.Instances

Goal state before:
pp: M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g₁ g₂ : N →* P
⊢ { toFun := (g₁ * g₂).comp, map_one' := ⋯, map_mul' := ⋯ } =
    { toFun := g₁.comp, map_one' := ⋯, map_mul' := ⋯ } * { toFun := g₂.comp, map_one' := ⋯, map_mul' := ⋯ }

Tactic:
ext1 f
    exact mul_comp g₁ g₂ f

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
⊢ a = 0 ∨ ∃ u, a = ↑u

Tactic:
by
  simpa using em _

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

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

Tactic:
← mul_comm_div,

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

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
M : Type u_4
inst✝ : Nontrivial M
hM : MonoidWithZero M
h : ∀ (a : M), IsUnit a ∨ a = 0
a : M
h0 : a ≠ 0
⊢ a = ↑⋯.unit

Tactic:
IsUnit.unit_spec

Goal state after:
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
M : Type u_4
inst✝ : Nontrivial M
hM : MonoidWithZero M
h : ∀ (a : M), IsUnit a ∨ a = 0
a : M
h0 : a ≠ 0
⊢ a = a