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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e₁ : α ≃ β
o₁ : ∀ {a b : α}, s (e₁ a) (e₁ b) ↔ r a b
e₂ : α ≃ β
map_rel_iff'✝ : ∀ {a b : α}, s (e₂ a) (e₂ b) ↔ r a b
h : { toEquiv := e₁, map_rel_iff' := o₁ }.toEquiv = { toEquiv := e₂, map_rel_iff' := map_rel_iff'✝ }.toEquiv
⊢ { toEquiv := e₁, map_rel_iff' := o₁ } = { toEquiv := e₂, map_rel_iff' := map_rel_iff'✝ }

Tactic:
congr

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

Goal state before:
pp: case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
h : { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun = { toFun := toFun✝, monotone' := monotone'✝ }.toFun
⊢ { toFun := toFun✝¹, monotone' := monotone'✝¹ } = { toFun := toFun✝, monotone' := monotone'✝ }

Tactic:
congr

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

Goal state before:
pp: X : Type u_6
Y : Type u_7
inst✝² : LinearOrder X
inst✝¹ : DenselyOrdered X
inst✝ : Preorder Y
f : X → Y
hf : StrictMono f
⊢ ∀ (a₁ a₂ : ↑(Set.range f)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
simpa [← exists_and_left, ← exists_and_right, exists_comm, hf.lt_iff_lt]
    using fun _ _ ↦ exists_between

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

Goal state before:
pp: X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered X
a b : Y
h : a < b
c : X
hc : EquivLike.inv f a < c ∧ c < EquivLike.inv f b
⊢ a < f c ∧ f c < b

Tactic:
by simpa using hc

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

Goal state before:
pp: X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
H : DenselyOrdered Y
a b : X
h : a < b
c : Y
hc : f a < c ∧ c < f b
⊢ a < EquivLike.inv f c ∧ EquivLike.inv f c < b

Tactic:
by simpa using hc

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
⊢ |b|ₘ / |a|ₘ ≤ |a / b|ₘ

Tactic:
mabs_div_comm

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
⊢ |b|ₘ / |a|ₘ ≤ |b / a|ₘ
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case right
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ |b|ₘ ≤ |a / b|ₘ * |a|ₘ

Tactic:
mabs_div_comm

Goal state after:
case right
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ |b|ₘ ≤ |b / a|ₘ * |a|ₘ
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ 1 ≤ a * |a|ₘ

Tactic:
by
  grw [← mul_inv_cancel a, inv_le_mabs a]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ ↑n < ↑1 ↔ n = 0

Tactic:
cast_lt,

Goal state after:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ n < 1 ↔ n = 0
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: case inr.inl
α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
hc : a ≤ c
⊢ min a (b * c) = min a (min a b * min a c)

pp: case inr.inr
α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
hc : c ≤ a
⊢ min a (b * c) = min a (min a b * min a c)

Tactic:
· simp [hc, le_mul_left]

Goal state after:
case inr.inr
α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
hc : c ≤ a
⊢ min a (b * c) = min a (min a b * min a c)
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular (a * b) ∧ IsRegular (b * a) ↔ IsRegular a ∧ IsRegular b

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular (a * b) ∧ IsRegular (b * a) → IsRegular a ∧ IsRegular b

case refine_2
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular a ∧ IsRegular b → IsRegular (a * b) ∧ IsRegular (b * a)
Module: Mathlib.Algebra.Order.AddGroupWithTop

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

Tactic:
simp [add_assoc, add_neg_cancel_of_ne_top, add_neg_cancel_left_of_ne_top, *]

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 : α
hab : AddLECancellable (a - b)
h : b ≤ a
⊢ a - c - (a - b) = b - c

Tactic:
tsub_right_comm,

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hab : AddLECancellable (a - b)
h : b ≤ a
⊢ a - (a - b) - c = b - c
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℤ
h : a < 0
⊢ ↑a ≤ -1

Tactic:
rw [← Int.cast_one, ← Int.cast_neg, cast_le]

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℤ
h : a < 0
⊢ a ≤ -1
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℤ
h : a < 0
⊢ a ≤ -1

Tactic:
exact Int.le_sub_one_of_lt h

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

Goal state before:
pp: k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ 0 < findGreatest P k ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n

Tactic:
rw [Nat.pos_iff_ne_zero, Ne, findGreatest_eq_zero_iff]; push Not; rfl

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

Goal state before:
pp: G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
x y : WithZero (Multiplicative G)
hx : x ≠ 0
hy : y ≠ 0
⊢ x.log ≤ y.log ↔ x ≤ y

Tactic:
by
  rw [log_le_iff_le_exp hx, exp_log hy]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
y : WithZero α
a b : α
hy : ↑b ≤ y
⊢ b ≤ unzeroD a y

Tactic:
have hne : y ≠ 0 := ne_bot_of_le_ne_bot WithZero.coe_ne_zero hy
  rwa [le_unzeroD_iff hne]

Goal state after:
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
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : b ≤ n
⊢ ↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n

Tactic:
· obtain ⟨d, rfl⟩ := exists_add_of_le hb
      rw [Nat.cast_add, add_left_comm _ b, add_left_comm _ (b : R)]
      refine iff_of_true ?_ le_self_add
      exact le_add_of_nonneg_right <| ha.trans <| le_add_of_nonneg_right d.cast_nonneg

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
a b : α
hab : a < b
c : α
hc : ↑a < ↑c ∧ ↑c < ↑b
⊢ a < c ∧ c < b

Tactic:
by simpa using hc

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a b✝ : α
x✝¹ x✝ : Invertible a
b : α
hba : b * a = 1
hab : a * b = 1
c : α
invOf_mul_self✝ : c * a = 1
hac : a * c = 1
⊢ { invOf := b, invOf_mul_self := hba, mul_invOf_self := hab } =
    { invOf := c, invOf_mul_self := invOf_mul_self✝, mul_invOf_self := hac }

Tactic:
congr

Goal state after:
α : Type u
inst✝ : Monoid α
a b✝ : α
x✝¹ x✝ : Invertible a
b : α
hba : b * a = 1
hab : a * b = 1
c : α
invOf_mul_self✝ : c * a = 1
hac : a * c = 1
⊢ b = c
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
a b : α
hab : a < b
c : α
hc : ↑a < ↑c ∧ ↑c < ↑b
⊢ a < c ∧ c < b

Tactic:
by simpa using hc

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
m : α
inst✝ : Invertible m
n : ℕ
⊢ m ^ n * ⅟m ^ n = 1

Tactic:
rw [← (commute_invOf m).mul_pow, mul_invOf_self, one_pow]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁴ : MulOneClass R
inst✝³ : Monoid S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
ifr : Invertible (f r)
⊢ f ⅟r = ⅟(f r)

Tactic:
by
  obtain rfl : ifr = Invertible.map f r := Subsingleton.elim _ _; rfl

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

Goal state before:
pp: case mk.mk
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
floor✝¹ ceil✝¹ : R → ℕ
floor_of_neg✝¹ : ∀ {a : R}, a < 0 → floor✝¹ a = 0
gc_floor✝¹ : ∀ {a : R} {n : ℕ}, 0 ≤ a → (n ≤ floor✝¹ a ↔ ↑n ≤ a)
gc_ceil✝¹ : GaloisConnection ceil✝¹ Nat.cast
floor✝ ceil✝ : R → ℕ
floor_of_neg✝ : ∀ {a : R}, a < 0 → floor✝ a = 0
gc_floor✝ : ∀ {a : R} {n : ℕ}, 0 ≤ a → (n ≤ floor✝ a ↔ ↑n ≤ a)
gc_ceil✝ : GaloisConnection ceil✝ Nat.cast
this✝ : FloorSemiring.ceil = FloorSemiring.ceil
this : FloorSemiring.floor = FloorSemiring.floor
⊢ { floor := floor✝¹, ceil := ceil✝¹, floor_of_neg := floor_of_neg✝¹, gc_floor := gc_floor✝¹, gc_ceil := gc_ceil✝¹ } =
    { floor := floor✝, ceil := ceil✝, floor_of_neg := floor_of_neg✝, gc_floor := gc_floor✝, gc_ceil := gc_ceil✝ }

Tactic:
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 = 1 + ⅟b * a + (⅟a * b + 1) ↔ 1 = 1 + ⅟b * a + (1 + ⅟a * b)

Tactic:
add_comm _ 1

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
a : α
n0 : n ≤ 0
⊢ |a ^ n|ₘ = |a|ₘ ^ |n|

Tactic:
obtain ⟨m, h⟩ := Int.eq_ofNat_of_zero_le (neg_nonneg.2 n0)

Goal state after:
case inr
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
a : α
n0 : n ≤ 0
m : ℕ
h : -n = ↑m
⊢ |a ^ n|ₘ = |a|ₘ ^ |n|
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
a b : α
⊢ |a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b

Tactic:
by
  rw [abs_mul_abs_self]
  simp only [mul_add, add_comm, add_left_comm, mul_comm, sub_eq_add_neg, mul_one, mul_neg,
    neg_add_rev, neg_neg, add_assoc]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n✝ : ℕ
inst✝ : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
⊢ |a| * |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ (n + 1)

Tactic:
rw [pow_succ, ← mul_assoc, mul_comm |a|]

Goal state after:
case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n✝ : ℕ
inst✝ : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
⊢ |geomSum a b n| * |a| ≤ (↑n + 1) * max |a| |b| ^ n * max |a| |b|
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Monotone f
⊢ ∀ ⦃x : α⦄, x ∈ s → ∃ x_1 ∈ t, f x ≤ f x_1

Tactic:
rintro a ha

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Monotone f
a : α
ha : a ∈ s
⊢ ∃ x ∈ t, f a ≤ f x
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Antitone f
⊢ ∀ ⦃x : α⦄, x ∈ s → ∃ x_1 ∈ t, f x_1 ≤ f x

Tactic:
rintro a ha

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Antitone f
a : α
ha : a ∈ s
⊢ ∃ x ∈ t, f x ≤ f a
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
⊢ IsLUB s f ↔ ∀ (a : α), IsLUB (eval a '' s) (f a)

Tactic:
by
  classical
    refine
      ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => ?_⟩, fun H =>
        ⟨?_, ?_⟩⟩
    · suffices h : Function.update f a b ∈ upperBounds s from Function.update_self a b f ▸ H.2 h a
      exact fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩
    · exact fun g hg a => (H a).1 (mem_image_of_mem _ hg)
    · exact fun g hg a => (H a).2 ((Function.monotone_eval a).mem_upperBounds_image hg)

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Sort u_1
a : α
r : α → α → Prop
h : ¬Acc r a
⊢ ∃ b, ¬Acc r b ∧ r b a

Tactic:
rw [acc_def] at h

Goal state after:
α : Sort u_1
a : α
r : α → α → Prop
h : ¬∀ (b : α), r b a → Acc r b
⊢ ∃ b, ¬Acc r b ∧ r b a
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : PartialOrder α
b : α
⊢ Icc b b = {b}

Tactic:
exact Icc_self _

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
x : α
hx : x ∈ s
⊢ ∀ y ∈ s, ∃ z ∈ s, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z

Tactic:
y

Goal state after:
α : Type u_1
inst✝ : Preorder α
s t : Set α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
x : α
hx : x ∈ s
y : α
⊢ y ∈ s → ∃ z ∈ s, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z
Module: Mathlib.Control.Functor

Goal state before:
pp: case refl
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
⊢ { map := m, mapConst := mc } = { map := m, mapConst := mc' }

Tactic:
congr

Goal state after:
case refl.e_mapConst
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
⊢ mc = mc'
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u
inst✝ : Semiring α
num✝ denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ ↑num✝ * ⅟↑denom✝ = ↑num✝ * ⅟↑denom✝

Tactic:
congr

Goal state after:
case e_a.e_5
α : Type u
inst✝ : Semiring α
num✝ denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ inv✝¹ = inv✝
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ ↑num✝ * ⅟↑denom✝ = ↑num✝ * ⅟↑denom✝

Tactic:
congr

Goal state after:
case e_a.e_5
α : Type u
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ inv✝¹ = inv✝
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
⊢ ∃ a' ∈ Set.Ico 0 a, c < a' * b

Tactic:
by
  have hb : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha
  obtain ⟨a', ha', a_a'⟩ := exists_between ((div_lt_iff₀ hb).2 h)
  exact ⟨a', ⟨(div_nonneg hc hb.le).trans ha'.le, a_a'⟩, (div_lt_iff₀ hb).1 ha'⟩

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

Goal state before:
pp: α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
ih : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝

Tactic:
congr

Goal state after:
case e_head
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
ih : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ head✝¹ = head✝

case e_tail
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
ih : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ tail✝¹ = tail✝
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
hn : n = 0
⊢ (if m + n = 0 then 0 else 0 ^ (m + n)) = if n = 0 then 0 else if m = 0 then 0 else 0 ^ m * 0 ^ n

Tactic:
simp +contextual [hn, zero_zpow]

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
hn : ¬n = 0
⊢ (if m + n = 0 then 0 else 0 ^ (m + n)) = if n = 0 then 0 else if m = 0 then 0 else 0 ^ m * 0 ^ n

Tactic:
simp +contextual [hn, zero_zpow]

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

Goal state before:
pp: α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ a :: ((b :: l).dropLast ++ [(b :: l).getLast ⋯]) = a :: b :: l

Tactic:
congr

Goal state after:
case e_tail
α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ (b :: l).dropLast ++ [(b :: l).getLast ⋯] = b :: l
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : Semiring M
X₁ X₂ a : M
⊢ a * X₁ + a * X₂ = a * (X₁ + X₂)

Tactic:
simp [mul_add]

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

Goal state before:
pp: d : ℕ
h : d ≠ 0
w : (Int.natAbs 0).Coprime d
⊢ { num := 0, den := d, den_nz := h, reduced := w } = 0

Tactic:
congr

Goal state after:
case e_den
d : ℕ
h : d ≠ 0
w : (Int.natAbs 0).Coprime d
⊢ d = 1
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: case pos
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : b = true
⊢ mkRat (↑(OfNat.ofNat m)) (10 ^ OfNat.ofNat d) = Rat.divInt ↑m ↑(10 ^ d)

Tactic:
congr

Goal state after:
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: case neg
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : ¬b = true
⊢ ↑(OfNat.ofNat m * 10 ^ OfNat.ofNat d) = ↑(m * 10 ^ d)

Tactic:
congr

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

Goal state before:
pp: p q✝ : ℚ≥0
n₁ n₂ d₁ d₂ : ℕ
C : ℚ≥0 → Sort u
q : ℚ≥0
H : (n d : ℕ) → d ≠ 0 → n.Coprime d → C (divNat n d)
⊢ C q

Tactic:
← q.num_divNat_den

Goal state after:
p q✝ : ℚ≥0
n₁ n₂ d₁ d₂ : ℕ
C : ℚ≥0 → Sort u
q : ℚ≥0
H : (n d : ℕ) → d ≠ 0 → n.Coprime d → C (divNat n d)
⊢ C (divNat q.num q.den)
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case right
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ ∃ x, ¬IsUnit x ∧ b = a * x

Tactic:
· rcases hd with ⟨c, rfl⟩
    refine ⟨c, ?_, rfl⟩
    rintro ⟨u, rfl⟩
    simp at hnd

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime y (x * z) ↔ IsRelPrime y z

Tactic:
isRelPrime_comm,

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime (x * z) y ↔ IsRelPrime y z
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a b : ℕ
⊢ ↑(divNat a b) = ↑(↑a / ↑b)

Tactic:
congr

Goal state after:
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a b : ℕ
⊢ divNat a b = ↑a / ↑b
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a : ℤ
b : ℕ
hb : ↑b ≠ 0
⊢ ↑(a /. ↑b) = ↑a / ↑b

Tactic:
cast_divInt_of_ne_zero,

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
a : ℤ
b : ℕ
hb : ↑b ≠ 0
⊢ ↑a / ↑↑b = ↑a / ↑b

case b0
α : Type u_3
inst✝ : DivisionRing α
a : ℤ
b : ℕ
hb : ↑b ≠ 0
⊢ ↑↑b ≠ 0
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(p.num * ↑q.den /. (↑p.den * q.num)) = ↑p / ↑q

Tactic:
cast_divInt_of_ne_zero,

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(p.num * ↑q.den) / ↑(↑p.den * q.num) = ↑p / ↑q

case b0
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(↑p.den * q.num) ≠ 0
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b x : R
e : ℕ
⊢ x ^ e * a + x ^ e * b = x ^ e * (a + b)

Tactic:
simp [mul_add]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst✝ : SupSet α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ sSup (range fun x ↦ g (f x)) = sSup (range fun y ↦ g y)

Tactic:
congr

Goal state after:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst✝ : SupSet α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ (range fun x ↦ g (f x)) = range fun y ↦ g y
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s t : Set β
⊢ ⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x

Tactic:
by
  simp_rw [mem_union, iSup_or, iSup_sup_eq]

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 [union_distrib_iInter_right]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Iic (⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, Iic (f i j)

Tactic:
Iic_iInf

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ uIoo a b = Ioo a b

Tactic:
uIoo,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ Ioo (min a b) (max a b) = Ioo a b
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ uIoo a b = Ioo b a

Tactic:
uIoo,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ Ioo (min a b) (max a b) = Ioo b a
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ uIoo a b = uIoo b a

Tactic:
uIoo,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioo (min a b) (max a b) = Ioo (min b a) (max b a)
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
⊢ ∀ y ∈ s, x ≤ y → Icc x y ⊆ s

Tactic:
y

Goal state after:
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
⊢ y ∈ s → x ≤ y → Icc x y ⊆ s
Module: Mathlib.Order.Antichain

Goal state before:
pp: case inr.inr
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r b a
⊢ a = b

Tactic:
exact h.eq' ha hb hab

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : α
hz : z ∈ Icc x y
⊢ z ∈ s

Tactic:
by
    obtain rfl := hs.eq hx hy (hz.1.trans hz.2)
    rw [Icc_self, mem_singleton_iff] at hz
    rwa [hz]

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
⊢ ∀ ⦃y : α⦄, y ∈ s → x = y

Tactic:
y

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
⊢ y ∈ s → x = y
Module: Mathlib.Order.Antichain

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hne : x ≠ y
h : r x y
⊢ False

Tactic:
exact ht hx hy hne h

Goal state after: