mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
⊢ Nat.find hₘ + n = Nat.find hₙ

Tactic:
refine le_antisymm ((le_find_iff _ _).2 fun m hm hpm => Nat.not_le.2 hm ?_) ?_

Goal state after:
case refine_1
n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
m : ℕ
hm : m < Nat.find hₘ + n
hpm : p m
⊢ Nat.find hₘ + n ≤ m

case refine_2
n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
⊢ Nat.find hₙ ≤ Nat.find hₘ + n
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: m k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n

Tactic:
by
  induction k generalizing m with
  | zero =>
    rw [eq_comm, Iff.comm]
    simp only [Nat.le_zero, ne_eq, findGreatest_zero, and_iff_left_iff_imp]
    rintro rfl
    exact ⟨fun h ↦ (h rfl).elim, fun n hlt heq ↦ by lia⟩
  | succ k ihk =>
    by_cases hk : P (k + 1)
    · rw [findGreatest_eq hk]
      constructor
      · rintro rfl
        exact ⟨le_refl _, fun _ ↦ hk, fun n hlt hle ↦ by lia⟩
      · rintro ⟨hle, h0, hm⟩
        rcases Decidable.lt_or_eq_of_le hle with hlt | rfl
        exacts [(hm hlt (le_refl _) hk).elim, rfl]
    · rw [findGreatest_of_not hk, ihk]
      grind

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
⊢ 1 ≤ ⌈a⌉₊ ↔ 0 < a

Tactic:
← zero_add 1,

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
⊢ 0 + 1 ≤ ⌈a⌉₊ ↔ 0 < a
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
hn : n ≠ 0
⊢ ⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ ⌈a⌉₊ ≤ n

Tactic:
← not_le,

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
hn : n ≠ 0
⊢ ⌈a⌉₊ = n ↔ ¬a ≤ ↑(n - 1) ∧ ⌈a⌉₊ ≤ n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
⊢ Nat.cast ⁻¹' Ioc a b = Ioc ⌊a⌋₊ ⌊b⌋₊

Tactic:
by
  ext
  simp [floor_lt, le_floor_iff, hb, ha]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), ⊥ < ↑z → ⊥ ≤ ↑z) ↔ ⊥ ≤ ⊥

Tactic:
simp [exists_lt, forall_gt_imp_ge_iff_le_of_dense]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.coe
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ⊥ < ↑z → ↑a✝ ≤ ↑z) ↔ ↑a✝ ≤ ⊥

Tactic:
simp [exists_lt, forall_gt_imp_ge_iff_le_of_dense]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ↑a✝ < ↑z → ⊥ ≤ ↑z) ↔ ⊥ ≤ ↑a✝

Tactic:
simp [exists_lt, forall_gt_imp_ge_iff_le_of_dense]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝¹ a✝ : α
⊢ (∀ (z : α), ↑a✝¹ < ↑z → ↑a✝ ≤ ↑z) ↔ ↑a✝ ≤ ↑a✝¹

Tactic:
simp [exists_lt, forall_gt_imp_ge_iff_le_of_dense]

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

Goal state before:
pp: G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeInf G₀
inst✝ : MulPosReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
⊢ (a ⊓ b) * c = a * c ⊓ b * c

Tactic:
by
  obtain (rfl | hc) := hc.eq_or_lt
  · simp
  · exact (OrderIso.mulRight₀ c hc).map_inf a b

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: case inl
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
h : IsUnit (f 0)
t : G₀
ht : f t ≠ 1
this : 1 * f 0 = f t * f 0
⊢ f t = 1

Tactic:
exact (h.mul_right_cancel this).symm

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

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t

Tactic:
inter_comm,

Goal state after:
α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (t ∩ s) (s ∪ t) ⊆ image2 f s t
Module: Mathlib.Order.Bounds.Image

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

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

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ s ∩ t ∪ t \ s = t

Tactic:
inter_comm,

Goal state after:
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ t ∩ s ∪ t \ s = t
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
f : α → β
s : Set ↑(range f)
x : ↑(rangeSplitting f '' s)
⊢ (fun x ↦ ⟨rangeSplitting f ↑x, ⋯⟩) ((fun x ↦ ⟨⟨f ↑x, ⋯⟩, ⋯⟩) x) = x

Tactic:
rcases x with ⟨x, ⟨y, ⟨m, rfl⟩⟩⟩
    simp [apply_rangeSplitting f]

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

Goal state before:
pp: case pos
γ : Type u_3
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ∃ j ∈ upperBounds (Iio i), j < i
⊢ ∃ j, IsLUB (Iio i) j

Tactic:
obtain ⟨j, hj_ub, hj_lt_i⟩ := h_exists_lt
    exact ⟨j, hj_ub, fun k hk_ub => hk_ub hj_lt_i⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
⊢ b < a ↔ ∃ c ∈ s, b < c

Tactic:
← not_le,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
⊢ ¬a ≤ b ↔ ∃ c ∈ s, ¬c ≤ b
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
⊢ ¬a ≤ b ↔ ∃ c ∈ s, ¬c ≤ b

Tactic:
isLUB_le_iff h,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
⊢ b ∉ upperBounds s ↔ ∃ c ∈ s, ¬c ≤ b
Module: Mathlib.Tactic.Positivity.Core

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

Tactic:
eq

Goal state after:
A : Type u_1
e : A
n d : ℕ
inst✝² : Semiring A
inst✝¹ : LinearOrder A
inst✝ : IsStrictOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
pos_invOf_d : 0 < ⅟↑d
pos_n : 0 < ↑n
⊢ 0 < ↑n * ⅟↑d
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
pos_invOf_d : 0 < ⅟↑d
pos_n : 0 < ↑n
⊢ 0 < e

Tactic:
eq

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
pos_n : 0 < ↑n
⊢ 0 < ↑n * ⅟↑d
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
pos_invOf_d : 0 < ⅟↑d
neg_n : ↑n < 0
neg : ↑n * ⅟↑d < 0
⊢ e ≠ 0

Tactic:
eq

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
neg_n : ↑n < 0
neg : ↑n * ⅟↑d < 0
⊢ ↑n * ⅟↑d ≠ 0
Module: Mathlib.Data.List.Forall2

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

Tactic:
rw [zip, zipWith, mem_cons] at hx
    match hx with
    | Or.inl rfl => exact h₁
    | Or.inr h₃ => exact forall₂_zip h₂ h₃

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

Goal state before:
pp: case inr
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l.insertIdx n b
hn : l.length ≥ n
⊢ a = b ∨ a ∈ l

Tactic:
mem_insertIdx hn

Goal state after:
case inr
α : Type u
l : List α
n : ℕ
a b : α
h : a = b ∨ a ∈ l
hn : l.length ≥ n
⊢ a = b ∨ a ∈ l
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mp.cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
a : α
b : β
l1 : List α
l2 : List β
rab : R a b
a✝ : SublistForall₂ R l1 l2
ih : ∃ l, Forall₂ R l1 l ∧ l <+ l2
⊢ ∃ l, Forall₂ R (a :: l1) l ∧ l <+ b :: l2

Tactic:
obtain ⟨l, hl1, hl2⟩ := ih

Goal state after:
case mp.cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
a : α
b : β
l1 : List α
l2 : List β
rab : R a b
a✝ : SublistForall₂ R l1 l2
l : List β
hl1 : Forall₂ R l1 l
hl2 : l <+ l2
⊢ ∃ l, Forall₂ R (a :: l1) l ∧ l <+ b :: l2
Module: Mathlib.Data.List.Forall2

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

Tactic:
obtain ⟨l, hl1, hl2⟩ := ih

Goal state after:
case mp.cons_right
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
a✝¹ : β
l₁✝ : List α
l₂✝ : List β
a✝ : SublistForall₂ R l₁✝ l₂✝
l : List β
hl1 : Forall₂ R l₁✝ l
hl2 : l <+ l₂✝
⊢ ∃ l, Forall₂ R l₁✝ l ∧ l <+ a✝¹ :: l₂✝
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m ≤ l₁.length
hn : n ≤ l₂.length
a : α
⊢ a :: l₁ ~ a :: l₂ ↔ l₁ ~ l₂

Tactic:
perm_cons

Goal state after:
α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m ≤ l₁.length
hn : n ≤ l₂.length
a : α
⊢ l₁ ~ l₂ ↔ l₁ ~ l₂
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
a b c : α
⊢ a ∈ [b, c] ↔ a = b ∨ a = c

Tactic:
by
  rw [mem_cons, mem_singleton]

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

Goal state before:
pp: α : Type u
l : List α
a : α
⊢ l <+ [a] ↔ l = [] ∨ l = [a]

Tactic:
constructor <;> rintro (_ | _) <;> aesop

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

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ a /. b = 0 /. b ↔ a = 0

Tactic:
divInt_eq_divInt_iff b0 b0,

Goal state after:
a b : ℤ
b0 : b ≠ 0
⊢ a * b = 0 * b ↔ a = 0
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: ⊢ 1 ≠ 0

Tactic:
← divInt_one_one,

Goal state after:
⊢ 1 /. 1 ≠ 0
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: a : ℚ
ha : 0 ≤ a
⊢ 0 ≤ a⁻¹

Tactic:
by
  rw [inv_def]
  exact divInt_nonneg (Int.natCast_nonneg a.den) (num_nonneg.mpr ha)

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

Goal state before:
pp: case inr.refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ d = n / q.num * ↑q.den

Tactic:
refine Int.eq_mul_div_of_mul_eq_mul_of_dvd_left ?_ hqdn this

Goal state after:
case inr.refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ q.num ≠ 0
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case a
q₁ q₂ : ℚ
⊢ q₁.den.gcd q₂.den ∣ q₂.den

Tactic:
exact Nat.gcd_dvd_right _ _

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

Goal state before:
pp: n✝¹ num✝ n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsNNRat (NNRat.divNat ↑n✝¹ ↑n✝) num✝ denom✝

Tactic:
NNRat.divNat_eq_div

Goal state after:
n✝¹ num✝ n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsNNRat (↑↑n✝¹ / ↑↑n✝) num✝ denom✝
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : DivisionRing α
inst✝¹ : DivisionRing β
inst✝ : RingHomClass F α β
f : F
q : ℚ
⊢ f ↑q = ↑q

Tactic:
by rw [cast_def, map_div₀, map_intCast, map_natCast, cast_def]

Goal state after:
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 = g r

Tactic:
rw [← r.num_div_den, div_eq_mul_inv, map_mul, map_mul, h, eq_on_inv₀ f g]
    apply h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
⊢ ∀ (a b c : PUnit), a ≤ b ⇨ c ↔ min a b ≤ c

Tactic:
intros; trivial

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
⊢ ∀ (a : PUnit), a ⇨ ⊥ = aᶜ

Tactic:
intros; trivial

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
⊢ ∀ (a b c : PUnit), a \ b ≤ c ↔ a ≤ max b c

Tactic:
intros; trivial

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
⊢ ∀ (a : PUnit), ⊤ \ a = ￢a

Tactic:
intros; trivial

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

Goal state before:
pp: ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
⊢ ⋂ i ∈ s, t ∩ f i = t ∩ ⋂ i ∈ s, f i

Tactic:
inter_comm,

Goal state after:
ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
⊢ ⋂ i ∈ s, t ∩ f i = (⋂ i ∈ s, f i) ∩ t
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
a : α
s : Set α
⊢ ⨅ b ∈ s, a ⊔ b ≤
    ⨆ i,
      ⨅ j,
        match i, j with
        | { down := true }, j => a
        | { down := false }, j => ↑j

Tactic:
simp only [minAx.iSup_iInf_eq, iSup_ulift, iSup_bool_eq, le_iInf_iff]

Goal state after:
α : Type u
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
a : α
s : Set α
⊢ ∀
    (i :
      (i : ULift Bool) →
        match i with
        | { down := true } => PUnit
        | { down := false } => ↑s),
    ⨅ b ∈ s, a ⊔ b ≤ a ⊔ ↑(i { down := false })
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst✝⁸ : Max α
inst✝⁷ : Min α
inst✝⁶ : LE α
inst✝⁵ : LT α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : CompleteLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
x✝ : Set α
⊢ IsLUB ((fun {y} ↦ f y) '' x✝) (f (sSup x✝))

Tactic:
rw [map_sSup]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst✝⁸ : Max α
inst✝⁷ : Min α
inst✝⁶ : LE α
inst✝⁵ : LT α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : CompleteLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
x✝ : Set α
⊢ IsLUB ((fun {y} ↦ f y) '' x✝) (⨆ a ∈ x✝, f a)
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : Frame.MinimalAxioms β
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
a : α
s : Set α
⊢ ⨆ i ∈ s, f a ⊓ f i ≤ f (sSup (min a '' s))

Tactic:
simp_rw [← map_inf]

Goal state after:
α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : Frame.MinimalAxioms β
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
a : α
s : Set α
⊢ ⨆ i ∈ s, f (a ⊓ i) ≤ f (sSup (min a '' s))
Module: Mathlib.Tactic.NormNum.Abs

Goal state before:
pp: α : Type u_1
inst✝² : DivisionRing α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
num den : ℕ
ra : IsNNRat a num den
⊢ IsNNRat |a| num den

Tactic:
obtain ⟨ha1, rfl⟩ := ra

Goal state after:
α : Type u_1
inst✝² : DivisionRing α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible ↑den
⊢ IsNNRat |↑num * ⅟↑den| num den
Module: Mathlib.Tactic.NormNum.Abs

Goal state before:
pp: α : Type u_1
inst✝² : DivisionRing α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
num den : ℕ
ra : IsRat a (Int.negOfNat num) den
⊢ IsNNRat |a| num den

Tactic:
obtain ⟨ha1, rfl⟩ := ra

Goal state after:
α : Type u_1
inst✝² : DivisionRing α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible ↑den
⊢ IsNNRat |↑(Int.negOfNat num) * ⅟↑den| num den
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ ↑(p.num * q.den) < ↑(q.num * p.den)

pp: case hb
K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ 0 < ↑p.den

pp: case hd
K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ 0 < ↑q.den

Tactic:
Nat.cast_lt (α := K),

Goal state after:
K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ p.num * q.den < q.num * p.den

case hb
K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ 0 < ↑p.den

case hd
K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ 0 < ↑q.den
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
p : ℚ≥0
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑p ≤ OfNat.ofNat n ↔ p ≤ OfNat.ofNat n

Tactic:
by
  simp [← cast_le (K := K)]

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

Goal state before:
pp: K : Type u_5
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
p : ℚ≥0
n : ℕ
inst✝ : n.AtLeastTwo
⊢ OfNat.ofNat n ≤ ↑p ↔ OfNat.ofNat n ≤ p

Tactic:
by
  simp [← cast_le (K := K)]

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
c : M
hc : c ≠ 1
⊢ (mulSupport fun x ↦ c) = univ

Tactic:
ext x; simp [hc]

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h : decide (num✝¹ * ↑db < num✝ * ↑da) = true
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db

Tactic:
have h := Int.cast_strictMono (R := α) <| of_decide_eq_true h
    have ha : 0 < ⅟(da : α) := pos_invOf_of_invertible_cast da
    have hb : 0 < ⅟(db : α) := pos_invOf_of_invertible_cast db
    have h := (mul_lt_mul_of_pos_left · hb) <| mul_lt_mul_of_pos_right h ha
    rw [← mul_assoc, Int.commute_cast] at h
    simp? at h says simp only [Int.cast_mul, Int.cast_natCast, mul_invOf_cancel_right'] at h
    rwa [Int.commute_cast] at h

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

Goal state before:
pp: case inr
m n : ℕ
hm : 1 < m
⊢ n ! = m ! ↔ n = m

Tactic:
rw [eq_comm, factorial_inj hm, eq_comm]

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

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
q : ℚ≥0
⊢ ↑↑q = ↑q

Tactic:
Rat.cast_def,

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
q : ℚ≥0
⊢ ↑(↑q).num / ↑(↑q).den = ↑q
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
q : ℚ
h : 0 ≤ q
⊢ ↑⟨q, h⟩ = ↑q

Tactic:
by
  simp only [NNRat.cast_def, NNRat.num_mk, Nat.cast_natAbs, NNRat.den_mk, Rat.cast_def]
  rw [abs_of_nonneg (by simpa)]

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

Goal state before:
pp: K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : y < 1
y_pos : 0 < y
q : ℕ
hq : x⁻¹ < y⁻¹ ^ q
⊢ y ^ q < x

Tactic:
by rwa [inv_pow, inv_lt_inv₀ hx (pow_pos y_pos _)] at hq

Goal state after:
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
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 0 < n
⊢ R (f (l + 1 • a)) (f y)

Tactic:
have hy : R (f (l + n • a)) (f y) := by
        rw [← sub_add_cancel y (n • a), map_add_zsmul, map_add_zsmul]
        refine hR _ <| hf _ ?_ _ (Ioc_subset_Icc_self hny) hny.1; simpa

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 0 < n
hy : R (f (l + n • a)) (f y)
⊢ R (f (l + 1 • a)) (f y)
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: case mpr
α : Type u_1
l : List α
a : α
⊢ l = [] ∨ l = [a] → l <+~ [a]

Tactic:
rintro (rfl | rfl)

Goal state after:
case mpr.inl
α : Type u_1
a : α
⊢ [] <+~ [a]

case mpr.inr
α : Type u_1
a : α
⊢ [a] <+~ [a]
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_1
α : Type u_1
s : Multiset α
a : α
hs : s ⊂ {a}
b : α
hb : b ∈ s
⊢ {a} ⊆ s

Tactic:
obtain rfl := mem_singleton.1 (hs.1 hb)

Goal state after:
case refine_1
α : Type u_1
s : Multiset α
b : α
hb : b ∈ s
hs : s ⊂ {b}
⊢ {b} ⊆ s
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_2
α : Type u_1
s : Multiset α
a : α
⊢ s = 0 → s ⊂ {a}

Tactic:
rintro rfl
    simp

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

Goal state before:
pp: case nil
α : Type u
h : ∀ (a : α), ¬[a, a] <+ []
⊢ [].Nodup

pp: case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ (a : α), ¬[a, a] <+ tail✝) → tail✝.Nodup
h : ∀ (a : α), ¬[a, a] <+ head✝ :: tail✝
⊢ (head✝ :: tail✝).Nodup

Tactic:
· exact nodup_nil

Goal state after:
case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ (a : α), ¬[a, a] <+ tail✝) → tail✝.Nodup
h : ∀ (a : α), ¬[a, a] <+ head✝ :: tail✝
⊢ (head✝ :: tail✝).Nodup
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l.dedup
⊢ ∀ (b : α), b ∈ pwFilter (fun x1 x2 ↦ x1 ≠ x2) l → a ≠ b

Tactic:
simpa only [forall_mem_ne] using! h

Goal state after: