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

Goal state before:
pp: α : Sort u_1
inst✝ : Subsingleton α
p : α → Prop
x✝¹ x✝ : Subtype p
x : α
property✝¹ : p x
y : α
property✝ : p y
⊢ ⟨x, property✝¹⟩ = ⟨y, property✝⟩

Tactic:
cases Subsingleton.elim x y; rfl

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case inl
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : p x
⊢ x = y

Tactic:
rcases em (p y) with (hy | hy)

Goal state after:
case inl.inl
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : p x
hy : p y
⊢ x = y

case inl.inr
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : p x
hy : ¬p y
⊢ x = y
Module: Mathlib.Logic.Basic

Goal state before:
pp: case inr
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : ¬p x
⊢ x = y

Tactic:
rcases em (p y) with (hy | hy)

Goal state after:
case inr.inl
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : ¬p x
hy : p y
⊢ x = y

case inr.inr
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : ¬p x
hy : ¬p y
⊢ x = y
Module: Mathlib.Logic.Function.Basic

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

Tactic:
replace h := @h (Function.update default i x) (Function.update default i y) ?_

Goal state after:
case refine_2
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
h : update default i x = update default i y
⊢ x = y

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)
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : M
n : ℕ
⊢ (fun x ↦ a • x)^[n + 1] = fun x ↦ a ^ (n + 1) • x

Tactic:
by ext; simp [smul_iterate, pow_succ, smul_smul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Option α → β
i : Option α
⊢ i.elim (f none) (f ∘ some) = f i

Tactic:
cases i <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
f : γ → α
x : α
i : Option γ
⊢ (i.elim (h x) fun j ↦ h (f j)) = h (i.elim x f)

Tactic:
cases i <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β → γ
f : γ → α
x : α
g : γ → β
y : β
i : Option γ
⊢ (i.elim (h x y) fun j ↦ h (f j) (g j)) = h (i.elim x f) (i.elim y g)

Tactic:
cases i <;> rfl

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq

Tactic:
by_cases h : a < b

Goal state after:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
h : a < b
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq

case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
h : ¬a < b
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ ¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
simp_rw [not_monotone_not_antitone_iff_exists_le_le, ← and_assoc]
  refine exists₃_congr (fun a b c ↦ and_congr_left <|
    fun h ↦ (Ne.le_iff_lt ?_).and <| Ne.le_iff_lt ?_) <;>
  (rintro rfl; simp at h)

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

Goal state before:
pp: case negSucc.succ
α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ (casesOn -[n + 1+1] f fun n ↦ g (n + 1)) < casesOn (-[n + 1+1] + 1) f fun n ↦ g (n + 1)

Tactic:
· exact hg (Nat.lt_succ_self _)

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ Disjoint a b ∧ Codisjoint ↑a ↑b ↔ Disjoint a b ∧ Codisjoint a b

Tactic:
codisjoint_coe

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

Goal state before:
pp: case mp
α : Type u_1
a : α
n : ℕ
hn : n > 0
H : (List.replicate n a).Nodup
⊢ List.replicate n a = [a]

Tactic:
simp only [List.nodup_replicate] at H

Goal state after:
case mp
α : Type u_1
a : α
n : ℕ
hn : n > 0
H : n ≤ 1
⊢ List.replicate n a = [a]
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y ≤ x ∧ ¬Disjoint y x ↔ ¬Disjoint y x

Tactic:
and_iff_right sdiff_le

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ ¬Disjoint y x ↔ ¬Disjoint y x
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
i : α₁ ⊕ α₂
⊢ ((e.sumCongr f).trans (g.sumCongr h)) i = ((e.trans g).sumCongr (f.trans h)) i

Tactic:
cases i <;> rfl

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

Goal state before:
pp: α : Type u_9
β : Type u_10
i : α ⊕ β
⊢ ((Equiv.refl α).sumCongr (Equiv.refl β)) i = (Equiv.refl (α ⊕ β)) i

Tactic:
cases i <;> rfl

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ (x \ y)ᶜ = x ⇨ y

Tactic:
rw [sdiff_eq, himp_eq, compl_inf, compl_compl, sup_comm]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
rw [symmDiff_comm, inf_comm, sdiff_symmDiff_left]

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
inst✝¹ : DecidableEq α✝
α : Type u_9
inst✝ : Nontrivial α
⊢ Nontrivial (Perm α)

Tactic:
obtain ⟨a : α⟩ := Nontrivial.to_nonempty (α := α)

Goal state after:
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
inst✝¹ : DecidableEq α✝
α : Type u_9
inst✝ : Nontrivial α
a : α
⊢ Nontrivial (Perm α)
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' s ⊆ f '' (t ∪ s)

Tactic:
exact image_mono subset_union_right

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' (range f ∩ s) = f ⁻¹' s

Tactic:
by
  rw [inter_comm, preimage_inter_range]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ StrictMono (rangeSplitting f)

Tactic:
by
  refine fun x y h ↦ hf.reflect_lt ?_
  simpa [apply_rangeSplitting f]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α
g : γ → α
s : Set β
t : Set γ
h : ∀ (b : β), b ∈ s → ∀ (c : γ), c ∈ t → f b ≠ g c
b : β
hb : b ∈ s
c : γ
hc : c ∈ t
eq : f b = g c
⊢ g c ∈ ⊥

Tactic:
exact h b hb c hc eq

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

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

Tactic:
Int.leInduction,

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

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

Tactic:
Int.leInduction,

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

Goal state before:
pp: case refine_1
a b c d m n✝ : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
⊢ (k : ℤ) → m ≤ k → ((k_1 : ℤ) → k_1 < k → motive k_1) → (k_1 : ℤ) → k_1 < k + 1 → motive k_1

pp: case refine_2
a b c d m n✝ : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
⊢ (k : ℤ) → k ≤ m → ((k_1 : ℤ) → k_1 < k → motive k_1) → (k_1 : ℤ) → k_1 < k - 1 → motive k_1

Tactic:
· intro _n _ ih l _
    exact if hlm : l < m then lt l hlm else ge l (by lia) fun k _ ↦ ih k (by lia)

Goal state after:
case refine_2
a b c d m n✝ : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
⊢ (k : ℤ) → k ≤ m → ((k_1 : ℤ) → k_1 < k → motive k_1) → (k_1 : ℤ) → k_1 < k - 1 → motive k_1
Module: Mathlib.Algebra.Group.TypeTags.Basic

Goal state before:
pp: case inr
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i : ι
a : M i
j : ι
h : j ≠ i
⊢ single i (ofMul a) j = ofMul (mulSingle i a j)

Tactic:
simp only [single, ne_eq, h, not_false_eq_true, Function.update_of_ne, zero_apply, mulSingle,
      one_apply, ofMul_one]

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

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

Tactic:
Nat.mod_add_div

Goal state after:
M : Type u_4
inst✝ : Monoid M
a : M
n m : ℕ
ha : a ^ n = 1
⊢ a ^ m = a ^ m
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
m n : ℕ
⊢ a ^ (↑m - ↑n) = a ^ m / a ^ n

Tactic:
simpa [div_eq_mul_inv] using zpow_sub a m n

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
k : ℤ
n : ℕ
⊢ (fun x ↦ x ^ k)^[n + 1] = fun x ↦ x ^ k ^ (n + 1)

Tactic:
by ext; simp [zpow_iterate, Int.pow_succ', zpow_mul]

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✝ : MulOneClass M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ 1 * f x = f x

Tactic:
rw [← one, ← mul, one_mul]

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

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

Tactic:
rw [← inv_div b c, div_inv_eq_mul, mul_comm, div_mul_div_cancel]

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

Goal state before:
pp: α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a = 1 ∧ b = 1 → a * b = 1

Tactic:
by
    rintro ⟨rfl, rfl⟩
    exact mul_one _

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

Goal state before:
pp: α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a = 1 ∧ b = 1 → a * b = 1

Tactic:
by
    rintro ⟨rfl, rfl⟩
    exact mul_one _

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

Goal state before:
pp: α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a = 1 ∧ b = 1 → a * b = 1

Tactic:
by
    rintro ⟨rfl, rfl⟩
    exact mul_one _

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : Bijective fun x ↦ a * x
⊢ (fun x ↦ a * x) (⋯.choose * a) = (fun x ↦ a * x) 1

Tactic:
simpa [mul_assoc] using congr_arg (· * a) (h.2 1).choose_spec

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

Goal state before:
pp: n : ℤ
⊢ sqrt (n * n) = ↑n.natAbs

Tactic:
rw [sqrt, ← natAbs_mul_self, toNat_natCast, Nat.sqrt_eq]

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

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

Tactic:
rw [inverse_unit, Units.inv_mul]

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x : M₀
⊢ IsUnit x ↔ x⁻¹ʳ * x = 1

Tactic:
by
  nontriviality M₀
  refine ⟨Ring.inverse_mul_cancel x, ?_⟩
  contrapose
  simp +contextual [not_isUnit_iff_inverse_eq_zero]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Ring α
F : Type u_1
inst✝² : Ring β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
⊢ (map ↑f) (-1) = -1

Tactic:
by
  simp only [Units.map_neg, map_one]

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

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

Tactic:
by
  simp [h, neg_one_pow_eq_ite]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ 1 ≤ a * b⁻¹ ↔ b ≤ a

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

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ d * b ≤ d * a

Tactic:
by gcongr; exact hcd.trans_le <| add_le_of_nonpos_left hc

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ b * d ≤ a * d

Tactic:
by gcongr; exact hcd.trans_le <| add_le_of_nonpos_left hc

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : Preorder G₀
inst✝ : ZeroLEOneClass G₀
a : G₀
⊢ a * a⁻¹ ≤ 1

Tactic:
by simpa only [div_eq_mul_inv] using div_self_le_one a

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
ha : a < 0
h : b < 1
⊢ a < a * b

Tactic:
by
  simpa only [mul_one] using mul_lt_mul_of_neg_left h ha

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
ha : a < 0
h : 1 < b
⊢ a * b < a

Tactic:
by
  simpa only [mul_one] using mul_lt_mul_of_neg_left h ha

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

Goal state before:
pp: α₁ : Sort u
α₂ : Sort v
α₃ : Sort x
γ : Sort w
inst✝ : Inhabited γ
e₁₂ : α₁ ↪ α₂
e₂₃ : α₂ ↪ α₃
f : α₁ → γ
a : α₃
⊢ extend (⇑e₂₃) (extend (⇑e₁₂) f fun a ↦ default) (fun a ↦ default) a = extend (⇑e₂₃ ∘ ⇑e₁₂) f (fun a ↦ default) a

Tactic:
e₁₂.injective.extend_comp e₂₃.injective,

Goal state after:
α₁ : Sort u
α₂ : Sort v
α₃ : Sort x
γ : Sort w
inst✝ : Inhabited γ
e₁₂ : α₁ ↪ α₂
e₂₃ : α₂ ↪ α₃
f : α₁ → γ
a : α₃
⊢ extend (⇑e₂₃) (extend (⇑e₁₂) f fun a ↦ default) (fun a ↦ default) a =
    extend (⇑e₂₃) (extend (⇑e₁₂) f ((fun a ↦ default) ∘ ⇑e₂₃)) (fun a ↦ default) a
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this✝ : 1 = a * a.gcdA c + c * a.gcdB c
this : b * a * a.gcdA c + b * c * a.gcdB c = b
⊢ a ∣ b

Tactic:
rw [← this]

Goal state after:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this✝ : 1 = a * a.gcdA c + c * a.gcdB c
this : b * a * a.gcdA c + b * c * a.gcdB c = b
⊢ a ∣ b * a * a.gcdA c + b * c * a.gcdB c
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case right
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ a ^ n = 1

Tactic:
· rw [← Nat.mul_div_cancel' (m.gcd_dvd_right n), pow_mul, hmn, one_pow]

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

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
ha : a = 0
⊢ b * a = b * 0

Tactic:
by rw [ha]

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

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsRightRegular b
ha : a = 0
⊢ a * b = 0 * b

Tactic:
by rw [ha]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Monoid α
inst✝ : LinearOrder α
a b : αˣ
⊢ ↑(a ⊔ b) = if a ≤ b then ↑b else ↑a

Tactic:
← apply_ite

Goal state after:
α : Type u_1
inst✝¹ : Monoid α
inst✝ : LinearOrder α
a b : αˣ
⊢ ↑(a ⊔ b) = ↑(if a ≤ b then b else a)
Module: Mathlib.Algebra.Order.Monoid.Units

Goal state before:
pp: α : Type u_1
inst✝¹ : Monoid α
inst✝ : LinearOrder α
a b : αˣ
⊢ ↑(a ⊓ b) = if a ≤ b then ↑a else ↑b

Tactic:
← apply_ite

Goal state after:
α : Type u_1
inst✝¹ : Monoid α
inst✝ : LinearOrder α
a b : αˣ
⊢ ↑(a ⊓ b) = ↑(if a ≤ b then a else b)
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : AddLeftMono α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftReflectLT α
hb : AddLECancellable b
hca : c ≤ a
h : a - b < a - c
⊢ c < b

Tactic:
conv_lhs at h => rw [← tsub_add_cancel_of_le hca]

Goal state after:
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : AddLeftMono α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftReflectLT α
hb : AddLECancellable b
hca : c ≤ a
h : a - c + c - b < a - c
⊢ c < b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithTop α
a✝ : α
⊢ map (⇑f) (↑a✝ + b) = map ⇑f ↑a✝ + map (⇑f) b

Tactic:
induction b

Goal state after:
case coe.top
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝ : α
⊢ map (⇑f) (↑a✝ + ⊤) = map ⇑f ↑a✝ + map ⇑f ⊤

case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map (⇑f) (↑a✝¹ + ↑a✝) = map ⇑f ↑a✝¹ + map ⇑f ↑a✝
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
⊢ a + a - (b + b) = a - b + (a - b)

Tactic:
obtain h | h := le_total a b

Goal state after:
case inl
α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
h : a ≤ b
⊢ a + a - (b + b) = a - b + (a - b)

case inr
α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
h : b ≤ a
⊢ a + a - (b + b) = a - b + (a - b)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
M : Type u_1
N : Type u_2
inst✝¹ : One M
inst✝ : One N
f : OneHom M N
⊢ map (⇑f) 1 = 1

Tactic:
by rw [WithTop.map_one, map_one, coe_one]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
⊢ 0 ≤ ↑n * x + ↑n * ↑n

Tactic:
by
  have hnx : 0 < n → 0 ≤ x + n := fun hn => by
    have := _root_.add_le_add (neg_le_of_abs_le hx) (cast_one_le_of_pos hn)
    rwa [neg_add_cancel] at this
  have hnx' : n < 0 → x + n ≤ 0 := fun hn => by
    have := _root_.add_le_add (le_of_abs_le hx) (cast_le_neg_one_of_neg hn)
    rwa [add_neg_cancel] at this
  rw [← mul_add, mul_nonneg_iff]
  rcases lt_trichotomy n 0 with (h | rfl | h)
  · exact Or.inr ⟨mod_cast h.le, hnx' h⟩
  · simp [le_total 0 x]
  · exact Or.inl ⟨mod_cast h.le, hnx h⟩

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
b : WithBot α
h : b ≠ ⊥
⊢ a = b.unbot h ↔ ↑a = b

Tactic:
induction b

Goal state after:
case bot
α : Type u_1
a : α
h : ⊥ ≠ ⊥
⊢ a = ⊥.unbot h ↔ ↑a = ⊥

case coe
α : Type u_1
a a✝ : α
h : ↑a✝ ≠ ⊥
⊢ a = (↑a✝).unbot h ↔ ↑a = ↑a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
b c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
⊢ ⊥ + c ≤ b + c ↔ ⊥ ≤ b

Tactic:
induction b

Goal state after:
case bot.bot
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
⊢ ⊥ + c ≤ ⊥ + c ↔ ⊥ ≤ ⊥

case bot.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a✝ : WithTop α
⊢ ⊥ + c ≤ ↑a✝ + c ↔ ⊥ ≤ ↑a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
b c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a✝ : WithTop α
⊢ ↑a✝ + c ≤ b + c ↔ ↑a✝ ≤ b

Tactic:
induction b

Goal state after:
case coe.bot
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a✝ : WithTop α
⊢ ↑a✝ + c ≤ ⊥ + c ↔ ↑a✝ ≤ ⊥

case coe.coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a✝¹ a✝ : WithTop α
⊢ ↑a✝¹ + c ≤ ↑a✝ + c ↔ ↑a✝¹ ≤ ↑a✝