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

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

Tactic:
· exact absurd h₃ h₁

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
⊢ Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y) (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x))
      (k + 1) m n =
    m * npowRec' (k + 1) n

Tactic:
generalize hk : k + 1 = k'

Goal state after:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
k' : ℕ
hk : k + 1 = k'
⊢ Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y) (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x))
      k' m n =
    m * npowRec' k' n
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
inv_mul_cancel_right a b

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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
inst✝ : Symm r
⊢ (∀ (a : α), ∃! b, r a b) ↔ ∃ f, Involutive f ∧ ∀ {a b : α}, r a b ↔ f a = b

Tactic:
by
  simp [Std.Symm.forall_existsUnique_iff', funext_iff]

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

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

Tactic:
by intros; ext; exact one_mul _

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ a = b

Tactic:
by
  rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq_eq_eq le_refl not_le]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
le✝¹ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), le✝¹ a a
le_trans✝¹ : ∀ (a b c : α), le✝¹ a b → le✝¹ b c → le✝¹ a c
A_iff : ∀ (a b : α), A_lt a b ↔ le✝¹ a b ∧ ¬le✝¹ b a
le✝ B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), le✝ a a
le_trans✝ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
B_iff : ∀ (a b : α), B_lt a b ↔ le✝ a b ∧ ¬le✝ b a
⊢ { le := le✝¹, lt := A_lt, le_refl := le_refl✝¹, le_trans := le_trans✝¹, lt_iff_le_not_ge := A_iff }.toLE =
      { le := le✝, lt := B_lt, le_refl := le_refl✝, le_trans := le_trans✝, lt_iff_le_not_ge := B_iff }.toLE →
    { le := le✝¹, lt := A_lt, le_refl := le_refl✝¹, le_trans := le_trans✝¹, lt_iff_le_not_ge := A_iff } =
      { le := le✝, lt := B_lt, le_refl := le_refl✝, le_trans := le_trans✝, lt_iff_le_not_ge := B_iff }

Tactic:
rintro ⟨⟩
    have : A_lt = B_lt := by
      funext a b
      rw [A_iff, B_iff]
    cases this
    congr

Goal state after:
Module: Mathlib.Order.Basic

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

Tactic:
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
x y : α
⊢ x ≤ y ↔ x ≤ y

Tactic:
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
x y : α
⊢ x ≤ y ↔ x ≤ y

Tactic:
exact H x y

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

Goal state before:
pp: α : Type u
ι : Sort u_1
f : ι → α
⊢ Function.Injective (rangeFactorization f) ↔ Function.Injective f

Tactic:
simp [Function.Injective, rangeFactorization]

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b c : α
⊢ Disjoint a (b ⊔ c) ↔ Disjoint a b ∧ Disjoint a c

Tactic:
by
  simp only [disjoint_iff, inf_sup_left, sup_eq_bot_iff]

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ ({a} ∩ s).Nonempty ↔ a ∈ s

Tactic:
singleton_inter_nonempty

Goal state after:
α : Type u_1
s : Set α
a : α
⊢ a ∈ s ↔ a ∈ s
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: x : Prop
⊢ x = True ∨ x ∈ {False}

Tactic:
mem_singleton_iff

Goal state after:
x : Prop
⊢ x = True ∨ x = False
Module: Mathlib.Order.GaloisConnection.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
⊢ (∀ (a : β) (b : α), u a ≤ b ↔ a ≤ l b) = ∀ (a : α) (b : β), b ≤ l a ↔ u b ≤ a

Tactic:
by
  rw [forall_comm]; simp only [Iff.comm]

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : yᶜ ≤ x
⊢ xᶜ ≤ y

Tactic:
simpa only [compl_compl] using compl_le_compl h

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
p : α → Prop
q : β → Prop
r : γ → Prop
e : α ≃ β
f : β ≃ γ
h : ∀ (a : α), p a ↔ q (e a)
h' : ∀ (b : β), q b ↔ r (f b)
⊢ ∀ (a : α), p a ↔ r ((e.trans f) a)

Tactic:
exact fun a => (h a).trans (h' <| e a)

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
α : Type ?u.12
p : Option α → Type v
h : ∀ (a : p none), False
⊢ ∀ (x : Option α) (a : p x), x.isSome = true

Tactic:
intro x
    cases x
    · intro n
      exfalso
      exact h n
    · intro _
      exact rfl

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
exact le_sup_of_le_right le_sdiff_sup

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
⊢ BooleanAlgebra α

Tactic:
apply e.injective.booleanAlgebra <;> intros <;> first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c ≤ a ∆ c ⊔ b ∆ c

Tactic:
trans c \ (a ⊓ b)

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c ≤ c \ (a ⊓ b)

α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c \ (a ⊓ b) ≤ a ∆ c ⊔ b ∆ c
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
p : α × β → Prop
⊢ (∃ x, x ∈ s ×ˢ t ∧ p x) ↔ ∃ x, x ∈ s ∧ ∃ y, y ∈ t ∧ p (x, y)

Tactic:
by
  simp [and_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ range (extend f g g') ⊆ range g ∪ g' '' (range f)ᶜ

Tactic:
rintro _ ⟨y, rfl⟩
  rw [extend_def]
  split_ifs with h
  exacts [Or.inl (mem_range_self _), Or.inr (mem_image_of_mem _ h)]

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

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

Tactic:
by rw [← inv_div, mul_div_cancel_left]

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✝¹ : Monoid M
inst✝ : Monoid N
u : (M × N)ˣ
⊢ (fun u ↦ { val := (↑u.1, ↑u.2), inv := (↑u.1⁻¹, ↑u.2⁻¹), val_inv := ⋯, inv_val := ⋯ })
      (((Units.map (MonoidHom.fst M N)).prod (Units.map (MonoidHom.snd M N))) u) =
    u

Tactic:
simp only [MonoidHom.prod_apply, Units.coe_map, MonoidHom.coe_fst, MonoidHom.coe_snd,
      Prod.mk.eta, Units.coe_map_inv, Units.mk_val]

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

Goal state before:
pp: case neg
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
hx : ¬p x
⊢ ({ toFun := fun f ↦ f.extendDomain (Equiv.refl { x // p x }), map_one' := ⋯ } (f.subtypePerm h₁)) x = f x

Tactic:
OneHom.coe_mk,

Goal state after:
case neg
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
hx : ¬p x
⊢ ((f.subtypePerm h₁).extendDomain (Equiv.refl { x // p x })) x = f x
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case succ
M₀ : Type u_1
G₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
a✝ : M₀
n✝ : ℕ
inst✝ : NoZeroDivisors M₀
a : M₀
x✝ : IsNilpotent a
n : ℕ
ih : a ^ n = 0 → a = 0
ha : a ^ n * a = 0
⊢ a = 0

Tactic:
mul_eq_zero

Goal state after:
case succ
M₀ : Type u_1
G₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
a✝ : M₀
n✝ : ℕ
inst✝ : NoZeroDivisors M₀
a : M₀
x✝ : IsNilpotent a
n : ℕ
ih : a ^ n = 0 → a = 0
ha : a ^ n = 0 ∨ a = 0
⊢ a = 0
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:
apply H; rw [h, Nat.cast_zero]

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

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

Tactic:
Int.negSucc_add_ofNat,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(subNatNat n m.succ) = ↑-[m+1] + ↑↑n
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a : R
⊢ 1 / -a = 1 / (-1 * a)

Tactic:
by rw [neg_eq_neg_one_mul]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
by
  by_cases hab : IsUnit (a * b)
  · obtain ⟨⟨a, rfl⟩, b, rfl⟩ := h.isUnit_mul_iff.mp hab
    rw [← Units.val_mul, inverse_unit, inverse_unit, inverse_unit, ← Units.val_mul, mul_inv_rev]
  obtain ha | hb := not_and_or.mp (mt h.isUnit_mul_iff.mpr hab)
  · rw [inverse_non_unit _ hab, inverse_non_unit _ ha, mul_zero]
  · rw [inverse_non_unit _ hab, inverse_non_unit _ hb, zero_mul]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a : G₀
ha : 0 < a
b c : G₀
hbc : b < c
⊢ a⁻¹ * (a * b) < a⁻¹ * (a * c)

Tactic:
by simpa [ha.ne']

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a ≤ 1
hn : 0 ≤ n
⊢ a ^ n ≤ 1

Tactic:
simpa using zpow_right_anti₀ ha₀ ha₁ hn

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a ≤ 1
hn : n ≤ 0
⊢ 1 ≤ a ^ n

Tactic:
simpa using zpow_right_anti₀ ha₀ ha₁ hn

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
hn : 0 < n
⊢ a ^ n < 1

Tactic:
simpa using zpow_right_strictAnti₀ ha₀ ha₁ hn

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
hn : n < 0
⊢ 1 < a ^ n

Tactic:
simpa using zpow_right_strictAnti₀ ha₀ ha₁ hn

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a : G₀
ha : 0 < a
b c : G₀
hbc : b < c
⊢ b * a * a⁻¹ < c * a * a⁻¹

Tactic:
by simpa [ha.ne']

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

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

Tactic:
by
  rw [lt_div_iff₀ ha, lt_div_iff₀' hc]

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
r : α → α → Prop
f : α ↪ β
a b : α
⊢ Relation.Map r (⇑f) (⇑f) (f a) (f b) ↔ r a b

Tactic:
by grind [Relation.onFun_map_eq_of_injective (r := r) f.injective]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
inst✝ : Archimedean R
x : R
a✝ : Nontrivial R
n : ℕ
h : x ≤ n • 1
⊢ x ≤ ↑n

Tactic:
← nsmul_one

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
inst✝ : Archimedean R
x : R
a✝ : Nontrivial R
n : ℕ
h : x ≤ n • 1
⊢ x ≤ n • 1
Module: Mathlib.Algebra.Order.Archimedean.Defs

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
n : ℕ
hn : x < n • 1
⊢ x < ↑n

Tactic:
← nsmul_one

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
n : ℕ
hn : x < n • 1
⊢ x < n • 1
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
n : ℕ
h : a < 1
hn : n ≠ 0
⊢ a ^ n < 1

Tactic:
by
  rcases Nat.exists_eq_succ_of_ne_zero hn with ⟨k, rfl⟩
  rw [pow_succ']
  exact mul_lt_one_of_lt_of_le h (pow_le_one_of_le h.le _)

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

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ b ^ n * a ^ 2 ≤ b ^ n * (b * a)

Tactic:
by grw [hab]

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

Goal state before:
pp: case negSucc
α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
a : α
k : ℕ
⊢ (-a) ^ (2 * Int.negSucc k + 1) = -a ^ (2 * Int.negSucc k + 1)

Tactic:
simp_rw [Int.negSucc_eq, show 2 * -(↑k + 1) + (1 : ℤ) = - (1 + k*2) by grind, _root_.zpow_neg]

Goal state after:
case negSucc
α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
a : α
k : ℕ
⊢ ((-a) ^ (1 + ↑k * 2))⁻¹ = -(a ^ (1 + ↑k * 2))⁻¹
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s : ℕ
h : s.succ ≠ 0
⊢ s.succ.gcdA 0 = 1

Tactic:
simp [gcdA, xgcd, xgcdAux, Nat.strongRec_eq]

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

Goal state before:
pp: case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, x.P y (b % a, s, t) → x.P y (a, s', t') → x.P y ((b % a).xgcdAux s t a s' t')
⊢ ∀ {s t s' t' : ℤ}, x.P y (a, s, t) → x.P y (b, s', t') → x.P y (a.xgcdAux s t b s' t')

Tactic:
intro s t s' t' p p'

Goal state after:
case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, x.P y (b % a, s, t) → x.P y (a, s', t') → x.P y ((b % a).xgcdAux s t a s' t')
s t s' t' : ℤ
p : x.P y (a, s, t)
p' : x.P y (b, s', t')
⊢ x.P y (a.xgcdAux s t b s' t')
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: a b c : ℤ
habc : a ∣ c * b
hab : a.gcd b = 1
⊢ a ∣ c

Tactic:
exact dvd_of_dvd_mul_left_of_gcd_one habc hab

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

Goal state before:
pp: α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
⊢ min a (b * c) = min a (min a b * min a c)

Tactic:
by
  rcases le_total a b with hb | hb
  · simp [hb, le_mul_right]
  · rcases le_total a c with hc | hc
    · simp [hc, le_mul_left]
    · simp [hb, hc]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
ha : a ≠ ⊤
⊢ b - a = 0 ↔ b = a

Tactic:
← sub_self_eq_zero_of_ne_top ha,

Goal state after:
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
ha : a ≠ ⊤
⊢ b - a = a - a ↔ b = a
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 : α
h : c ≤ b
⊢ a - c ≤ b - c ↔ a ≤ b

Tactic:
rw [tsub_le_iff_right, tsub_add_cancel_of_le h]

Goal state after:
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 : α
h : c ≤ b
h2 : a - c < b - c
⊢ a < b

Tactic:
refine ((tsub_le_tsub_iff_right h).mp h2.le).lt_of_ne ?_

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h : c ≤ b
h2 : a - c < b - c
⊢ a ≠ b
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x y : WithTop α
⊢ x < y ↔ (∃ a, x = ↑a) ∧ y = ⊤ ∨ ∃ a b, a < b ∧ x = ↑a ∧ y = ↑b

Tactic:
by
  grind [WithTop.lt_def']

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

Goal state before:
pp: P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : P (n + 1)
⊢ findGreatest P (n + 1) = n + 1

Tactic:
by simp [Nat.findGreatest, h]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : PartialOrder α
x y : WithBot α
⊢ x ≤ y → y ≤ x → x = y

Tactic:
by cases x <;> cases y <;> simp [le_def]; simpa using le_antisymm

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

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
⊢ StrictMono Int.cast

Tactic:
obtain ⟨h⟩ : NeZero (1 : α) := inferInstance
  refine strictMono_int_of_lt_succ fun n => (intCast_mono (Int.le_add_one (le_refl _))).lt_of_ne ?_
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ ↑a ≤ max ↑b ↑c ↔ a ≤ max b c

Tactic:
simp only [WithZero.coe_le_coe, le_max_iff]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
ha : 0 ≤ a
⊢ ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1

Tactic:
rw [← le_floor_iff ha, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt ha, Nat.lt_add_one_iff,
    le_antisymm_iff, and_comm]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
x y z : WithBot α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
cases x <;> cases y <;> cases z <;> simp [← coe_inf, ← coe_sup]

Goal state after:
case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝² a✝¹ a✝ : α
⊢ (a✝² ⊔ a✝¹) ⊓ (a✝² ⊔ a✝) ≤ a✝² ⊔ a✝¹ ⊓ a✝
Module: Mathlib.Order.Directed

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
i j k : ι
hi : f i ≤ f k
hj : f j ≤ f k
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e j)) (extend e f ⊥ z)

Tactic:
use e k

Goal state after:
case h
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
i j k : ι
hi : f i ≤ f k
hj : f j ≤ f k
⊢ (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ (e k)) ∧
    (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e j)) (extend e f ⊥ (e k))
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
⊢ Subsingleton (FloorSemiring R)

Tactic:
refine ⟨fun H₁ H₂ => ?_⟩
  have : H₁.ceil = H₂.ceil := funext fun a => (H₁.gc_ceil.l_unique H₂.gc_ceil) fun n => rfl
  have : H₁.floor = H₂.floor := by
    ext a
    rcases lt_or_ge a 0 with h | h
    · rw [H₁.floor_of_neg, H₂.floor_of_neg] <;> exact h
    · refine eq_of_forall_le_iff fun n => ?_
      rw [H₁.gc_floor, H₂.gc_floor] <;> exact h
  cases H₁
  cases H₂
  congr

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ 1 = 2 + ⅟b * a + ⅟a * b ↔ -2 + 1 = -2 + (2 + ⅟b * a + ⅟a * b)

Tactic:
add_right_inj

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ 1 = 2 + ⅟b * a + ⅟a * b ↔ 1 = 2 + ⅟b * a + ⅟a * b
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
c a b : K
hc : c ≠ 0
⊢ (a + b / c) * c = a * c + b

Tactic:
right_distrib,

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
c a b : K
hc : c ≠ 0
⊢ a * c + b / c * c = a * c + b
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: case pos
K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℕ
h : a = 0
⊢ a ^ (↑n + 1) = a ^ ↑n * a

pp: case neg
K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℕ
h : ¬a = 0
⊢ a ^ (↑n + 1) = a ^ ↑n * a

Tactic:
· rw [← Int.natCast_add_one, zpow_natCast, zpow_natCast, pow_succ]

Goal state after:
case neg
K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℕ
h : ¬a = 0
⊢ a ^ (↑n + 1) = a ^ ↑n * a
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : Preorder α
⊢ a ≤ b ↔ a ≤ b ∧ ¬b ≤ a ∨ AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b

Tactic:
AntisymmRel

Goal state after:
α : Type u_1
a b : α
inst✝ : Preorder α
⊢ a ≤ b ↔ a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case pos.refine_1
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ⊆ Ioc a b

pp: case pos.refine_2
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ Ioc a b ⊆ s

Tactic:
· rw [← Icc_sdiff_left]
      exact subset_sdiff_singleton hc ha

Goal state after:
case pos.refine_2
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ Ioc a b ⊆ s
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Preorder β
f g : α ↪o β
⊢ range ⇑f = range ⇑g ↔ f = g

Tactic:
by
  rw [f.strictMono.range_inj g.strictMono, DFunLike.coe_fn_eq]

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeInf α
a b : α
⊢ Iic a ∩ Iic b = Iic (a ⊓ b)

Tactic:
by
  ext x
  simp [Iic]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
a : α
b : β
hs : s.Nonempty
ht : t.Nonempty
ha : IsLUB s a
hb : IsLUB t b
⊢ IsLUB (s ×ˢ t) (a, b)

Tactic:
by simp_all +contextual [IsLUB, IsLeast, lowerBounds]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ a < b / c ↔ b < c * a

Tactic:
rw [mul_comm, lt_div_iff_of_neg hc]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a

Tactic:
rw [← one_div, div_le_iff_of_neg ha, ← div_eq_inv_mul, div_le_iff_of_neg hb, one_mul]

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ a / b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
by
  simp [division_def, mul_nonpos_iff]

Goal state after: