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

Goal state before:
pp: b : Bool
n : Nat
⊢ (b.toNat + 2 * n) / 2 = n

Tactic:
add_mul_div_left,

Goal state after:
b : Bool
n : Nat
⊢ b.toNat / 2 + n = n

case H
b : Bool
n : Nat
⊢ 0 < 2
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
one : motive 1
bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (Nat.bit b n)
⊢ binaryRecFromOne zero one bit 1 = one

Tactic:
rw [binaryRecFromOne, binaryRec'_one, dif_pos rfl]

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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
⊢ r a c

Tactic:
by
  rcases trichotomous_of r b c with (h₃ | rfl | h₃)
  · exact _root_.trans h₁ h₃
  · exact h₁
  · exact absurd h₃ h₂

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

Goal state before:
pp: ι : Sort u_3
α : ι → Type u_1
β : ι → Type u_2
f f' : (i : ι) → α i
g g' : (i : ι) → β i
⊢ Function.prod f g = Function.prod f' g' ↔ f = f' ∧ g = g'

Tactic:
simp [funext_iff, Prod.ext_iff, forall_and]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c ∨ ReflTransGen r c b✝
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

Tactic:
rcases IH with (IH | IH)
    · rcases cases_head IH with (rfl | ⟨e, be, ec⟩)
      · exact Or.inr (single bd)
      · cases U bd be
        exact Or.inl ec
    · exact Or.inr (IH.tail bd)

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

Goal state before:
pp: α : Type u
f g : α → α
h : Commute f g
n : ℕ
⊢ (f ∘ g)^[n] = f^[n] ∘ g^[n]

Tactic:
by
  induction n with
  | zero => rfl
  | succ n ihn =>
    funext x
    simp only [ihn, (h.iterate_right n).eq, iterate_succ, comp_apply]

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

Goal state before:
pp: α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f.trans g = Equiv.refl α ↔ f = g.symm

Tactic:
by
  rw [← Equiv.coe_inj, coe_trans, coe_refl, ← eq_symm_comp, comp_id, Equiv.coe_inj]

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

Goal state before:
pp: M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst✝¹ : Mul R
inst✝ : IsRightCancelMul R
r₁ r₂ : R
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂

Tactic:
simpa using h r₁

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

Goal state before:
pp: M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst✝¹ : Mul R
inst✝ : IsLeftCancelMul R
r₁ r₂ : Rᵐᵒᵖ
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂

Tactic:
simpa using h r₁.unop

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

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → MulOneClass (f i)
a✝ : (i : I) → f i
x✝ : I
⊢ (1 * a✝) x✝ = a✝ x✝

Tactic:
exact one_mul _

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

Goal state before:
pp: case inl
n m : ℕ
h : n ≤ m
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

pp: case inr
n m : ℕ
h : m < n
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

Tactic:
· simp [h]

Goal state after:
case inr
n m : ℕ
h : m < n
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case inl
n m : ℕ
h : m ≤ n
⊢ n ∣ m - n ↔ n ∣ m ∨ m ≤ n

pp: case inr
n m : ℕ
h : n < m
⊢ n ∣ m - n ↔ n ∣ m ∨ m ≤ n

Tactic:
· simp [h]

Goal state after:
case inr
n m : ℕ
h : n < m
⊢ n ∣ m - n ↔ n ∣ m ∨ m ≤ n
Module: Mathlib.Order.PropInstances

Goal state before:
pp: α : Type u_2
inst✝ : Subsingleton α
r : α → α → Prop
x✝ : Std.Irrefl r
⊢ ∀ (a b : α), r a b = ⊥ a b

Tactic:
simp [not_rel_of_subsingleton]

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

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i

Tactic:
· exact h_mon h₁

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b : α
hab : a ⊔ b = b
hba : b ⊔ a = a
⊢ a = b

Tactic:
by rwa [← hba, sup_comm]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : DistribLattice α
x y z : α
h₁ : x ⊓ z ≤ y ⊓ z
h₂ : x ⊔ z ≤ y ⊔ z
⊢ y ⊓ z ⊔ x = (y ⊔ x) ⊓ (x ⊔ z)

Tactic:
rw [sup_inf_right, sup_comm x]

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

Goal state before:
pp: α : Type u
s : Set α
⊢ (s = ∅ ∨ ∃ x, s = {x}) → s.Subsingleton

Tactic:
rintro (_ | ⟨_, rfl⟩)

Goal state after:
case inl
α : Type u
s : Set α
h✝ : s = ∅
⊢ s.Subsingleton

case inr
α : Type u
w✝ : α
⊢ {w✝}.Subsingleton
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
rw [le_himp_iff, inf_idem]

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
hinf : a ⊓ c ≤ b
hsup : b ≤ a ⊔ c
⊢ a \ b ⊔ b \ c = a \ c

Tactic:
by
  refine (sdiff_triangle ..).antisymm' <| sup_le ?_ <| by simpa [sup_comm]
  rw [← sdiff_inf_self_left (b := c)]
  exact sdiff_le_sdiff_left hinf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h : ¬(e (some x)).isSome = true
hn : e none = none
⊢ False

Tactic:
rw [Option.not_isSome_iff_eq_none, ← hn] at h

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h : e (some x) = e none
hn : e none = none
⊢ False
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Top α
inst✝¹ : HImp α
inst✝ : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ a ≤ ⊤

Tactic:
rw [← le, map_top]

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Top α
inst✝¹ : HImp α
inst✝ : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ f a ≤ ⊤
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Nonempty
⊢ t \ s ⊂ t

Tactic:
simpa [inter_eq_self_of_subset_right hst]

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

Goal state before:
pp: α : Type u_1
t s s' : Set α
⊢ s' ∩ t ∪ s ∩ tᶜ = s' ∩ t ∪ s \ t

Tactic:
sdiff_eq

Goal state after:
α : Type u_1
t s s' : Set α
⊢ s' ∩ t ∪ s ∩ tᶜ = s' ∩ t ∪ s ∩ tᶜ
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
rw [sdiff_sup, sdiff_sdiff_right, sdiff_sdiff_right, sup_inf_left, sup_comm, sup_inf_sdiff,
          sup_inf_left, sup_comm (z \ y), sup_inf_sdiff]

Goal state after:
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.20
α : ι → Type u_9
β : ι → Type u_10
p : (i : ι) × (α i ⊕ β i)
⊢ Sum.elim (Sigma.map id fun x ↦ inl) (Sigma.map id fun x ↦ inr)
      ((fun p ↦ Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd) p) =
    p

Tactic:
by
    rcases p with ⟨i, a | b⟩ <;> rfl

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

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

Tactic:
rw [inf_comm x, inf_comm, inf_sdiff_assoc]

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
⊢ RightInverse (Sum.elim succ fun x ↦ 0) fun n ↦ Nat.casesOn n (inr PUnit.unit) inl

Tactic:
rintro (_ | _)

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
val✝ : ℕ
⊢ (fun n ↦ Nat.casesOn n (inr PUnit.unit) inl) (Sum.elim succ (fun x ↦ 0) (inl val✝)) = inl val✝

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
val✝ : PUnit
⊢ (fun n ↦ Nat.casesOn n (inr PUnit.unit) inl) (Sum.elim succ (fun x ↦ 0) (inr val✝)) = inr val✝
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
⊢ RightInverse (Sum.elim succ fun x ↦ 0) fun n ↦ Nat.casesOn n (inr PUnit.unit) inl

Tactic:
rintro (_ | _) <;> rfl

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
a c d : α
h : (fun x ↦ swap a x) c = (fun x ↦ swap a x) d
⊢ c = d

Tactic:
simp only at h

Goal state after:
α : Sort u_1
inst✝ : DecidableEq α
a c d : α
h : swap a c = swap a d
⊢ c = d
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.13
⊢ RightInverse (Sum.elim (Prod.mk false) (Prod.mk true)) fun p ↦ if p.fst = true then inr p.snd else inl p.snd

Tactic:
rintro (_ | _)

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.13
val✝ : α
⊢ (fun p ↦ if p.fst = true then inr p.snd else inl p.snd) (Sum.elim (Prod.mk false) (Prod.mk true) (inl val✝)) =
    inl val✝

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.13
val✝ : α
⊢ (fun p ↦ if p.fst = true then inr p.snd else inl p.snd) (Sum.elim (Prod.mk false) (Prod.mk true) (inr val✝)) =
    inr val✝
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.13
⊢ RightInverse (Sum.elim (Prod.mk false) (Prod.mk true)) fun p ↦ if p.fst = true then inr p.snd else inl p.snd

Tactic:
rintro (_ | _) <;> rfl

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Unique ι
⊢ range f = {f default}

Tactic:
aesop (add simp [Unique.eq_default])

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

Goal state before:
pp: case refine_1.left
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i
⊢ f ∈ {i | i ∈ s ∧ p i}.pi t₁

Tactic:
rintro i ⟨his, hpi⟩

Goal state after:
case refine_1.left
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i
i : ι
his : i ∈ s
hpi : p i
⊢ f i ∈ t₁ i
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case refine_1.right
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i
⊢ f ∈ {i | i ∈ s ∧ ¬p i}.pi t₂

Tactic:
rintro i ⟨his, hpi⟩

Goal state after:
case refine_1.right
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i
i : ι
his : i ∈ s
hpi : ¬p i
⊢ f i ∈ t₂ i
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:
refine
    ⟨fun h => or_iff_not_imp_right.2 ?_, fun h => h.elim pi_mono fun h' => h'.symm ▸ empty_subset _⟩

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi t₁ ⊆ s.pi t₂
⊢ ¬s.pi t₁ = ∅ → ∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
⊢ update f i ⁻¹' s.pi t = t i

Tactic:
ext x
  refine ⟨fun h => ?_, fun hx j hj => ?_⟩
  · convert! h i hi
    simp
  · obtain rfl | h := eq_or_ne j i
    · simpa
    · rw [update_of_ne h]
      exact hf j hj h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
h : BijOn f ∅ t
⊢ t = ∅

Tactic:
by simpa using h.surjOn

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

Goal state before:
pp: ι : 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✝¹ : One M
inst✝ : One N
f : OneHom M N
g : N → M
h₁ : LeftInverse g ⇑f
⊢ g (f 1) = 1

Tactic:
h₁

Goal state after:
ι : 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✝¹ : One M
inst✝ : One N
f : OneHom M N
g : N → M
h₁ : LeftInverse g ⇑f
⊢ 1 = 1
Module: Mathlib.Data.Int.Init

Goal state before:
pp: motive : ℤ → Sort u_1
b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ zero ≍
    match b - b with
    | ofNat n => inductionOn'.pos b zero succ n
    | -[n+1] => inductionOn'.neg b zero pred n

Tactic:
rw [b.sub_self, ← cast_eq_iff_heq]

Goal state after:
motive : ℤ → Sort u_1
b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ cast ?m.44 zero =
    match 0 with
    | ofNat n => inductionOn'.pos b zero succ n
    | -[n+1] => inductionOn'.neg b zero pred n

motive : ℤ → Sort u_1
b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ motive b = (fun x ↦ motive x) (b + 0)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
⊢ f '' s = g ⁻¹' s

Tactic:
by
  ext x
  constructor
  · rintro ⟨y, hy, rfl⟩
    rw [mem_preimage, hgf hy]; exact hy
  · intro hx
    refine ⟨g x, hx, Set.InjOn.rightInvOn_of_leftInvOn ginj hgf (Set.mapsTo_preimage g s) ?_ hx⟩
    intro y hy
    simpa [hgf hy] using hy

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
a b : M
n : ℕ
⊢ (a * b) ^ (n + 1) = a ^ (n + 1) * b ^ (n + 1)

Tactic:
by rw [pow_succ', pow_succ', pow_succ', mul_pow, mul_mul_mul_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Type u_3
M : Type u_4
inst✝ : DivisionMonoid α
a b c d : α
⊢ 1⁻¹ = 1

Tactic:
simpa only [one_div, inv_inv] using (inv_div (1 : α) 1).symm

Goal state after:
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✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M × N
⊢ (1 * x✝).1 = x✝.1

Tactic:
exact one_mul _

Goal state after:
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✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M × N
⊢ (1 * x✝).2 = x✝.2

Tactic:
exact one_mul _

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
hb : b ≠ 0
⊢ a * b = 0 ↔ a = 0

Tactic:
by simp [hb]

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
hb : b ≠ 0
⊢ a * b ≠ 0 ↔ a ≠ 0

Tactic:
by simp [hb]

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

Goal state before:
pp: case pos
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a✝ b x a : G₀
h : a = 0
⊢ a⁻¹⁻¹ = a

pp: case neg
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a✝ b x a : G₀
h : ¬a = 0
⊢ a⁻¹⁻¹ = a

Tactic:
· simp [h]

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

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁶ : MonoidWithZero M₀
inst✝⁵ : MonoidWithZero M₀'
inst✝⁴ : Zero A
inst✝³ : MulActionWithZero M₀ A
inst✝² : Zero A'
inst✝¹ : SMul M₀ A'
p : Prop
inst✝ : Decidable p
f : M₀' →*₀ M₀
r s : M₀'
m : A
⊢ (r * s) • m = r • s • m

Tactic:
change f (r * s) • m = f r • f s • m

Goal state after:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁶ : MonoidWithZero M₀
inst✝⁵ : MonoidWithZero M₀'
inst✝⁴ : Zero A
inst✝³ : MulActionWithZero M₀ A
inst✝² : Zero A'
inst✝¹ : SMul M₀ A'
p : Prop
inst✝ : Decidable p
f : M₀' →*₀ M₀
r s : M₀'
m : A
⊢ f (r * s) • m = f r • f s • m
Module: Mathlib.Algebra.CharZero.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m n : ℕ
h : ↑m = ↑n
⊢ m = n

Tactic:
by
    induction m generalizing n with
    | zero => rw [H n]; rw [← h, Nat.cast_zero]
    | succ m ih =>
      cases n
      · apply H; rw [h, Nat.cast_zero]
      · simp only [Nat.cast_succ, add_right_cancel_iff] at h; rwa [ih]

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

Goal state before:
pp: n : ℕ
⊢ n ≤ n.sqrt * n.sqrt + n.sqrt + n.sqrt

Tactic:
← succ_mul

Goal state after:
n : ℕ
⊢ n ≤ n.sqrt.succ * n.sqrt + n.sqrt
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m n : ℕ
⊢ Even (m ^ n) ↔ Even m ∧ n ≠ 0

Tactic:
induction n with grind

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

Goal state before:
pp: m : ℤ
n : ℕ
⊢ Even (m ^ n) ↔ Even m ∧ n ≠ 0

Tactic:
induction n with grind

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

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : ∀ (x : R), r * x = 0 → x = 0
r₁ r₂ : R
eq : (fun x ↦ r * x) r₁ = (fun x ↦ r * x) r₂
⊢ r * (r₁ - r₂) = 0

Tactic:
by simp_rw [mul_sub, eq, sub_self]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NonAssocSemiring α
n : ℕ
inst✝ : n.AtLeastTwo
a : α
⊢ OfNat.ofNat n • a = OfNat.ofNat n * a

Tactic:
simp [nsmul_eq_mul]

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

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ d * (b * b⁻¹) * a = d * b * (d⁻¹ * c) ↔ d * a = b * c

Tactic:
hb.mul_inv_cancel,

Goal state after:
M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ d * 1 * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: n : ℕ
⊢ ∃ k, Xor (n = 2 * k) (n = 2 * k + 1)

Tactic:
obtain ⟨k, rfl⟩ | ⟨k, rfl⟩ := even_or_odd n <;>
  · use k
    grind

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

Goal state before:
pp: R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : -1 ≠ 1
⊢ (-1) ^ n = -1 ↔ Odd n

Tactic:
by simp [neg_one_pow_eq_ite, h.symm]

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

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

Tactic:
rintro rfl
    exact h.not_ge le_tsub_add

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b : α
⊢ 1 < a * b⁻¹ ↔ b < a

Tactic:
rw [← mul_lt_mul_iff_right b, one_mul, inv_mul_cancel_right]

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c d : α
⊢ a * b⁻¹ < d⁻¹ * c ↔ a * d < c * b

Tactic:
mul_inv_lt_inv_mul_iff,

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c d : α
⊢ d * a < c * b ↔ a * d < c * b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
a b c d : α
hab : a < b
hcd : c < d
⊢ a * d⁻¹ < c⁻¹ * b

Tactic:
mul_inv_lt_inv_mul_iff,

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
a b c d : α
hab : a < b
hcd : c < d
⊢ c * a < b * d
Module: Mathlib.Algebra.Order.Monoid.Defs

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
mul_le_mul_right : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b
toIsOrderedMonoid : IsOrderedMonoid α := { mul_le_mul_left := mul_le_mul_left }
le_of_mul_le_mul_left : ∀ (a b c : α), a * b ≤ a * c → b ≤ c
a b c : α
h : b * a ≤ c * a
⊢ b ≤ c

Tactic:
rw [mul_comm _ a, mul_comm _ a] at h; exact le_of_mul_le_mul_left a b c h

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

Goal state before:
pp: M₀ : Type u_2
inst✝⁵ : MonoidWithZero M₀
inst✝⁴ : PartialOrder M₀
a b c d : M₀
inst✝³ : PosMulMono M₀
inst✝² : PosMulStrictMono M₀
inst✝¹ : MulPosStrictMono M₀
inst✝ : DecidableLE M₀
h1 : a < c
h2 : b < d
h3 : 0 ≤ a
h4 : 0 ≤ b
b0 : 0 = b
⊢ a * b < c * d

Tactic:
by
    rw [← b0, mul_zero]; exact mul_pos (h3.trans_lt h1) (h4.trans_lt h2)

Goal state after:
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: one : Type u_1
α : Type u_2
inst✝ : Unique one
f : one ↪ α
⊢ (fun a ↦ { toFun := fun x ↦ a, inj' := ⋯ }) ((fun f ↦ f default) f) = f

Tactic:
by ext; simp [Unique.uniq]

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddLeftMono R
inst✝ : NoZeroDivisors R
r : R
⊢ r ^ 2 = 0 ↔ r = 0

Tactic:
exact sq_eq_zero_iff

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a < c⁻¹ * b ↔ a * c < b

Tactic:
rw [lt_inv_mul_iff₀ hc, mul_comm]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b * c⁻¹ < a ↔ b < c * a

Tactic:
mul_inv_lt_iff₀ hc,

Goal state after:
G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b < a * c ↔ b < c * a
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
f : α ↪o β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
a₁ a₂ : α
h : Disjoint (f a₁) (f a₂)
x : α
⊢ x ≤ a₁ → x ≤ a₂ → x ≤ ⊥

Tactic:
h₁

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
f : α ↪o β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
a₁ a₂ : α
h : Disjoint (f a₁) (f a₂)
x : α
h₁ : x ≤ a₁
⊢ x ≤ a₂ → x ≤ ⊥
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a b : ℤ
H : b ≠ 0
⊢ a % b < |b|

Tactic:
← emod_abs

Goal state after:
a b : ℤ
H : b ≠ 0
⊢ a % |b| < |b|
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝¹ : MulZeroClass R
a : R
inst✝ : Nontrivial R
la : IsLeftRegular a
⊢ a ≠ 0

Tactic:
by
  rintro rfl
  rcases exists_pair_ne R with ⟨x, y, xy⟩
  refine xy (la ?_)
  simp

Goal state after: