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

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b : G
h : Commute a b
n : ℕ
⊢ (a * b) ^ Int.negSucc n = a ^ Int.negSucc n * b ^ Int.negSucc n

Tactic:
simp [h.mul_pow, (h.pow_pow _ _).eq, mul_inv_rev]

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

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

Tactic:
mul_inv_cancel_left,

Goal state after:
G : Type u_1
inst✝ : Group G
a✝ b✝ a b : G
⊢ a * a⁻¹ = 1
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case refine_1
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map f)
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
⊢ Pi.map f (update default i x) = Pi.map f (update default i y)

Tactic:
Pi.map_update,

Goal state after:
case refine_1
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map f)
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
⊢ update (Pi.map f default) i (f i x) = Pi.map f (update default i y)
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case refine_1
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map f)
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
⊢ update (Pi.map f default) i (f i x) = Pi.map f (update default i y)

Tactic:
Pi.map_update,

Goal state after:
case refine_1
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map f)
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
⊢ update (Pi.map f default) i (f i x) = update (Pi.map f default) i (f i y)
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.refl
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {motive : (a : α) → ReflTransGen r a b → Prop},
    motive b ⋯ → (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯) → motive a a✝
motive : (a : α) → ReflTransGen r a c → Prop
refl : motive c ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), motive c_1 h → motive a ⋯
⊢ motive b ⋯

Tactic:
exact head hbc _ refl

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.inl.inr
α : 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
e : α
be : r b✝ e
ec : ReflTransGen r e c
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

Tactic:
cases U bd be
        exact Or.inl ec

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ min a (min b c) = min b (min a c)

Tactic:
rw [← min_assoc, min_comm a, min_assoc]

Goal state after:
Module: Mathlib.Order.Basic

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

Tactic:
ext x y; exact H x y

Goal state after:
Module: Mathlib.Order.Basic

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

Tactic:
ext x y; exact H x y

Goal state after:
Module: Mathlib.Order.Basic

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

Tactic:
ext x y; exact H x y

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁸ : LinearOrder β
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Max α
inst✝⁴ : Min α
inst✝³ : Ord α
inst✝² : DecidableEq α
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x✝¹ x✝ : α
⊢ Ord.compare x✝¹ x✝ = compareOfLessAndEq x✝¹ x✝

Tactic:
by
    simp_rw [← compare, LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq, ← lt,
      hf.eq_iff]

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

Goal state before:
pp: k : ℕ
⊢ 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)

Tactic:
by
  obtain rfl | hk : k = 0 ∨ k > 0 := k.eq_zero_or_pos
  · decide
  · have hk0 : 0 < 2 * k ^ 2 := Nat.mul_pos Nat.two_pos (Nat.pow_pos hk)
    calc 2 * k ^ 2
      _ < 2 * k ^ 2 + 2 * k ^ 2 := Nat.lt_add_of_pos_left hk0
      _ = (2 * k) ^ 2 := by rw [Nat.mul_pow, ← Nat.add_mul]
      _ ≤ (2 ^ k) ^ 2 := Nat.pow_le_pow_left (Nat.mul_le_pow (by decide : 2 ≠ 1) _) 2
      _ = 2 ^ (2 * k) := (Nat.pow_mul' _ _ _).symm

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a a' : α
ha : a' ≤ a
⊢ ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)

Tactic:
b

Goal state after:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a a' : α
ha : a' ≤ a
b : β
⊢ Acc (fun x1 x2 ↦ x1 < x2) (a', b)
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case step
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℕ → β
a : ℕ
h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))
b c : ℕ
hab : a ≤ b
m✝ : ℕ
b_lt_k : b.succ.le m✝
r_b_k : r (f b) (f m✝)
⊢ r (f b) (f m✝.succ)

Tactic:
exact _root_.trans r_b_k (h _ (hab.trans_lt b_lt_k).le)

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

Goal state before:
pp: ⊢ Monotone fun n ↦ n ^ n

Tactic:
by
  refine monotone_nat_of_le_succ fun n ↦ ?_
  rw [Nat.pow_succ]
  exact (Nat.pow_le_pow_left n.le_succ _).trans (Nat.le_mul_of_pos_right _ n.succ_pos)

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
ha : Disjoint x.fst y.fst
hb : Disjoint x.snd y.snd
z : α × β
hza : z ≤ x
hzb : z ≤ y
⊢ z ≤ ⊥

Tactic:
exact ⟨ha hza.1 hzb.1, hb hza.2 hzb.2⟩

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 y ∧ Codisjoint x y ↔
    (Disjoint x.fst y.fst ∧ Codisjoint x.fst y.fst) ∧ Disjoint x.snd y.snd ∧ Codisjoint x.snd y.snd

Tactic:
Prod.disjoint_iff,

Goal state after:
α : 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 y ↔
    (Disjoint x.fst y.fst ∧ Codisjoint x.fst y.fst) ∧ Disjoint x.snd y.snd ∧ Codisjoint x.snd y.snd
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
p : Prop
inst✝ : Decidable p
t : p → Set α
x : α
⊢ (x ∈ if h : p then t h else ∅) ↔ ∃ h, x ∈ t h

Tactic:
simp only [mem_dite, mem_empty_iff_false, imp_false, not_not]

Goal state after:
α : Type u
p : Prop
inst✝ : Decidable p
t : p → Set α
x : α
⊢ (∀ (h : p), x ∈ t h) ∧ p ↔ ∃ h, x ∈ t h
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: case mp
α : Type u
s : Set α
h : Subsingleton ↑s
a : α
ha : a ∈ s
⊢ ∀ ⦃y : α⦄, y ∈ s → a = y

Tactic:
b

Goal state after:
case mp
α : Type u
s : Set α
h : Subsingleton ↑s
a : α
ha : a ∈ s
b : α
⊢ b ∈ s → a = b
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
h : a ⊔ c ≤ b ⊔ c
⊢ a \ c ≤ b \ c

Tactic:
rw [← sup_sdiff_right_self, ← @sup_sdiff_right_self _ _ b]

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
h : a ⊔ c ≤ b ⊔ c
⊢ (a ⊔ c) \ c ≤ (b ⊔ c) \ c
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ insert a s \ t ⊆ insert a (s \ t)

Tactic:
by
  rintro b ⟨rfl | hbs, hbt⟩ <;> simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : β
⊢ (fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e)) ((fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩)) b) = b

Tactic:
by
          by_cases h : b = x <;> simp [h]

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

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

Tactic:
by
  rw [inf_assoc, sup_inf_right, sup_inf_sdiff, inf_sup_right, inf_sdiff_left]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by simp [← symmDiff_assoc]

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

Goal state before:
pp: case succ
α : Type u_1
f : α → α
n : ℕ
ih : preimage f^[n] = (preimage f)^[n]
⊢ preimage (f^[n] ∘ f) = preimage f ∘ (preimage f)^[n]

Tactic:
preimage_comp_eq,

Goal state after:
case succ
α : Type u_1
f : α → α
n : ℕ
ih : preimage f^[n] = (preimage f)^[n]
⊢ preimage f ∘ preimage f^[n] = preimage f ∘ (preimage f)^[n]
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
x : α
y : β
⊢ (x, y) ∈ s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ ↔ (x, y) ∈ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)

Tactic:
simp [and_assoc, and_left_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∃ s, s ⊆ range f ∧ p s) ↔ ∃ s, p (f '' s)

Tactic:
rw [← exists_range_iff, range_image]; rfl

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

Goal state before:
pp: α : Type u_1
⊢ diagonal α = univ ↔ Subsingleton α

Tactic:
simp only [subsingleton_iff, eq_univ_iff_forall, Prod.forall, mem_diagonal_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ (f ⁻¹' s).Nonempty ↔ s.Nonempty

Tactic:
rw [← image_nonempty, hf.image_preimage]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
t₁ t₂ : (i : ι) → Set (α i)
⊢ Disjoint (univ.pi t₁) (univ.pi t₂) ↔ ∃ i, Disjoint (t₁ i) (t₂ i)

Tactic:
by
  simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, univ_pi_eq_empty_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
⊢ g '' f '' s = s

Tactic:
by rw [← image_comp, h.comp_eq_id, image_id]

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

Goal state before:
pp: case mpr
α : Type u_1
s t u : Set α
⊢ s ∩ t ⊆ s ∩ u → val ⁻¹' t ⊆ val ⁻¹' u

Tactic:
· intro h x a
    exact (h ⟨x.2, a⟩).2

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

Goal state before:
pp: G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
a : G
⊢ f (a ^ 0) = f a ^ 0

Tactic:
rw [pow_zero, pow_zero, map_one]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop (Pow.pow x✝ ↑x✝¹.succ) = unop (Pow.pow x✝ ↑x✝¹ * x✝)

Tactic:
Pow.pow

Goal state after:
α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop (op (unop x✝ ^ ↑x✝¹.succ)) = unop (op (unop x✝ ^ ↑x✝¹) * x✝)
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop (op (unop x✝ ^ ↑x✝¹.succ)) = unop (op (unop x✝ ^ ↑x✝¹) * x✝)

Tactic:
unop_op,

Goal state after:
α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop x✝ ^ ↑x✝¹.succ = unop (op (unop x✝ ^ ↑x✝¹) * x✝)
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop x✝ * unop x✝ ^ x✝¹ = unop x✝ * unop (op (unop x✝ ^ ↑x✝¹))

Tactic:
unop_op,

Goal state after:
α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop x✝ * unop x✝ ^ x✝¹ = unop x✝ * unop x✝ ^ ↑x✝¹
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✝ : DivInvMonoid 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 (x * y⁻¹)

Tactic:
by rw [div, mul, inv, div_eq_mul_inv]

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

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

Tactic:
rw [← div_eq_one, H, div_eq_one]

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

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

Tactic:
rw [mul_left_comm, div_mul_cancel, mul_comm]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
a : M
inst✝ : Subsingleton Mˣ
⊢ IsUnit a → a = 1

Tactic:
rintro ⟨u, rfl⟩; simp [u.eq_one]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a / b)

Tactic:
rw [div_eq_mul_inv]; exact ha.mul hb.inv

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✝¹ : Semigroup M
inst✝ : Semigroup N
x✝² x✝¹ x✝ : M × N
⊢ x✝² * x✝¹ * x✝ = x✝² * (x✝¹ * x✝)

Tactic:
ext <;> exact mul_assoc ..

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✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝ : G × H
⊢ x✝ ^ 0 = 1

Tactic:
by ext <;> exact DivInvMonoid.zpow_zero' _

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
n : ℕ
inst✝ : Nontrivial M₀
⊢ 0 ^ n = 0 → n ≠ 0

Tactic:
rintro h rfl; simp at h

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
a b : R
h : a + b = 1
⊢ a • x + b • y = b • y - b • x + (a • x + b • x)

Tactic:
sub_add_add_cancel,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
a b : R
h : a + b = 1
⊢ a • x + b • y = b • y + a • x
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: case pred
i✝ : ℕ
a✝ : IsSquare (-↑i✝).sign ↔ 0 ≤ -↑i✝
⊢ IsSquare (-↑i✝ - 1).sign ↔ 0 ≤ -↑i✝ - 1

Tactic:
sign_eq_neg_one_of_neg (by lia),

Goal state after:
case pred
i✝ : ℕ
a✝ : IsSquare (-↑i✝).sign ↔ 0 ≤ -↑i✝
⊢ IsSquare (-1) ↔ 0 ≤ -↑i✝ - 1
Module: Mathlib.Logic.Nontrivial.Basic

Goal state before:
pp: I : Type u_3
f : I → Type u_4
i' : I
inst : ∀ (i : I), Nonempty (f i)
inst✝ : Nontrivial (f i')
⊢ Nontrivial ((i : I) → f i)

Tactic:
let := Classical.decEq (∀ i : I, f i)

Goal state after:
I : Type u_3
f : I → Type u_4
i' : I
inst : ∀ (i : I), Nonempty (f i)
inst✝ : Nontrivial (f i')
this : DecidableEq ((i : I) → f i) := Classical.decEq ((i : I) → f i)
⊢ Nontrivial ((i : I) → f i)
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
⊢ (↑u)⁻¹ʳ = ↑u⁻¹

Tactic:
inverse,

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
⊢ (if h : IsUnit ↑u then ↑h.unit⁻¹ else 0) = ↑u⁻¹
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

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

pp: case neg
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
a✝ : Nontrivial M₀
h : ¬IsUnit a
⊢ a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ

Tactic:
· rw [Ring.inverse_inverse h]

Goal state after:
case neg
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
a✝ : Nontrivial M₀
h : ¬IsUnit a
⊢ a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
p : (g : G₀) → g ≠ 0 → Prop
⊢ (∃ g hg, p g hg) ↔ ∃ g hg, p ↑(mk0 g hg) ⋯

Tactic:
by simp_rw [val_mk0]

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

Goal state before:
pp: case negSucc
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑(a✝ + 1) = 0
⊢ -[a✝+1] = 0

Tactic:
Nat.cast_eq_zero

Goal state after:
case negSucc
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : a✝ + 1 = 0
⊢ -[a✝+1] = 0
Module: Mathlib.Algebra.Field.Defs

Goal state before:
pp: A : Type u_2
inst✝ : DivisionRing A
m : ℚ
⊢ m • 1 = ↑m

Tactic:
by
  rw [Rat.smul_def, mul_one]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 ↦ x1 < x2
a : M
⊢ ∀ {n₁ n₂ : N}, (fun x1 x2 ↦ x1 ≤ x2) n₁ n₂ → (fun x1 x2 ↦ x1 ≤ x2) (μ a n₁) (μ a n₂)

Tactic:
b

Goal state after:
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 ↦ x1 < x2
a : M
b : N
⊢ ∀ {n₂ : N}, (fun x1 x2 ↦ x1 ≤ x2) b n₂ → (fun x1 x2 ↦ x1 ≤ x2) (μ a b) (μ a n₂)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ a ^ 2 + a * b = 0

Tactic:
by rw [sq, ← mul_add, hab, mul_zero]

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

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
a b c d : α
inst✝ : MulRightMono α
⊢ d * (a * b⁻¹) * b ≤ d * (d⁻¹ * c) * b ↔ d * a ≤ c * b

Tactic:
mul_inv_cancel_left,

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
a b c d : α
inst✝ : MulRightMono α
⊢ d * (a * b⁻¹) * b ≤ c * b ↔ d * a ≤ c * b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b c d : α
inst✝ : MulRightStrictMono α
⊢ d * (a * b⁻¹) * b < d * (d⁻¹ * c) * b ↔ d * a < c * b

Tactic:
mul_inv_cancel_left,

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b c d : α
inst✝ : MulRightStrictMono α
⊢ d * (a * b⁻¹) * b < c * b ↔ d * a < c * b
Module: Mathlib.Algebra.Order.Monoid.Defs

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : Preorder α
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c
a b : α
h : a ≤ b
c : α
⊢ a + c ≤ c + b

Tactic:
add_comm c

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : Preorder α
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c
a b : α
h : a ≤ b
c : α
⊢ a + c ≤ b + c
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : b + b * c ≤ a + c
⊢ 1 + (b + b * c) ≤ 1 + (c + a)

Tactic:
add_comm c

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : b + b * c ≤ a + c
⊢ 1 + (b + b * c) ≤ 1 + (a + c)
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case 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 : r x y
⊢ x = y

Tactic:
have := hf h

Goal state after:
case 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 : r x y
this : s (f x) (f y)
⊢ x = y
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case inr.inr
α : 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 : r y x
⊢ x = y

Tactic:
have := hf h

Goal state after:
case inr.inr
α : 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 : r y x
this : s (f y) (f x)
⊢ x = y
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
⊢ Injective toEmbedding

Tactic:
rintro ⟨f, -⟩ ⟨g, -⟩

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α ↪ β
map_rel_iff'✝¹ : ∀ {a b : α}, s (f a) (f b) ↔ r a b
g : α ↪ β
map_rel_iff'✝ : ∀ {a b : α}, s (g a) (g b) ↔ r a b
⊢ { toEmbedding := f, map_rel_iff' := map_rel_iff'✝¹ }.toEmbedding =
      { toEmbedding := g, map_rel_iff' := map_rel_iff'✝ }.toEmbedding →
    { toEmbedding := f, map_rel_iff' := map_rel_iff'✝¹ } = { toEmbedding := g, map_rel_iff' := map_rel_iff'✝ }
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 : α ⊕ γ},
    Sum.LiftRel s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } a) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } b) ↔
      Sum.LiftRel r t a b

Tactic:
by rintro (a | b) (c | d) <;> simp [f.map_rel_iff, g.map_rel_iff]

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 : α ⊕ γ},
    Sum.Lex s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } a) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } b) ↔ Sum.Lex r t a b

Tactic:
by rintro (a | b) (c | d) <;> simp [f.map_rel_iff, g.map_rel_iff]

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

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
a : α
⊢ ∀ {b : α},
    { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
b

Goal state after:
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
a b : α
⊢ { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } a ≤
      { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } b ↔
    a ≤ b
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: case refine_1
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
a : X
⊢ ∀ (a_1 : X), f a ≤ f a_1 ↔ a_1 ≤ a

Tactic:
b

Goal state after:
case refine_1
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
a b : X
⊢ f a ≤ f b ↔ b ≤ a
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a) * (c * (c⁻¹ * (b ⊓ a)⁻¹)) = (b ⊔ a) / (b ⊓ a)

Tactic:
mul_inv_cancel_left,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a) * (b ⊓ a)⁻¹ = (b ⊔ a) / (b ⊓ a)
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝² : Semigroup α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedMul α
a b c : α
hbc : b ≤ b * c
⊢ (fun x1 x2 ↦ x1 * x2) a b ≤ (fun x1 x2 ↦ x1 * x2) a (b * c)

Tactic:
le_iff_exists_mul

Goal state after:
α : Type u
inst✝² : Semigroup α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedMul α
a b c : α
hbc : b ≤ b * c
⊢ ∃ c_1, (fun x1 x2 ↦ x1 * x2) a (b * c) = (fun x1 x2 ↦ x1 * x2) a b * c_1