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

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

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

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

Goal state before:
pp: case refine_2.inl
α : Type u_1
inst✝ : Preorder α
s t : Set α
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hts : IsCofinalFor t s
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
⊢ ∃ z ∈ s ∪ t, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z

Tactic:
obtain ⟨x', hx', hxx'⟩ := hts.union_right hx

Goal state after:
case refine_2.inl
α : Type u_1
inst✝ : Preorder α
s t : Set α
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hts : IsCofinalFor t s
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
x' : α
hx' : x' ∈ s
hxx' : x ≤ x'
⊢ ∃ z ∈ s ∪ t, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
⊢ Icc a b = Icc c d ↔ a = c ∧ b = d

Tactic:
refine ⟨fun heq ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
heq : Icc a b = Icc c d
⊢ a = c ∧ b = d
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Ioo x y)
a : α
ha : a ∈ Ioo x y
⊢ ∃ b, b < ⟨a, ha⟩

Tactic:
rcases exists_between ha.1 with ⟨b, hb₁, hb₂⟩

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Ioo x y)
a : α
ha : a ∈ Ioo x y
b : α
hb₁ : x < b
hb₂ : b < a
⊢ ∃ b, b < ⟨a, ha⟩
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Ioc x y)
a : α
ha : a ∈ Ioc x y
⊢ ∃ b, b < ⟨a, ha⟩

Tactic:
rcases exists_between ha.1 with ⟨b, hb₁, hb₂⟩

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Ioc x y)
a : α
ha : a ∈ Ioc x y
b : α
hb₁ : x < b
hb₂ : b < a
⊢ ∃ b, b < ⟨a, ha⟩
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: «$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$inst» : Semiring «$α»
«$na» «$nb» : ℕ
⊢ AddMonoidWithOne «$α»

Tactic:
apply AddCommMonoidWithOne.toAddMonoidWithOne

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
this : a⁻¹ < b⁻¹ ↔ a / b < 1
⊢ a⁻¹ < b⁻¹ ↔ b < a

Tactic:
div_lt_iff_of_neg hb,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
this : a⁻¹ < b⁻¹ ↔ 1 * b < a
⊢ a⁻¹ < b⁻¹ ↔ b < a
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : b < c
hab : a ≤ b
⊢ AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Icc a b)

Tactic:
exact sub_inv_antitoneOn_Iio.mono <| (Set.Icc_subset_Iio_iff hab).mpr ha

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 : α
hb : b < 0
⊢ a / b < 1 ↔ b < a

Tactic:
div_lt_iff_of_neg hb,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ 1 * b < a ↔ b < a
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case e'_3
α : Type u_1
inst✝¹ : DecidableEq α
P : α → Prop
inst✝ : DecidablePred P
l : List α
a x✝ : α
⊢ (decide ¬P x✝) = !decide (P x✝)

Tactic:
simp only [decide_not]

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

Goal state before:
pp: α : Type u
a b : α
l : List α
c : α
hc : c ∈ (a :: b :: l).getLast?
⊢ (a :: b :: l).dropLast ++ [c] = a :: b :: l

Tactic:
getLast?_cons_cons

Goal state after:
α : Type u
a b : α
l : List α
c : α
hc : c ∈ (b :: l).getLast?
⊢ (a :: b :: l).dropLast ++ [c] = a :: b :: l
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
f₁ f₂ L : M
HL : L ≠ 0
⊢ (L * f₁ = L * f₂) = (f₁ = f₂)

Tactic:
mul_right_inj' HL

Goal state after:
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
f₁ f₂ L : M
HL : L ≠ 0
⊢ (f₁ = f₂) = (f₁ = f₂)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
l : List α
a : α
f : α → M
hf : ∀ (a' : α), a' ≠ a → a' ∈ l → f a' = 1
⊢ (map f l).prod = f a ^ count a l

Tactic:
induction l generalizing a with

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

Goal state before:
pp: α : Type u
β : Type v
f g : α → β → α
a : α
l : List β
H : ∀ (a : α) (b : β), b ∈ l → f a b = g a b
⊢ foldl f a l = foldl g a l

Tactic:
induction l generalizing a with

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

Goal state before:
pp: G : Type u_7
inst✝ : DivInvMonoid G
a b : G
l : List G
⊢ (a :: b :: l).alternatingProd = a / b * l.alternatingProd

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_7
inst✝ : DivInvMonoid G
a b : G
l : List G
⊢ (a :: b :: l).alternatingProd = a * b⁻¹ * l.alternatingProd
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ (a :: l).alternatingProd = a / l.alternatingProd

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ (a :: l).alternatingProd = a * l.alternatingProd⁻¹
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
p : α → Bool
⊢ map (fun a ↦ ↑a) (filter (fun x ↦ p ↑x) l.attach) = map (fun x ↦ ↑(Subtype.map id ⋯ x)) (filter p l).attach

Tactic:
Subtype.map,

Goal state after:
α : Type u
l : List α
p : α → Bool
⊢ map (fun a ↦ ↑a) (filter (fun x ↦ p ↑x) l.attach) = map (fun x ↦ id ↑x) (filter p l).attach
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ n /. x / (d /. x) = n /. d

Tactic:
div_eq_mul_inv,

Goal state after:
x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ n /. x * (d /. x)⁻¹ = n /. d
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ x /. n / (x /. d) = d /. n

Tactic:
div_eq_mul_inv,

Goal state after:
x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ x /. n * (x /. d)⁻¹ = d /. n
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ divNat n₁ d₁ = divNat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁

Tactic:
← coe_inj

Goal state after:
n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ ↑(divNat n₁ d₁) = ↑(divNat n₂ d₂) ↔ n₁ * d₂ = n₂ * d₁
Module: Mathlib.Algebra.Group.Commute.Basic

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbd : Commute b d
hbc : Commute b⁻¹ c
⊢ a / b * (c / d) = a * c / (b * d)

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbd : Commute b d
hbc : Commute b⁻¹ c
⊢ a * b⁻¹ * (c * d⁻¹) = a * c * (b * d)⁻¹
Module: Mathlib.Algebra.Group.Commute.Basic

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbc : Commute b c
hbd : Commute b⁻¹ d
hcd : Commute c⁻¹ d
⊢ a / b / (c / d) = a / c / (b / d)

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbc : Commute b c
hbd : Commute b⁻¹ d
hcd : Commute c⁻¹ d
⊢ a * b⁻¹ * (c * d⁻¹)⁻¹ = a * c⁻¹ * (b * d⁻¹)⁻¹
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ p = q

pp: case hbd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ Commute ↑p.den ↑q.den

pp: case hb
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ ↑p.den ≠ 0

pp: case hd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ ↑q.den ≠ 0

Tactic:
on_goal 1 => rw [← p.num_div_den, ← q.num_div_den, div_eq_div_iff]

Goal state after:
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ↑p.num * ↑q.den = ↑q.num * ↑p.den

case hb
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ↑p.den ≠ 0

case hd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ↑q.den ≠ 0

case hbd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ Commute ↑p.den ↑q.den

case hb
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ ↑p.den ≠ 0

case hd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ ↑q.den ≠ 0
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
this : ↑a * ↑d = ↑n * ↑b
⊢ ↑a / ↑b =
    ↑{ num := n, den := d, den_nz := h, reduced := c }.num / ↑{ num := n, den := d, den_nz := h, reduced := c }.den

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
this : ↑a * ↑d = ↑n * ↑b
⊢ ↑a * (↑b)⁻¹ =
    ↑{ num := n, den := d, den_nz := h, reduced := c }.num / ↑{ num := n, den := d, den_nz := h, reduced := c }.den
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ≥0 M₀
inst✝ : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
h : ∀ (n : ℕ), f ↑n = g ↑n
r : ℚ≥0
⊢ f (↑r.num / ↑r.den) = g (↑r.num / ↑r.den)

Tactic:
div_eq_mul_inv,

Goal state after:
F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ≥0 M₀
inst✝ : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
h : ∀ (n : ℕ), f ↑n = g ↑n
r : ℚ≥0
⊢ f (↑r.num * (↑r.den)⁻¹) = g (↑r.num * (↑r.den)⁻¹)
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
h : ∀ (m : ℤ), f ↑m = g ↑m
r : ℚ
⊢ f (↑r.num / ↑r.den) = g (↑r.num / ↑r.den)

Tactic:
div_eq_mul_inv,

Goal state after:
F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
h : ∀ (m : ℤ), f ↑m = g ↑m
r : ℚ
⊢ f (↑r.num * (↑r.den)⁻¹) = g (↑r.num * (↑r.den)⁻¹)
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
⊢ (a ≠ b) = (1 / gcd * (bd * a') ≠ 1 / gcd * (ad * b'))

Tactic:
rw [eq_iff_iff, not_iff_not, cancel_factors_eq ha hb had hbd hgcd]

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

Goal state before:
pp: R : Type u
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : LE R
inst✝ : CanonicallyOrderedAdd R
⊢ MulRightMono R

Tactic:
refine ⟨fun a b c h => ?_⟩
  dsimp [swap]
  rcases exists_add_of_le h with ⟨c, rfl⟩
  rw [add_mul]
  apply self_le_add_right

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : Semifield α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ (a - b) / c = a / c - b / c

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u_1
inst✝⁵ : Semifield α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ (a - b) * c⁻¹ = a * c⁻¹ - b * c⁻¹
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
x : γ
s : (i : ι) → κ i → Set γ
⊢ x ∈ ⋂ i, ⋂ j, s i j ↔ ∀ (i : ι) (j : κ i), x ∈ s i j

Tactic:
by
  simp_rw [mem_iInter]

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

Goal state before:
pp: α : Type u_1
ι : Type u_12
t : Set ι
s : ι → Set α
H : Nonempty α
w : ⋃ i ∈ t, s i = ⊤
⊢ t.Nonempty

Tactic:
by
  obtain ⟨x, m, -⟩ := exists_set_mem_of_union_eq_top t s w H.some
  exact ⟨x, m⟩

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
s : ι → Set α
h_Union : (⋃ i, s i).Nonempty
⊢ Nonempty ι

Tactic:
obtain ⟨x, hx⟩ := h_Union
  exact ⟨Classical.choose <| mem_iUnion.mp hx⟩

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋃ i, ⋃ j, s i j) ∩ t = ⋃ i, ⋃ j, s i j ∩ t

Tactic:
by simp_rw [iUnion_inter]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : Frame α
a : α
f : ι → α
⊢ Disjoint a (⨆ i, f i) ↔ ∀ (i : ι), Disjoint a (f i)

Tactic:
by
  simpa only [disjoint_comm] using @iSup_disjoint_iff

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
a : α
⊢ (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ (b : α), b ∈ s → a ≠ b → r a b ∧ r b a

Tactic:
simp only [insert_eq, pairwise_union, pairwise_singleton, true_and, mem_singleton_iff, forall_eq]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
inst✝ : Std.Symm r
⊢ {a, b}.Pairwise r ↔ a ≠ b → r a b

Tactic:
simp [pairwise_insert_of_symm]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
inst✝ : Std.Symm r
⊢ {a, b}.Pairwise r ↔ a ≠ b → r a b

Tactic:
by
  simp [pairwise_insert_of_symm]

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Preorder α
ht : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun x ↦ x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun x ↦ x ∈ s) b
x : α
hx : x ∈ t
y : α
hyx : y ≤ x
hy : Maximal (fun x ↦ x ∈ s) y
⊢ x ∈ {x | Maximal (fun x ↦ x ∈ s) x}

Tactic:
← ht.eq (h y hy) hx hyx

Goal state after:
α : Type u_1
s t : Set α
inst✝ : Preorder α
ht : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun x ↦ x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun x ↦ x ∈ s) b
x : α
hx : x ∈ t
y : α
hyx : y ≤ x
hy : Maximal (fun x ↦ x ∈ s) y
⊢ y ∈ {x | Maximal (fun x ↦ x ∈ s) x}
Module: Mathlib.Algebra.Order.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : S}, f x < f y ↔ x < y
a : S
ha : 0 < a
b c : S
hbc : b < c
⊢ a * b < a * c

Tactic:
rw [← lt, mul, mul]; refine mul_lt_mul_of_pos_left (lt.2 hbc) ?_; rwa [← zero, lt]

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a : α
⊢ a⁺ᵐ / a⁻ᵐ = a

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a : α
⊢ a⁺ᵐ * a⁻ᵐ⁻¹ = a
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁺ᵐ * a⁻ᵐ = |a|ₘ

Tactic:
by
  rw [oneLePart_def, sup_mul, one_mul, leOnePart_def, mul_sup, mul_one, mul_inv_cancel, sup_assoc,
    ← sup_assoc a, sup_eq_right.2 le_sup_right]
  exact sup_eq_left.2 <| one_le_mabs a

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

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

Tactic:
rw [← Nat.add_assoc]
    apply Nat.le_of_lt
    apply add_factorial_succ_lt_factorial_add_succ
    assumption

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

Goal state before:
pp: n k : ℕ
⊢ n ! * ((n + 1).ascFactorial k * (n + 1 + k)) = (n + k + 1) * (n + k)!

Tactic:
← Nat.mul_assoc,

Goal state after:
n k : ℕ
⊢ n ! * (n + 1).ascFactorial k * (n + 1 + k) = (n + k + 1) * (n + k)!
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f (x / y) ≤ f x + f y

Tactic:
div_eq_mul_inv,

Goal state after:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f (x * y⁻¹) ≤ f x + f y
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
h : k.succ ≤ n.succ
⊢ (n - k)! * ((n + 1) * n.descFactorial k) = n.succ !

Tactic:
← Nat.mul_assoc,

Goal state after:
n k : ℕ
h : k.succ ≤ n.succ
⊢ (n - k)! * (n + 1) * n.descFactorial k = n.succ !
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case pos
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ (n - k - (m - k))! * ((n - k).descFactorial (m - k) * n.descFactorial k) = n !

Tactic:
← Nat.mul_assoc,

