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

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

Tactic:
union_comm,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a < b
⊢ Ioo a b ∪ {a} = Ico a b
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : WellFoundedLT β
inst✝ : Preorder α
⊢ Subsingleton (α ≃o β)

Tactic:
refine ⟨fun f g ↦ ?_⟩
  change f.symm.symm = g.symm.symm
  rw [Subsingleton.elim f.symm]

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
h : Invertible ↑denom✝
⊢ -(↑num✝ * ⅟↑denom✝) = ↑num✝.neg * ⅟↑denom✝

Tactic:
rw [← neg_mul, ← Int.cast_neg]; rfl

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

Goal state before:
pp: case mp
α : Type u_1
a b : List α
⊢ Forall₂ (fun x1 x2 ↦ x1 = x2) a b → a = b

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
a b : List α
h : Forall₂ (fun x1 x2 ↦ x1 = x2) a b
⊢ a = b
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ : List β
h₁ : [].length = l₂.length
h₂ : ∀ {a : α} {b : β}, (a, b) ∈ [].zip l₂ → R a b
⊢ Forall₂ R [] l₂

Tactic:
cases length_eq_zero_iff.1 h₁.symm

Goal state after:
case nil.refl
α : Type u_1
β : Type u_2
R : α → β → Prop
h₁ : [].length = [].length
h₂ : ∀ {a : α} {b : β}, (a, b) ∈ [].zip [] → R a b
⊢ Forall₂ R [] []
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case cons.cons
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, l₁.length = l₂.length → (∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₁ : (a :: l₁).length = (b :: l₂).length
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1
⊢ Forall₂ R (a :: l₁) (b :: l₂)

Tactic:
simp only [length_cons, succ.injEq] at h₁

Goal state after:
case cons.cons
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, l₁.length = l₂.length → (∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1
h₁ : l₁.length = l₂.length
⊢ Forall₂ R (a :: l₁) (b :: l₂)
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : a * b < c
⊢ ∃ a' > a, a' * b < c

Tactic:
by
  rcases le_or_gt b 0 with hb | hb
  · obtain ⟨a', ha'⟩ := exists_gt a
    exact ⟨a', ha', hc.trans_le' (antitone_mul_right hb ha'.le)⟩
  · obtain ⟨a', ha', hc'⟩ := exists_between ((lt_div_iff₀ hb).2 hc)
    exact ⟨a', ha', (lt_div_iff₀ hb).1 hc'⟩

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
⊢ SublistForall₂ R l₁ l₂ → ∃ l, Forall₂ R l₁ l ∧ l <+ l₂

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : SublistForall₂ R l₁ l₂
⊢ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
⊢ (∃ l, Forall₂ R l₁ l ∧ l <+ l₂) → SublistForall₂ R l₁ l₂

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
⊢ SublistForall₂ R l₁ l₂
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case inl.inr.ha
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
⊢ ¬l₁ ~ l₂.insertIdx n a

Tactic:
intro h

Goal state after:
case inl.inr.ha
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
h : l₁ ~ l₂.insertIdx n a
⊢ False
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
⊢ Perm ∘r Perm = Perm

Tactic:
by
  funext a c; apply propext
  constructor
  · exact fun ⟨b, hab, hba⟩ => Perm.trans hab hba
  · exact fun h => ⟨a, Perm.refl a, h⟩

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

Goal state before:
pp: case mp
α : Type u
⊢ Injective length → Subsingleton α

Tactic:
intro h

Goal state after:
case mp
α : Type u
h : Injective length
⊢ Subsingleton α
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ → (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
h : (Forall₂ r ∘r Perm) l₁ l₃
⊢ (Perm ∘r Forall₂ r) l₁ l₃
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
x✝ : α
⊢ x✝ ∈ l → x✝ = b ∨ x✝ = a ↔ x✝ ≠ b → x✝ ≠ a → ¬x✝ ∈ l

Tactic:
rw [← and_imp, ← not_or, not_imp_not]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
L : List ι
f : ι → M
G : Type u_8
inst✝¹ : FunLike G M N
inst✝ : MonoidHomClass G M N
g : G
⊢ (map (⇑g ∘ f) L).prod = g (map f L).prod

Tactic:
rw [← prod_hom, map_map]

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

Goal state before:
pp: α : Type u
l : List α
a : α
⊢ (l ++ [a]).reverse = a :: l.reverse

Tactic:
by
  rw [reverse_append]; rfl

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

Goal state before:
pp: case cons.none
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
ha : f a = none
⊢ filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)

Tactic:
intro h

Goal state after:
case cons.none
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
ha : f a = none
h : filterMap f (a :: l) = map g (a :: l)
⊢ ∀ (x : α), x ∈ a :: l → f x = some (g x)
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q r : ℚ
⊢ q * r = mkRat (q.num * r.num) (q.den * r.den)

Tactic:
mul_def,

Goal state after:
q r : ℚ
⊢ normalize (q.num * r.num) (q.den * r.den) ⋯ = mkRat (q.num * r.num) (q.den * r.den)
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q a b c : ℚ
⊢ 1 ≠ 0

Tactic:
by decide

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

Goal state before:
pp: m e : ℕ
⊢ ¬false = true

Tactic:
by decide

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

Goal state before:
pp: a : ℤ
ha : a ≤ 0
b : ℕ
⊢ mkRat a b ≤ 0

Tactic:
obtain rfl | hb := eq_or_ne b 0
  · simp
  · exact (mkRat_nonpos_iff a hb).mpr ha

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

Goal state before:
pp: q : ℚ≥0
⊢ ↑q = ↑q.num / ↑(↑q).den

Tactic:
← Int.cast_natCast q.num,

Goal state after:
q : ℚ≥0
⊢ ↑q = ↑↑q.num / ↑(↑q).den
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by
    rw [← NNRat.den_coe, ← Int.cast_natCast q.num, ← NNRat.num_coe]; exact (num_div_den _).symm

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

Goal state before:
pp: p q : ℚ≥0
⊢ 1 ≠ 0

Tactic:
by decide

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

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a x y : G
⊢ SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x

Tactic:
simp_rw [SemiconjBy, ← mul_inv_rev, inv_inj, eq_comm]

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

Goal state before:
pp: q : ℚ≥0
⊢ ↑q * ↑↑(↑q).den = ↑q.num

Tactic:
← Int.cast_natCast q.num,

Goal state after:
q : ℚ≥0
⊢ ↑q * ↑↑(↑q).den = ↑↑q.num
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q r : ℚ≥0
⊢ q * r = divNat (q.num * r.num) (q.den * r.den)

Tactic:
ext; simp [Rat.mul_eq_mkRat, Rat.mkRat_eq_divInt, num_coe, den_coe]

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
⊢ a ^ n ∣ a ^ m → n ≤ m

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
⊢ n ≤ m
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (q₁ * q₂).den ∣ q₁.den * q₂.den

Tactic:
mul_def,

Goal state after:
q₁ q₂ : ℚ
⊢ (normalize (q₁.num * q₂.num) (q₁.den * q₂.den) ⋯).den ∣ q₁.den * q₂.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (q₁ * q₂).num = q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))

Tactic:
mul_def,

Goal state after:
q₁ q₂ : ℚ
⊢ (normalize (q₁.num * q₂.num) (q₁.den * q₂.den) ⋯).num =
    q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (q₁ * q₂).den = q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)

Tactic:
mul_def,

Goal state after:
q₁ q₂ : ℚ
⊢ (normalize (q₁.num * q₂.num) (q₁.den * q₂.den) ⋯).den =
    q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q * r) = ↑q * ↑r

Tactic:
mul_def,

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(divNat (q.num * r.num) (q.den * r.den)) = ↑q * ↑r
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * ⅟↑denom✝) = ↑num✝ * ⅟↑denom✝

Tactic:
simp only; norm_cast

Goal state after:
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionSemiring R
inst✝ : CharZero R
num✝ denom✝ : ℕ
qi : ℚ≥0
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * ⅟↑denom✝) = ↑num✝ * ⅟↑denom✝

Tactic:
simp only; norm_cast

Goal state after:
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * ⅟↑denom✝) = ↑num✝ * ⅟↑denom✝

Tactic:
simp only; norm_cast

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b₁ b₂ : R
h : IsNat (a₁ + b₁) 0
⊢ a₁ + a₂ + (b₁ + b₂) = a₂ + b₂

Tactic:
rw [add_add_add_comm, h.1, Nat.cast_zero, add_pf_zero_add]

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

Goal state before:
pp: β : Type u_2
ι : Type u_12
x : ι → β
t : ι → Set β
⊢ (⋃ i, t i) ∪ ⋃ i, {x i} = range x ∪ ⋃ i, t i

Tactic:
union_comm,

Goal state after:
β : Type u_2
ι : Type u_12
x : ι → β
t : ι → Set β
⊢ (⋃ i, t i) ∪ ⋃ i, {x i} = (⋃ i, t i) ∪ range x
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : ⋃ i, Es i = univ
Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
J : Set ι
x_in_U : ∃ i ∈ J, x ∈ Es i
⊢ i ∈ J

Tactic:
obtain ⟨j, j_in_J, hjx⟩ := x_in_U

Goal state after:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : ⋃ i, Es i = univ
Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
J : Set ι
j : ι
j_in_J : j ∈ J
hjx : x ∈ Es j
⊢ i ∈ J
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α → Set β
b : β
hb : b ∈ ⋃ i, t i
⊢ ∃ a, b ∈ t a

Tactic:
simpa using hb

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
⊢ sInf (f '' Icc a b) = f a

Tactic:
refine IsGLB.csInf_eq ?_ ((nonempty_Icc.mpr hab).image f)
  refine isGLB_iff_le_iff.mpr (fun b' ↦ ⟨?_, ?_⟩)
  · intro hb'
    rintro _ ⟨x, hx, rfl⟩
    exact hb'.trans <| h' (left_mem_Icc.mpr hab) hx hx.1
  · exact fun hb' ↦ hb' ⟨a, by simp [hab]⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
a b : α
h : b ≤ a
⊢ [[a, b]] = Icc b a

Tactic:
by rw [uIcc, inf_eq_right.2 h, sup_eq_left.2 h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f a ⊓ f b) (f a ⊔ f b))

Tactic:
← hf.map_sup,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f a ⊓ f b) (f (max a b)))

case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ b ∈ [[a, b]]
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f a ⊓ f b) (f a ⊔ f b))

Tactic:
← hf.map_sup,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f (max a b)) (f a ⊔ f b))

case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ b ∈ [[a, b]]
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
⊢ (Disjoint on fun b ↦ (fun a ↦ f a b) '' s) x y

Tactic:
refine disjoint_iff_inf_le.mpr ?_
    rintro _ ⟨⟨a, ha, hab⟩, b, hb, rfl⟩
    exact h (congr_arg Prod.snd <| ht (mk_mem_prod ha hx) (mk_mem_prod hb hy) hab)

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬univ.Pairwise (Disjoint on f)
⊢ ∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
obtain ⟨i, _hi, j, _hj, h⟩ := exists_lt_mem_inter_of_not_pairwiseDisjoint h

Goal state after:
α : Type u_1
ι : Type u_4
inst✝ : LinearOrder ι
f : ι → Set α
h✝ : ¬univ.Pairwise (Disjoint on f)
i : ι
_hi : i ∈ univ
j : ι
_hj : j ∈ univ
h : i < j ∧ ∃ x, x ∈ f i ∩ f j
⊢ ∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α}, b ∈ [[a, c]] → a ≤ c → Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ Ι b a ∪ Ι b c = Ι a c

Tactic:
union_comm,

Goal state after:
case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α}, b ∈ [[a, c]] → a ≤ c → Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ Ι b c ∪ Ι b a = Ι a c
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
hf : Function.Injective f
h : ∀ (x y : α), s (f x) (f y) → r x y
c : Set β
hrc : IsChain s c
x✝ : α
ha : x✝ ∈ f ⁻¹' c
y✝ : α
hb : y✝ ∈ f ⁻¹' c
hne : x✝ ≠ y✝
⊢ r x✝ y✝ ∨ r y✝ x✝

Tactic:
have := hrc ha hb (fun h ↦ hne (hf h))

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
hf : Function.Injective f
h : ∀ (x y : α), s (f x) (f y) → r x y
c : Set β
hrc : IsChain s c
x✝ : α
ha : x✝ ∈ f ⁻¹' c
y✝ : α
hb : y✝ ∈ f ⁻¹' c
hne : x✝ ≠ y✝
this : (fun x y ↦ s x y ∨ s y x) (f x✝) (f y✝)
⊢ r x✝ y✝ ∨ r y✝ x✝
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
⊢ IsStrongAntichain r' (f '' s)

Tactic:
by
  rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ hab c
  obtain ⟨c, rfl⟩ := hf c
  exact (hs ha hb (ne_of_apply_ne _ hab) _).imp (mt <| h _ _) (mt <| h _ _)

Goal state after:
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✝² : IsOrderedRing 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
⊢ 0 ≤ 1

Tactic:
by simp only [← le, zero, one, zero_le_one]

Goal state after:
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
⊢ 0 < f a

Tactic:
rwa [← zero, lt]

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : InfSet α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddBelow t
⊢ sInf t = default

Tactic:
by
  simp [sInf, ht]

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

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
q : ℚ≥0
ha : 0 ≤ a
⊢ 0 ≤ q • a

Tactic:
rw [NNRat.smul_def]

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
q : ℚ≥0
ha : 0 ≤ a
⊢ 0 ≤ ↑q * a
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : { x // 0 ≤ x }
⊢ 0 ≤ q • ↑a

Tactic:
rw [NNRat.smul_def]

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : { x // 0 ≤ x }
⊢ 0 ≤ ↑q * ↑a
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : α
ha : 0 ≤ a
⊢ 0 ≤ q • a

Tactic:
rw [NNRat.smul_def]

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : α
ha : 0 ≤ a
⊢ 0 ≤ ↑q * a
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case mp
n : ℕ
⊢ n ! = 1 → n ≤ 1

Tactic:
intro h

Goal state after:
case mp
n : ℕ
h : n ! = 1
⊢ n ≤ 1
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ 2 ≤ 1 → (n + 1) ^ 1 < (n + 1).ascFactorial 1

Tactic:
by intro; contradiction

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

Goal state before:
pp: n : ℕ
⊢ 2 ≤ 1 → (n + 1).ascFactorial 1 < (n + 1) ^ 1

Tactic:
by intro; contradiction

Goal state after:
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✝² : Mul β
inst✝¹ : LE β
inst✝ : SubmultiplicativeHomClass F α β
f : F
a b c : α
⊢ f (a / c) ≤ f (a / b) * f (b / c)

Tactic:
simpa only [div_mul_div_cancel] using map_mul_le_mul f (a / b) (b / c)

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

Goal state before:
pp: n : ℕ
⊢ 2 ≤ 1 → 1 ≤ n → (n + 1 - 1) ^ 1 < n.descFactorial 1

Tactic:
by intro; contradiction

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ 2 ≤ 1 → n.descFactorial 1 < n ^ 1

Tactic:
by intro; contradiction

Goal state after:
Module: Mathlib.Tactic.NormNum.OfScientific

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
a✝ n✝ : ℕ
⊢ ↑(if false = true then NNRat.divNat (↑a✝) (10 ^ ↑n✝) else ↑(↑a✝ * 10 ^ ↑n✝)) = ↑(a✝ * 10 ^ n✝)

Tactic:
if_neg Bool.false_ne_true

Goal state after:
α : Type u_1
inst✝ : DivisionSemiring α
a✝ n✝ : ℕ
⊢ ↑↑(↑a✝ * 10 ^ ↑n✝) = ↑(a✝ * 10 ^ n✝)
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
h : 0 < 0
⊢ ¬0 < 0

Tactic:
by decide

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

Goal state before:
pp: case mp
k m : ℕ+
⊢ k ∣ m → ↑k ∣ ↑m

Tactic:
intro h

Goal state after:
case mp
k m : ℕ+
h : k ∣ m
⊢ ↑k ∣ ↑m
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case mpr
k m : ℕ+
⊢ ↑k ∣ ↑m → k ∣ m

Tactic:
intro h

Goal state after:
case mpr
k m : ℕ+
h : ↑k ∣ ↑m
⊢ k ∣ m
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: k m : ℕ+
⊢ k ∣ m ↔ m.mod k = k

Tactic:
dvd_iff

Goal state after:
k m : ℕ+
⊢ ↑k ∣ ↑m ↔ m.mod k = k
Module: Mathlib.Data.PNat.Basic

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

Tactic:
intro h

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

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

Tactic:
intro h

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

Goal state before:
pp: m n : ℕ+
⊢ n.mod m = m → m ≤ n

Tactic:
intro h

Goal state after:
m n : ℕ+
h : n.mod m = m
⊢ m ≤ n
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:
rw [le_floor, Int.cast_le]

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
n : ℕ
⊢ ⌊a - ↑n⌋ = ⌊a⌋ - ↑n

Tactic:
rw [← Int.cast_natCast, floor_sub_intCast]

Goal state after:
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
n : ℤ
hn : 0 < n
a : R
⊢ ⌊a * ↑n⌋ / n = ⌊a⌋

Tactic:
refine eq_of_forall_le_iff fun m ↦ ?_
  rw [Int.le_ediv_iff_mul_le hn, le_floor, le_floor, cast_mul,
    mul_le_mul_iff_of_pos_right (cast_pos.mpr hn)]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
⊢ ¬IsCyclic α

Tactic:
intro h

Goal state after:
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
⊢ False
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case mp
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
s : Set R
y : R
hy : y ∈ s
⊢ ∃ i, (∃ x ∈ s, x - ↑i = fract y) ∧ fract y ∈ Ico 0 1

Tactic:
exact ⟨⌊y⌋, ⟨y, hy, rfl⟩, fract_nonneg y, fract_lt_one y⟩

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑n * ⅟↑d⌋ = ↑(n / d)

Tactic:
simp only [invOf_eq_inv, ← div_eq_mul_inv]

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑n / ↑d⌋ = ↑(n / d)
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌈↑n * ⅟↑d⌉ = ↑(-(-↑n / ↑d)).toNat

Tactic:
simp only [invOf_eq_inv, ← div_eq_mul_inv]

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌈↑n / ↑d⌉ = ↑(-(-↑n / ↑d)).toNat