mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c✝ : α
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
a b c : α
⊢ Decidable.decide (r a b) = true → Decidable.decide (r b c) = true → Decidable.decide (r a c) = true

Tactic:
simpa using trans a b c

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Std.Refl r ↔ Eq ≤ r

Tactic:
by
  unfold Pi.hasLe Prop.le
  grind [Std.Refl]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
⊢ (r ∘r p) ∘r q = r ∘r p ∘r q

Tactic:
funext a d
  apply propext
  constructor
  · exact fun ⟨c, ⟨b, hab, hbc⟩, hcd⟩ ↦ ⟨b, hab, c, hbc, hcd⟩
  · exact fun ⟨b, hab, c, hbc, hcd⟩ ↦ ⟨c, ⟨b, hab, hbc⟩, hcd⟩

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

Goal state before:
pp: α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ ⇑g ∘ ⇑f = id ↔ f = g.symm

Tactic:
← eq_symm_comp,

Goal state after:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ ⇑f = ⇑g.symm ∘ id ↔ f = g.symm
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
motive : α → Prop
ha : b ≤ a → motive a
hb : a ≤ b → motive b
⊢ motive (max a b)

Tactic:
by
  rw [max_def]; split_ifs with h
  exacts [hb h, ha (le_of_not_ge h)]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case lt
α : Type u_1
inst✝ : LT α
a b : α
⊢ lt.Compares (toDual a) (toDual b) ↔ lt.Compares b a

pp: case eq
α : Type u_1
inst✝ : LT α
a b : α
⊢ eq.Compares (toDual a) (toDual b) ↔ eq.Compares b a

pp: case gt
α : Type u_1
inst✝ : LT α
a b : α
⊢ gt.Compares (toDual a) (toDual b) ↔ gt.Compares b a

Tactic:
exacts [Iff.rfl, eq_comm, Iff.rfl]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case lt
α : Type u_1
inst✝ : LT α
a b : αᵒᵈ
⊢ lt.Compares (ofDual a) (ofDual b) ↔ lt.Compares b a

pp: case eq
α : Type u_1
inst✝ : LT α
a b : αᵒᵈ
⊢ eq.Compares (ofDual a) (ofDual b) ↔ eq.Compares b a

pp: case gt
α : Type u_1
inst✝ : LT α
a b : αᵒᵈ
⊢ gt.Compares (ofDual a) (ofDual b) ↔ gt.Compares b a

Tactic:
exacts [Iff.rfl, eq_comm, Iff.rfl]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ (cmp x y).swap = (cmp x' y').swap

Tactic:
swap_inj

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ cmp x y = cmp x' y'
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp y x = cmp y' x'
⊢ (cmp y x).swap = (cmp y' x').swap

Tactic:
swap_inj

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp y x = cmp y' x'
⊢ cmp y x = cmp y' x'
Module: Mathlib.Order.Monotone.Defs

Goal state before:
pp: ι : Type u_1
α : Type u
β : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (β i)
inst✝ : Preorder α
f : α → (i : ι) → β i
⊢ Antitone f ↔ ∀ (i : ι), Antitone fun x ↦ f x i

Tactic:
simp [Antitone, Pi.le_def, @forall_comm ι]

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case mpr
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ (∀ (i : ι), Disjoint (f i) (g i)) → Disjoint f g

Tactic:
intro h x hf hg i
    apply h i (hf i) (hg i)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictMonoOn (f ∘ ⇑ofDual) s ↔ StrictAntiOn f s

Tactic:
strictMonoOn_comp_ofDual_iff

Goal state after:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictAntiOn f s ↔ StrictAntiOn f s
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 : α × β
⊢ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd → Disjoint x y

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

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

Goal state before:
pp: α : Type u
⊢ univ = {∅} ↔ IsEmpty α

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ by simp⟩

Goal state after:
α : Type u
h : univ = {∅}
⊢ IsEmpty α
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ (b ⊔ c) ⊓ a ≤ b ⊓ a ⊔ c ⊓ a

Tactic:
← le_himp_iff,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ b ⊔ c ≤ a ⇨ b ⊓ a ⊔ c ⊓ a
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✝³ : Bot α
inst✝² : Compl α
inst✝¹ : HImp α
inst✝ : HeytingAlgebra β
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_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ f a ⇨ ⊥ = (f a)ᶜ

Tactic:
himp_bot

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Max α
inst✝⁷ : Min α
inst✝⁶ : LE α
inst✝⁵ : LT α
inst✝⁴ : Top α
inst✝³ : Bot α
inst✝² : Compl α
inst✝¹ : HImp α
inst✝ : HeytingAlgebra β
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_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ (f a)ᶜ = (f a)ᶜ
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : (x ⊔ z) ⊓ y = y
⊢ y ⊓ x ⊔ z = y

Tactic:
rwa [sup_inf_right, inf_sup_right, sup_comm x, inf_sup_self, inf_comm, sup_comm z,
        hs, sup_eq_left]

Goal state after:
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₁ : Surjective f₁
h₂ : ∀ (a : α₁), Surjective (f₂ a)
⊢ Surjective (Sigma.map f₁ f₂)

Tactic:
by
  simp only [Surjective, Sigma.forall, h₁.forall]
  exact fun i ↦ (h₂ _).forall.2 fun x ↦ ⟨⟨i, x⟩, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' (t ∩ range Subtype.val) = f '' (t ∩ s)

Tactic:
Subtype.range_coe

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' (t ∩ s) = f '' (t ∩ s)
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
γ : Type u_3
δ : Type u_4
s : Set α
a b : α → γ × δ
⊢ EqOn a b s ↔ EqOn (Prod.fst ∘ a) (Prod.fst ∘ b) s ∧ EqOn (Prod.snd ∘ a) (Prod.snd ∘ b) s

Tactic:
grind [EqOn]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
hf : EqOn f f' s
hg : EqOn g g' t
⊢ EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)

Tactic:
grind [EqOn]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
hβ : Nonempty β
⊢ range (const α) = {f | ∀ (x y : α), f x = f y}

Tactic:
refine (range_eq_iff _ _).mpr ⟨fun _ _ _ ↦ rfl, fun f hf ↦ ?_⟩
  rcases isEmpty_or_nonempty α with h | ⟨⟨a⟩⟩
  · exact hβ.elim fun b ↦ ⟨b, Subsingleton.elim _ _⟩
  · exact ⟨f a, funext fun x ↦ hf _ _⟩

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ val ⁻¹' (s ∩ t) = val ⁻¹' t

Tactic:
preimage_coe_self_inter

Goal state after:
α : Type u_1
s t : Set α
⊢ val ⁻¹' t = val ⁻¹' t
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
ht : (s.pi t).Nonempty
i : ι
⊢ t i ⊆ eval i '' s.pi t

Tactic:
obtain ⟨f, hf⟩ := ht

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i
hf : f ∈ s.pi t
⊢ t i ⊆ eval i '' s.pi t
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
i : ι
inst✝ : DecidableEq ι
s : Set (α i)
x : (x : ι) → α x
⊢ x ∈ eval i ⁻¹' s ↔ x ∈ univ.pi (update (fun x ↦ univ) i s)

Tactic:
simp [@forall_update_iff _ (fun i => Set (α i)) _ _ _ _ fun i' y => x i' ∈ y]

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

Goal state before:
pp: a : ℤ
⊢ (-a).pred.succ = -a

Tactic:
succ_pred

Goal state after:
a : ℤ
⊢ -a = -a
Module: Mathlib.Data.Int.Init

Goal state before:
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:
exact fun n _ hn l _ ↦ hn l (by lia)

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

Goal state before:
pp: a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = b * k / b * d

Tactic:
rw [Int.mul_ediv_cancel_left _ hb]

Goal state after:
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = k * d
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: case succ
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
y : M₀
⊢ f (x ^ (n + 1) * y) = f x ^ (n + 1) * f y

Tactic:
rw [pow_succ', pow_succ', mul_assoc, mul_assoc, hx, hn]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
⊢ NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), x * y = 0 → y = 0

Tactic:
by
  simp only [noZeroDivisors_iff, or_iff_not_imp_left]
  exact ⟨fun h a ha b eq ↦ h eq ha, fun h a b eq ha ↦ h a ha b eq⟩

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:
rw [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.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroHomClass F α β
a : α
f : F
neZero : NeZero (f a)
h : a = 0
⊢ f 0 = 0

Tactic:
exact ZeroHomClass.map_zero f

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f g : α →*₀ β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f; obtain ⟨⟨_, _⟩, _⟩ := g; congr

Goal state after:
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₀
m : A
⊢ 1 • m = m

Tactic:
change f 1 • m = m; simp

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

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

Tactic:
← e,

Goal state after:
case succ
R : Type u
inst✝ : AddGroupWithOne R
m n n✝ : ℕ
e : n - m = n✝ + 1
⊢ -↑(n - m) = ↑m - ↑n
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: m n : ℕ
⊢ m.sqrt < n ↔ m < n ^ 2

Tactic:
by simp only [← not_le, le_sqrt']

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

Goal state before:
pp: α : Type u_3
inst✝ : Ring α
⊢ IsDomain α ↔ NoZeroDivisors α ∧ Nontrivial α

Tactic:
← isCancelMulZero_iff_noZeroDivisors,

Goal state after:
α : Type u_3
inst✝ : Ring α
⊢ IsDomain α ↔ IsCancelMulZero α ∧ Nontrivial α
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_3
inst✝ : Ring α
⊢ NoZeroDivisors α ↔ IsDomain α ∨ Subsingleton α

Tactic:
← isCancelMulZero_iff_noZeroDivisors,

Goal state after:
α : Type u_3
inst✝ : Ring α
⊢ IsCancelMulZero α ↔ IsDomain α ∨ Subsingleton α
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : ¬2 = 0 → f (x * y) = f x * f y
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
exact hxy h_two

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:
rw [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.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
ha : a ≠ 0
⊢ a ^ (-n) * a ^ n = 1

Tactic:
rw [zpow_neg]; exact inv_mul_cancel₀ (zpow_ne_zero n ha)

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
⊢ b * (a / b) = a

Tactic:
rw [mul_comm, div_mul_cancel_of_imp h]

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

Goal state before:
pp: R : Type u
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NoZeroDivisors R
a b : R
h : Commute a b
⊢ a * a = b * b ↔ a = b ∨ a = -b

Tactic:
by
  rw [← sub_eq_zero, h.mul_self_sub_mul_self_eq, mul_eq_zero, or_comm, sub_eq_zero,
    add_eq_zero_iff_eq_neg]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : Rˣ
⊢ a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b

Tactic:
Units.ext_iff,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : Rˣ
⊢ ↑(a ^ 2) = ↑(b ^ 2) ↔ ↑a = ↑b ∨ ↑a = ↑(-b)
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ u⁻¹ = u ↔ u = 1 ∨ u = -1

Tactic:
rw [inv_eq_iff_mul_eq_one]
  simp only [Units.ext_iff]
  push_cast
  exact mul_self_eq_one_iff

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : M
⊢ 0 • a = 0

Tactic:
by simp_rw [HSMul.hSMul, SMul.smul, Int.cast_zero]; exact zero_smul R a

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

Goal state before:
pp: case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)
⊢ r b c

Tactic:
rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c]
    exact h a⁻¹ bc

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

Goal state before:
pp: case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r b c
⊢ r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)

Tactic:
rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c] at bc
    exact h a⁻¹ bc

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

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Contravariant M N μ fun x1 x2 ↦ x1 ≤ x2
a : M
b c : N
bc : (fun x1 x2 ↦ x1 = x2) (μ a b) (μ a c)
⊢ (fun x1 x2 ↦ x1 = x2) b c

pp: case refine_3
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : (Contravariant M N μ fun x1 x2 ↦ x1 < x2) ∧ Contravariant M N μ fun x1 x2 ↦ x1 = x2
a : M
b c : N
bc : (fun x1 x2 ↦ x1 ≤ x2) (μ a b) (μ a c)
⊢ (fun x1 x2 ↦ x1 ≤ x2) b c

Tactic:
· exact (h a bc.le).antisymm (h a bc.ge)

Goal state after:
case refine_3
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : (Contravariant M N μ fun x1 x2 ↦ x1 < x2) ∧ Contravariant M N μ fun x1 x2 ↦ x1 = x2
a : M
b c : N
bc : (fun x1 x2 ↦ x1 ≤ x2) (μ a b) (μ a c)
⊢ (fun x1 x2 ↦ x1 ≤ x2) b c
Module: Mathlib.Algebra.Order.GroupWithZero.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : IsMulCommutative α
⊢ PosMulReflectLT α ↔ MulPosReflectLT α

Tactic:
by
  simp [posMulReflectLT_iff, mulPosReflectLT_iff, mul_comm']

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

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

Tactic:
rw [← mul_lt_mul_iff_left a]
  simp

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ a * a ≤ 1 ↔ a ≤ 1

Tactic:
by contrapose!; exact one_lt_mul_self_iff

Goal state after:
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:
contrapose!
  exact fun h => mul_lt_mul_of_le_of_lt h.1 h.2

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

Goal state before:
pp: α : Type u_1
s : Semiring α
⊢ OfNat.ofNat (1 + 1) = OfNat.ofNat 1 + 1

Tactic:
change Nat.cast 2 = 1 + 1
      rw [one_add_one_eq_two]
      rfl

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

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
⊢ Function.Injective fun x ↦ if h : p ↑x then Sum.inl ⟨↑x, h⟩ else Sum.inr ⟨↑x, ⋯⟩

Tactic:
intro x y
    dsimp only
    split_ifs <;> simp [Subtype.ext_iff]

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
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
⊢ a ^ 2 + (a + b) * b = a ^ 2

Tactic:
rw [← hab, zero_mul, add_zero]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ fst.prod snd = id

Tactic:
by
  ext ⟨x, y⟩ : 2
  rfl

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
⊢ |b|ₘ / |a|ₘ ≤ |a / b|ₘ

Tactic:
by rw [mabs_div_comm]; apply mabs_div_mabs_le_mabs_div

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

Goal state before:
pp: α : Type u
d y : α
x : WithOne α
⊢ unoneD d x = y ↔ x = ↑y ∨ x = 1 ∧ y = d

Tactic:
induction x

Goal state after:
case one
α : Type u
d y : α
⊢ unoneD d 1 = y ↔ 1 = ↑y ∨ 1 = 1 ∧ y = d

case coe
α : Type u
d y a✝ : α
⊢ unoneD d ↑a✝ = y ↔ ↑a✝ = ↑y ∨ ↑a✝ = 1 ∧ y = d
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
x : WithBot α
hx : x ≠ ⊥
y : WithBot α
⊢ y ≤ y + x

Tactic:
induction x

Goal state after:
case bot
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
y : WithBot α
hx : ⊥ ≠ ⊥
⊢ y ≤ y + ⊥

case coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
y : WithBot α
a✝ : α
hx : ↑a✝ ≠ ⊥
⊢ y ≤ y + ↑a✝
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
x : WithBot α
hx : x ≠ ⊥
y : WithBot α
⊢ y ≤ x + y

Tactic:
induction x

Goal state after:
case bot
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
y : WithBot α
hx : ⊥ ≠ ⊥
⊢ y ≤ ⊥ + y

case coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
y : WithBot α
a✝ : α
hx : ↑a✝ ≠ ⊥
⊢ y ≤ ↑a✝ + y
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: β : Type u_2
inst✝ : MulOneClass β
x : WithZero β
⊢ ↑(map' (MonoidHom.id β)) x = (MonoidHom.id (WithZero β)) x

Tactic:
induction x

Goal state after:
case zero
β : Type u_2
inst✝ : MulOneClass β
⊢ ↑(map' (MonoidHom.id β)) 0 = (MonoidHom.id (WithZero β)) 0

case coe
β : Type u_2
inst✝ : MulOneClass β
a✝ : β
⊢ ↑(map' (MonoidHom.id β)) ↑a✝ = (MonoidHom.id (WithZero β)) ↑a✝
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
f : α →* β
g : β →* γ
x : WithZero α
⊢ (map' g) ((map' f) x) = (map' (g.comp f)) x

Tactic:
induction x

Goal state after:
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
f : α →* β
g : β →* γ
⊢ (map' g) ((map' f) 0) = (map' (g.comp f)) 0

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
f : α →* β
g : β →* γ
a✝ : α
⊢ (map' g) ((map' f) ↑a✝) = (map' (g.comp f)) ↑a✝
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b c a : α
⊢ - -a = a

Tactic:
obtain rfl | ha := eq_or_ne a ⊤

Goal state after:
case inl
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b c : α
⊢ - -⊤ = ⊤

case inr
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b c a : α
ha : a ≠ ⊤
⊢ - -a = a
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case inr.hba
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b c a : α
ha : a ≠ ⊤
⊢ - -a + -a = 0

Tactic:
simp [add_comm, add_neg_cancel_of_ne_top, ha]

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case inr.hac
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b c a : α
ha : a ≠ ⊤
⊢ -a + a = 0

Tactic:
simp [add_comm, add_neg_cancel_of_ne_top, ha]

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
⊢ -(a + b) = -b + -a

Tactic:
obtain rfl | ha := eq_or_ne a ⊤

Goal state after:
case inl
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b✝ c b : α
⊢ -(⊤ + b) = -b + -⊤

case inr
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
ha : a ≠ ⊤
⊢ -(a + b) = -b + -a
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ 0 ≤ a - a

Tactic:
obtain rfl | ha := eq_or_ne a ⊤

Goal state after:
case inl
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
⊢ 0 ≤ ⊤ - ⊤

case inr
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
⊢ 0 ≤ a - a
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case inr
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
⊢ 0 ≤ a - a

Tactic:
rw [sub_self_eq_zero_of_ne_top ha]

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

Goal state before:
pp: α : Type u
inst✝³ : Add α
w x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightStrictMono α
xz : x < z
yw : y < w
⊢ x + y < z + w

Tactic:
by
  apply (WithTop.add_lt_add_left xz.ne_top yw).trans_le
  cases w
  · simp
  · exact (WithTop.add_lt_add_right coe_ne_top xz).le

Goal state after: