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

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithBot α
⊢ ⊥ < x ↔ x ≠ ⊥

Tactic:
cases x <;> simp

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝³ : Add α
x y z : WithBot α
inst✝² : LE α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
hx : x ≠ ⊥
x✝ : y ≤ z
⊢ x + y ≤ x + z

Tactic:
gcongr

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝³ : Add α
x y z : WithBot α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
hz : z ≠ ⊥
x✝ : x ≤ y
⊢ x + z ≤ y + z

Tactic:
gcongr

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝³ : Add α
w x y z : WithBot α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightMono α
hw : w ≠ ⊥
hwy : w ≤ y
hxz : x < z
⊢ w + z ≤ y + z

Tactic:
gcongr

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝³ : Add α
w x y z : WithBot α
inst✝² : Preorder α
inst✝¹ : AddLeftMono α
inst✝ : AddRightStrictMono α
hx : x ≠ ⊥
hwy : w < y
hxz : x ≤ z
⊢ y + x ≤ y + z

Tactic:
gcongr

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : WithBot α
b : α
⊢ x ≤ ↑(unbotD b x)

Tactic:
cases x <;> simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : OrderBot α
⊢ x < ↑⊥ ↔ x = ⊥

Tactic:
cases x <;> simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : WithBot α
⊢ x = ⊥ ↔ ∀ (b : α), x < ↑b

Tactic:
cases x <;> simp

Goal state after:
case coe
α : Type u_1
inst✝ : Preorder α
a✝ : α
⊢ ∃ x, ¬a✝ < x
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : WithZero α
b : α
⊢ x ≤ ↑(unzeroD b x)

Tactic:
cases x <;> simp

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

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
ha : 0 ≤ a
m : ℕ
⊢ m * n ≤ ⌊a * ↑n⌋₊ ↔ m ≤ ⌊a⌋₊

Tactic:
le_floor_iff (mul_nonneg ha (cast_nonneg' n)),

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

Tactic:
rw [← cast_one, floor_add_natCast ha 1]

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

Tactic:
gcongr

Goal state after:
case h₁
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
⊢ a ≤ ↑⌈a⌉₊

case h₂
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
⊢ b ≤ ↑⌈b⌉₊
Module: Mathlib.Algebra.Group.Invertible.Basic

Goal state before:
pp: α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible (a * b)
inst✝ : Invertible b
⊢ b * ⅟(a * b) * a = 1

Tactic:
← (isUnit_of_invertible b).mul_left_inj,

Goal state after:
α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible (a * b)
inst✝ : Invertible b
⊢ b * ⅟(a * b) * a * b = 1 * b
Module: Mathlib.Algebra.Order.GroupWithZero.OrderIso

Goal state before:
pp: G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a : G₀
ha : 0 < a
b c : G₀
⊢ b * a⁻¹ ≤ c * a⁻¹ ↔ b ≤ c

Tactic:
exact mul_le_mul_iff_left₀ (a := a⁻¹) (Right.inv_pos.mpr ha)

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

Goal state before:
pp: G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulZeroOneClass M₀'
inst✝² : Nontrivial M₀'
inst✝¹ : FunLike F G₀ M₀'
inst✝ : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀ˣ
hx : ↑a ≠ 0
H : f ↑a = 0
⊢ 1 = 0

Tactic:
rw [← map_one f, ← Units.mul_inv a, map_mul, H, zero_mul]

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

Goal state before:
pp: R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ (x + y) * (x ^ n + y ^ n) ≤ (x + y) * (x + y) ^ n

Tactic:
gcongr

Goal state after:
case hbc
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := ⋯
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x ^ n + y ^ n ≤ (x + y) ^ n
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ^ n + b ^ n ≤ (a + b) ^ n + (a + b) ^ n

Tactic:
gcongr

Goal state after:
case hab
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ≤ a + b

case hab
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ b ≤ a + b
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
hab : a ≤ b
⊢ a ^ (n + 1) ≤ b ^ (n + 1)

Tactic:
gcongr

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
hba : b ≤ a
⊢ b ^ (n + 1) ≤ a ^ (n + 1)

Tactic:
gcongr

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

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

Tactic:
gcongr

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

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

case h₂
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n✝ : ℕ
inst✝ : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
⊢ |a| ≤ max |a| |b|
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 ≤ ⊤

Tactic:
exact le_top

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

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

Tactic:
gcongr

Goal state after:
case ha
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
n : ℕ
⊢ 0 ≤ |a - b|

case hbc
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
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 ↦ ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Preorder β
f g : α ≃o β
⊢ f = g
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 ↦ ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : WellFoundedLT β
inst✝ : Preorder α
f g : α ≃o β
⊢ f = g
Module: Mathlib.Order.Hom.Set

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

Tactic:
refine ⟨fun f g ↦ ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedGT α
inst✝ : Preorder β
f g : α ≃o β
⊢ f = g
Module: Mathlib.Order.Hom.Set

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

Tactic:
refine ⟨fun f g ↦ ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : WellFoundedGT β
inst✝ : Preorder α
f g : α ≃o β
⊢ f = g
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
k : α
n : ℕ
x a a' : α
h : k + a = a'
⊢ k + term n x a = term n x a'

Tactic:
simp [h.symm, term, add_comm, add_assoc]

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

Tactic:
by
    have pos_invOf_d : (0 < ⅟(d : A)) := pos_invOf_of_invertible_cast d
    have pos_n : (0 < (n : A)) := Int.cast_pos (n := n) |>.2 (of_decide_eq_true h)
    rw [eq]
    exact mul_pos pos_n pos_invOf_d

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

Goal state before:
pp: α : Type ?u.3
inst✝ : Semiring α
k : ℕ
b c : α
hc1 : c * ↑k * b = 1
hc2 : b * (c * ↑k) = 1
⊢ Invertible b

Tactic:
exact ⟨_, hc1, hc2⟩

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
inst✝ : IsStrictOrderedRing α
h : a / b ≤ c / d
he : 0 ≤ e
⊢ a / b * (1 / e) ≤ c / d * (1 / e)

Tactic:
gcongr

Goal state after:
case ha
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
inst✝ : IsStrictOrderedRing α
h : a / b ≤ c / d
he : 0 ≤ e
⊢ 0 ≤ 1 / e
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
m n : ℤ
inst✝ : IsStrictOrderedRing α
a₁ a₂ : α
h : a₁ < a₂
⊢ (a₁ + a₁) / 2 < (a₁ + a₂) / 2

Tactic:
gcongr

Goal state after:
case hc
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
m n : ℤ
inst✝ : IsStrictOrderedRing α
a₁ a₂ : α
h : a₁ < a₂
⊢ 0 < 2
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
m n : ℤ
inst✝ : IsStrictOrderedRing α
a₁ a₂ : α
h : a₁ < a₂
⊢ (a₁ + a₂) / 2 < (a₂ + a₂) / 2

Tactic:
gcongr

Goal state after:
case hc
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
m n : ℤ
inst✝ : IsStrictOrderedRing α
a₁ a₂ : α
h : a₁ < a₂
⊢ 0 < 2
Module: Mathlib.Algebra.BigOperators.Group.List.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : Monoid M
inst✝ : Monoid N
l✝ : List ι
r : M → N → Prop
f : ι → M
g : ι → N
h₁ : r 1 1
h₂ : ∀ ⦃i : ι⦄ ⦃a : M⦄ ⦃b : N⦄, r a b → r (f i * a) (g i * b)
a : ι
l : List ι
hl : r (map f l).prod (map g l).prod
⊢ r (map f (a :: l)).prod (map g (a :: l)).prod

Tactic:
by simp only [map_cons, prod_cons, h₂ hl]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ b / -c < -a ↔ b < -(a * -c)

Tactic:
div_lt_iff₀ (neg_pos.2 hc),

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ b < -a * -c ↔ b < -(a * -c)
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
l₁ l₂ : List α
n : ℕ
a : α
h : l₁.length = n
⊢ takeD n (l₁ ++ l₂) a = l₁

Tactic:
by
  rw [← h]; apply takeD_left

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ 0 < a / b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
simp only [division_def, mul_pos_iff, inv_pos, inv_lt_zero]

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

Goal state before:
pp: case cons.a
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a✝² : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ S a✝² b✝

Tactic:
solve_by_elim

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

Goal state before:
pp: case cons.a
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a✝² : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ Forall₂ S l₁✝ l₂✝

Tactic:
solve_by_elim

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

Goal state before:
pp: case inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ |q - r| * ↑n * max |q| |r| ^ (n - 1) ≤ |q - r| * ↑n * (B + 1) ^ (n - 1)

Tactic:
gcongr

Goal state after:
case ha
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ 0 ≤ |q - r| * ↑n

case ha
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ 0 ≤ max |q| |r|

case hab
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ max |q| |r| ≤ B + 1
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ 2 * (ε * a) * b * ε⁻¹ ≤ ((ε * a) ^ 2 + b ^ 2) * ε⁻¹

Tactic:
gcongr

Goal state after:
case ha
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ 0 ≤ ε⁻¹
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case cons.cons
α : Type u_1
β : Type u_2
r : α → β → Prop
l u✝ : List α
u : α
l₁✝ l₂✝¹ : List α
_hlu : l₁✝ ~ l₂✝¹
ih : ∀ {v : List β}, Forall₂ r l₂✝¹ v → (Forall₂ r ∘r Perm) l₁✝ v
b✝ : β
l₂✝ : List β
hab : r u b✝
huv' : Forall₂ r l₂✝¹ l₂✝
⊢ (Forall₂ r ∘r Perm) (u :: l₁✝) (b✝ :: l₂✝)

Tactic:
rcases ih huv' with ⟨l₂, h₁₂, h₂₃⟩

Goal state after:
case cons.cons
α : Type u_1
β : Type u_2
r : α → β → Prop
l u✝ : List α
u : α
l₁✝ l₂✝¹ : List α
_hlu : l₁✝ ~ l₂✝¹
ih : ∀ {v : List β}, Forall₂ r l₂✝¹ v → (Forall₂ r ∘r Perm) l₁✝ v
b✝ : β
l₂✝ : List β
hab : r u b✝
huv' : Forall₂ r l₂✝¹ l₂✝
l₂ : List β
h₁₂ : Forall₂ r l₁✝ l₂
h₂₃ : l₂ ~ l₂✝
⊢ (Forall₂ r ∘r Perm) (u :: l₁✝) (b✝ :: l₂✝)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case nil
M : Type u_4
inst✝ : Monoid M
h : [].prod ≠ 1
⊢ 0 < [].length

pp: case cons
M : Type u_4
inst✝ : Monoid M
head✝ : M
tail✝ : List M
h : (head✝ :: tail✝).prod ≠ 1
⊢ 0 < (head✝ :: tail✝).length

Tactic:
· simp at h

Goal state after:
case cons
M : Type u_4
inst✝ : Monoid M
head✝ : M
tail✝ : List M
h : (head✝ :: tail✝).prod ≠ 1
⊢ 0 < (head✝ :: tail✝).length
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
M : Type u_4
inst✝ : Monoid M
l✝ : List M
i : M
l : List M
hil : (∀ (x : M), x ∈ l → x = 1) → l.prod = 1
hl : ∀ (x : M), x ∈ i :: l → x = 1
⊢ i * 1 = 1

Tactic:
hl _ mem_cons_self,

Goal state after:
case cons
M : Type u_4
inst✝ : Monoid M
l✝ : List M
i : M
l : List M
hil : (∀ (x : M), x ∈ l → x = 1) → l.prod = 1
hl : ∀ (x : M), x ∈ i :: l → x = 1
⊢ 1 * 1 = 1
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
b : M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
⊢ a * ((b :: l).erase a).prod = (b :: l).prod

Tactic:
obtain rfl | ⟨ne, h⟩ := List.eq_or_ne_mem_of_mem ha
    · simp only [erase_cons_head, prod_cons]
    rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc,
      comm a ha b mem_cons_self, mul_assoc,
      ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]

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

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : ι → α → α
op₂ : ι → β → β
op₃ : ι → γ → γ
a : α
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)
⊢ foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)

Tactic:
revert a
  induction l <;> intros <;> [rfl; simp only [*, foldr]]

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

Goal state before:
pp: ⊢ 0 ≠ 1

Tactic:
rw [ne_comm, ← divInt_one_one, divInt_ne_zero]

Goal state after:
⊢ 1 ≠ 0

⊢ 1 ≠ 0
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: α : Type u_2
L : List (List α)
i : ℕ
⊢ drop (take i (map length L)).sum L.flatten = (drop i L).flatten

Tactic:
induction L generalizing i
  · simp
  · cases i <;> simp [*]

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]

Goal state after:
α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ p x → Forall p l → q x ∧ Forall q l
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
hpq : p * q ≤ 0
⊢ (p * q).toNNRat = p.toNNRat * 0

Tactic:
toNNRat_eq_zero.2 hpq,

Goal state after:
case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
hpq : p * q ≤ 0
⊢ 0 = p.toNNRat * 0
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case left
α : Type u_1
inst✝ : CommMonoidWithZero α
b : α
hd : 0 ∣ b
hnd : ¬b ∣ 0
⊢ False

Tactic:
exact hnd (dvd_zero _)

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

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

Tactic:
rw [Int.ediv_mul_cancel hqdn]

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

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

Tactic:
simpa only [sub_eq_add_neg, neg_den] using add_den_dvd_lcm q₁ (-q₂)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n n' : ℕ
r : R
hr : ↑n = r
hn : n' = n
a : R
⊢ n' • a = r * a

Tactic:
by
  subst_vars
  simp only [nsmul_eq_mul]

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

Goal state before:
pp: case inr
R : Type u
inst✝⁵ : NonUnitalNonAssocSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hcb : c ≤ b
⊢ a * (b - c) + a * c = a * b

Tactic:
← mul_add,

Goal state after:
case inr
R : Type u
inst✝⁵ : NonUnitalNonAssocSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hcb : c ≤ b
⊢ a * (b - c + c) = a * b
Module: Mathlib.Tactic.Ring.Common

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

Tactic:
by
  simp [ha.out]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
b : β
p : β → Prop
s : (x : β) → x = b ∨ p x → Set α
⊢ ⋂ x, ⋂ (h : x = b ∨ p x), s x h = s b ⋯ ∩ ⋂ x, ⋂ (h : p x), s x ⋯

Tactic:
by
  simp only [iInter_or, iInter_inter_distrib, iInter_iInter_eq_left]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLinearOrder α
f : (i : ι) → κ i → α
⊢ (∀ b < ⊤, ∃ i, b < f i.fst i.snd) ↔ ∀ b < ⊤, ∃ i j, b < f i j

Tactic:
PSigma.exists

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ Iic (sInf s) = ⋂ a ∈ s, Iic a

Tactic:
rw [sInf_eq_iInf, Iic_iInf₂]

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

Goal state before:
pp: case neg.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
h₂ : b ≤ a
⊢ min a b = if a ≤ b then a else b

Tactic:
simp [show ¬(a ≤ b) from fun h => hab (le_antisymm h h₂), h₂]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : Frame α
a : α
f : ι → α
⊢ Disjoint a (⨆ i, f i) ↔ ∀ (i : ι), Disjoint a (f i)

Tactic:
simpa only [disjoint_comm] using @iSup_disjoint_iff

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

Goal state before:
pp: case neg.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
h₂ : b ≤ a
⊢ max a b = if a ≤ b then b else a

Tactic:
simp [show ¬(a ≤ b) from fun h => hab (le_antisymm h h₂), h₂]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : CompleteBooleanAlgebra α
f : ι → α
⊢ (iSup f)ᶜᶜ = (⨅ i, (f i)ᶜ)ᶜ

Tactic:
simp [compl_iInf]

Goal state after: