mathlib-initiative/mathlib-tactics huggingface dataset:
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⁻¹
⊢ a * b = c

Tactic:
by
  rwa [← eq_mul_inv_iff_mul_eq₀]; rintro rfl; simp [ha] at h

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

Goal state before:
pp: case negSucc
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f (-1 * (↑x + 1)) = g (-1 * (↑x + 1))

Tactic:
f.map_mul,

Goal state after:
case negSucc
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f (-1) * f (↑x + 1) = g (-1 * (↑x + 1))
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
f✝ : S✝ → R
hf✝ : Injective f✝
inst✝²⁰ : Add S✝
inst✝¹⁹ : Mul S✝
inst✝¹⁸ : Zero S✝
inst✝¹⁷ : One S✝
inst✝¹⁶ : Neg S✝
inst✝¹⁵ : Sub S✝
inst✝¹⁴ : SMul ℕ S✝
inst✝¹³ : SMul ℤ S✝
inst✝¹² : Pow S✝ ℕ
inst✝¹¹ : NatCast S✝
inst✝¹⁰ : IntCast S✝
S : Type ?u.36
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Add S
inst✝⁶ : SMul ℕ S
inst✝⁵ : Neg S
inst✝⁴ : Sub S
inst✝³ : SMul ℤ S
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddGroupWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
neg : ∀ (x : S), f (-x) = -f x
sub : ∀ (x y : S), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ f ↑↑n = f ↑n

Tactic:
rw [natCast, intCast, Int.cast_natCast]

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

Goal state before:
pp: R : Type u_5
inst✝ : NonAssocRing R
m : ℤ
⊢ m • 1 = ↑m

Tactic:
by
  rw [zsmul_eq_mul, mul_one]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
⊢ Even n → ∀ (a : α), (-a) ^ n = a ^ n

Tactic:
by
  rintro ⟨c, rfl⟩ a
  simp_rw [← two_mul, pow_mul, neg_sq]

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

Goal state before:
pp: R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
⊢ ↑n = 0 ∨ ↑n = 1

Tactic:
obtain hn | hn := Nat.even_or_odd n

Goal state after:
case inl
R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
hn : Even n
⊢ ↑n = 0 ∨ ↑n = 1

case inr
R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
hn : Odd n
⊢ ↑n = 0 ∨ ↑n = 1
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this✝ : MulLeftMono α
this : MulRightMono α
⊢ a * b ≤ c * d ∧ c * d ≤ a * b ↔ a = c ∧ b = d

Tactic:
eq_true (mul_le_mul' hac hbd),

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this✝ : MulLeftMono α
this : MulRightMono α
⊢ True ∧ c * d ≤ a * b ↔ a = c ∧ b = d
Module: Mathlib.Algebra.Order.Monoid.Defs

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : Preorder α
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c
a b : α
h : a ≤ b
c : α
⊢ c + a ≤ c + b

Tactic:
by
    rw [add_comm c, add_comm c]; exact add_le_add_left a b h c

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₀
ha₀ : 0 < a
ha₁ : a < 1
⊢ StrictAnti fun n ↦ a ^ n

Tactic:
refine strictAnti_int_of_succ_lt fun n ↦ ?_
  rw [zpow_add_one₀ ha₀.ne']
  exact mul_lt_of_lt_one_right (zpow_pos ha₀ _) ha₁

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

Goal state before:
pp: case mp
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
a : R
⊢ 0 < a * a → a ≠ 0

pp: case mpr
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
a : R
⊢ a ≠ 0 → 0 < a * a

Tactic:
· rintro h rfl
    rw [mul_zero] at h
    exact h.false

Goal state after:
case mpr
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
a : R
⊢ a ≠ 0 → 0 < a * a
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
a d : R
inst✝¹ : PosMulMono R
inst✝ : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
ba : b * a ≤ max d b * max c a
cd : c * d ≤ max a c * max b d
⊢ d * c ≤ max a c * max d b

Tactic:
simpa [mul_comm, max_comm] using cd

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

Goal state before:
pp: G₀ : Type u_3
inst✝¹ : CommGroupWithZero G₀
inst✝ : Preorder G₀
a b c : G₀
h : 0 ≤ a / b
⊢ c * a / (c * b) ≤ a / b

Tactic:
obtain rfl | hc := eq_or_ne c 0
  · simpa
  · rw [mul_div_mul_left _ _ hc]

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

Goal state before:
pp: G₀ : Type u_3
inst✝¹ : CommGroupWithZero G₀
inst✝ : Preorder G₀
a b c : G₀
h : a / b ≤ 0
⊢ a / b ≤ c * a / (c * b)

Tactic:
obtain rfl | hc := eq_or_ne c 0
  · simpa
  · rw [mul_div_mul_left _ _ hc]

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

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ 0 ≤ (x - a) * (x - b) ↔ x ≤ a ∨ b ≤ x

Tactic:
by
  rw [mul_nonneg_iff, sub_nonneg, sub_nonneg, sub_nonpos, sub_nonpos,
    and_iff_right_of_imp h.trans, and_iff_left_of_imp h.trans', or_comm]

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

Goal state before:
pp: case e'_2
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LE α
inst✝² : LE β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ b = f (EquivLike.inv f b)

Tactic:
exact (EquivLike.right_inv f _).symm

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

Goal state before:
pp: this : ∀ (a : ℤ) (n : ℕ), |a / ↑n| ≤ |a|
a b : ℤ
n : ℕ
⊢ |a / -↑n| ≤ |a|

Tactic:
rw [Int.ediv_neg, abs_neg]

Goal state after:
this : ∀ (a : ℤ) (n : ℕ), |a / ↑n| ≤ |a|
a b : ℤ
n : ℕ
⊢ |a / ↑n| ≤ |a|
Module: Mathlib.Algebra.GroupWithZero.Regular

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

Tactic:
conv_lhs => rw [← zero_mul b]
  exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha]⟩

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x✝ y✝ z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
x y z : WithTop α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) x y) ((fun x1 x2 ↦ x1 + x2) x z)

Tactic:
by
    cases x <;> cases y <;> cases z <;> simp [← coe_add]; simpa using fun _ ↦ by gcongr

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Ring

Goal state before:
pp: case inl
α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
h : m ≤ n
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
rw [Nat.sub_eq_zero_of_le h, cast_zero, tsub_eq_zero_of_le]

Goal state after:
case inl
α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
h : m ≤ n
⊢ ↑m ≤ ↑n
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x✝ y✝ z✝ : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
x y z : WithBot α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) x y) ((fun x1 x2 ↦ x1 + x2) x z)

Tactic:
by
    cases x <;> cases y <;> cases z <;> simp [← coe_add]; simpa using fun _ ↦ by gcongr

Goal state after:
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 : WithBot α
a✝ : α
⊢ map (⇑f) (↑a✝ + b) = map ⇑f ↑a✝ + map (⇑f) b

Tactic:
· induction b
    · exact (add_bot _).symm
    · rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]
      rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
z : α
hlt : z < unzero hx
⊢ ∃ y, y ≠ 0 ∧ y < x

Tactic:
rw [← WithZero.coe_lt_coe, WithZero.coe_unzero hx] at hlt

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
x : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
z : α
hlt : ↑z < x
⊢ ∃ y, y ≠ 0 ∧ y < x
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a : R
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊

Tactic:
· exact cast_le.1 ((floor_le ha).trans <| le_ceil _)

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ ↑(-x) * ↑(-y) = ↑x * ↑y

Tactic:
by
  rw [← val_mulLeft, ← val_mulLeft, ← AddUnits.ext_iff, ← neg_inj, ← y.neg_mulLeft, neg_neg]
  apply AddUnits.ext
  simp [neg_mul_eq_mul_neg]

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)
⊢ -2 + 1 = ⅟b * a + ⅟a * b ↔ -1 + 0 = ⅟b * a + ⅟a * b

Tactic:
rw [← one_add_one_eq_two, neg_add, add_assoc, neg_add_cancel]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Semigroup α
inst✝² : Semigroup β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f✝ : F
a b : α
f : α ≃* β := ↑f✝
h : f✝ a ∣ f✝ b
⊢ f.invFun (f.toFun a) ∣ b

Tactic:
← f.left_inv b

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Semigroup α
inst✝² : Semigroup β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f✝ : F
a b : α
f : α ≃* β := ↑f✝
h : f✝ a ∣ f✝ b
⊢ f.invFun (f.toFun a) ∣ f.invFun (f.toFun b)
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: u : ℤˣ
⊢ (↑u).natAbs * (↑u⁻¹).natAbs = 1

Tactic:
rw [← natAbs_mul, Units.mul_inv]

Goal state after:
u : ℤˣ
⊢ natAbs 1 = 1
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case inl
v : ℤ
h : 1 * v = -1
⊢ 1 = 1 ∧ v = -1 ∨ 1 = -1 ∧ v = 1

pp: case inr
v : ℤ
h : -1 * v = -1
⊢ -1 = 1 ∧ v = -1 ∨ -1 = -1 ∧ v = 1

Tactic:
· exact Or.inl ⟨rfl, one_mul v ▸ h⟩

Goal state after:
case inr
v : ℤ
h : -1 * v = -1
⊢ -1 = 1 ∧ v = -1 ∨ -1 = -1 ∧ v = 1
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f₂ a ≤ f₂ b

Tactic:
← h ha,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f₁ a ≤ f₂ b
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f₂ a < f₂ b

Tactic:
← h ha,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f₁ a < f₂ b
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
⊢ image2 f' (g' '' s) ((fun b ↦ b) '' t) = image2 f' (g' '' s) t

Tactic:
rw [image_id']

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

Goal state before:
pp: α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
⊢ image2 f' ((fun a ↦ a) '' s) (g' '' t) = image2 f' s (g' '' t)

Tactic:
rw [image_id']

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

Goal state before:
pp: α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
⊢ image2 f' (g' '' t) ((fun a ↦ a) '' s) = image2 f' (g' '' t) s

Tactic:
rw [image_id']

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
⊢ image2 f' ((fun b ↦ b) '' t) (g' '' s) = image2 f' t (g' '' s)

Tactic:
rw [image_id']

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
a : α
s : Set α
hf : StrictMono f
⊢ IsLeast (f '' s) (f a) ↔ IsLeast s a

Tactic:
by
  simp [IsLeast, hf.injective.eq_iff, hf.mem_lowerBounds_image]

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
wf : WellFounded (Function.swap r)
inst✝ : Nonempty α
h : Relator.LeftTotal r
a : α
ha : ∀ (x : α), x ∈ Set.univ → ¬Function.swap r x a
⊢ False

Tactic:
obtain ⟨b, hab⟩ := h a

Goal state after:
α : Type u_1
r : α → α → Prop
wf : WellFounded (Function.swap r)
inst✝ : Nonempty α
h : Relator.LeftTotal r
a : α
ha : ∀ (x : α), x ∈ Set.univ → ¬Function.swap r x a
b : α
hab : r a b
⊢ False
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a < b
⊢ Ico a b \ Ioo a b = {a}

Tactic:
by
  rw [← Ico_sdiff_left, sdiff_sdiff_cancel_left (singleton_subset_iff.2 <| left_mem_Ico.2 h)]

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

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

Tactic:
insert_eq_of_mem hb

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

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

Tactic:
insert_eq_of_mem hb

Goal state after:
case pos.refine_2
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioc 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
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Preorder β
f g : α ≃o β
⊢ univ = range ⇑g

Tactic:
range_eq

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Preorder β
f g : α ≃o β
⊢ univ = univ
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: case inl
γ : Type u_3
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_eq_i : j = i
⊢ j = i ∨ Iio i = Iic j

Tactic:
exact Or.inl hj_eq_i

Goal state after:
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝² : Ring A
inst✝¹ : PartialOrder A
inst✝ : IsStrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ e ≠ 0

Tactic:
rw [NormNum.IsInt.neg_to_eq h rfl]
  simp only [ne_eq, neg_eq_zero]
  apply ne_of_gt
  simpa using! w

Goal state after:
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝² : Ring A
inst✝¹ : LinearOrder A
inst✝ : IsStrictOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
⊢ 0 < e

Tactic:
have pos_invOf_d : (0 < ⅟(d : A)) := pos_invOf_of_invertible_cast d

Goal state after:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝² : Ring A
inst✝¹ : LinearOrder A
inst✝ : IsStrictOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
pos_invOf_d : 0 < ⅟↑d
⊢ 0 < e
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝² : Ring A
inst✝¹ : LinearOrder A
inst✝ : IsStrictOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n < 0) = true
⊢ e ≠ 0

Tactic:
have pos_invOf_d : (0 < ⅟(d : A)) := pos_invOf_of_invertible_cast d

Goal state after:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝² : Ring A
inst✝¹ : LinearOrder A
inst✝ : IsStrictOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n < 0) = true
pos_invOf_d : 0 < ⅟↑d
⊢ e ≠ 0
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ (na.mul ↑db).add (-(nb * ↑da)) = (↑k).mul nc

Tactic:
exact h₁

Goal state after:
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) = (a✝, b✝) ∨ (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
h₁ : R x y
⊢ R x y

Tactic:
exact h₁

Goal state after:
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a₁✝¹ : α
l₁✝¹ : List α
hbc : Rₐ a₁✝¹ head✝
tbc : SublistForall₂ Rₐ l₁✝¹ tail✝
a₁✝ : α
l₁✝ : List α
hab : Rₐ a₁✝ a₁✝¹
tab : SublistForall₂ Rₐ l₁✝ l₁✝¹
⊢ SublistForall₂ Rₐ (a₁✝ :: l₁✝) (head✝ :: tail✝)

Tactic:
exact SublistForall₂.cons (_root_.trans hab hbc) (ih _ _ tab tbc)

Goal state after:
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ -↑(↑x✝¹ + 1) * x✝ = -(↑↑x✝¹.succ * x✝)

Tactic:
Rat.neg_mul

Goal state after:
q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ -(↑(↑x✝¹ + 1) * x✝) = -(↑↑x✝¹.succ * x✝)
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
h : q ≠ 0
⊢ q * q⁻¹ = 1

Tactic:
by ext; simp [h]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
⊢ x * 1 = x * (d * e)

Tactic:
conv =>
            lhs
            rw [he, hdx]
            simp [mul_assoc]

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case left
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ (↑c / ↑d).num = c

Tactic:
num_div_eq_of_coprime hd0 h2

Goal state after:
case left
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ c = c
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
⊢ (⨆ i, if h : p i then f i h else g i h) = ⨆ x, (⨆ (h : p x), f x h) ⊔ ⨆ (h : ¬p x), g x h

Tactic:
congr 1 with i

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
⊢ (if h : p i then f i h else g i h) = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ (⋂₀ S)ᶜᶜ = (⋃₀ (compl '' S))ᶜ

Tactic:
compl_sInter

Goal state after:
α : Type u_1
S : Set (Set α)
⊢ (⋃₀ (compl '' S))ᶜ = (⋃₀ (compl '' S))ᶜ
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
a b c : α
h : (fun b ↦ [[b, a]]) b = (fun b ↦ [[b, a]]) c
⊢ b = c

Tactic:
rw [Set.ext_iff] at h
  exact eq_of_mem_uIcc_of_mem_uIcc ((h _).1 left_mem_uIcc) ((h _).2 left_mem_uIcc)

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ univ.Pairwise r ↔ Pairwise r

Tactic:
by
  simp only [Set.Pairwise, Pairwise, mem_univ, forall_const]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : PartialOrder A
inst✝ : IsConcreteLE A B
p q : A
⊢ p ≤ q ∧ ¬q ≤ p ↔ p ≤ q ∧ ∃ x, x ∈ q ∧ ¬x ∈ p

Tactic:
not_le_iff_exists

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : PartialOrder A
inst✝ : IsConcreteLE A B
p q : A
⊢ (p ≤ q ∧ ∃ x, x ∈ q ∧ ¬x ∈ p) ↔ p ≤ q ∧ ∃ x, x ∈ q ∧ ¬x ∈ p
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: i n : ℕ
h✝ : 1 < 2
⊢ 1 + (n + 1)! ≤ (1 + n) * (1 + n)! + (1 + n)!

Tactic:
Nat.add_comm 1 n,

Goal state after:
i n : ℕ
h✝ : 1 < 2
⊢ 1 + (n + 1)! ≤ (n + 1) * (n + 1)! + (n + 1)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n.descFactorial (k + 1) ≤ n ^ (k + 1)

Tactic:
rw [descFactorial_succ, Nat.pow_succ, Nat.mul_comm _ n]
    exact Nat.mul_le_mul (Nat.sub_le _ _) (descFactorial_le_pow _ k)

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : 2 ≤ k + 2
⊢ n.descFactorial (k + 1) * (n - (k + 1)) < n ^ (k + 1) * n

Tactic:
exact Nat.mul_lt_mul_of_le_of_lt (descFactorial_le_pow _ _) (by lia) (Nat.pow_pos <| by lia)

Goal state after:
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
n : ℤ
⊢ ↑(↑n)⁻¹ = (↑n)⁻¹

Tactic:
rcases n with n | n
  · simp [cast_inv_nat]
  · simp only [Int.cast_negSucc, cast_neg, inv_neg, cast_inv_nat]

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

Goal state before:
pp: case mp
k m : ℕ+
h : ↑m % ↑k = 0
⊢ m.mod k = k

Tactic:
apply PNat.eq

Goal state after:
case mp
k m : ℕ+
h : ↑m % ↑k = 0
⊢ ↑(m.mod k) = ↑k
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: m k : ℕ+
h : k ∣ m
⊢ k * m.divExact k = m

Tactic:
apply PNat.eq

Goal state after:
m k : ℕ+
h : k ∣ m
⊢ ↑(k * m.divExact k) = ↑m
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
z a : ℤ
⊢ a ≤ ⌊↑z⌋ ↔ a ≤ z

Tactic:
by rw [le_floor, Int.cast_le]

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
ha : Surjective fun x ↦ 1 ^ x
⊢ False

Tactic:
rcases exists_ne (1 : α) with ⟨b, hb⟩
    simpa [hb.symm] using ha b

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
m : ℤ
⊢ fract (a + ↑m) = fract a

Tactic:
fract

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
m : ℤ
⊢ a + ↑m - ↑⌊a + ↑m⌋ = fract a
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
m : ℕ
⊢ fract (a + ↑m) = fract a

Tactic:
fract

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
m : ℕ
⊢ a + ↑m - ↑⌊a + ↑m⌋ = fract a