mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
⊢ binaryRec zero bit (Nat.bit b n) = bit b n (binaryRec zero bit n)

Tactic:
by_cases h' : n.bit b = 0

Goal state after:
case pos
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : Nat.bit b n = 0
⊢ binaryRec zero bit (Nat.bit b n) = bit b n (binaryRec zero bit n)

case neg
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : ¬Nat.bit b n = 0
⊢ binaryRec zero bit (Nat.bit b n) = bit b n (binaryRec zero bit n)
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ ReflGen (TransGen r) = ReflTransGen r

Tactic:
ext x y
  simp_rw [reflTransGen_iff_eq_or_transGen, reflGen_iff]

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_1
β : Sort u_2
ra : α → α → Prop
rb : β → β → Prop
φ : Quot ra → Quot rb → Sort u_3
qa : Quot ra
qb : Quot rb
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ca : ∀ {b : β} {a₁ a₂ : α}, ra a₁ a₂ → f a₁ b ≍ f a₂ b
cb : ∀ {a : α} {b₁ b₂ : β}, rb b₁ b₂ → f a b₁ ≍ f a b₂
a₁ a₂ : α
pa : ra a₁ a₂
b : β
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
          simp

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_1
β : Sort u_2
ra : α → α → Prop
rb : β → β → Prop
φ : Quot ra → Quot rb → Sort u_3
qa : Quot ra
qb : Quot rb
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ca : ∀ {b : β} {a₁ a₂ : α}, ra a₁ a₂ → f a₁ b ≍ f a₂ b
cb : ∀ {a : α} {b₁ b₂ : β}, rb b₁ b₂ → f a b₁ ≍ f a b₂
a₁ a₂ : α
pa : ra a₁ a₂
b : β
h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
          simp

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: ι : Type u_3
α : ι → Sort u_4
s : (i : ι) → Setoid (α i)
p : ((i : ι) → Quotient (s i)) → Prop
f : (i : ι) → Quotient (s i)
h : ∀ (a : (i : ι) → α i), p fun i ↦ ⟦a i⟧
⊢ p fun i ↦ ⟦(f i).out⟧

Tactic:
apply h

Goal state after:
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
n : ℕ
⊢ (Pi.map f)^[n] = Pi.map fun i ↦ (f i)^[n]

Tactic:
induction n <;> simp [*, map_comp_map]

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

Goal state before:
pp: case refine_1
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
x✝ : FaithfulSMul R A
r₁ r₂ : R
hr : (fun r ↦ r • 1) r₁ = (fun r ↦ r • 1) r₂
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
⊢ r₁ • a = r₂ • a

Tactic:
simp only at hr
    rw [← one_mul a, ← smul_mul_assoc, ← smul_mul_assoc, hr]

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
motive : α → Prop
ha : b ≤ a → motive a
hb : a ≤ b → motive b
⊢ motive (max a b)

Tactic:
rw [max_def]; split_ifs with h
  exacts [hb h, ha (le_of_not_ge h)]

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

Goal state before:
pp: case pos
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : p y
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y

Tactic:
have hx : p x := hp h hy
    simpa [hx, hy] using hf h

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

Goal state before:
pp: case zero
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
⊢ r (f a) (f (a + 1))

Tactic:
apply h

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ Disjoint {a} s ↔ ¬a ∈ s

Tactic:
simp [Set.disjoint_iff, subset_def]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: ι : Type u_1
π : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → SemilatticeSup (π i)
f : (i : ι) → π i
i : ι
a b : π i
j : ι
⊢ update f i (a ⊔ b) j = (update f i a ⊔ update f i b) j

Tactic:
by obtain rfl | hji := eq_or_ne j i <;> simp [update_of_ne, *]

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 (x ⊔ y)

Tactic:
apply h

Goal state after:
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α : Type u₀
⊢ mapEquiv f (Equiv.refl α) = Equiv.refl (f α)

Tactic:
ext; simp [mapEquiv]

Goal state after:
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 : a ≤ b
⊢ ⊥ ≤ c ↔ a ≤ max b c

pp: case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
h : ¬a ≤ b
⊢ a ≤ c ↔ a ≤ max b c

Tactic:
· exact iff_of_true bot_le (le_sup_of_le_left h)

Goal state after:
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
h : ¬a ≤ b
⊢ a ≤ c ↔ a ≤ max b c
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
t s s' u : Set α
⊢ u ⊆ t.ite s s' ↔ u ∩ t ⊆ s ∧ u \ t ⊆ s'

Tactic:
simp only [subset_def, ← forall_and]
  refine forall_congr' fun x => ?_
  by_cases hx : x ∈ t <;> simp [*, Set.ite]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : { y // y ≠ x }
⊢ (↑((optionSubtype x).symm e)).symm ↑b = some (e.symm b)

Tactic:
simp only [optionSubtype, coe_fn_symm_mk, Subtype.coe_mk,
             Subtype.coe_eta, dite_eq_ite, ite_eq_right_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : { y // y ≠ x }
⊢ ↑b = x → none = some (e.symm b)
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
rw [← sdiff_sdiff_eq_self hxz, h, sdiff_sdiff_eq_self hyz]

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c

Tactic:
by rw [himp_eq, isCompl_compl.le_sup_right_iff_inf_left_le]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
hy : y = x
⊢ {x}.piecewise f g y = update g x (f x) y

pp: case neg
α : Type u_1
β : Type u_2
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
hy : ¬y = x
⊢ {x}.piecewise f g y = update g x (f x) y

Tactic:
· subst y
    simp

Goal state after:
case neg
α : Type u_1
β : Type u_2
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
hy : ¬y = x
⊢ {x}.piecewise f g y = update g x (f x) y
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : s ⊆ t
x : β
⊢ x ∈ f ⁻¹' s → x ∈ f ⁻¹' t

Tactic:
apply h

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ {x} = {x'}

Tactic:
apply h

Goal state after:
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ f '' {x} = f '' {x'}
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
⊢ s.pi t₁ ⊆ s.pi t₂ ↔ (∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i) ∨ s.pi t₁ = ∅

Tactic:
by
  refine
    ⟨fun h => or_iff_not_imp_right.2 ?_, fun h => h.elim pi_mono fun h' => h'.symm ▸ empty_subset _⟩
  rw [← Ne, ← nonempty_iff_ne_empty]
  intro hne i hi
  simpa only [eval_image_pi hi hne, eval_image_pi hi (hne.mono h)] using
    image_mono (f := fun f : ∀ i, α i => f i) h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : Disjoint s t
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ Disjoint (f '' s) (f '' t)

Tactic:
disjoint_iff_inter_eq_empty

Goal state after:
α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : s ∩ t = ∅
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' s ∩ f '' t = ∅
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: case mk.mk
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : MulOne M
inst✝ : MulOne N
toOneHom✝¹ : OneHom M N
map_mul'✝¹ : ∀ (x y : M), toOneHom✝¹.toFun (x * y) = toOneHom✝¹.toFun x * toOneHom✝¹.toFun y
toOneHom✝ : OneHom M N
map_mul'✝ : ∀ (x y : M), toOneHom✝.toFun (x * y) = toOneHom✝.toFun x * toOneHom✝.toFun y
h :
  (fun f ↦ f.toFun) { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ } =
    (fun f ↦ f.toFun) { toOneHom := toOneHom✝, map_mul' := map_mul'✝ }
⊢ ⇑toOneHom✝¹ = ⇑toOneHom✝

Tactic:
exact h

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

Goal state before:
pp: m : ℤ
motive : (n : ℤ) → m ≤ n → Sort u_1
base : motive m ⋯
succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯
⊢ Int.inductionOn' (motive := fun x ↦ (hmn : m ≤ x) → motive x hmn) m m (fun x ↦ base)
      (fun k hle ih x ↦ succ k hle (ih hle)) (fun x x_1 x_2 x_3 ↦ ⋯.elim) ⋯ =
    base

Tactic:
inductionOn'_self

Goal state after:
m : ℤ
motive : (n : ℤ) → m ≤ n → Sort u_1
base : motive m ⋯
succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯
⊢ base = base
Module: Mathlib.Data.Int.Init

Goal state before:
pp: m : ℤ
motive : (n : ℤ) → m ≤ n → Sort u_1
base : motive m ⋯
succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯
⊢ Int.leInduction base succ m ⋯ = base

Tactic:
by
  rw [Int.leInduction, inductionOn'_self]

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

Goal state before:
pp: m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
⊢ Int.inductionOn' (motive := fun x ↦ (hnm : x ≤ m) → motive x hnm) m m (fun x ↦ base) (fun x x_1 x_2 x_3 ↦ ⋯.elim)
      (fun k hle ih x ↦ pred k hle (ih hle)) ⋯ =
    base

Tactic:
inductionOn'_self

Goal state after:
m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
⊢ base = base
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
n : ℕ
⊢ (a * b)⁻¹ ^ (n + 1) = a⁻¹ ^ (n + 1) * b⁻¹ ^ (n + 1)

Tactic:
mul_inv,

Goal state after:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
n : ℕ
⊢ (a⁻¹ * b⁻¹) ^ (n + 1) = a⁻¹ ^ (n + 1) * b⁻¹ ^ (n + 1)
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
rw [mul_assoc, ← mul_assoc b⁻¹, inv_mul_cancel, one_mul]

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

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

Tactic:
by
  rw [mul_assoc, ← mul_assoc b⁻¹, inv_mul_cancel, one_mul]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : αˣ
b : α
⊢ ↑a * ↑a⁻¹ * b = b

Tactic:
mul_inv,

Goal state after:
α : Type u
inst✝ : Monoid α
a : αˣ
b : α
⊢ 1 * b = b
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ ↑(u₁ / u₂) = ↑u₁ /ₚ u₂

Tactic:
divp,

Goal state after:
α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ ↑(u₁ / u₂) = ↑u₁ * ↑u₂⁻¹
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
u : αˣ
⊢ a /ₚ u = a * (↑u)⁻¹

Tactic:
divp,

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✝ : Monoid α
a : α
b : αˣ
⊢ a * (↑b * ↑b⁻¹) = a

Tactic:
mul_inv,

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

Goal state before:
pp: α : Type u
inst✝ : CommMonoid α
x y : α
u : αˣ
⊢ x /ₚ u * y = x * y /ₚ u

Tactic:
divp,

Goal state after:
α : Type u
inst✝ : CommMonoid α
x y : α
u : αˣ
⊢ x * ↑u⁻¹ * y = x * y /ₚ u
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : CommMonoid α
x y : α
u : αˣ
⊢ x * ↑u⁻¹ * y = x * y /ₚ u

Tactic:
divp,

Goal state after:
α : Type u
inst✝ : CommMonoid α
x y : α
u : αˣ
⊢ x * ↑u⁻¹ * y = x * y * ↑u⁻¹
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
h : IsUnit a
⊢ a * b = a * 1 ↔ b = 1

Tactic:
h.mul_right_inj

Goal state after:
M : Type u_1
inst✝ : Monoid M
a b : M
h : IsUnit a
⊢ b = 1 ↔ b = 1
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : IsMulTorsionFree M
inst✝ : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ a.1 = b.1

Tactic:
apply pow_left_injective hn

Goal state after:
case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : IsMulTorsionFree M
inst✝ : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ (fun a ↦ a ^ n) a.1 = (fun a ↦ a ^ n) b.1
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : IsMulTorsionFree M
inst✝ : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ a.2 = b.2

Tactic:
apply pow_left_injective hn

Goal state after:
case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : IsMulTorsionFree M
inst✝ : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ (fun a ↦ a ^ n) a.2 = (fun a ↦ a ^ n) b.2
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
⊢ swap x z = swap z x

Tactic:
swap_comm

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
x y z : α
hxy : x ≠ y
hxz : x ≠ z
⊢ swap z x = swap z x
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
⊢ f (if p then 0 else 1) = if p then 0 else 1

Tactic:
by
  split_ifs with h <;> simp

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

Goal state before:
pp: M₀✝ : Type u_1
G₀ : Type u_2
a b c : M₀✝
inst✝² : MulZeroOneClass M₀✝
M₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
inst✝ : IsLeftCancelMulZero M₀
a✝ b✝ : M₀
h : a✝ * b✝ = 1
⊢ b✝ * a✝ = 1

Tactic:
cases subsingleton_or_nontrivial M₀

Goal state after:
case inl
M₀✝ : Type u_1
G₀ : Type u_2
a b c : M₀✝
inst✝² : MulZeroOneClass M₀✝
M₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
inst✝ : IsLeftCancelMulZero M₀
a✝ b✝ : M₀
h : a✝ * b✝ = 1
h✝ : Subsingleton M₀
⊢ b✝ * a✝ = 1

case inr
M₀✝ : Type u_1
G₀ : Type u_2
a b c : M₀✝
inst✝² : MulZeroOneClass M₀✝
M₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
inst✝ : IsLeftCancelMulZero M₀
a✝ b✝ : M₀
h : a✝ * b✝ = 1
h✝ : Nontrivial M₀
⊢ b✝ * a✝ = 1
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
⊢ f (if p then 1 else 0) = if p then 1 else 0

Tactic:
by
  split_ifs with h <;> simp

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

Goal state before:
pp: M₀✝ : Type u_1
G₀ : Type u_2
a b c : M₀✝
inst✝² : MulZeroOneClass M₀✝
M₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
inst✝ : IsRightCancelMulZero M₀
a✝ b✝ : M₀
h : a✝ * b✝ = 1
⊢ b✝ * a✝ = 1

Tactic:
cases subsingleton_or_nontrivial M₀

Goal state after:
case inl
M₀✝ : Type u_1
G₀ : Type u_2
a b c : M₀✝
inst✝² : MulZeroOneClass M₀✝
M₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
inst✝ : IsRightCancelMulZero M₀
a✝ b✝ : M₀
h : a✝ * b✝ = 1
h✝ : Subsingleton M₀
⊢ b✝ * a✝ = 1

case inr
M₀✝ : Type u_1
G₀ : Type u_2
a b c : M₀✝
inst✝² : MulZeroOneClass M₀✝
M₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
inst✝ : IsRightCancelMulZero M₀
a✝ b✝ : M₀
h : a✝ * b✝ = 1
h✝ : Nontrivial M₀
⊢ b✝ * a✝ = 1
Module: Mathlib.Algebra.GroupWithZero.Basic

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

Tactic:
rw [div_eq_mul_inv, inv_zero, mul_zero]

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

Goal state before:
pp: case pos
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
hlm : l < m
⊢ lt l hlm = Int.strongRec lt ge l

Tactic:
rw [strongRec_of_lt hlm]

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

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

Tactic:
apply h

Goal state after:
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : NonUnitalNonAssocSemiring β
toMulHom✝¹ : α →ₙ* β
map_zero'✝¹ : toMulHom✝¹.toFun 0 = 0
map_add'✝¹ : ∀ (x y : α), toMulHom✝¹.toFun (x + y) = toMulHom✝¹.toFun x + toMulHom✝¹.toFun y
toMulHom✝ : α →ₙ* β
map_zero'✝ : toMulHom✝.toFun 0 = 0
map_add'✝ : ∀ (x y : α), toMulHom✝.toFun (x + y) = toMulHom✝.toFun x + toMulHom✝.toFun y
h :
  (fun f ↦ f.toFun) { toMulHom := toMulHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f ↦ f.toFun) { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ ⇑toMulHom✝¹ = ⇑toMulHom✝

Tactic:
exact h

Goal state after:
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
toMonoidHom✝¹ : α →* β
map_zero'✝¹ : (↑toMonoidHom✝¹).toFun 0 = 0
map_add'✝¹ : ∀ (x y : α), (↑toMonoidHom✝¹).toFun (x + y) = (↑toMonoidHom✝¹).toFun x + (↑toMonoidHom✝¹).toFun y
toMonoidHom✝ : α →* β
map_zero'✝ : (↑toMonoidHom✝).toFun 0 = 0
map_add'✝ : ∀ (x y : α), (↑toMonoidHom✝).toFun (x + y) = (↑toMonoidHom✝).toFun x + (↑toMonoidHom✝).toFun y
h :
  (fun f ↦ (↑f.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f ↦ (↑f.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ ⇑toMonoidHom✝¹ = ⇑toMonoidHom✝

Tactic:
exact h

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit a⁻¹ʳ
⊢ IsUnit a

Tactic:
cases subsingleton_or_nontrivial M₀

Goal state after:
case inl
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit a⁻¹ʳ
h✝ : Subsingleton M₀
⊢ IsUnit a

case inr
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit a⁻¹ʳ
h✝ : Nontrivial M₀
⊢ IsUnit a
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
h : b = a⁻¹ * c
⊢ a * b = c

Tactic:
← eq_inv_mul_iff_mul_eq₀

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
h : b = a⁻¹ * c
⊢ b = a⁻¹ * c

G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
h : b = a⁻¹ * c
⊢ a ≠ 0
Module: Mathlib.Algebra.Ring.Units

Goal state before:
pp: α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ a - b /ₚ u = (a * ↑u - b) /ₚ u

Tactic:
simp only [divp, sub_mul, Units.mul_inv_cancel_right]

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * (↑u₂ * ↑u₂⁻¹) * ↑u₁⁻¹ + ↑u₂⁻¹ * (↑u₁⁻¹ * ↑u₁) * b

Tactic:
mul_inv,

Goal state after:
α : Type u
inst✝ : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * 1 * ↑u₁⁻¹ + ↑u₂⁻¹ * (↑u₁⁻¹ * ↑u₁) * b
Module: Mathlib.Algebra.Ring.Units

Goal state before:
pp: R : Type x
inst✝ : Semiring R
a : Rˣ
b : R
⊢ ↑a + b = ↑a * (1 + ↑a⁻¹ * b)

Tactic:
rw [mul_add, mul_one, ← mul_assoc, Units.mul_inv, one_mul]

Goal state after:
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 - b) * (a + b)

Tactic:
by
  rw [mul_add, sub_mul, sub_mul, h.eq, sub_add_sub_cancel]

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

Goal state before:
pp: N : Type u_2
r : N → N → Prop
inst✝ : Group N
⊢ Covariant N N (fun x1 x2 ↦ x1 * x2) r ↔ Contravariant N N (fun x1 x2 ↦ x1 * x2) r

Tactic:
refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩
  · rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c]
    exact h a⁻¹ bc
  · rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c] at bc
    exact h a⁻¹ bc

Goal state after:
Module: Mathlib.Order.MinMax

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b : α
hf : MonotoneOn f s
ha : a ∈ s
hb : b ∈ s
⊢ f (max a b) = max (f a) (f b)

Tactic:
by
  rcases le_total a b with h | h <;>
    simp only [max_eq_right, max_eq_left, hf ha hb, hf hb ha, h]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a - b ≤ c ↔ a - c ≤ b

Tactic:
rw [tsub_le_iff_left, tsub_le_iff_right]

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

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c : α
hc : AddLECancellable c
h : b + c - c < b
⊢ False

Tactic:
simp [hc] at h

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ 1 ≤ a * b⁻¹ ↔ b ≤ a

Tactic:
le_mul_inv_iff₀ hb,

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ 1 * b ≤ a ↔ b ≤ a
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : x = y
⊢ x = y

Tactic:
exact h

Goal state after: