mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single.single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a✝ b✝ c✝ : α
inst✝ : IsTrans α r
a b c : α
h₂ : r b c
h₁ : r a b
⊢ ReflGen r a c

Tactic:
exact single (trans_of r h₁ h₂)

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h : ReflTransGen r a b
⊢ a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b

Tactic:
by
  induction h using Relation.ReflTransGen.head_induction_on <;> grind

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

Goal state before:
pp: case mk
α : Sort u
β : Sort v
γ : Sort w
e₂ : α ≃ β
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : RightInverse invFun✝ toFun✝
h₁ : { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun = e₂.toFun
h₂ : { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun = e₂.invFun
⊢ { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } = e₂

Tactic:
cases e₂

Goal state after:
case mk.mk
α : Sort u
β : Sort v
γ : Sort w
toFun✝¹ : α → β
invFun✝¹ : β → α
left_inv✝¹ : LeftInverse invFun✝¹ toFun✝¹
right_inv✝¹ : RightInverse invFun✝¹ toFun✝¹
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : RightInverse invFun✝ toFun✝
h₁ :
  { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun
h₂ :
  { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.invFun =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun
⊢ { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
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✝¹ : SMul α β
inst✝ : IsScalarTower M α β
g : N → M
⊢ Sort ?u.25

Tactic:
by
    haveI := comp α g; haveI := comp β g; exact IsScalarTower N α β

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ min a b ≤ b

Tactic:
by
  rw [min_def]
  split_ifs with h <;> simp [h]

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), NoMinOrder (π i)
a : (i : ι) → π i
⊢ ∃ b, b < a

Tactic:
obtain ⟨b, hb⟩ := exists_lt (a <| Classical.arbitrary _)

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), NoMinOrder (π i)
a : (i : ι) → π i
b : π (Classical.arbitrary ι)
hb : b < a (Classical.arbitrary ι)
⊢ ∃ b, b < a
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: case refl
α : Type u_1
hA : PartialOrder α
A B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ ≤ ⊤

Tactic:
exact @le_top _ _ A _

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ ⊤ ⊓ (x' ⊔ x ⊔ y') = ⊤

Tactic:
top_inf_eq,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ x' ⊔ x ⊔ y' = ⊤
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : Max α
inst✝³ : Min α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : DistribLattice β
f : α → β
hf_inj : 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
a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c

Tactic:
rw [← le, map_inf, map_sup, map_sup, map_sup, map_inf]

Goal state after:
α : Type u
β : Type v
inst✝⁴ : Max α
inst✝³ : Min α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : DistribLattice β
f : α → β
hf_inj : 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
a b c : α
⊢ (f a ⊔ f b) ⊓ (f a ⊔ f c) ≤ f a ⊔ f b ⊓ f c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ ⊤ ⊓ (a ⇨ b) = b

Tactic:
top_inf_eq,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ a ⇨ b = b
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
· refine le_compl_comm.1 ((compl_anti compl_sup_le_himp).trans ?_)
    rw [compl_sup_distrib, le_compl_iff_disjoint_right, disjoint_right_comm, ←
      le_compl_iff_disjoint_right]
    exact inf_himp_le

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
sdiff_self

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a : α
⊢ ⊥ = ⊥
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ ≤ ￢a ⊔ a

Tactic:
exact Codisjoint.top_le codisjoint_hnot_left

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ b \ a = b \ a

Tactic:
by
  rw [symmDiff_def, sup_sdiff, sdiff_idem, sdiff_sdiff_self, bot_sup_eq]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
f : α → β
s : Set α
⊢ f '' s = ∅ ↔ s = ∅

Tactic:
by
  simp only [eq_empty_iff_forall_notMem]
  exact ⟨fun H a ha => H _ ⟨_, ha, rfl⟩, fun H b ⟨_, ha, _⟩ => H _ ha⟩

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
⊢ range f ∩ s ⊆ range f ∩ s' → f ⁻¹' s ⊆ f ⁻¹' s'

Tactic:
intro r x hx
    simp_all only [subset_inter_iff, inter_subset_left, true_and, mem_preimage,
      mem_inter_iff, mem_range, true_and]
    aesop

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
⊢ f ⁻¹' s ⊆ f ⁻¹' s' → range f ∩ s ⊆ range f ∩ s'

Tactic:
intro r x hx
    simp_all only [subset_inter_iff, inter_subset_left, true_and, mem_preimage,
      mem_inter_iff, mem_range, true_and]
    aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x✝ : ∃ g, ∀ (x : ↑s), f ↑x = ↑(g x)
x : α
hx : x ∈ s
g : ↑s → ↑t
hg : ∀ (x : ↑s), f ↑x = ↑(g x)
⊢ f x ∈ t

Tactic:
rw [hg ⟨x, hx⟩]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x✝ : ∃ g, ∀ (x : ↑s), f ↑x = ↑(g x)
x : α
hx : x ∈ s
g : ↑s → ↑t
hg : ∀ (x : ↑s), f ↑x = ↑(g x)
⊢ ↑(g ⟨x, hx⟩) ∈ t
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case neg
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i ↦ if i ∈ s then f i else g i) j (f j) i

Tactic:
· by_cases h' : i ∈ s <;> simp [h, h']

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

Goal state before:
pp: X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
⊢ map_fst ⁻¹' pullbackDiagonal f = pullbackDiagonal snd

Tactic:
ext ⟨⟨p₁, p₂⟩, he⟩

Goal state after:
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ ⟨(p₁, p₂), he⟩ ∈ map_fst ⁻¹' pullbackDiagonal f ↔ ⟨(p₁, p₂), he⟩ ∈ pullbackDiagonal snd
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
s t : Set α
x : α × α
⊢ x ∈ (s ∩ t).offDiag ↔ x ∈ s.offDiag ∩ t.offDiag

Tactic:
simp only [mem_offDiag, mem_inter_iff]

Goal state after:
α : Type u_1
s t : Set α
x : α × α
⊢ (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 ↔
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set β
h : Codisjoint s t
⊢ Codisjoint (f ⁻¹' s) (f ⁻¹' t)

Tactic:
simp only [codisjoint_iff_le_sup, Set.sup_eq_union, top_le_iff, ← Set.preimage_union] at h ⊢
  rw [h]; rfl

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

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

Tactic:
intro hne i hi

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi t₁ ⊆ s.pi t₂
hne : (s.pi t₁).Nonempty
i : ι
hi : i ∈ s
⊢ t₁ i ⊆ t₂ i
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
h : ∀ (a : α), a ∈ s → p (f a)
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ p (f a)

Tactic:
exact h _ ha

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
⊢ (∃ a, a ∈ s ∧ p (f a)) → ∃ b, b ∈ t ∧ p b

Tactic:
rintro ⟨a, ha, h⟩; exact ⟨f a, hf.mapsTo ha, h⟩

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

Goal state before:
pp: case inl
G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
a : G
⊢ a ^ 0 = 1 ↔ a = 1 ∨ 0 = 0

Tactic:
simp [zpow_eq_one_iff_left, *]

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

Goal state before:
pp: case inr
G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
n : ℤ
a : G
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1 ∨ n = 0

Tactic:
simp [zpow_eq_one_iff_left, *]

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
ha : Injective fa
hf : InjOn f (range fa)
⊢ InjOn fb (range f)

Tactic:
rw [← image_univ] at *

Goal state after:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Injective fa
hf : InjOn f (fa '' univ)
⊢ InjOn fb (f '' univ)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
t₁ : Set β₁
t₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : SurjOn f₁ s₁ t₁
h₂ : SurjOn f₂ s₂ t₂
x : β₁ × β₂
hx : x ∈ t₁ ×ˢ t₂
a₁ : α₁
ha₁ : a₁ ∈ s₁
hx₁ : f₁ a₁ = x.1
⊢ x ∈ (fun x ↦ (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂

Tactic:
obtain ⟨a₂, ha₂, hx₂⟩ := h₂ hx.2

Goal state after:
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
t₁ : Set β₁
t₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : SurjOn f₁ s₁ t₁
h₂ : SurjOn f₂ s₂ t₂
x : β₁ × β₂
hx : x ∈ t₁ ×ˢ t₂
a₁ : α₁
ha₁ : a₁ ∈ s₁
hx₁ : f₁ a₁ = x.1
a₂ : α₂
ha₂ : a₂ ∈ s₂
hx₂ : f₂ a₂ = x.2
⊢ x ∈ (fun x ↦ (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
h : ∀ (a : α), e a ∈ t ↔ a ∈ s
b : β
hb : b ∈ t
⊢ e (e.symm b) ∈ t

Tactic:
by rwa [apply_symm_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
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:
by split_ifs <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
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:
by split_ifs <;> rfl

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
n : ℕ
hn : n ≠ 0
a : M
⊢ a * a ^ (n - 1) = a ^ n

Tactic:
by
  rw [← pow_succ', Nat.sub_add_cancel <| Nat.one_le_iff_ne_zero.2 hn]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
n : ℕ
⊢ (fun x ↦ x * a)^[n + 1] = fun x ↦ x * a ^ (n + 1)

Tactic:
simp [pow_succ', mul_right_iterate]

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

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

Tactic:
by rw [inv, mul, mul_inv_rev, mul, inv, inv]

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

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

Tactic:
rwa [← mul_assoc, Units.inv_mul, one_mul] at this

Goal state after:
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; rfl

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

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

Tactic:
rw [div_eq_mul_inv, h.mul_inv_cancel_right]

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

Goal state before:
pp: 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
x✝ : Mˣ × Nˣ
u₁ : Mˣ
u₂ : Nˣ
⊢ ((Units.map (MonoidHom.fst M N)).prod (Units.map (MonoidHom.snd M N)))
      ((fun u ↦ { val := (↑u.1, ↑u.2), inv := (↑u.1⁻¹, ↑u.2⁻¹), val_inv := ⋯, inv_val := ⋯ }) (u₁, u₂)) =
    (u₁, u₂)

Tactic:
simp only [Units.map, MonoidHom.coe_fst, Units.inv_eq_val_inv,
      MonoidHom.coe_snd, MonoidHom.prod_apply, Prod.mk.injEq]
    exact ⟨rfl, rfl⟩

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
⊢ 1 ≠ 0

Tactic:
intro h
  rcases exists_pair_ne M₀ with ⟨x, y, hx⟩
  apply hx
  calc
    x = 1 * x := by rw [one_mul]
    _ = 0 := by rw [h, zero_mul]
    _ = 1 * y := by rw [h, zero_mul]
    _ = y := by rw [one_mul]

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

Goal state before:
pp: M₀ : Type u_1
a b : M₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : IsLeftCancelMulZero M₀
ha : a ≠ 0
⊢ a * b = a ↔ b = 1

Tactic:
rw [Iff.comm, ← mul_right_inj' ha, mul_one]

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₀
    · exact Subsingleton.elim _ _
    exact (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero
      (left_ne_zero_of_mul_eq_one h)).mul_eq_one_symm h

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

Goal state before:
pp: M : Type u_1
A : Type u_7
inst✝¹ : AddGroup A
inst✝ : DistribSMul M A
r : M
x y : A
⊢ r • (x - y) = r • x - r • y

Tactic:
sub_eq_add_neg,

Goal state after:
M : Type u_1
A : Type u_7
inst✝¹ : AddGroup A
inst✝ : DistribSMul M A
r : M
x y : A
⊢ r • (x + -y) = r • x - r • y
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
A : Type u_7
inst✝¹ : AddGroup A
inst✝ : DistribSMul M A
r : M
x y : A
⊢ r • (x + -y) = r • x - r • y

Tactic:
sub_eq_add_neg,

Goal state after:
M : Type u_1
A : Type u_7
inst✝¹ : AddGroup A
inst✝ : DistribSMul M A
r : M
x y : A
⊢ r • (x + -y) = r • x + -(r • y)
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 • x * g • x⁻¹ = 1

Tactic:
← smul_mul',

Goal state after:
case neg
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x : β
hx : ¬x = 0
⊢ g • (x * x⁻¹) = 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
x : M
⊢ 0 • f x = 0

Tactic:
rw [← f.map_zero, ← smul, zero_smul]

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

Goal state before:
pp: case refine_3
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 : ℤ
hkm : k ≤ m
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
x✝ : ∀ (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
⊢ 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 ⋯) l ⋯ =
    Int.strongRec lt ge l

Tactic:
ih'

Goal state after:
case refine_3
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 : ℤ
hkm : k ≤ m
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
x✝ : ∀ (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
⊢ (fun k_1 x ↦ Int.strongRec lt ge k_1) l ⋯ = Int.strongRec lt ge l

case refine_3
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 : ℤ
hkm : k ≤ m
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
x✝ : ∀ (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
⊢ ∀ (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
Module: Mathlib.Algebra.Group.Nat.Hom

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b : M
n : ℕ
⊢ ((multiplesHom M).toFun (a + b)) n = ((multiplesHom M).toFun a + (multiplesHom M).toFun b) n

Tactic:
by simp [nsmul_add]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ -(b / a) = -b / a

Tactic:
neg_div

Goal state after:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ -(b / a) = -(b / a)
Module: Mathlib.Algebra.Group.Commute.Units

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
hx : ¬IsUnit a
n : ℕ
⊢ IsUnit (a ^ n) ↔ n = 0

Tactic:
rcases n with (_ | n) <;>
  simp [hx]

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
by
  obtain (⟨ha, hb⟩ | ⟨ha, hb⟩ | ⟨ha, hb⟩) :
      (IsUnit a ∧ ¬ IsUnit b) ∨ (¬ IsUnit a ∧ IsUnit b) ∨ (IsUnit a ∧ IsUnit b) := by grind
  · have : ¬ IsUnit (a * b) := by simpa [ha.mul_left_iff]
    simp [Ring.inverse_non_unit, hb, this]
  · have : ¬ IsUnit (a * b) := by simpa [hb.mul_right_iff]
    simp [Ring.inverse_non_unit, ha, this]
  · simp [Ring.inverse_of_isUnit, ha, hb, ha.mul hb, ← Units.val_mul, ← mul_inv_rev]
    simp

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

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

Tactic:
sub_eq_add_neg,

Goal state after:
α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ a /ₚ u + -(b /ₚ u) = (a - b) /ₚ u
Module: Mathlib.Algebra.Ring.Units

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

Tactic:
sub_eq_add_neg,

Goal state after:
α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ a /ₚ u + -(b /ₚ u) = (a + -b) /ₚ u
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝ : CommRing R
a b : R
⊢ (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2

Tactic:
sub_eq_add_neg,

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
a b : R
⊢ (a - b) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b

Tactic:
sub_eq_add_neg,

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

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
h : IsUnit 2
a : α
⊢ Odd (a - 1 + 1)

Tactic:
exact (Even.of_isUnit_two h _).add_one

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

Goal state before:
pp: α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : MulLeftMono α
a b : α
h : MulLECancellable (a * b)
c d : α
hcd : b * c ≤ b * d
⊢ a * b * c ≤ a * b * d

Tactic:
rw [mul_assoc, mul_assoc]

Goal state after:
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : MulLeftMono α
a b : α
h : MulLECancellable (a * b)
c d : α
hcd : b * c ≤ b * d
⊢ a * (b * c) ≤ a * (b * d)
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₀
inst✝ : ZeroLEOneClass M₀
ha₀ : 0 < a
ha₁ : a ≠ 1
⊢ Injective fun x ↦ a ^ x

Tactic:
by
  obtain ha₁ | ha₁ := ha₁.lt_or_gt
  · exact (pow_right_strictAnti₀ ha₀ ha₁).injective
  · exact (pow_right_strictMono₀ ha₁).injective

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
⊢ ∀ {a b : α × γ},
    Prod.Lex s u ({ toFun := Prod.map ⇑f ⇑g, inj' := ⋯ } a) ({ toFun := Prod.map ⇑f ⇑g, inj' := ⋯ } b) ↔
      Prod.Lex r t a b

Tactic:
by simp [Prod.lex_def, f.map_rel_iff, g.map_rel_iff, f.inj]

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

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ (x - a) * (x - b) < 0 ↔ a < x ∧ x < b

Tactic:
mul_neg_iff,

Goal state after:
R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ 0 < x - a ∧ x - b < 0 ∨ x - a < 0 ∧ 0 < x - b ↔ a < x ∧ x < b