Goal state after:
case pos
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ (n - k - (m - k))! * (n - k).descFactorial (m - k) * n.descFactorial k = n !
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
p : ℚ
n : ℕ
⊢ ↑p.num ^ n / ↑p.den ^ n = (↑p.num / ↑p.den) ^ n

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
p : ℚ
n : ℕ
⊢ ↑p.num ^ n * (↑p.den ^ n)⁻¹ = (↑p.num / ↑p.den) ^ n
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
n : ℕ
⊢ ↑q.num ^ n / ↑q.den ^ n = (↑q.num / ↑q.den) ^ n

Tactic:
div_eq_mul_inv,

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
n : ℕ
⊢ ↑q.num ^ n * (↑q.den ^ n)⁻¹ = (↑q.num / ↑q.den) ^ n
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
⊢ k * (x - ↑⌊x⌋) = 1 ↔ ∃ n, k * x = k * ↑n + 1

Tactic:
mul_sub,

Goal state after:
R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
⊢ k * x - k * ↑⌊x⌋ = 1 ↔ ∃ n, k * x = k * ↑n + 1
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : ℚ
this : ↑(x + 1 / 2) = ↑x + 1 / 2
⊢ round ↑x = round x

Tactic:
rw [round_eq, round_eq, ← this, floor_cast]

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
a : R
inst✝ : IsOrderedRing R
ha : fract a ≠ 0
⊢ ↑⌈a⌉ = a + 1 - fract a

Tactic:
(or_iff_right ha).mp (fract_eq_zero_or_add_one_sub_ceil a)

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
a : R
inst✝ : IsOrderedRing R
ha : fract a ≠ 0
⊢ ↑⌈a⌉ = a + 1 - (a + 1 - ↑⌈a⌉)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
a : R
inst✝ : IsOrderedRing R
ha : fract a ≠ 0
⊢ ↑⌈a⌉ - a = 1 - fract a

Tactic:
(or_iff_right ha).mp (fract_eq_zero_or_add_one_sub_ceil a)

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
a : R
inst✝ : IsOrderedRing R
ha : fract a ≠ 0
⊢ ↑⌈a⌉ - a = 1 - (a + 1 - ↑⌈a⌉)
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
b : H
inst✝² : AddCommGroupWithOne G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H 1 b
f : F
n : ℤ
x : G
⊢ f (↑n + x) = f x + n • b

Tactic:
by
  rw [← map_zsmul_add, zsmul_one]

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

Goal state before:
pp: case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this : 0 < a - 1
⊢ ↑⌈(a - 1)⁻¹⌉ - ↑⌈(a - 1)⁻¹⌉ / a < 1

Tactic:
div_eq_mul_inv,

Goal state after:
case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this : 0 < a - 1
⊢ ↑⌈(a - 1)⁻¹⌉ - ↑⌈(a - 1)⁻¹⌉ * a⁻¹ < 1
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case refine_2
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : (y ^ n)⁻¹ ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ x ≤ y ^ n

Tactic:
inv_le_inv₀ (pow_pos ypos _) xpos

Goal state after:
case refine_2
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : x ≤ y ^ n
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ x ≤ y ^ n
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
g : G
p q : P
⊢ g * (p /ₛ q) = g / (q /ₛ p)

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
g : G
p q : P
⊢ g * (p /ₛ q) = g * (q /ₛ p)⁻¹
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
⊢ ↑⌈a⌉₊ = ↑⌈a⌉

Tactic:
rw [← Int.natCast_ceil_eq_ceil ha, Int.cast_natCast]

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

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
⊢ x < ↑(z + 1) / ↑n ∧ ↑(z + 1) / ↑n < y

Tactic:
rw [div_lt_iff₀ n0']

Goal state after:
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
⊢ x < ↑(z + 1) / ↑n ∧ ↑(z + 1) < y * ↑n
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case bot
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
x : WithBot M
hxy : 0 < ⊥
⊢ ∃ n, x ≤ n • ⊥

Tactic:
exact absurd hxy bot_le.not_gt

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₃ /ₛ p₂) / (p₃ /ₛ p₁) = p₁ /ₛ p₂

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₃ /ₛ p₂) * (p₃ /ₛ p₁)⁻¹ = p₁ /ₛ p₂
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
a : α
s : Multiset α
h : ¬a ∈ t
⊢ (s + t).erase a = s.erase a + t

Tactic:
by
  rw [Multiset.add_comm, erase_add_right_neg s h, Multiset.add_comm]

Goal state after:
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ ⟦l₁⟧ - ⟦l₂⟧ = foldl erase ⟦l₁⟧ ⟦l₂⟧

Tactic:
change ofList (l₁.diff l₂) = foldl erase l₁ l₂

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ ↑(l₁.diff l₂) = foldl erase ↑l₁ ↑l₂