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

Goal state before:
pp: S : Type u_3
inst✝ : Semigroup S
a b : S
reg : IsLeftRegular a
⊢ Commute (a * b) a ↔ Commute a b

Tactic:
by
  simp [commute_iff_eq, mul_assoc, reg.eq_iff, eq_comm]

Goal state after:
Module: Mathlib.Logic.Relation

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

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

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
exact trans hab (.single hbc) ih (single hbc)

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
reflGen_eq_self

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
⊢ TransGen r = TransGen r
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : SMul M α
inst✝³ : SMul Mᵐᵒᵖ α
inst✝² : IsCentralScalar M α
inst✝¹ : SMul N α
inst✝ : SMulCommClass M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ MulOpposite.unop m • n • a = n • MulOpposite.unop m • a

Tactic:
smul_comm

Goal state after:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : SMul M α
inst✝³ : SMul Mᵐᵒᵖ α
inst✝² : IsCentralScalar M α
inst✝¹ : SMul N α
inst✝ : SMulCommClass M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ n • MulOpposite.unop m • a = n • MulOpposite.unop m • a
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : SMul M α
inst✝³ : SMul N α
inst✝² : SMul Nᵐᵒᵖ α
inst✝¹ : IsCentralScalar N α
inst✝ : SMulCommClass M N α
m : M
n : Nᵐᵒᵖ
a : α
⊢ m • MulOpposite.unop n • a = MulOpposite.unop n • m • a

Tactic:
smul_comm

Goal state after:
M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : SMul M α
inst✝³ : SMul N α
inst✝² : SMul Nᵐᵒᵖ α
inst✝¹ : IsCentralScalar N α
inst✝ : SMulCommClass M N α
m : M
n : Nᵐᵒᵖ
a : α
⊢ MulOpposite.unop n • m • a = MulOpposite.unop n • m • a
Module: Mathlib.Data.Option.Basic

Goal state before:
pp: α : Type u_1
d : α
⊢ (fun x ↦ x.getD d) ∘ some = id

Tactic:
by
  ext
  simp only [Function.comp_apply, getD_some, id_eq]

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

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

Tactic:
| ind x IH =>

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
x y : α × β
⊢ (Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd) ∧ Codisjoint x.fst y.fst ∧ Codisjoint x.snd y.snd ↔
    (Disjoint x.fst y.fst ∧ Codisjoint x.fst y.fst) ∧ Disjoint x.snd y.snd ∧ Codisjoint x.snd y.snd

Tactic:
and_and_and_comm

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

Goal state before:
pp: n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : ¬f 0 = f 1
hlt : f 1 < f 0
g : ℕ → ℕ := fun i ↦ f (i + 1)
hg_anti : Antitone g
p : ℕ
hp : p ≤ f 1
hp' : ∀ (m : ℕ), p ≤ m → g m = g p
⊢ p + 1 ≤ n

Tactic:
omega

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u_1
A B : Lattice α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B

Tactic:
cases A
  cases B
  cases SemilatticeSup.ext H
  cases SemilatticeInf.ext H
  congr

Goal state after:
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)
x y : α
hxy : x ≤ y
⊢ f x ≤ f y

Tactic:
← sup_eq_right.2 hxy

Goal state after:
α : Type u
β : Type v
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
f : α → β
h : ∀ (x y : α), f x ≤ f (x ⊔ y)
x y : α
hxy : x ≤ y
⊢ f x ≤ f (x ⊔ y)
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α : Type u₀
x✝ : f α
⊢ ⇑(Equiv.refl α) <$> x✝ = id x✝

Tactic:
apply LawfulFunctor.id_map

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

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

Tactic:
by rw [inf_comm, inf_inf_sdiff]

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

Goal state before:
pp: α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x : β₁ i
j : α₁
y : β₁ j
h : Sigma.map f₁ f₂ ⟨i, x⟩ = Sigma.map f₁ f₂ ⟨j, y⟩
⊢ ⟨i, x⟩ = ⟨j, y⟩

Tactic:
by
    obtain rfl : i = j := h₁ (Sigma.mk.inj_iff.mp h).1
    obtain rfl : x = y := h₂ i (sigma_mk_injective h)
    rfl

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

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

pp: case i
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = ⊥

Tactic:
· calc
      x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y)) := by
          rw [sup_inf_right]
      _ = (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) := by ac_rfl
      _ = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y) := by
          rw [sup_inf_self, sup_sdiff_left, ← sup_assoc, sup_inf_left, sdiff_sup_self',
            inf_sup_right, sup_comm y, inf_sdiff_sup_right, inf_sup_left x z y]
      _ = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ (x ⊓ y ⊔ x \ y))) := by ac_rfl
      _ = x := by simp

Goal state after:
case i
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = ⊥
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
p : α → Prop
q : β → Prop
r : γ → Prop
e : α ≃ β
f : β ≃ γ
h : ∀ (a : α), p a ↔ q (e a)
h' : ∀ (b : β), q b ↔ r (f b)
⊢ ∀ (a : α), p a ↔ r ((e.trans f) a)

Tactic:
by as_aux_lemma => exact fun a => (h a).trans (h' <| e a)

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
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), s₂ x y ↔ s₁ ↑x ↑y
a : Quotient s₁
ha : p₂ a
⊢ (fun a ↦ a.liftOn (fun a ↦ ⟨⟦↑a⟧, ⋯⟩) ⋯)
      ((fun a ↦ Quotient.hrecOn (motive := fun x ↦ p₂ x → Quotient s₂) (↑a) (fun a h ↦ ⟦⟨a, ⋯⟩⟧) ⋯ ⋯) ⟨a, ha⟩) =
    ⟨a, ha⟩

Tactic:
induction a using Quotient.inductionOn

Goal state after:
case h
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), s₂ x y ↔ s₁ ↑x ↑y
a✝ : α
ha : p₂ ⟦a✝⟧
⊢ (fun a ↦ a.liftOn (fun a ↦ ⟨⟦↑a⟧, ⋯⟩) ⋯)
      ((fun a ↦ Quotient.hrecOn (motive := fun x ↦ p₂ x → Quotient s₂) (↑a) (fun a h ↦ ⟦⟨a, ⋯⟩⟧) ⋯ ⋯) ⟨⟦a✝⟧, ha⟩) =
    ⟨⟦a✝⟧, ha⟩
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
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), s₂ x y ↔ s₁ ↑x ↑y
a : Quotient s₂
⊢ (fun a ↦ Quotient.hrecOn (motive := fun x ↦ p₂ x → Quotient s₂) (↑a) (fun a h ↦ ⟦⟨a, ⋯⟩⟧) ⋯ ⋯)
      ((fun a ↦ a.liftOn (fun a ↦ ⟨⟦↑a⟧, ⋯⟩) ⋯) a) =
    a

Tactic:
induction a using Quotient.inductionOn

Goal state after:
case h
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), s₂ x y ↔ s₁ ↑x ↑y
a✝ : Subtype p₁
⊢ (fun a ↦ Quotient.hrecOn (motive := fun x ↦ p₂ x → Quotient s₂) (↑a) (fun a h ↦ ⟦⟨a, ⋯⟩⟧) ⋯ ⋯)
      ((fun a ↦ a.liftOn (fun a ↦ ⟨⟦↑a⟧, ⋯⟩) ⋯) ⟦a✝⟧) =
    ⟦a✝⟧
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case mp.inl
α : Type u_9
inst✝ : DecidableEq α
s : Set α
j : α
hj : ¬j ∈ s
a : α
ha hi : a ∈ s
⊢ (swap a j) a ∈ insert j s \ {a}

Tactic:
rw [swap_apply_left]

Goal state after:
case mp.inl
α : Type u_9
inst✝ : DecidableEq α
s : Set α
j : α
hj : ¬j ∈ s
a : α
ha hi : a ∈ s
⊢ j ∈ insert j s \ {a}
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁

Tactic:
constructor
  · intro heq
    have h₁ : (s₁ ×ˢ t₁ : Set _).Nonempty := by rwa [← heq]
    rw [prod_nonempty_iff] at h h₁
    rw [← fst_image_prod s h.2, ← fst_image_prod s₁ h₁.2, heq, eq_self_iff_true, true_and, ←
      snd_image_prod h.1 t, ← snd_image_prod h₁.1 t₁, heq]
  · grind

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

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
h : (i : α) → δ i → δ' i
x : α
⊢ h x (s.piecewise f g x) = s.piecewise (fun x ↦ h x (f x)) (fun x ↦ h x (g x)) x

Tactic:
by_cases hx : x ∈ s

Goal state after:
case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
h : (i : α) → δ i → δ' i
x : α
hx : x ∈ s
⊢ h x (s.piecewise f g x) = s.piecewise (fun x ↦ h x (f x)) (fun x ↦ h x (g x)) x

case neg
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
h : (i : α) → δ i → δ' i
x : α
hx : ¬x ∈ s
⊢ h x (s.piecewise f g x) = s.piecewise (fun x ↦ h x (f x)) (fun x ↦ h x (g x)) x
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
δ'' : α → Sort u_9
f' g' : (i : α) → δ' i
h : (i : α) → δ i → δ' i → δ'' i
x : α
⊢ h x (s.piecewise f g x) (s.piecewise f' g' x) = s.piecewise (fun x ↦ h x (f x) (f' x)) (fun x ↦ h x (g x) (g' x)) x

Tactic:
by_cases hx : x ∈ s

Goal state after:
case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
δ'' : α → Sort u_9
f' g' : (i : α) → δ' i
h : (i : α) → δ i → δ' i → δ'' i
x : α
hx : x ∈ s
⊢ h x (s.piecewise f g x) (s.piecewise f' g' x) = s.piecewise (fun x ↦ h x (f x) (f' x)) (fun x ↦ h x (g x) (g' x)) x

case neg
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
δ'' : α → Sort u_9
f' g' : (i : α) → δ' i
h : (i : α) → δ i → δ' i → δ'' i
x : α
hx : ¬x ∈ s
⊢ h x (s.piecewise f g x) (s.piecewise f' g' x) = s.piecewise (fun x ↦ h x (f x) (f' x)) (fun x ↦ h x (g x) (g' x)) x
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
x : α
⊢ s.piecewise f f x = f x

Tactic:
by_cases hx : x ∈ s

Goal state after:
case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
x : α
hx : x ∈ s
⊢ s.piecewise f f x = f x

case neg
α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
x : α
hx : ¬x ∈ s
⊢ s.piecewise f f x = f x
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : ¬i ∈ s
⊢ eval i '' s.pi t = if (s.pi t).Nonempty then univ else ∅

Tactic:
classical
  ext xᵢ
  simp only [eval, mem_image, mem_pi, Set.Nonempty, mem_ite_empty_right, mem_univ, and_true]
  constructor
  · rintro ⟨x, hx, rfl⟩
    exact ⟨x, hx⟩
  · rintro ⟨x, hx⟩
    refine ⟨Function.update x i xᵢ, ?_⟩
    simpa +contextual [(ne_of_mem_of_not_mem · hi)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : MapsTo (⇑g) s t
a : α
ha : a ∈ s
⊢ ↑(f (g a)) = (g.extendDomain f) ↑(f a)

Tactic:
extendDomain_apply_image

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : SurjOn (⇑g) s t
b : α
hb : b ∈ s
ha : g b ∈ t
⊢ (g.extendDomain f) ↑(f b) = ↑(f (g b))

Tactic:
extendDomain_apply_image

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

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

Tactic:
by
  rw [eq_inv_of_mul_eq_one_left h, one_div]

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

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

Tactic:
eq_inv_of_mul_eq_one_right h,

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a * b = 1
⊢ a⁻¹ = 1 / a
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : Mul α
a x y : αᵐᵒᵖ
⊢ SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y

Tactic:
by
  conv_rhs => rw [← op_unop a, ← op_unop x, ← op_unop y, semiconjBy_op]

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:
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: case hmul
α : Type u_1
β : Type u_2
inst✝¹ : Monoid β
r : α → α → Prop
inst✝ : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
this : Std.Symm fun x1 x2 ↦ p x1 ∧ p x2
⊢ ∀ {a b c : α}, r a b → r b c → p a ∧ p b → p b ∧ p c → p a ∧ p c → f a c = f a b * f b c

Tactic:
exact fun rab rbc pab _pbc pac => hmul rab rbc pab.1 pab.2 pac.2

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
u : αˣ
⊢ ↑u⁻¹ * ↑u = 1

Tactic:
Units.inv_mul

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
u : αˣ
⊢ 1 = 1
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 0 + 1 = 1

Tactic:
zero_add

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 1 = 1
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: A : Type u_2
inst✝ : AddMonoidWithOne A
n : ℕ
⊢ (n + 1) • 1 = ↑(n + 1)

Tactic:
by simp [succ_nsmul, nsmul_one n]

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

Goal state before:
pp: case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : m = 0
⊢ a ^ (m + n) = a ^ m * a ^ n

Tactic:
simp [hm]

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

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

Tactic:
smul_one

Goal state after:
case neg
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x : β
hx : ¬x = 0
⊢ 1 = 1
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: m n : ℤ
| m.gcd n

Tactic:
← m.emod_add_mul_ediv n,

Goal state after:
m n : ℤ
| (m % n + n * (m / n)).gcd n
Module: Mathlib.Data.Nat.Cast.Basic

Goal state before:
pp: case zero
α : Type u_1
inst✝ : NonAssocSemiring α
a : α
⊢ 0 • a = a * ↑0

Tactic:
rw [zero_nsmul, Nat.cast_zero, mul_zero]

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

Goal state before:
pp: case pos
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : IsUnit (a * b)
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
obtain ⟨⟨a, rfl⟩, b, rfl⟩ := h.isUnit_mul_iff.mp hab

Goal state after:
case pos
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀ˣ
h : Commute ↑a ↑b
hab : IsUnit (↑a * ↑b)
⊢ (↑a * ↑b)⁻¹ʳ = (↑b)⁻¹ʳ * (↑a)⁻¹ʳ
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
⊢ ↑u⁻¹ * ↑u = 1

Tactic:
Units.inv_mul

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
⊢ 1 = 1
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : (-1) ^ n = 1
⊢ (-1) ^ (n + 1) = -1

Tactic:
rw [pow_succ, h, one_mul]

Goal state after:
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: β : Type u_4
inst✝ : AddGroup β
f : ℤ →+ β
n : ℤ
⊢ f n = n • f 1

Tactic:
by
  rw [← zmultiplesHom_symm_apply, ← zmultiplesHom_apply, Equiv.apply_symm_apply]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
f✝ : S → R
hf✝ : Injective f✝
inst✝¹² : Add S
inst✝¹¹ : Mul S
inst✝¹⁰ : Zero S
inst✝⁹ : One S
inst✝⁸ : Neg S
inst✝⁷ : Sub S
inst✝⁶ : SMul ℕ S
inst✝⁵ : SMul ℤ S
inst✝⁴ : Pow S ℕ
inst✝³ : NatCast S
inst✝² : IntCast S
f : S → R
hf : Injective f
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
⊢ f (-x * y) = f (-(x * y))

Tactic:
by rw [neg, mul, neg, neg_mul, mul]

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : PosMulStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ a * b < a * c

Tactic:
rw [← lt, mul, mul]; exact mul_lt_mul_of_pos_left (lt.2 hbc) (by rwa [← zero, lt])

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ d * a = 0 + d * a

Tactic:
zero_add

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ d * a = d * a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a b : M₀
inst✝ : PosMulStrictMono M₀
ha : 0 < a
hb : 1 < b
⊢ a < a * b

Tactic:
by
  simpa using mul_lt_mul_of_pos_left hb ha

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ a * d = 0 + a * d

Tactic:
zero_add

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ a * d = a * d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

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

Tactic:
by
  obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

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₀
hb : b ≤ 0
⊢ b ≤ a * (a⁻¹ * b)

Tactic:
by
  obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

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₀
hb : 0 ≤ b
⊢ a⁻¹ * (a * b) ≤ b

Tactic:
by
  obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

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₀
hb : b ≤ 0
⊢ b ≤ a⁻¹ * (a * b)

Tactic:
by
  obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ d * a = 0 + d * a

Tactic:
zero_add

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ d * a = d * a
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ a * d = 0 + a * d

Tactic:
zero_add

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ a * d = a * d
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
a d : R
inst✝¹ : PosMulMono R
inst✝ : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
⊢ b * a ≤ max d b * max c a

Tactic:
gcongr
    exacts [ha, hd.trans <| le_max_left d b, le_max_right d b, le_max_right c a]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a✝ b✝ : β
h : s a✝ b✝
⊢ r (surjInv hf a✝) (surjInv hf b✝)

Tactic:
by simpa only [o, surjInv_eq hf] using h

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

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
rra : IsRightRegular a
⊢ IsRightRegular (a ^ n)

Tactic:
rw [IsRightRegular, ← mul_right_iterate]
  exact rra.iterate n

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

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ 0 + b = b

Tactic:
zero_add

Goal state after:
case inl
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ b = b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case some.none
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b : α
⊢ ↑a + Option.some b ≤ ↑a + none → Option.some b ≤ none

Tactic:
simp [some_eq_coe, ← coe_add, none_eq_bot]

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

Goal state before:
pp: case mpr
m : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ (p m ∧ ∀ (n : ℕ), n < m → ¬p n) → Nat.find h = m

Tactic:
rintro ⟨hm, hlt⟩
    have := Nat.find_min' h hm
    grind

Goal state after: