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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hab : a ∣ b
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a ∣ b ^ (n + 1)

Tactic:
rw [pow_succ']

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hab : a ∣ b
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a ∣ b * b ^ n
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
p₁ : α → Prop
⊢ p₁ ∈ l → ∀ (j : α → Prop), j ∈ l → ((∀ (a : α), p₁ a) ↔ ∀ (a : α), j a)

Tactic:
hp₁

Goal state after:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
p₁ : α → Prop
hp₁ : p₁ ∈ l
⊢ ∀ (j : α → Prop), j ∈ l → ((∀ (a : α), p₁ a) ↔ ∀ (a : α), j a)
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
p₁ : α → Prop
⊢ p₁ ∈ l → ∀ (j : α → Prop), j ∈ l → ((∃ a, p₁ a) ↔ ∃ a, j a)

Tactic:
hp₁

Goal state after:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
p₁ : α → Prop
hp₁ : p₁ ∈ l
⊢ ∀ (j : α → Prop), j ∈ l → ((∃ a, p₁ a) ↔ ∃ a, j a)
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
f₁ f₂ : α →ₙ+* β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ (g.comp f₂) x = g (f₂ x)

Tactic:
comp_apply

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
f₁ f₂ : α →ₙ+* β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ g (f₂ x) = g (f₂ x)
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
g : β →+* γ
f₁ f₂ : α →+* β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ (g.comp f₂) x = g (f₂ x)

Tactic:
comp_apply

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
g : β →+* γ
f₁ f₂ : α →+* β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ g (f₂ x) = g (f₂ x)
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
ha : a ≠ 0
h : a = c * b⁻¹
⊢ b ≠ 0

Tactic:
rintro rfl

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a c : G₀
ha : a ≠ 0
h : a = c * 0⁻¹
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
h : b = a⁻¹ * c
⊢ a ≠ 0

Tactic:
rintro rfl

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
b c : G₀
hb : b ≠ 0
h : b = 0⁻¹ * c
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
h : n < m
⊢ 0 ^ (m - n) = 0 ^ m * (0 ^ n)⁻¹

Tactic:
rw [zero_pow (Nat.ne_of_gt <| Nat.sub_pos_of_lt h), zero_pow (by lia), zero_mul]

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

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

Tactic:
push_cast

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ ↑u * ↑u = 1 ↔ ↑u = 1 ∨ ↑u = -1
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

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

Tactic:
rintro rfl

Goal state after:
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 : N
bc : μ a b < μ a b
⊢ False
Module: Mathlib.Algebra.Ring.Parity

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

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

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

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a - (b + c) = a - c - b

Tactic:
by
  rw [add_comm]
  apply tsub_add_eq_tsub_tsub

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

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a - b < c
⊢ a ≠ b + c

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c : α
hb : AddLECancellable b
h : b + c - b < c
⊢ False
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : a - c < b
⊢ a ≠ b + c

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c : α
hc : AddLECancellable c
h : b + c - c < b
⊢ False
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : a + c < b
⊢ a ≠ b - c

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c : α
hc : AddLECancellable c
h : b - c + c < b
⊢ False
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:

Tactic:
a - b = a + d - d - b := by rw [add_tsub_cancel_right]
           _ = c + b - b - d := by rw [h, tsub_right_comm]
           _ = c - d := by rw [add_tsub_cancel_right]

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

Goal state before:
pp: α : Type u_1
inst✝³ : LE α
inst✝² : MulOneClass α
inst✝¹ : IsMulCommutative α
inst✝ : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ a ≤ b * a ↔ 1 ≤ b

Tactic:
by
  rw [mul_comm', ha.le_mul_iff_one_le_right]

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

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝² : MulZeroClass α
a✝ b✝ c✝ d : α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLE α
a : α>0
b c : α
h : ↑a * b < ↑a * c
⊢ b ≠ c

Tactic:
rintro rfl

Goal state after:
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝² : MulZeroClass α
a✝ b✝ c d : α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLE α
a : α>0
b : α
h : ↑a * b < ↑a * b
⊢ False
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝² : MulZeroClass α
a✝ b✝ c✝ d : α
inst✝¹ : PartialOrder α
inst✝ : MulPosReflectLE α
a : α>0
b c : α
h : b * ↑a < c * ↑a
⊢ b ≠ c

Tactic:
rintro rfl

Goal state after:
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝² : MulZeroClass α
a✝ b✝ c d : α
inst✝¹ : PartialOrder α
inst✝ : MulPosReflectLE α
a : α>0
b : α
h : b * ↑a < b * ↑a
⊢ False
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁵ : MulZeroClass α
a b c d : α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulReflectLE α
inst✝² : MulPosReflectLE α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
ha : 0 < a
hc : 0 < c
hab : a ≤ b
hcd : c ≤ d
h : b * d ≤ a * d
⊢ b ≤ a

Tactic:
exact le_of_mul_le_mul_of_pos_right h <| hc.trans_le hcd

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

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
a : M₀
inst✝ : PosMulMono M₀
h₀ : 0 ≤ a
h₁ : a < 1
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a ^ (n + 1) < 1

Tactic:
rw [pow_succ']

Goal state after:
M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
a : M₀
inst✝ : PosMulMono M₀
h₀ : 0 ≤ a
h₁ : a < 1
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a * a ^ n < 1
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a : M₀
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
ha : 1 < a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 1 < a ^ (n + 1)

Tactic:
rw [pow_succ']

Goal state after:
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a : M₀
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
ha : 1 < a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 1 < a * a ^ n
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
a b : R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)

Tactic:
have := le_total a 0

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
a b : R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
this : a ≤ 0 ∨ 0 ≤ a
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosMono G₀
n : ℤ
hn : 0 < n
⊢ StrictMonoOn (fun a ↦ a ^ n) {a | 0 ≤ a}

Tactic:
by
  lift n to ℕ using hn.le; simpa using pow_left_strictMonoOn₀ (by lia)

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
⊢ b ^ 2 = b ^ 2 + a * (a + b)

Tactic:
by rw [← hab, mul_zero, add_zero]

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₀
hc : 0 < c
⊢ b / c ≤ a ↔ b ≤ c * a

Tactic:
by
  rw [div_le_iff₀ hc, mul_comm]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
a b : α
h : s ({ toFun := f, inj' := ⋯ } a) ({ toFun := f, inj' := ⋯ } b)
⊢ r a b

Tactic:
· refine Not.imp_symm (Std.Trichotomous.trichotomous a b · fun h' ↦ asymm (H _ _ h') h) ?_
    exact (irrefl _ <| · ▸ h)

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✝ : MulLeftMono M
a : M
h : a < 1
k : ℕ
hn : k.succ ≠ 0
⊢ a ^ k.succ < 1

Tactic:
rw [pow_succ']

Goal state after:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
h : a < 1
k : ℕ
hn : k.succ ≠ 0
⊢ a * a ^ k < 1
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
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
by
  obtain ab | ab := le_total a b
  · exact mabs_mul_eq_mul_mabs_le ab
  · simpa only [mul_comm, and_comm] using mabs_mul_eq_mul_mabs_le ab

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

Tactic:
rintro rfl

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ |a / a|ₘ ≤ 1
Module: Mathlib.Data.Nat.Cast.NeZero

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
h : NeZero ↑n
⊢ n ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
h : NeZero ↑0
⊢ False
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case H1
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    ↑b % ↑a = ↑x * s + ↑y * t →
      ↑a = ↑x * s' + ↑y * t' →
        ↑((b % a).xgcdAux s t a s' t').1 =
          ↑x * ((b % a).xgcdAux s t a s' t').2.1 + ↑y * ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : ↑a = ↑x * s + ↑y * t
p' : ↑b = ↑x * s' + ↑y * t'
k : ℤ
⊢ ↑x * s' + ↑y * t' - (↑x * s * k + ↑y * t * k) = ↑x * s' + (↑y * t' - ↑y * (k * t)) - ↑x * (k * s)

Tactic:
mul_comm k t,

Goal state after:
case H1
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    ↑b % ↑a = ↑x * s + ↑y * t →
      ↑a = ↑x * s' + ↑y * t' →
        ↑((b % a).xgcdAux s t a s' t').1 =
          ↑x * ((b % a).xgcdAux s t a s' t').2.1 + ↑y * ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : ↑a = ↑x * s + ↑y * t
p' : ↑b = ↑x * s' + ↑y * t'
k : ℤ
⊢ ↑x * s' + ↑y * t' - (↑x * s * k + ↑y * t * k) = ↑x * s' + (↑y * t' - ↑y * (t * k)) - ↑x * (k * s)
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝² : MulOneClass α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedMul α
a b : α
h : a < b
c : α
hc : b = a * c
⊢ c ≠ 1

Tactic:
rintro rfl

Goal state after:
α : Type u
inst✝² : MulOneClass α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedMul α
a b : α
h : a < b
hc : b = a * 1
⊢ False
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
c : α
⊢ b = a * c → (a ≠ b ↔ 1 < c)

Tactic:
rintro rfl

Goal state after:
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ a ≠ a * c ↔ 1 < c
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: case mp
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ c = 1 → a = a * c

Tactic:
rintro rfl

Goal state after:
case mp
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
⊢ a = a * 1
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝¹ : MulZeroClass R
a : R
inst✝ : Nontrivial R
la : IsLeftRegular a
⊢ a ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
la : IsLeftRegular 0
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝¹ : MulZeroClass R
a : R
inst✝ : Nontrivial R
ra : IsRightRegular a
⊢ a ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
ra : IsRightRegular 0
⊢ False
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
h : a + b = 0
⊢ a ≠ ⊤

Tactic:
rintro rfl

Goal state after:
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b✝ c b : α
h : ⊤ + b = 0
⊢ False
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:
rintro rfl

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c : α
h : c ≤ a
h2 : a - c < a - c
⊢ False
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 : α
hc : AddLECancellable c
h : c ≤ b
⊢ a = b - c → a + c = b

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c : α
hc : AddLECancellable c
h : c ≤ b
⊢ b - c + c = 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 : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + c
⊢ a - b ≠ c

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + (a - b)
⊢ False
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 : α
hc : AddLECancellable c
h : c ≤ b
h' : a < b - c
⊢ a + c ≠ b

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c : α
hc : AddLECancellable c
h : c ≤ a + c
h' : a < a + c - c
⊢ False
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
ha : AddLECancellable a
h : a - b < a
⊢ b ≠ 0

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a : α
ha : AddLECancellable a
h : a - 0 < a
⊢ False
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
⊢ DenselyOrdered α ↔ Nontrivial αˣ ∧ DenselyOrdered αˣ

Tactic:
by
  refine ⟨fun H ↦ ⟨?_, ?_⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩
  · obtain ⟨x, hx, hx'⟩ := exists_between (zero_lt_one' α)
    exact ⟨Units.mk0 x hx.ne', 1, by simpa [Units.ext_iff] using hx'.ne⟩
  · refine ⟨fun x y h ↦ ?_⟩
    obtain ⟨z, hz⟩ := exists_between (Units.val_lt_val.mpr h)
    refine ⟨Units.mk0 z (ne_zero_of_lt hz.1), by simp [← Units.val_lt_val, hz]⟩
  · refine ⟨fun x y h ↦ ?_⟩
    lift y to αˣ using (ne_zero_of_lt h).isUnit
    obtain rfl | hx := eq_zero_or_pos x
    · obtain ⟨z, hz⟩ := exists_one_lt' (α := αˣ)
      exact ⟨(y * z⁻¹ : αˣ), by simp, Units.val_lt_val.mpr <| by simp [hz]⟩
    · lift x to αˣ using hx.ne'.isUnit
      obtain ⟨z, hz, hz'⟩ := H₂.dense x y (Units.val_lt_val.mpr h)
      exact ⟨z, by simp [hz, hz']⟩

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : NoBotOrder α
h : ∀ (b : α), x ≤ ↑b
y : α
⊢ ↑y ≠ x

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoBotOrder α
y : α
h : ∀ (b : α), ↑y ≤ ↑b
⊢ False
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case zero
P : ℕ → Prop
inst✝ : DecidablePred P
m : ℕ
⊢ m = 0 → (¬m = 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n = 0 → ¬P n

Tactic:
rintro rfl

Goal state after:
case zero
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ (¬0 = 0 → P 0) ∧ ∀ ⦃n : ℕ⦄, 0 < n → n = 0 → ¬P n
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case pos.mp
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ k + 1 = m → m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n

Tactic:
rintro rfl

Goal state after:
case pos.mp
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
hk : P (k + 1)
⊢ k + 1 ≤ k + 1 ∧ (k + 1 ≠ 0 → P (k + 1)) ∧ ∀ ⦃n : ℕ⦄, k + 1 < n → n ≤ k + 1 → ¬P n
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ⌈a⌉ < z ↔ a ≤ ↑z - 1

Tactic:
by rw [← le_sub_one_iff, ceil_le]; norm_cast

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
zero_le : ∀ (a : α), 0 ≤ a
⊢ IsOrderedAddMonoid (WithZero α)

Tactic:
have := WithZero.addLeftMono zero_le
  exact ⟨fun _ _ ↦ add_le_add_left, by simpa [add_comm] using fun _ _ ↦ add_le_add_left⟩

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
inst✝ : IsStrictOrderedRing R
ha : a ≤ 0
⊢ a = 0 → ⌊a⌋₊ = 0

Tactic:
rintro rfl

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ 0
⊢ ⌊0⌋₊ = 0
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

Tactic:
rw [eq_tsub_iff_add_eq_of_le (le_floor h), ← floor_add_natCast _, tsub_add_cancel_of_le h]

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ 0 ≤ a - ↑n
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
⊢ n ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
inst✝ : ExistsAddOfLE R
hn : Odd 0
⊢ False
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
⊢ n ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
hn : Odd 0
⊢ False
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ - b⁻¹ = (b - a) / (a * b)

Tactic:
by
  rw [inv_eq_one_div, inv_eq_one_div, div_sub_div _ _ ha hb, one_mul, mul_one]

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

Goal state before:
pp: case inr
α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
this : y ≤ x
⊢ ψ x ≤ ψ y

Tactic:
induction le_antisymm l this

Goal state after:
case inr.refl
α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : x ∈ s
l : x ≤ x
ψyx : ψ x ≤ ψ x
this : x ≤ x
⊢ ψ x ≤ ψ x
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
⊢ image2 f (s ∪ s') t = image2 f s t ∪ image2 f s' t

Tactic:
← image_prod,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
⊢ (fun x ↦ f x.1 x.2) '' (s ∪ s') ×ˢ t = (fun x ↦ f x.1 x.2) '' s ×ˢ t ∪ (fun x ↦ f x.1 x.2) '' s' ×ˢ t
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
a : α
⊢ image2 f (insert a s) t = (fun b ↦ f a b) '' t ∪ image2 f s t

Tactic:
insert_eq,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
a : α
⊢ image2 f ({a} ∪ s) t = (fun b ↦ f a b) '' t ∪ image2 f s t
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
b : β
⊢ image2 f s (insert b t) = (fun a ↦ f a b) '' s ∪ image2 f s t

Tactic:
insert_eq,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
b : β
⊢ image2 f s ({b} ∪ t) = (fun a ↦ f a b) '' s ∪ image2 f s t
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
b : β
⊢ image2 f s (insert b t) = (fun a ↦ f a b) '' s ∪ image2 f s t

Tactic:
by
  rw [insert_eq, image2_union_right, image2_singleton_right]

Goal state after: