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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 < x2
a : { x // 0 ≤ x }
b c : α
h : (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ ↑x * y) a b) ((fun x y ↦ ↑x * y) a c)
ha : 0 = ↑a
⊢ b < c

pp: case inr
α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 < x2
a : { x // 0 ≤ x }
b c : α
h : (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ ↑x * y) a b) ((fun x y ↦ ↑x * y) a c)
ha : 0 < ↑a
⊢ b < c

Tactic:
· simp [← ha] at h

Goal state after:
case inr
α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 < x2
a : { x // 0 ≤ x }
b c : α
h : (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ ↑x * y) a b) ((fun x y ↦ ↑x * y) a c)
ha : 0 < ↑a
⊢ b < c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 < x2
a : { x // 0 ≤ x }
b c : α
h : (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ y * ↑x) a b) ((fun x y ↦ y * ↑x) a c)
ha : 0 = ↑a
⊢ b < c

pp: case inr
α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 < x2
a : { x // 0 ≤ x }
b c : α
h : (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ y * ↑x) a b) ((fun x y ↦ y * ↑x) a c)
ha : 0 < ↑a
⊢ b < c

Tactic:
· simp [← ha] at h

Goal state after:
case inr
α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 < x2
a : { x // 0 ≤ x }
b c : α
h : (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ y * ↑x) a b) ((fun x y ↦ y * ↑x) a c)
ha : 0 < ↑a
⊢ b < c
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: case inr.inr
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
a b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : a < 0
⊢ a * b < 0

Tactic:
· exact mul_neg_of_neg_of_pos ha (nab ha.le)

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a : G₀
ha : 0 < a
⊢ a⁻¹ < 1 ↔ 1 < a

Tactic:
simpa using inv_mul_lt_one₀ ha (b := 1)

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ (a ^ ↑(n + 1))⁻¹

Tactic:
inv_nonneg,

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ ↑(n + 1)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a ≤ 1
n : ℤ
⊢ a ^ n * a ≤ a ^ n

Tactic:
exact mul_le_of_le_one_right (zpow_nonneg ha₀.le _) ha₁

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a✝ b✝ : α
⊢ r ((Embedding.quotientOut α) ⟦a✝⟧) ((Embedding.quotientOut α) ⟦b✝⟧) ↔ Quotient.lift₂ r H ⟦a✝⟧ ⟦b✝⟧

Tactic:
apply iff_iff_eq.2 (H _ _ _ _ _ _) <;> apply Quotient.mk_out

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

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
⊢ ∀ {a b : α},
    { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
by
      intro a b
      apply le_iff_le_of_cmp_eq_cmp
      convert! (h a (f b)).symm
      apply gf

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

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ IsMax (f.symm (f x)) → IsMax (f x)

Tactic:
exact f.symm.strictMono.isMax_of_apply

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
⊢ |a / b|ₘ ≤ |a|ₘ * |b|ₘ

Tactic:
by
  rw [div_eq_mul_inv, ← mabs_inv b]
  exact mabs_mul_le a _

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

Goal state before:
pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : b ≤ d
⊢ |b / d|ₘ ≤ max (c / d) (d / a)

Tactic:
mabs_of_le_one <| div_le_one'.mpr h,

Goal state after:
case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : b ≤ d
⊢ (b / d)⁻¹ ≤ max (c / d) (d / a)
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : b ≤ d
⊢ d / b ≤ max (c / d) (d / a)

Tactic:
exact le_max_of_le_right <| div_le_div_left' hac _

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
⊢ |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ

Tactic:
apply le_of_mul_le_of_one_le_right _ (one_le_mabs _)

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
⊢ |?m.37|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftReflectLE α
⊢ AddCommMonoid α

Tactic:
by infer_instance

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

Goal state before:
pp: case neg.mp
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : a < b
h' : 0 ≤ c
⊢ a ≤ c + b

Tactic:
simpa using add_le_add h' h.le

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

Goal state before:
pp: case zero
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
b c : WithZero α
hbc : b ≤ c
⊢ 0 + b ≤ 0 + c

Tactic:
zero_add,

Goal state after:
case zero
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
b c : WithZero α
hbc : b ≤ c
⊢ b ≤ 0 + c
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
inst✝ : IsStrictOrderedRing R
⊢ 0 + 1 ≤ ⌊a⌋₊ ↔ 1 ≤ a

Tactic:
zero_add,

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
⊢ 1 ≤ ⌊a⌋₊ ↔ 1 ≤ 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
inst✝ : IsStrictOrderedRing R
⊢ ⌊a⌋₊ = 0 ↔ a < 1

Tactic:
by
  rw [← lt_one_iff, ← @cast_one R]
  exact floor_lt' Nat.one_ne_zero

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
⊢ ⌈a⌉₊ = 0 ↔ a ≤ 0

Tactic:
by rw [← Nat.le_zero, ceil_le, Nat.cast_zero]

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
⊢ Nat.cast ⁻¹' Ici a = Ici ⌈a⌉₊

Tactic:
by
  ext
  simp [ceil_le]

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

Goal state before:
pp: α : Type u
inst✝ : MulOneClass α
r : α
hr : Invertible r
s si : α
hs : s = r
hsi : si = ⅟r
⊢ s * si = 1

Tactic:
rw [hs, hsi, mul_invOf_self]

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:
by rw [← (commute_invOf m).mul_pow, mul_invOf_self, one_pow]

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

Goal state before:
pp: 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
hf : ∃ x, f x ≠ 1
a : G₀
h : IsUnit (f a)
⊢ IsUnit a

Tactic:
rcases eq_or_ne a 0 with (rfl | h)
    · obtain ⟨t, ht⟩ := hf
      refine (ht ?_).elim
      have := map_mul f t 0
      rw [← one_mul (f (t * 0)), mul_zero] at this
      exact (h.mul_right_cancel this).symm
    · exact ⟨⟨a, a⁻¹, mul_inv_cancel₀ h, inv_mul_cancel₀ h⟩, rfl⟩

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

Goal state before:
pp: R : Type u_3
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
a : R
ha : a < 0
⊢ 0 < a ^ 2

Tactic:
rw [sq]

Goal state after:
R : Type u_3
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
a : R
ha : a < 0
⊢ 0 < a * a
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a : ℤˣ
⊢ |↑↑a| = 1

Tactic:
by
  cases Int.units_eq_one_or a <;> simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ image2 f (image2 g s t) u = image2 g' (image2 f' s u) t

Tactic:
by
  rw [image2_swap g, image2_swap g']
  exact image2_assoc fun _ _ _ => h_right_comm _ _ _

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
⊢ Iic a \ Iio a = {a}

Tactic:
by
  rw [← Iic_sdiff_right, sdiff_sdiff_cancel_left (singleton_subset_iff.2 self_mem_Iic)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Preorder β
f g : α ≃o β
⊢ f.toOrderEmbedding = g.toOrderEmbedding

Tactic:
← OrderEmbedding.range_inj,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Preorder β
f g : α ≃o β
⊢ range ⇑f.toOrderEmbedding = range ⇑g.toOrderEmbedding
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
f : α → α → α
a b : α
na nb nc da db dc k : ℕ
⊢ f = HAdd.hAdd →
    IsNNRat a na da →
      IsNNRat b nb db → (na.mul db).add (nb.mul da) = k.mul nc → da.mul db = k.mul dc → IsNNRat (f a b) nc dc

Tactic:
rintro rfl ⟨_, rfl⟩ ⟨_, rfl⟩ (h₁ : na * db + nb * da = k * nc) (h₂ : da * db = k * dc)

Goal state after:
α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * db + nb * da = k * nc
h₂ : da * db = k * dc
⊢ IsNNRat (↑na * ⅟↑da + ↑nb * ⅟↑db) nc dc
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
⊢ f = HAdd.hAdd →
    IsRat a na da →
      IsRat b nb db → (na.mul ↑db).add (nb.mul ↑da) = (↑k).mul nc → da.mul db = k.mul dc → IsRat (f a b) nc dc

Tactic:
rintro rfl ⟨_, rfl⟩ ⟨_, rfl⟩ (h₁ : na * db + nb * da = k * nc) (h₂ : da * db = k * dc)

Goal state after:
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
⊢ IsRat (↑na * ⅟↑da + ↑nb * ⅟↑db) nc dc
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
⊢ a / 2 ≤ a ↔ 0 ≤ a

Tactic:
by
  rw [div_le_iff₀ (zero_lt_two' α), mul_two, le_add_iff_nonneg_left]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB ((fun a ↦ 0) '' s) 0

Tactic:
hs.nonempty.image_const

Goal state after:
case inr
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB {0} 0
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: case zero.nil
α : Type u
m : ℕ
⊢ dropSlice 0 m [] = take 0 [] ++ drop (0 + m) []

Tactic:
grind [dropSlice]

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

Goal state before:
pp: case zero.cons
α : Type u
m : ℕ
head✝ : α
tail✝ : List α
⊢ dropSlice 0 m (head✝ :: tail✝) = take 0 (head✝ :: tail✝) ++ drop (0 + m) (head✝ :: tail✝)

Tactic:
grind [dropSlice]

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

Goal state before:
pp: case succ.nil
α : Type u
m n✝ : ℕ
a✝ : ∀ (xs : List α), dropSlice n✝ m xs = take n✝ xs ++ drop (n✝ + m) xs
⊢ dropSlice (n✝ + 1) m [] = take (n✝ + 1) [] ++ drop (n✝ + 1 + m) []

Tactic:
grind [dropSlice]

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

Goal state before:
pp: case succ.cons
α : Type u
m n✝ : ℕ
a✝ : ∀ (xs : List α), dropSlice n✝ m xs = take n✝ xs ++ drop (n✝ + m) xs
head✝ : α
tail✝ : List α
⊢ dropSlice (n✝ + 1) m (head✝ :: tail✝) = take (n✝ + 1) (head✝ :: tail✝) ++ drop (n✝ + 1 + m) (head✝ :: tail✝)

Tactic:
grind [dropSlice]

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

Goal state before:
pp: case nil.zero
α : Type u
j : ℕ
⊢ (dropSlice 0 j []).length = [].length - min j ([].length - 0)

Tactic:
grind [dropSlice]

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

Goal state before:
pp: case nil.succ
α : Type u
j n✝ : ℕ
⊢ (dropSlice (n✝ + 1) j []).length = [].length - min j ([].length - (n✝ + 1))

Tactic:
grind [dropSlice]

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

Goal state before:
pp: case cons.zero
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (i j : ℕ), (dropSlice i j tail✝).length = tail✝.length - min j (tail✝.length - i)
j : ℕ
⊢ (dropSlice 0 j (head✝ :: tail✝)).length = (head✝ :: tail✝).length - min j ((head✝ :: tail✝).length - 0)

Tactic:
grind [dropSlice]

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

Goal state before:
pp: case cons.succ
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (i j : ℕ), (dropSlice i j tail✝).length = tail✝.length - min j (tail✝.length - i)
j n✝ : ℕ
⊢ (dropSlice (n✝ + 1) j (head✝ :: tail✝)).length = (head✝ :: tail✝).length - min j ((head✝ :: tail✝).length - (n✝ + 1))

Tactic:
grind [dropSlice]

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

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

Tactic:
constructor <;> intro h
  · induction h with
    | nil => exact ⟨nil, Forall₂.nil, nil_sublist _⟩
    | @cons a b l1 l2 rab _ ih =>
      obtain ⟨l, hl1, hl2⟩ := ih
      exact ⟨b :: l, Forall₂.cons rab hl1, hl2.cons_cons b⟩
    | cons_right _ ih =>
      obtain ⟨l, hl1, hl2⟩ := ih
      exact ⟨l, hl1, hl2.trans (Sublist.cons _ (Sublist.refl _))⟩
  · obtain ⟨l, hl1, hl2⟩ := h
    revert l₁
    induction hl2 with
    | slnil =>
      intro l₁ hl1
      rw [forall₂_nil_right_iff.1 hl1]
      exact SublistForall₂.nil
    | cons _ _ ih => intro l₁ hl1; exact SublistForall₂.cons_right (ih hl1)
    | cons_cons _ _ ih =>
      intro l₁ hl1
      obtain - | ⟨hr, hl⟩ := hl1
      exact SublistForall₂.cons hr (ih hl)

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

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
l : List α
h : l ≠ []
h' : l.head! ∈ l.head! :: l.tail
⊢ l.head! ∈ l

Tactic:
cons_head!_tail h

Goal state after:
α : Type u
inst✝ : Inhabited α
l : List α
h : l ≠ []
h' : l.head! ∈ l
⊢ l.head! ∈ l
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
l : List α
h : l ≠ []
⊢ l.head! ∈ l

Tactic:
by
  have h' : l.head! ∈ l.head! :: l.tail := mem_cons_self
  rwa [cons_head!_tail h] at h'

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

Goal state before:
pp: case refine_1
α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <+: l₂
a : α
h : a ∈ l₁
⊢ idxOf a l₂ < l₁.length

Tactic:
exact hl.idxOf_eq_of_mem h ▸ idxOf_lt_length_of_mem h

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β → β
b : β
hf : ∀ (a : α), f a b = b
a : α
l : List α
⊢ foldr f b (a :: l) = b

Tactic:
rw [foldr_cons, foldr_fixed' hf l, hf a]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Semiring α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : AddLeftMono α
inst✝ : PosMulMono α
⊢ MonoidWithZero { x // 0 ≤ x }

Tactic:
by infer_instance

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

Goal state before:
pp: α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
l : List α
⊢ foldrM f b l = foldr (fun a mb ↦ mb >>= f a) (pure b) l

Tactic:
by induction l <;> simp [*]

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

Goal state before:
pp: q a b c : ℚ
⊢ AddGroup ℚ

Tactic:
by infer_instance

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

Goal state before:
pp: q a b c : ℚ
⊢ AddCommMonoid ℚ

Tactic:
by infer_instance

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

Goal state before:
pp: q a b c : ℚ
⊢ AddMonoid ℚ

Tactic:
by infer_instance

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

Goal state before:
pp: q a b c : ℚ
⊢ AddLeftCancelSemigroup ℚ

Tactic:
by infer_instance

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

Goal state before:
pp: q a b c : ℚ
⊢ AddRightCancelSemigroup ℚ

Tactic:
by infer_instance

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

Goal state before:
pp: q a b c : ℚ
⊢ AddCommSemigroup ℚ

Tactic:
by infer_instance

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

Goal state before:
pp: q a b c : ℚ
⊢ AddSemigroup ℚ

Tactic:
by infer_instance

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

Goal state before:
pp: q a b c : ℚ
⊢ Monoid ℚ

Tactic:
by infer_instance

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

Goal state before:
pp: q a b c : ℚ
⊢ CommSemigroup ℚ

Tactic:
by infer_instance

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

Goal state before:
pp: q a b c : ℚ
⊢ Semigroup ℚ

Tactic:
by infer_instance

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

Goal state before:
pp: q : ℚ
n d : ℤ
hq : q ≠ 0
hqnd : q = n /. d
this : n = 0
⊢ q = 0

Tactic:
by simpa [this] using hqnd

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

Goal state before:
pp: q : ℚ
n d : ℤ
hq : q ≠ 0
hqnd : q = n /. d
this : d = 0
⊢ q = 0

Tactic:
by simpa [this] using hqnd

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

Goal state before:
pp: α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ Forall p (x :: l) → Forall q (x :: l)

Tactic:
simp only [forall_cons, and_imp]
    rw [← and_imp]
    exact And.imp (h x) (Forall.imp h)

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

Goal state before:
pp: ⊢ CommSemiring ℚ

Tactic:
by infer_instance

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

Goal state before:
pp: ⊢ Semiring ℚ

Tactic:
by infer_instance

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

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

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

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

Goal state before:
pp: r : ℚ
hr : 0 ≤ r
p q : ℚ
hpq : p ≤ q
⊢ r * p ≤ r * q

Tactic:
by
    simpa [mul_sub, sub_nonneg] using Rat.mul_nonneg hr (sub_nonneg.2 hpq)

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
h : a ∣ b
⊢ a * ↑u * ↑u⁻¹ = a

Tactic:
rw [mul_assoc, u.mul_inv, mul_one]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
⊢ IsPrimal (m * n)

Tactic:
obtain rfl | h0 := eq_or_ne m 0

Goal state after:
case inl
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
n : α
hn : IsPrimal n
hm : IsPrimal 0
⊢ IsPrimal (0 * n)

case inr
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
h0 : m ≠ 0
⊢ IsPrimal (m * n)
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case mpr
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
⊢ IsSquare q

Tactic:
refine ⟨nr / dr, ?_⟩

Goal state after:
case mpr
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
⊢ q = ↑nr / ↑dr * (↑nr / ↑dr)
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: n : ℕ
⊢ IsSquare ↑n ↔ IsSquare n

Tactic:
isSquare_iff,

Goal state after:
n : ℕ
⊢ IsSquare (↑n).num ∧ IsSquare (↑n).den ↔ IsSquare n
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: z : ℤ
⊢ IsSquare ↑z ↔ IsSquare z

Tactic:
isSquare_iff,

Goal state after:
z : ℤ
⊢ IsSquare (↑z).num ∧ IsSquare (↑z).den ↔ IsSquare z
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
e : divNat a b = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
hd : ↑d = 0
this : Rat.divInt ↑a ↑b = ↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
⊢ d ∣ b

Tactic:
by simpa [Int.natCast_dvd_natCast, this] using Rat.den_dvd a b

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

Goal state before:
pp: case nil
α : Type u
m : Type u → Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
⊢ traverse pure nil = pure nil

Tactic:
traverse

Goal state after:
case nil
α : Type u
m : Type u → Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
⊢ pure nil = pure nil
Module: Mathlib.Tactic.CancelDenoms.Core

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

Tactic:
mul_le_mul_iff_right₀,

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ (a ≤ b) = (bd * a' ≤ ad * b')

α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b₁ b₂ c₁ c₂ : R
x✝¹ : a₁ + b₁ = c₁
x✝ : a₂ + b₂ = c₂
⊢ a₁ + a₂ + (b₁ + b₂) = c₁ + c₂

Tactic:
subst_vars; simp [add_assoc, add_left_comm]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
b : ℕ
hb : IsNat b 1
⊢ a ^ b = a

Tactic:
by simp [hb.out]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
inst✝ : CompleteLattice α
f : ι → α
x✝ : α
⊢ x✝ ∈ Ici (⨆ i, f i) ↔ x✝ ∈ ⋂ i, Ici (f i)

Tactic:
simp only [mem_Ici, iSup_le_iff, mem_iInter]

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:
by
  simp_rw [Iic_iInf]

Goal state after: