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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
y : β
v : WithBot α
⊢ ↑y = map f v ↔ ∃ x, v = ↑x ∧ f x = y

Tactic:
cases v

Goal state after:
case bot
α : Type u_1
β : Type u_2
f : α → β
y : β
⊢ ↑y = map f ⊥ ↔ ∃ x, ⊥ = ↑x ∧ f x = y

case coe
α : Type u_1
β : Type u_2
f : α → β
y : β
a✝ : α
⊢ ↑y = map f ↑a✝ ↔ ∃ x, ↑a✝ = ↑x ∧ f x = y
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c : α
h : b ≤ a * c⁻¹
⊢ b * c ≤ a

Tactic:
simpa only [inv_inv] using mul_inv_le_of_le_mul₀ zero_le zero_le h

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

Goal state before:
pp: case pos
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n

pp: case neg
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n

Tactic:
· 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]

Goal state after:
case neg
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P 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 : R
n : ℕ
ha : 0 ≤ a
⊢ ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ < n + 1

Tactic:
Nat.lt_add_one_iff,

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

pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n a : ℕ
⊢ 0 ≤ ↑n

Tactic:
Nat.cast_le

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n a : ℕ
⊢ a ≤ n ↔ a ≤ n

R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n a : ℕ
⊢ 0 ≤ ↑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 : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
⊢ ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ < n + 1

Tactic:
Nat.lt_add_one_iff,

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
⊢ ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ ⌊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 : R
n : ℕ
hn : n ≠ 0
⊢ ⌈a⌉₊ = n ↔ n < ⌈a⌉₊ + (0 + 1) ∧ ⌈a⌉₊ ≤ n

Tactic:
Nat.lt_add_one_iff,

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

Goal state before:
pp: case inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : a ≤ 0
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

pp: case inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

Tactic:
· rw [floor_of_nonpos ha, floor_of_nonpos (tsub_nonpos_of_le (ha.trans n.cast_nonneg)), zero_tsub]

Goal state after:
case inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
Module: Mathlib.Order.Directed

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
a b : β
ha : ¬∃ i, e i = a
⊢ ∃ z, (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ a) (extend e f ⊥ z) ∧ (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)

Tactic:
use b
    simp [Function.extend_apply' _ _ _ ha]

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: β : Type u_2
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirectedOrder β
b : β
hb : IsMax b
hb' : IsMin b
c : β
hac : c < b
this : b ≤ b
⊢ False

Tactic:
exact hb'.not_lt hac

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

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

Tactic:
obtain (rfl | hc) := hc.eq_or_lt

Goal state after:
case inl
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeInf G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
hc : 0 ≤ 0
⊢ 0 * (a ⊓ b) = 0 * a ⊓ 0 * b

case inr
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeInf G₀
inst✝ : PosMulReflectLT G₀
c : G₀
hc✝ : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ c * (a ⊓ b) = c * a ⊓ c * b
Module: Mathlib.Algebra.Order.GroupWithZero.OrderIso

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

Tactic:
obtain (rfl | hc) := hc.eq_or_lt

Goal state after:
case inl
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
hc : 0 ≤ 0
⊢ 0 * (a ⊔ b) = 0 * a ⊔ 0 * b

case inr
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
inst✝ : PosMulReflectLT G₀
c : G₀
hc✝ : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ c * (a ⊔ b) = c * a ⊔ c * b
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:
obtain (rfl | hc) := hc.eq_or_lt

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

case inr
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeInf G₀
inst✝ : MulPosReflectLT G₀
c : G₀
hc✝ : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ (a ⊓ b) * c = a * c ⊓ b * c
Module: Mathlib.Algebra.Order.GroupWithZero.OrderIso

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

Tactic:
obtain (rfl | hc) := hc.eq_or_lt

Goal state after:
case inl
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hc : 0 ≤ 0
⊢ (a ⊔ b) * 0 = a * 0 ⊔ b * 0

case inr
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
inst✝ : MulPosReflectLT G₀
c : G₀
hc✝ : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ (a ⊔ b) * c = a * c ⊔ b * c
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: case neg
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : ¬a = 0
⊢ f a⁻¹ = (f a)⁻¹

Tactic:
apply eq_inv_of_mul_eq_one_left

Goal state after:
case neg
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : ¬a = 0
⊢ f a⁻¹ * f a = 1
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: case h
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ Commute 2 (a ^ 2 + b ^ 2)

Tactic:
simp [Commute, SemiconjBy, two_mul, mul_two]

Goal state after:
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
m : ℕ
h : -n = ↑m
⊢ |a ^ m|ₘ = |a|ₘ ^ m

Tactic:
exact mabs_pow m _

Goal state after:
Module: Mathlib.Order.BoundedOrder.Monotone

Goal state before:
pp: α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : Preorder β
inst✝ : OrderTop β
f : α → β
H : StrictMono f
a : α
h_top : f a = ⊤
x : α
p : β
⊢ p ≤ f a

Tactic:
by
      rw [h_top]
      exact le_top

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:
acc_def

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.WellFounded

Goal state before:
pp: α : Type u_1
β : Type u_2
r : β → β → Prop
inst✝ : Std.Trichotomous r
wf : WellFounded r
f : α → β
s : Set α
hne : s.Nonempty
a : α
has : a ∈ s
⊢ ¬r (f a) (f (⋯.min s hne))

Tactic:
exact wf.onFun.not_lt_min s has

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
u s : Set α
⊢ (fun x ↦ ↑((Set.image f s hf).symm x)) ⁻¹' u = Subtype.val ⁻¹' f '' u

Tactic:
ext ⟨b, a, has, rfl⟩
  simp [hf.eq_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t

Tactic:
rw [directedOn_union_iff] at h

Goal state after:
α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t ∧ IsCofinalFor s t
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: case e_a.e_5
α : Type u
inst✝ : Semiring α
num✝ denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ inv✝¹ = inv✝

Tactic:
apply Subsingleton.elim

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

Goal state before:
pp: case e_a.e_5
α : Type u
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ inv✝¹ = inv✝

Tactic:
apply Subsingleton.elim

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

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

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

Tactic:
· exact sub_inv_antitoneOn_Ioi.mono <| (Set.Icc_subset_Ioi_iff hab).mpr ha

Goal state after:
case neg
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : c < a
hab : ¬a ≤ b
⊢ AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Icc a b)
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
h : a < b
⊢ 1 / b < 1 / a

Tactic:
by
  rwa [div_lt_iff_of_neg' hb, ← div_eq_mul_one_div, div_lt_one_of_neg (h.trans hb)]

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

Goal state before:
pp: α : 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
a✝ : α
b✝ : β
h : (a✝, b✝) ∈ l₁.zip l₂
⊢ (a✝, b✝) ∈ (a :: l₁).zip (b :: l₂)

Tactic:
by
            simp only [zip, zipWith, mem_cons, Prod.mk.injEq]; right
            simpa [zip] using h

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ c ≤ a * b

Tactic:
refine le_of_forall_gt_imp_ge_of_dense fun d hd ↦ ?_
  obtain ⟨a', ha', hd⟩ := exists_mul_left_lt₀ hd
  obtain ⟨b', hb', hd⟩ := exists_mul_right_lt₀ hd
  exact (h a' ha' b' hb').trans hd.le

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

Goal state before:
pp: α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
a : α
n : ℕ
hl : ∀ (x : α), x ∈ l → p x
ha : p a
⊢ (pmap f l hl).insertIdx n (f a ha) = pmap f (l.insertIdx n a) ⋯

Tactic:
by
  induction n generalizing l with
  | zero => cases l <;> simp
  | succ n ihn => cases l <;> simp_all

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

Goal state before:
pp: case swap'
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
x✝ y✝ : α
l₁✝ l₂✝ : List α
h✝ : l₁✝ ~ l₂✝
r : ∀ (b : β), foldr f b l₁✝ = foldr f b l₂✝
b : β
⊢ f y✝ (f x✝ (foldr f b l₁✝)) = f x✝ (f y✝ (foldr f b l₂✝))

Tactic:
lcomm.left_comm,

Goal state after:
case swap'
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
x✝ y✝ : α
l₁✝ l₂✝ : List α
h✝ : l₁✝ ~ l₂✝
r : ∀ (b : β), foldr f b l₁✝ = foldr f b l₂✝
b : β
⊢ f x✝ (f y✝ (foldr f b l₁✝)) = f x✝ (f y✝ (foldr f b l₂✝))
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mpr
α : Type u
l₁ l₂ : List α
⊢ (l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩) →
    l₁ = l₂

Tactic:
intro ⟨h₁, h₂⟩

Goal state after:
case mpr
α : Type u
l₁ l₂ : List α
h₁ : l₁.length = l₂.length
h₂ : ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩
⊢ l₁ = l₂
Module: Mathlib.Data.List.Basic

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

Tactic:
induction l generalizing a with
  | nil => rfl
  | cons hd tl ih =>
    unfold foldl
    rw [ih _ fun a b bin => H a b <| mem_cons_of_mem _ bin, H a hd mem_cons_self]

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

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

Tactic:
rw [← neg_divInt, num_divInt_den]

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

Goal state before:
pp: q✝ a b c : ℚ
n : ℕ
q : ℚ
⊢ (n + 1) • q = n • q + q

Tactic:
by
    change ((n + 1 : Int) : Rat) * q = _
    rw [Rat.intCast_add, Rat.add_mul, Rat.intCast_one, Rat.one_mul]
    rfl

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

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

Tactic:
simp [Rat.div_def', num_coe, den_coe]

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

Goal state before:
pp: n : ℕ
a : ℚ≥0
⊢ a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹

Tactic:
ext; apply Field.zpow_neg'

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

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

Tactic:
Int.natAbs_mul,

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

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

Tactic:
Int.natAbs_mul,

Goal state after:
q : ℚ
⊢ q.den * q.den / (q.num.natAbs * q.num.natAbs).gcd (q.den * q.den) = q.den * q.den
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 }
hd : ↑d ≠ 0
hb' : b ≠ 0
e : divNat a b = divNat n d
⊢ ↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩ = ↑a / ↑b

Tactic:
divNat_inj hb' h

Goal state after:
α : 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 }
hd : ↑d ≠ 0
hb' : b ≠ 0
e : a * d = n * b
⊢ ↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩ = ↑a / ↑b
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ (Int.negOfNat a).pow b = Int.ofNat c

Tactic:
by
  rw [← hb, Int.negOfNat_eq, Int.pow_eq, pow_mul, neg_pow_two, ← pow_mul, two_mul, pow_add, ← hc,
    ← h1]
  simp

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Field α
n e e' : α
h : n * e = e'
h2 : n ≠ 0
⊢ e * n = e'

Tactic:
by rwa [mul_comm] at h

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

Goal state before:
pp: R : Type u
inst✝⁷ : NonAssocSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : CanonicallyOrderedAdd R
inst✝⁴ : Sub R
inst✝³ : OrderedSub R
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : MulRightMono R
inst✝ : AddLeftReflectLE R
a b : R
⊢ (a - 1) * b = a * b - b

Tactic:
by rw [tsub_mul, one_mul]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
s : Set β
⊢ BddAbove (⇑e ⁻¹' s) ↔ BddAbove s

Tactic:
rw [← e.bddAbove_image, e.image_preimage]

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:
union_distrib_iInter_right

Goal state after:
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
obs : ∀ (J : Set ι), x ∈ ⋃ j ∈ J, Es j ↔ i ∈ J
obs' : ∀ (J : Set ι), x ∈ (⋃ j ∈ J, Es j)ᶜ ↔ i ∉ J
⊢ i ∉ I ↔ i ∈ Iᶜ

Tactic:
mem_compl_iff

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
obs : ∀ (J : Set ι), x ∈ ⋃ j ∈ J, Es j ↔ i ∈ J
obs' : ∀ (J : Set ι), x ∈ (⋃ j ∈ J, Es j)ᶜ ↔ i ∉ J
⊢ i ∉ I ↔ i ∉ I
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : ↑(⋃ i, t i)
| ↑x

Tactic:
← unionEqSigmaOfDisjoint h |>.symm_apply_apply x

Goal state after:
α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : ↑(⋃ i, t i)
| ↑((unionEqSigmaOfDisjoint h).symm ((unionEqSigmaOfDisjoint h) x))
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hb : BddAbove s
⊢ sSup ((fun a ↦ ↑a) '' s) = ⨆ a ∈ s, ↑a

Tactic:
sSup_image

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hb : BddAbove s
⊢ ⨆ a ∈ s, ↑a = ⨆ a ∈ s, ↑a
Module: Mathlib.Data.SetLike.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : PartialOrder A
inst✝ : IsConcreteLE A B
S T : A
⊢ ↑S ⊂ ↑T ↔ S < T

Tactic:
by
  rw [ssubset_iff_subset_ne, lt_iff_le_and_ne, coe_subset_coe, SetLike.coe_ne_coe]

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
this : Std.Symm fun a b ↦ r a b ∨ r b a
⊢ IsChain r (s ∪ t) ↔ IsChain r s ∧ IsChain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a

Tactic:
rw [IsChain, IsChain, IsChain, pairwise_union_of_symm]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
f : ι → M × N
⊢ mulSupport f = (mulSupport fun x ↦ (f x).1) ∪ mulSupport fun x ↦ (f x).2

Tactic:
simp only [← mulSupport_prodMk]

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
ha : a < 1
⊢ 1 < a⁻ᵐ

Tactic:
rwa [leOnePart_eq_inv.2 ha.le, one_lt_inv']

Goal state after:
Module: Mathlib.Data.Int.Cast.Field

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
n : ℤ
hn : ↑n ≠ 0
k : ℤ
this : n ≠ 0
⊢ ↑(n * k / n) = ↑(n * k) / ↑n

Tactic:
Int.mul_ediv_cancel_left _ this,

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
hn : ↑n ≠ 0
k : ℤ
this : n ≠ 0
⊢ ↑k = ↑(n * k) / ↑n
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
rcases n.eq_zero_or_pos with rfl | hn

Goal state after:
case inl
k j : ℕ
⊢ ascFactorial 0 (j + 1) ≤ (j + 1)! * 0 ^ (j + 1)

case inr
n k j : ℕ
hn : n > 0
⊢ n.ascFactorial (j + 1) ≤ (j + 1)! * n ^ (j + 1)
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✝² : Add β
inst✝¹ : LE β
inst✝ : MulLEAddHomClass F α β
f : F
a b c : α
⊢ f (a / c) ≤ f (a / b) + f (b / c)

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

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

Goal state before:
pp: k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑k + ↑k * (q + 1).pred = 0 + ↑k * (q + 1)

Tactic:
Nat.pred_succ,

Goal state after:
k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑k + ↑k * q = 0 + ↑k * (q + 1)
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 1 - fract x ≤ fract x
this : 0 < fract x
⊢ |x - ↑⌈x⌉| = 1 - fract x

Tactic:
abs_sub_comm,

Goal state after:
case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 1 - fract x ≤ fract x
this : 0 < fract x
⊢ |↑⌈x⌉ - x| = 1 - fract x
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: n : ℕ+
a : ℕ
h : a ∣ ↑n
⊢ 0 < a

Tactic:
by
  apply pos_iff_ne_zero.2
  intro hzero
  rw [hzero] at h
  exact PNat.ne_zero n (eq_zero_of_zero_dvd h)

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 b : R
⊢ a + b ≤ ↑⌈a + b⌉

Tactic:
exact le_ceil _

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
r : α
n d : ℕ
⊢ IsNNRat r n d → IsNNRat (fract r) (n % d) d

Tactic:
rintro ⟨inv, rfl⟩
  refine ⟨inv, ?_⟩
  simp only [invOf_eq_inv, ← div_eq_mul_inv, fract_div_natCast_eq_div_natCast_mod]

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

Goal state before:

Tactic:
y ≤ l + a + n • a := sub_le_iff_le_add.1 hny.2
        _ = l + (n + 1) • a := by rw [add_comm n, add_smul, one_smul, add_assoc]
        _ ≤ l + (0 : ℤ) • a := by gcongr; lia
        _ ≤ x := by simpa using hx.1

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
g₁ g₂ : G
p : P
h : g₁ • p = g₂ • p
⊢ g₁ = g₂

Tactic:
by
  rw [← smul_sdiv g₁ p, h, smul_sdiv]

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

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

Tactic:
refine ⟨z + 1, ?_⟩

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