mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.AdaptationNote

Goal state before:
pp: ⊢ True

Tactic:
trivial

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

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

Tactic:
rw [rel_congr_left h₁, rel_congr_right h₂]

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

Goal state before:
pp: R : Type u_2
inst✝ : Mul R
⊢ (∀ (a : R), IsLeftRegular a) ∧ IsRightCancelMul R ↔ ∀ (r : R), IsRegular r

Tactic:
isRightCancelMul_iff,

Goal state after:
R : Type u_2
inst✝ : Mul R
⊢ ((∀ (a : R), IsLeftRegular a) ∧ ∀ (a : R), IsRightRegular a) ↔ ∀ (r : R), IsRegular r
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m n : ℕ
hn : n ≠ 0
a : M
ha : 1 * a = a
⊢ npowRec (m + n) a = npowRec m a * npowRec n a

Tactic:
by
  obtain _ | n := n; · exact (hn rfl).elim
  induction n with
  | zero => simp only [npowRec, ha]
  | succ n ih => rw [← Nat.add_assoc, npowRec, ih n.succ_ne_zero]; simp only [npowRec, mul_assoc]

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1)

Tactic:
by rw [pow_succ, ← mul_assoc, ← pow_add, ← pow_succ, Nat.add_assoc]

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

Goal state before:
pp: case refine_2
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
h : f = g
⊢ g x = g y

Tactic:
Subsingleton.elim x y

Goal state after:
case refine_2
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
h : f = g
⊢ g y = g y
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s ↦ ⟨U, cast ⋯ s⟩
s t : Set T
h : g s = g t
this : cast hU (g s).snd = cast hU (g t).snd
⊢ s = t

Tactic:
simp only [g, cast_cast, cast_eq] at this
      assumption

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

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (∀ (x : α), p x (update f a b x)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)

Tactic:
by
  rw [← and_forall_ne a, update_self]
  simp +contextual

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

Goal state before:
pp: α : Sort u
f : α → α
h : Involutive f
P : Prop
inst✝ : Decidable P
x : α
⊢ f (if P then x else f x) = if ¬P then x else f x

Tactic:
by rw [apply_ite f, h, ite_not]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
A B : Set (α → β)
hAB : A ⊆ B
hA : A.SeparatesPoints
x y : α
hne : x ≠ y
f : α → β
hfA : f ∈ A
hne' : f x ≠ f y
⊢ ∃ f, f ∈ B ∧ f x ≠ f y

Tactic:
exact ⟨f, hAB hfA, hne'⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ (flip p ∘r flip r) c a → flip (r ∘r p) c a

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

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case inr
α : Type u_1
r : α → α → Prop
a b : α
hab : r a b
⊢ SymmGen (Function.swap r) a b

Tactic:
exact of_rel_symm hab

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b✝ c : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a

Tactic:
induction hdb with
      | refl => exact ⟨e, refl, ReflGen.single hde⟩
      | @tail f b _ hfb ih =>
        rcases ih with ⟨a, hea, hfa⟩
        cases hfa with
        | refl => exact ⟨b, hea.tail hfb, ReflGen.refl⟩
        | single hfa =>
          rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
          exact ⟨c, hea.trans hac, hbc⟩

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h : Surjective (Sum.map f g)
c : γ
⊢ ∃ a, f a = c

Tactic:
obtain ⟨a | b, h⟩ := h (inl c)

Goal state after:
case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
a : α
h : Sum.map f g (inl a) = inl c
⊢ ∃ a, f a = c

case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
b : β
h : Sum.map f g (inr b) = inl c
⊢ ∃ a, f a = c
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ NoMinOrder α ↔ ∀ (x : α), ¬IsMin x

Tactic:
by
  simp [noMinOrder_iff', IsMin, lt_iff_le_not_ge]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h : x < y
h₁ : ¬y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

Tactic:
· exact Or.inl ⟨LE.le.lt_of_not_ge h.1.1 h₁, h.1.2⟩

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case eq
α : Type u_1
inst✝ : LT α
a b : α
⊢ eq.swap.Compares a b ↔ eq.Compares b a

Tactic:
exact eq_comm

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → BoundedOrder (α' i)
f g : (i : ι) → α' i
⊢ IsCompl f g ↔ ∀ (i : ι), IsCompl (f i) (g i)

Tactic:
simp_rw [_root_.isCompl_iff, disjoint_iff, codisjoint_iff, forall_and]

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

Goal state before:
pp: f : ℕ → ℕ
hf : StrictMono f
m n : ℕ
⊢ f n + m ≤ f (n + m)

Tactic:
induction m with

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

Goal state before:
pp: n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : f 0 = f 1
flat : ∀ (j : ℕ), f j = f (j + 1)
m : ℕ
x✝ : 0 ≤ m
⊢ f m = f 0

Tactic:
induction m with

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

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

Tactic:
by
  rw [inter_comm, singleton_inter_eq_empty]

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

Goal state before:
pp: case some.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝¹ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝¹
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

Tactic:
rw [removeNoneAux_some _ ⟨_, h1⟩]

Goal state after:
case some.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝¹ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝¹
val✝ : β
h2 : e (some x) = some val✝
⊢ e.symm (some (e.removeNoneAux x)) = some x
Module: Mathlib.Data.Sigma.Basic

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

Tactic:
obtain rfl : x = y := h₂ i (sigma_mk_injective h)

Goal state after:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x : β₁ i
h : Sigma.map f₁ f₂ ⟨i, x⟩ = Sigma.map f₁ f₂ ⟨i, x⟩
⊢ ⟨i, x⟩ = ⟨i, x⟩
Module: Mathlib.Order.SymmDiff

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

Tactic:
exact le_sup_of_le_left le_sdiff_sup

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by rw [symmDiff_comm, symmDiff_eq_left]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : α × β
⊢ x✝ ∈ univ ×ˢ univ ↔ x✝ ∈ univ

Tactic:
exact iff_of_eq (true_and _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Prod.swap '' s ×ˢ t = t ×ˢ s

Tactic:
rw [image_swap_eq_preimage_swap, preimage_swap_prod]

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

Goal state before:
pp: case inl
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i = i
⊢ i ∈ ⇑σ '' s → i ∈ s

Tactic:
rintro ⟨j, hj, h⟩

Goal state after:
case inl
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i = i
j : α
hj : j ∈ s
h : σ j = i
⊢ i ∈ s
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ range (s.piecewise f g) → y ∈ f '' s ∪ g '' sᶜ

Tactic:
rintro ⟨x, rfl⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
⊢ s.piecewise f g x ∈ f '' s ∪ g '' sᶜ
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s : Set α
⊢ val ⁻¹' s = univ

Tactic:
rw [← preimage_range, range_coe]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
⊢ ∃ a, f a = y

Tactic:
have := mem_singleton y

Goal state after:
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
this : y ∈ {y}
⊢ ∃ a, f a = y
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : b ∈ s.pi fun i ↦ f i '' t i
i : ι
hi : i ∈ s
⊢ ∃ a, f i a = b i ∧ (i ∈ s → a ∈ t i)

Tactic:
then

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : b ∈ s.pi fun i ↦ f i '' t i
i : ι
hi : i ∈ s
⊢ ∃ a, f i a = b i ∧ (i ∈ s → a ∈ t i)
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✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
a b : G
⊢ f a * f b⁻¹ = f a * (f b)⁻¹

Tactic:
map_inv

Goal state after:
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
a b : G
⊢ f a * (f b)⁻¹ = f a * (f b)⁻¹
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
g : ι → G
n : ℤ
⊢ ⇑f ∘ (g ^ n) = ⇑f ∘ g ^ n

Tactic:
ext; simp [map_zpow' f hf]

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

Goal state before:
pp: G : Type u_3
inst✝ : DivInvMonoid G
x y : G
⊢ x * (1 / y) = x / y

Tactic:
rw [div_eq_mul_inv, one_mul, 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 : G
h : b⁻¹ * a = c
⊢ a = b * c

Tactic:
simp [h.symm, mul_inv_cancel_left]

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₁
h : x * y = 1
⊢ f x⁻¹ = f y

Tactic:
by
      rw [inv, inv_eq_of_mul_eq_one_right (by rw [← mul, h, one])]

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

Goal state before:
pp: M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = f x
⊢ g 1 = 1

Tactic:
by ext; rw [h 1]; exact f.map_one

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

Goal state before:
pp: G₀ : Type u
M₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ a b : G₀
hb : b ≠ 0
⊢ a * b / b = a

Tactic:
rw [div_eq_mul_inv, mul_assoc, mul_inv_cancel₀ hb, mul_one]

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

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝² : MulZeroClass M₀
inst✝¹ : Mul M₀'
inst✝ : Zero M₀'
f : M₀ → M₀'
hf : Surjective f
zero : f 0 = 0
mul : ∀ (a b : M₀), f (a * b) = f a * f b
x : M₀
⊢ 0 * f x = 0

Tactic:
by simp only [← zero, ← mul, zero_mul]

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

Goal state before:
pp: α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p (f x) ↔ p x
n : ℕ
⊢ ∀ (x : α), p ((f ^ Int.negSucc n) x) ↔ p x

Tactic:
zpow_negSucc

Goal state after:
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p (f x) ↔ p x
n : ℕ
⊢ ∀ (x : α), p ((f ^ (n + 1))⁻¹ x) ↔ p x
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a * a⁻¹ * a = a

Tactic:
rw [mul_inv_cancel₀ h, one_mul]

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

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
h : ↑(m + 1) = ↑0
⊢ ↑(m + 1) = 0

Tactic:
rw [h, Nat.cast_zero]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddMonoidWithOne M
inst✝ : CharZero M
⊢ 1 ≠ 0

Tactic:
trivial

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

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(↑m + ↑n) = ↑↑m + ↑↑n

Tactic:
simp [← Int.natCast_add]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r s : R
y : M
⊢ (r - s) • y = r • y - s • y

Tactic:
by
  simp [add_smul, sub_eq_add_neg]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : NonAssocRing α
m : ℕ
⊢ ∀ (n : ℤ), ↑(↑m * n) = ↑↑m * ↑n

Tactic:
induction m with

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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : NonAssocRing α
m : ℕ
⊢ ∀ (n : ℤ), ↑(-↑m * n) = ↑(-↑m) * ↑n

Tactic:
induction m with

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

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

Tactic:
· simp [Ring.inverse_of_isUnit, ha, hb, ha.mul hb, ← Units.val_mul, ← mul_inv_rev]
    simp

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
n : ℕ
ha : a ≠ 0
⊢ a ^ Int.negSucc n ≠ 0

Tactic:
zpow_negSucc

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
n : ℕ
ha : a ≠ 0
⊢ (a ^ (n + 1))⁻¹ ≠ 0
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
⊢ Odd (a + (a + 1))

Tactic:
simp [← add_assoc]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.NatCast

Goal state before:
pp: case bc
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : LE α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 1

Tactic:
exact zero_le_one

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.NatCast

Goal state before:
pp: case bc
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : LE α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddRightMono α
⊢ 0 ≤ 1

Tactic:
exact zero_le_one

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.NatCast

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftMono α
⊢ 0 < 3

Tactic:
rw [← two_add_one_eq_three]
  exact lt_add_of_lt_of_nonneg zero_lt_two zero_le_one

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

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : ¬c = b
⊢ ¬c * a = b * a

Tactic:
obtain h | h := h

Goal state after:
case inl
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : b ≤ c
⊢ ¬c * a = b * a

case inr
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬c * a = b * a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : ¬c = b
⊢ ¬a * c = a * b

Tactic:
obtain h | h := h

Goal state after:
case inl
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h' : ¬c = b
h : b ≤ c
⊢ ¬a * c = a * b

case inr
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬a * c = a * b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightMono α
a₁ a₂ b₁ b₂ : α
⊢ a₁ * b₁ ≤ a₂ * b₂ → a₁ < a₂ ∨ b₁ ≤ b₂

Tactic:
by
  contrapose!
  exact fun h => mul_lt_mul_of_le_of_lt h.1 h.2

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ a₁ * b₁ < a₂ * b₂ ↔ a₁ < a₂ ∨ b₁ < b₂

Tactic:
by
  refine ⟨lt_or_lt_of_mul_lt_mul, fun h => ?_⟩
  rcases h with ha' | hb'
  · exact mul_lt_mul_of_lt_of_le ha' hb
  · exact mul_lt_mul_of_le_of_lt ha hb'

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

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
inst✝ : ZeroLEOneClass M₀
n : ℕ
⊢ 0 ≤ 1

Tactic:
exact zero_le_one

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 : s ↪r t
⊢ ∀ {a b : α}, t ((f.trans g.toEmbedding) a) ((f.trans g.toEmbedding) b) ↔ r a b

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

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

Goal state before:
pp: case inl.inl
α : 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 c : α
⊢ Sum.LiftRel s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl a))
      ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl c)) ↔
    Sum.LiftRel r t (Sum.inl a) (Sum.inl c)

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

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

Goal state before:
pp: case inl.inr
α : 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 : α
d : γ
⊢ Sum.LiftRel s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl a))
      ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr d)) ↔
    Sum.LiftRel r t (Sum.inl a) (Sum.inr d)

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

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

Goal state before:
pp: case inr.inl
α : 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
b : γ
c : α
⊢ Sum.LiftRel s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr b))
      ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl c)) ↔
    Sum.LiftRel r t (Sum.inr b) (Sum.inl c)

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

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

Goal state before:
pp: case inr.inr
α : 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
b d : γ
⊢ Sum.LiftRel s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr b))
      ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr d)) ↔
    Sum.LiftRel r t (Sum.inr b) (Sum.inr d)

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

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

Goal state before:
pp: case inl.inl
α : 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 c : α
⊢ Sum.Lex s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl a)) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl c)) ↔
    Sum.Lex r t (Sum.inl a) (Sum.inl c)

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

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

Goal state before:
pp: case inl.inr
α : 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 : α
d : γ
⊢ Sum.Lex s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl a)) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr d)) ↔
    Sum.Lex r t (Sum.inl a) (Sum.inr d)

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

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

Goal state before:
pp: case inr.inl
α : 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
b : γ
c : α
⊢ Sum.Lex s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr b)) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl c)) ↔
    Sum.Lex r t (Sum.inr b) (Sum.inl c)

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

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

Goal state before:
pp: case inr.inr
α : 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
b d : γ
⊢ Sum.Lex s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr b)) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr d)) ↔
    Sum.Lex r t (Sum.inr b) (Sum.inr d)

Tactic:
simp [f.map_rel_iff, g.map_rel_iff]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
⊢ ComplementedLattice β → ComplementedLattice α

Tactic:
by intro; exact f.symm.complementedLattice

Goal state after:
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hb : 1 ≤ b
⊢ |a|ₘ = b ↔ a = b ∨ a = b⁻¹

Tactic:
refine ⟨eq_or_eq_inv_of_mabs_eq, ?_⟩

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hb : 1 ≤ b
⊢ a = b ∨ a = b⁻¹ → |a|ₘ = b
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝⁶ : Group α
inst✝⁵ : LinearOrder α
β : Type u_2
F : Type u_3
inst✝⁴ : Group β
inst✝³ : LinearOrder β
inst✝² : FunLike F α β
inst✝¹ : OrderHomClass F α β
inst✝ : MonoidHomClass F α β
f : F
a : α
⊢ max (f a) (f a⁻¹) = max (f a) (f a)⁻¹

Tactic:
map_inv

Goal state after:
α : Type u_1
inst✝⁶ : Group α
inst✝⁵ : LinearOrder α
β : Type u_2
F : Type u_3
inst✝⁴ : Group β
inst✝³ : LinearOrder β
inst✝² : FunLike F α β
inst✝¹ : OrderHomClass F α β
inst✝ : MonoidHomClass F α β
f : F
a : α
⊢ max (f a) (f a)⁻¹ = max (f a) (f a)⁻¹
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case refine_2
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ ↑(n * (n.gcdA k % ↑k).toNat % k) = ↑(↑n * n.gcdA k % ↑k).toNat

Tactic:
Int.natCast_mod,

Goal state after:
case refine_2
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ ↑(n * (n.gcdA k % ↑k).toNat) % ↑k = ↑(↑n * n.gcdA k % ↑k).toNat
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsRightRegular a
h : b * a = a
⊢ b = 1

Tactic:
by rwa [← ha.eq_iff, one_mul]

Goal state after: