mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: case zero
α : Type u_2
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
n : ℕ
hn : ↑n = ↑n.succ
⊢ ↑(n + 0) = ↑n

Tactic:
rfl

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

Goal state before:
pp: case succ
α : Type u_2
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
n : ℕ
hn : ↑n = ↑n.succ
k : ℕ
k_ih : ↑(n + k) = ↑n
⊢ ↑(n + (k + 1)) = ↑n

Tactic:
grind

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

Goal state before:
pp: α : Type u_2
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
n : ℕ
hn : ∀ (k : ℕ), ↑(n + k) = ↑n
h : n + (floor ↑n + 1) ≤ floor ↑n
⊢ False

Tactic:
grind

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

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
h : 1 ≠ 0
n : ℤ
⊢ ↑n ≠ ↑(n + 1)

Tactic:
grind

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

Goal state before:
pp: x y : WithZero (Multiplicative ℤ)
hx : x ≠ 0
hy : y ≠ 0
z : WithZero (Multiplicative ℤ)
hz : z ≠ 0
hzx : z ≤ x
hzy : z ≤ y
k : ℕ
hk : exp (-↑k) < z
⊢ ∃ k, exp (-↑k) < x ∧ exp (-↑k) < y

Tactic:
grind

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

Goal state before:
pp: case coe
G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
a✝ : Multiplicative G
⊢ ↑a✝ ≤ exp (↑a✝).log

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Set β
h : DirectedOn r (f '' s)
x : β
hx : x ∈ s
y : β
hy : y ∈ s
z : β
hz : z ∈ s
hz' : r (f x) (f z) ∧ r (f y) (f z)
⊢ ∃ z ∈ s, (r on f) x z ∧ (r on f) y z

Tactic:
grind

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ a - ↑⌊a⌋₊ ≤ 1

Tactic:
simpa [add_comm] using (lt_floor_add_one a).le

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

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁴ : MulOneClass R
inst✝³ : Monoid S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
⊢ f ⅟r = ⅟(f r)

Tactic:
rfl

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

Goal state before:
pp: case inl
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : a < 0
⊢ FloorSemiring.floor a = FloorSemiring.floor a

pp: case inr
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : 0 ≤ a
⊢ FloorSemiring.floor a = FloorSemiring.floor a

Tactic:
· rw [H₁.floor_of_neg, H₂.floor_of_neg] <;> exact h

Goal state after:
case inr
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : 0 ≤ a
⊢ FloorSemiring.floor a = FloorSemiring.floor a
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
a b : R
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ -(b + a) = a * ⅟b * a → -a = b + a * ⅟b * a

Tactic:
grind

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

Goal state before:
pp: G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a : G₀
ha : 0 < a
x✝ : G₀
⊢ (mulLeft₀ a ha).symm x✝ = (mulLeft₀ a⁻¹ ⋯) x✝

Tactic:
rfl

Goal state after:
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
x✝ : G₀
⊢ (mulRight₀ a ha).symm x✝ = (mulRight₀ a⁻¹ ⋯) x✝

Tactic:
rfl

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

Goal state before:
pp: case inl
G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst✝³ : GroupWithZero G₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : FunLike F' G₀ M₀'
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h : f 0 = g 0
⊢ f 0⁻¹ = g 0⁻¹

Tactic:
inv_zero,

Goal state after:
case inl
G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst✝³ : GroupWithZero G₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : FunLike F' G₀ M₀'
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h : f 0 = g 0
⊢ f 0 = g 0
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
x : R
h : IsSquare x
⊢ 0 ≤ x

Tactic:
rcases h with ⟨y, rfl⟩
  exact mul_self_nonneg y

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 : ℕ
⊢ 2 ^ (n + 1) * (a ^ (n + 2) + b ^ (n + 2)) = 2 ^ (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))

Tactic:
rfl

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

Goal state before:
pp: case zero
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
⊢ 2 ^ (0 + (0 - 1)) * (a ^ (2 * 0) + b ^ (2 * 0)) = 2 ^ (2 * 0 - 1) * (a ^ (2 * 0) + b ^ (2 * 0))

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: u : ℤˣ
⊢ natAbs 1 = 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case refine_1
h : 1 = 1 ∧ 1 = 1 ∨ 1 = -1 ∧ 1 = -1
⊢ 1 * 1 = 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case refine_2
h : -1 = 1 ∧ -1 = 1 ∨ -1 = -1 ∧ -1 = -1
⊢ -1 * -1 = 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case refine_1
h : 1 = 1 ∧ -1 = -1 ∨ 1 = -1 ∧ -1 = 1
⊢ 1 * -1 = -1

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case refine_2
h : -1 = 1 ∧ 1 = -1 ∨ -1 = -1 ∧ 1 = 1
⊢ -1 * 1 = -1

Tactic:
rfl

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionSemiring L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
q : ℚ≥0
⊢ ↑q.num / ↑q.den = ↑q.num / f ↑q.den

Tactic:
natCast

Goal state after:
K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionSemiring L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
q : ℚ≥0
⊢ ↑q.num / ↑q.den = ↑q.num / ↑q.den
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
p : γ → Prop
⊢ (∀ (z : γ), z ∈ image2 f s t → p z) ↔ ∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → p (f x y)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
p : γ → Prop
⊢ (∃ z, z ∈ image2 f s t ∧ p z) ↔ ∃ x, x ∈ s ∧ ∃ y, y ∈ t ∧ p (f x y)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = image2 (fun a b ↦ f b a) t s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

Tactic:
rcases le_total a 0 with ha | ha <;> rcases le_total b 0 with hb | hb <;>
    simp only [abs_of_nonpos, abs_of_nonneg, true_or, or_true, neg_mul, mul_neg, neg_neg, *]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
rw [← not_nonempty_iff_eq_empty, image2_nonempty_iff, not_and_or]
  simp [not_nonempty_iff_eq_empty]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f f' : α → β → γ
s : Set α
t : Set β
h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → f a b = f' a b
⊢ image2 f s t = image2 f' s t

Tactic:
grind

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_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
s : Set α
t : Set β
u : Set γ
v : Set δ
f : ε → ζ → ν
g : α → β → ε
h : γ → δ → ζ
f' : ε' → ζ' → ν
g' : α → γ → ε'
h' : β → δ → ζ'
h_comm : ∀ (a : α) (b : β) (c : γ) (d : δ), f (g a b) (h c d) = f' (g' a c) (h' b d)
⊢ image2 f (image2 g s t) (image2 h u v) = image2 f' (image2 g' s u) (image2 h' t v)

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
a b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
x✝ : Antisymmetrization (α × β) fun x1 x2 ↦ x1 ≤ x2
a✝ : α × β
⊢ uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯)
      (Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯ (Quot.mk (⇑(AntisymmRel.setoid (α × β) fun x1 x2 ↦ x1 ≤ x2)) a✝)) =
    Quot.mk (⇑(AntisymmRel.setoid (α × β) fun x1 x2 ↦ x1 ≤ x2)) a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
a b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
fst✝ : Antisymmetrization α fun x1 x2 ↦ x1 ≤ x2
snd✝ : Antisymmetrization β fun x1 x2 ↦ x1 ≤ x2
a✝¹ : α
a✝ : β
⊢ Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯
      (uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯)
        (Quot.mk (⇑(AntisymmRel.setoid α fun x1 x2 ↦ x1 ≤ x2)) a✝¹,
          Quot.mk (⇑(AntisymmRel.setoid β fun x1 x2 ↦ x1 ≤ x2)) a✝)) =
    (Quot.mk (⇑(AntisymmRel.setoid α fun x1 x2 ↦ x1 ≤ x2)) a✝¹,
      Quot.mk (⇑(AntisymmRel.setoid β fun x1 x2 ↦ x1 ≤ x2)) a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
a b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
a✝² : Antisymmetrization (α × β) fun x1 x2 ↦ x1 ≤ x2
a✝¹ : α × β
b✝ : Antisymmetrization (α × β) fun x1 x2 ↦ x1 ≤ x2
a✝ : α × β
⊢ { toFun := Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯, invFun := uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯),
          left_inv := ⋯, right_inv := ⋯ }
        (Quot.mk (⇑(AntisymmRel.setoid (α × β) fun x1 x2 ↦ x1 ≤ x2)) a✝¹) ≤
      { toFun := Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯, invFun := uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯),
          left_inv := ⋯, right_inv := ⋯ }
        (Quot.mk (⇑(AntisymmRel.setoid (α × β) fun x1 x2 ↦ x1 ≤ x2)) a✝) ↔
    Quot.mk (⇑(AntisymmRel.setoid (α × β) fun x1 x2 ↦ x1 ≤ x2)) a✝¹ ≤
      Quot.mk (⇑(AntisymmRel.setoid (α × β) fun x1 x2 ↦ x1 ≤ x2)) a✝

Tactic:
rfl

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

Goal state before:
pp: α : Type u
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
F : ι → (a : α) → π a
⊢ (∀ (a : α), BddAbove (range (eval a ∘ F))) ↔ ∀ (a : α), BddAbove (range fun i ↦ F i a)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
s : Set β
⊢ ⇑e.symm '' s = ⇑e ⁻¹' s

Tactic:
by
  ext; exact mem_image_iff_of_inverse e.right_inv e.left_inv

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.12
a : α
x✝ : ↑{a}
⊢ (fun x ↦ ⟨a, ⋯⟩) ((fun x ↦ PUnit.unit) ⟨a, ⋯⟩) = ⟨a, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
β : Sort u_3
γ : Sort u_4
p : α → Prop
inst✝³ : EquivLike E { x // p x } β
e : E
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : ¬p i
⊢ (if h : p i then update v j x (e ⟨i, h⟩) else w i) =
    update (fun i ↦ if h : p i then v (e ⟨i, h⟩) else w i) (↑(EquivLike.inv e j)) x i

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : ¬a < b
⊢ Ioc a b = Ico a b

Tactic:
rw [Ioc_eq_empty h, Ico_eq_empty h]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
hc : IsCofinalFor s t
⊢ IsCofinalFor (t ∪ s) t

Tactic:
rw [union_comm]

Goal state after:
α : Type u_1
inst✝ : Preorder α
s t : Set α
hc : IsCofinalFor s t
⊢ IsCofinalFor (s ∪ t) t
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ Ico a b ⊆ s

Tactic:
· rwa [← Ico_sdiff_left, sdiff_singleton_subset_iff, insert_eq_of_mem ha] at ho

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
a b : α
h : IsLUB s a
⊢ a ≤ b ↔ b ∈ Ici a

Tactic:
rfl

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

Goal state before:
pp: ι : Sort u_4
α : Type u_5
inst✝ : SemilatticeSup α
f g : ι → α
h : BddAbove (range fun x ↦ f x ⊔ g x)
b : α
hb : b ∈ upperBounds (range fun x ↦ f x ⊔ g x)
⊢ BddAbove (range f)

Tactic:
exact ⟨b, fun a ⟨i, ha⟩ ↦ ha ▸ le_sup_left.trans (hb ⟨i, rfl⟩)⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ Icc a b = Icc a b

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Functor

Goal state before:
pp: case map_const
γ : Type u_1
α✝ β✝ : Type u_2
⊢ mapConst = map ∘ Function.const β✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Functor

Goal state before:
pp: case id_map
γ : Type u_1
α✝ : Type u_2
x✝ : Const γ α✝
⊢ id <$> x✝ = x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Functor

Goal state before:
pp: case comp_map
γ : Type u_1
α✝ β✝ γ✝ : Type u_2
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : Const γ α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Control.Functor

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Functor F
inst✝² : Functor G
inst✝¹ : LawfulFunctor F
inst✝ : LawfulFunctor G
α : Type v
x : F (G α)
⊢ mk (mk x) = mk x

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ 1 / a ^ n < 1 / a ^ m

Tactic:
refine (one_div_lt_one_div ?_ ?_).2 (pow_lt_pow_right₀ a1 mn) <;>
    exact pow_pos (zero_lt_one.trans a1) _

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

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (ts.length + (is.length + 1), ts.length)
    (ts.length + 1 + is.length, ts.length + 1)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (is.length, is.length) (ts.length + 1 + is.length, ts.length + 1)

Tactic:
grind

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

Goal state before:
pp: α : Type u
x : List α
n : ℕ
⊢ take n x = x → x.length ≤ n

Tactic:
grind

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

Goal state before:
pp: case zero
α : Type u
l : List α
⊢ tail^[0] l = drop 0 l

Tactic:
rfl

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 : α
hb : b < 0
⊢ 1 ≤ a / b ↔ a ≤ b

Tactic:
le_div_iff_of_neg hb,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ a ≤ 1 * b ↔ 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
⊢ 1 < a / b ↔ a < b

Tactic:
rw [lt_div_iff_of_neg hb, one_mul]

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

Goal state before:
pp: α : Type u
l : List α
n i✝ : ℕ
a✝ : α
⊢ (take n l).tail[i✝]? = some a✝ ↔ (take (n - 1) l.tail)[i✝]? = some a✝

Tactic:
grind

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

Goal state before:
pp: α : Type u
l : List α
n i✝ : ℕ
a✝ : α
⊢ (take n l).dropLast[i✝]? = some a✝ ↔ (take (n - 1) l.dropLast)[i✝]? = some a✝

Tactic:
grind

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

Goal state before:
pp: α : Type u
l : List α
n i✝ : ℕ
a✝ : α
⊢ (drop n l).tail[i✝]? = some a✝ ↔ (drop n l.tail)[i✝]? = some a✝

Tactic:
grind

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

Goal state before:
pp: α : Type u
l : List α
n i✝ : ℕ
a✝ : α
⊢ (drop n l).dropLast[i✝]? = some a✝ ↔ (drop n l.dropLast)[i✝]? = some a✝

Tactic:
grind

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ a - a / 2 = a / 2

Tactic:
grind

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ a / 2 - a = -(a / 2)

Tactic:
grind

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

Goal state before:
pp: α : Type u
i j : ℕ
hj : 0 < j
xs : List α
hi : i < xs.length
⊢ (dropSlice i j xs).length < xs.length

Tactic:
grind

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

Goal state before:
pp: case mp.nil
α : Type u_1
a b : List α
⊢ [] = []

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ [] = []

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
⊢ Forall₂ R (drop l₁.length l) l₂

Tactic:
by
  have h' : Forall₂ R (drop (length l₁) l) (drop (length l₁) (l₁ ++ l₂)) :=
    forall₂_drop (length l₁) h
  rwa [drop_left] at h'

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

Goal state before:
pp: α : Type u
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
hk : n + k + 1 < (l.insertIdx n x).length
⊢ (l.insertIdx n x)[n + k + 1] = l[n + k]

Tactic:
grind

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

Goal state before:
pp: α : Type u
l : List α
x : α
i j : ℕ
h : i ≤ j
⊢ (take i (l.insertIdx j x)).length = (take i l).length

Tactic:
grind

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

Goal state before:
pp: α : Type u
l : List α
x : α
i j : ℕ
h : i ≤ j
⊢ ∀ (i_1 : ℕ) (h₁ : i_1 < (take i (l.insertIdx j x)).length) (h₂ : i_1 < (take i l).length),
    (take i (l.insertIdx j x))[i_1] = (take i l)[i_1]

Tactic:
grind

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

Goal state before:
pp: α : Type u
l : List α
i j : ℕ
h : i ≤ j
⊢ (take i (l.eraseIdx j)).length = (take i l).length

Tactic:
grind

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

Goal state before:
pp: α : Type u
l : List α
i j : ℕ
h : i ≤ j
⊢ ∀ (i_1 : ℕ) (h₁ : i_1 < (take i (l.eraseIdx j)).length) (h₂ : i_1 < (take i l).length),
    (take i (l.eraseIdx j))[i_1] = (take i l)[i_1]

Tactic:
grind

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

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

Tactic:
grind

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

Goal state before:
pp: case mp
α : Type u
h : Injective length
x y : α
⊢ [x].length = [y].length

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
b : β
⊢ foldr f b [] = foldr f b []

Tactic:
rfl

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

Goal state before:
pp: case mpr.nil.nil
α : Type u
hα : Subsingleton α
hl : [].length = [].length
⊢ [] = []

Tactic:
rfl

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

Goal state before:
pp: case none.none
α : Type u_1
p : none.toList ~ none.toList
⊢ none = none

Tactic:
rfl

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

Goal state before:
pp: α : Type u
l : List α
h : l ≠ []
⊢ (∃ a b, l = [a, b]) ↔ l = [l.head h, l.getLast h]

Tactic:
grind

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

Goal state before:
pp: α : Type u
p : α → Prop
a : α
l : List α
⊢ (∃ x, x ∈ a :: l ∧ p x) → p a ∨ ∃ x, x ∈ l ∧ p x

Tactic:
grind

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

Goal state before:
pp: α : Type u
p : α → Prop
a : α
l : List α
⊢ (∃ x, x ∈ a :: l ∧ p x) ↔ p a ∨ ∃ x, x ∈ l ∧ p x

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f g : α → List β
⊢ flatMap f l ++ flatMap g l ~ flatMap (fun x ↦ f x ++ g x) l

Tactic:
induction l with | nil => simp | cons a l IH => ?_

Goal state after:
case cons
α : Type u_1
β : Type u_2
f g : α → List β
a : α
l : List α
IH : flatMap f l ++ flatMap g l ~ flatMap (fun x ↦ f x ++ g x) l
⊢ flatMap f (a :: l) ++ flatMap g (a :: l) ~ flatMap (fun x ↦ f x ++ g x) (a :: l)
Module: Mathlib.Data.List.Basic

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

Tactic:
rfl

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

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

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u
l₂ : List α
h : l₂ ≠ []
⊢ ([] ++ l₂).getLast ⋯ = l₂.getLast h

Tactic:
grind

Goal state after: