mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M✝ : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁴ : Zero A
inst✝³ : SMulZeroClass M✝ A
R : Type u_12
S : Type u_13
M : Type u_14
inst✝² : Zero M
inst✝¹ : SMulZeroClass R M
inst✝ : SMul S M
f : R → S
hf : Surjective f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
c : R
⊢ f c • 0 = 0

Tactic:
rw [hsmul, smul_zero]

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

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(-↑(n + 1)) = -↑(n + 1)

Tactic:
neg_ofNat_succ

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑-[n+1] = -↑(n + 1)
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(-[m+1] + ↑n) = ↑-[m+1] + ↑↑n

Tactic:
rw [Int.negSucc_add_ofNat, cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_iff_eq_add,
      add_assoc, eq_neg_add_iff_add_eq, ← Nat.cast_add, ← Nat.cast_add, Nat.add_comm]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ b * (1 / -a) = b * -(1 / a)

Tactic:
by rw [one_div_neg_eq_neg_one_div]

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

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ Even a → Odd b → Odd (a + b)

Tactic:
rintro ⟨a, rfl⟩ ⟨b, rfl⟩

Goal state after:
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ Odd (a + a + (2 * b + 1))
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ Odd a → Odd b → Even (a + b)

Tactic:
rintro ⟨a, rfl⟩ ⟨b, rfl⟩

Goal state after:
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ Even (2 * a + 1 + (2 * b + 1))
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r b c
⊢ r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)

Tactic:
rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a] at bc

Goal state after:
case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r (b * a * a⁻¹) (c * a * a⁻¹)
⊢ r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ Odd a → Odd b → Odd (a * b)

Tactic:
rintro ⟨a, rfl⟩ ⟨b, rfl⟩

Goal state after:
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ Odd ((2 * a + 1) * (2 * b + 1))
Module: Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE

Goal state before:
pp: α : Type u
inst✝⁴ : MulOneClass α
inst✝³ : Preorder α
inst✝² : ExistsMulOfLE α
a b : α
inst✝¹ : MulLeftMono α
inst✝ : MulLeftReflectLE α
⊢ (∃ c, 1 ≤ c ∧ a * c = b) → a ≤ b

Tactic:
rintro ⟨c, hc, rfl⟩; exact le_mul_of_one_le_right' hc

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

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : LinearOrder M₀
inst✝¹ : PosMulStrictMono M₀
a : M₀
n : ℕ
inst✝ : ZeroLEOneClass M₀
ha : 0 ≤ a
hn : n ≠ 0
⊢ a ^ n ≤ 1 ↔ a ≤ 1

Tactic:
refine ⟨fun h ↦ ?_, pow_le_one₀ ha⟩

Goal state after:
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : LinearOrder M₀
inst✝¹ : PosMulStrictMono M₀
a : M₀
n : ℕ
inst✝ : ZeroLEOneClass M₀
ha : 0 ≤ a
hn : n ≠ 0
h : a ^ n ≤ 1
⊢ a ≤ 1
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (f a' = b)
⊢ Injective fun a' ↦ if a' = a then b else if f a' = b then f a else f a'

Tactic:
intro x

Goal state after:
α : Sort u_1
β : Sort u_2
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (f a' = b)
x : α
⊢ ∀ ⦃a₂ : α⦄,
    (fun a' ↦ if a' = a then b else if f a' = b then f a else f a') x =
        (fun a' ↦ if a' = a then b else if f a' = b then f a else f a') a₂ →
      x = a₂
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
⊢ Function.Injective fun x ↦ if h : p ↑x then Sum.inl ⟨↑x, h⟩ else Sum.inr ⟨↑x, ⋯⟩

Tactic:
intro x

Goal state after:
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
x : { x // p x ∨ q x }
⊢ ∀ ⦃a₂ : { x // p x ∨ q x }⦄,
    (fun x ↦ if h : p ↑x then Sum.inl ⟨↑x, h⟩ else Sum.inr ⟨↑x, ⋯⟩) x =
        (fun x ↦ if h : p ↑x then Sum.inl ⟨↑x, h⟩ else Sum.inr ⟨↑x, ⋯⟩) a₂ →
      x = a₂
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

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

Tactic:
← mul_inv_le_iff₀ ha,

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ ≤ b ↔ 1 * a⁻¹ ≤ b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 ≤ a * b
⊢ 2 * r * (2 * r) ≤ (a + b) * (a + b)

Tactic:
mul_mul_mul_comm,

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 ≤ a * b
⊢ 2 * 2 * (r * r) ≤ (a + b) * (a + b)
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
⊢ Injective f

Tactic:
intro x

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x : α
⊢ ∀ ⦃a₂ : α⦄, f x = f a₂ → x = a₂
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ (x - a) * (x - b) ≤ 0 ↔ a ≤ x ∧ x ≤ b

Tactic:
mul_nonpos_iff,

Goal state after:
R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ 0 ≤ x - a ∧ x - b ≤ 0 ∨ x - a ≤ 0 ∧ 0 ≤ x - b ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a) * (b ⊓ a)⁻¹ = (b ⊔ a) / (b ⊓ a)

Tactic:
← div_eq_mul_inv

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a) / (b ⊓ a) = (b ⊔ a) / (b ⊓ a)
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝² : Semigroup α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedMul α
a b c : α
hbc : b ≤ b * c
⊢ (fun x1 x2 ↦ x1 * x2) a b ≤ (fun x1 x2 ↦ x1 * x2) a (b * c)

Tactic:
rw [le_iff_exists_mul]

Goal state after:
α : Type u
inst✝² : Semigroup α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedMul α
a b c : α
hbc : b ≤ b * c
⊢ ∃ c_1, (fun x1 x2 ↦ x1 * x2) a (b * c) = (fun x1 x2 ↦ x1 * x2) a b * c_1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ a ^ m = 1 ∧ a ^ n = 1

Tactic:
constructor
    · rw [← Nat.mul_div_cancel' (m.gcd_dvd_left n), pow_mul, hmn, one_pow]
    · rw [← Nat.mul_div_cancel' (m.gcd_dvd_right n), pow_mul, hmn, one_pow]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a + (b - a) ≤ b

Tactic:
obtain ⟨c, rfl⟩ := exists_add_of_le h

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c : α
h : a ≤ a + c
⊢ a + (a + c - a) ≤ a + c
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
d : α
x y : WithBot α
⊢ unbotD d x = unbotD d y ↔ x = y ∨ x = ↑d ∧ y = ⊥ ∨ x = ⊥ ∧ y = ↑d

Tactic:
induction y <;> simp [unbotD_eq_iff, or_comm]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
p : WithBot α → Prop
⊢ (∀ (x : WithBot α), ↑a < x → p x) ↔ ∀ (b : α), a < b → p ↑b

Tactic:
by
  simp [WithBot.forall]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
p : WithBot α → Prop
⊢ (∀ (x : WithBot α), ↑a ≤ x → p x) ↔ ∀ (b : α), a ≤ b → p ↑b

Tactic:
by
  simp [WithBot.forall]

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
n : ℕ
hn : n ≠ 0
a : R
⊢ ⌊a * ↑n⌋₊ / n = ⌊a⌋₊

Tactic:
by
  rcases le_total a 0 with ha | ha
  · rw [floor_of_nonpos, floor_of_nonpos ha]
    · simp
    apply mul_nonpos_of_nonpos_of_nonneg ha n.cast_nonneg
  refine eq_of_forall_le_iff fun m ↦ ?_
  rw [le_div_iff_mul_le (zero_lt_of_ne_zero hn), le_floor_iff (mul_nonneg ha (cast_nonneg' n)),
    le_floor_iff ha, cast_mul, mul_le_mul_iff_of_pos_right (cast_pos'.mpr (zero_lt_of_ne_zero hn))]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝¹ : LT α
inst✝ : WellFoundedGT α
a x✝¹ : α
x✝ : ∀ (y : α), x✝¹ < y → Acc (fun x1 x2 ↦ x2 < x1) y
ih : ∀ (y : α), x✝¹ < y → Acc (fun x1 x2 ↦ x1 > x2) ↑y
⊢ ∀ (y : WithBot α), y > ↑x✝¹ → Acc (fun x1 x2 ↦ x1 > x2) y

Tactic:
simpa [WithBot.forall]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LT α
inst✝ : WellFoundedGT α
acc_some : ∀ (a : α), Acc (fun x1 x2 ↦ x1 > x2) ↑a
⊢ ∀ (y : WithBot α), ⊥ < y → Acc (fun x1 x2 ↦ x2 < x1) y

Tactic:
simpa [WithBot.forall]

Goal state after:
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:
by
    rw [← (isUnit_of_invertible b).mul_left_inj, mul_assoc, mul_assoc, invOf_mul_self, mul_one,
      one_mul]

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:
← (commute_invOf m).symm.mul_pow,

Goal state after:
α : Type u
inst✝¹ : Monoid α
m : α
inst✝ : Invertible m
n : ℕ
⊢ (⅟m * m) ^ n = 1
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
S : Type u_3
inst✝⁴ : Semiring S
inst✝³ : LinearOrder S
inst✝² : FloorSemiring S
b : S
inst✝¹ : IsStrictOrderedRing R
inst✝ : IsStrictOrderedRing S
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
⊢ ⌊a⌋₊ = ⌊b⌋₊

Tactic:
by
  have h₀ : 0 ≤ a ↔ 0 ≤ b := by simpa only [cast_zero] using h 0
  obtain ha | ha := lt_or_ge a 0
  · rw [floor_of_nonpos ha.le, floor_of_nonpos (le_of_not_ge <| h₀.not.mp ha.not_ge)]
  exact (le_floor <| (h _).1 <| floor_le ha).antisymm (le_floor <| (h _).2 <| floor_le <| h₀.1 ha)

Goal state after:
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
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b

Tactic:
obtain hab | hba := le_total a b

Goal state after:
case h₂.inl
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 + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b

case h₂.inr
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
⊢ a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : NeZero 2
a : K
⊢ a / 2 - a = -(a / 2)

Tactic:
← neg_sub,

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : NeZero 2
a : K
⊢ -(a - a / 2) = -(a / 2)
Module: Mathlib.Order.Bounds.Image

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

Tactic:
by
  simp only [bddAbove_pi, ← range_comp]
  rfl

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:
rw [acc_def] at h
  push Not at h
  simpa only [and_comm]

Goal state after:
Module: Mathlib.Algebra.Order.Invertible

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
inst✝ : Invertible a
⊢ ⅟a ≤ 0 ↔ a ≤ 0

Tactic:
by simp only [← not_lt, invOf_pos]

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

Tactic:
Ioc_eq_empty (mt le_of_lt h)

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
h : ¬a ≤ b
⊢ ∅ = ∅
Module: Mathlib.Order.Interval.Set.Basic

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

Tactic:
← Icc_sdiff_right,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ Icc a b \ (Icc a b \ {b}) = {b}
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s

Tactic:
intro x

Goal state after:
α : Type u_1
inst✝ : Preorder α
s t : Set α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
x : α
⊢ x ∈ s → ∀ y ∈ s, ∃ z ∈ s, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z
Module: Mathlib.Order.Interval.Set.Basic

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

Tactic:
← Icc_sdiff_right,

Goal state after:
case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Icc a b \ {b} ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ Icc a b ⊆ s
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: ι : Sort u_4
α : Type u_5
inst✝ : SemilatticeSup α
f g : ι → α
hf : BddAbove (range f)
hg : BddAbove (range g)
⊢ BddAbove (range fun x ↦ f x ⊔ g x)

Tactic:
by
  have ⟨af, haf⟩ := hf
  have ⟨ag, hag⟩ := hg
  exact ⟨af ⊔ ag, fun a ⟨i, ha⟩ ↦ ha ▸ sup_le_sup (haf ⟨i, rfl⟩) (hag ⟨i, rfl⟩)⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Icc a b ∩ Icc b c = {b}

Tactic:
rw [← Ici_inter_Iic, ← Iic_inter_Ici, inter_inter_inter_comm, Iic_inter_Ici]

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ici a ∩ Iic c ∩ Icc b b = {b}
Module: Mathlib.Order.Bounds.Basic

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

Tactic:
refine ⟨i, fun j hj => le_of_lt hj, ?_⟩
    rw [mem_lowerBounds]
    exact h_exists_lt

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

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝² : Ring A
inst✝¹ : PartialOrder A
inst✝ : IsStrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ e ≠ 0

Tactic:
NormNum.IsInt.neg_to_eq h rfl

Goal state after:
A : Type u_1
e : A
n : ℕ
inst✝² : Ring A
inst✝¹ : PartialOrder A
inst✝ : IsStrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ -↑n ≠ 0
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ IsRat (f a b) nc dc

Tactic:
rw [hf, sub_eq_add_neg]
  refine isRat_add rfl ra (isRat_neg (n' := -nb) rfl rb rfl) (k := k) (nc := nc) ?_ h₂
  rw [show Int.mul (-nb) _ = _ from neg_mul ..]; exact h₁

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

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ (l : List α), tail^[n] l = drop n l
l : List α
⊢ tail^[n + 1] l = drop (n + 1) l

Tactic:
cases l

Goal state after:
case succ.nil
α : Type u
n : ℕ
ih : ∀ (l : List α), tail^[n] l = drop n l
⊢ tail^[n + 1] [] = drop (n + 1) []

case succ.cons
α : Type u
n : ℕ
ih : ∀ (l : List α), tail^[n] l = drop n l
head✝ : α
tail✝ : List α
⊢ tail^[n + 1] (head✝ :: tail✝) = drop (n + 1) (head✝ :: tail✝)
Module: Mathlib.Algebra.Order.Field.Basic

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

Tactic:
by
  simp [division_def, mul_neg_iff]

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

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

Tactic:
simp [hb, hb.not_gt, one_le_div]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
h : Forall₂ R l₁ l₂
⊢ Forall₂ S l₁ l₂

Tactic:
by
  induction h <;> constructor <;> solve_by_elim

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

Goal state before:
pp: case zero
α : Type u
a : α
l : List α
hn : 0 ≠ l.length
⊢ (l.eraseIdx 0).insertIdx 0 a = l.set 0 a

Tactic:
cases l

Goal state after:
case zero.nil
α : Type u
a : α
hn : 0 ≠ [].length
⊢ ([].eraseIdx 0).insertIdx 0 a = [].set 0 a

case zero.cons
α : Type u
a head✝ : α
tail✝ : List α
hn : 0 ≠ (head✝ :: tail✝).length
⊢ ((head✝ :: tail✝).eraseIdx 0).insertIdx 0 a = (head✝ :: tail✝).set 0 a
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: case succ
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {l : List α}, n✝ ≠ l.length → (l.eraseIdx n✝).insertIdx n✝ a = l.set n✝ a
l : List α
hn : n✝ + 1 ≠ l.length
⊢ (l.eraseIdx (n✝ + 1)).insertIdx (n✝ + 1) a = l.set (n✝ + 1) a

Tactic:
cases l

Goal state after:
case succ.nil
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {l : List α}, n✝ ≠ l.length → (l.eraseIdx n✝).insertIdx n✝ a = l.set n✝ a
hn : n✝ + 1 ≠ [].length
⊢ ([].eraseIdx (n✝ + 1)).insertIdx (n✝ + 1) a = [].set (n✝ + 1) a

case succ.cons
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {l : List α}, n✝ ≠ l.length → (l.eraseIdx n✝).insertIdx n✝ a = l.set n✝ a
head✝ : α
tail✝ : List α
hn : n✝ + 1 ≠ (head✝ :: tail✝).length
⊢ ((head✝ :: tail✝).eraseIdx (n✝ + 1)).insertIdx (n✝ + 1) a = (head✝ :: tail✝).set (n✝ + 1) a
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R l₁.reverse l₂.reverse
⊢ Forall₂ R l₁ l₂

Tactic:
← reverse_reverse l₁,

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R l₁.reverse l₂.reverse
⊢ Forall₂ R l₁.reverse.reverse l₂
Module: Mathlib.Data.List.InsertIdx

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

Tactic:
cases l

Goal state after:
case zero.nil
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
hl : ∀ (x : α), x ∈ [] → p x
⊢ (pmap f [] hl).insertIdx 0 (f a ha) = pmap f ([].insertIdx 0 a) ⋯

case zero.cons
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
head✝ : α
tail✝ : List α
hl : ∀ (x : α), x ∈ head✝ :: tail✝ → p x
⊢ (pmap f (head✝ :: tail✝) hl).insertIdx 0 (f a ha) = pmap f ((head✝ :: tail✝).insertIdx 0 a) ⋯
Module: Mathlib.Data.List.InsertIdx

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

Tactic:
cases l

Goal state after:
case succ.nil
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
n : ℕ
ihn : ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x), (pmap f l hl).insertIdx n (f a ha) = pmap f (l.insertIdx n a) ⋯
hl : ∀ (x : α), x ∈ [] → p x
⊢ (pmap f [] hl).insertIdx (n + 1) (f a ha) = pmap f ([].insertIdx (n + 1) a) ⋯

case succ.cons
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
n : ℕ
ihn : ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x), (pmap f l hl).insertIdx n (f a ha) = pmap f (l.insertIdx n a) ⋯
head✝ : α
tail✝ : List α
hl : ∀ (x : α), x ∈ head✝ :: tail✝ → p x
⊢ (pmap f (head✝ :: tail✝) hl).insertIdx (n + 1) (f a ha) = pmap f ((head✝ :: tail✝).insertIdx (n + 1) a) ⋯
Module: Mathlib.Data.List.Forall2

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

Tactic:
exact ⟨b :: l, Forall₂.cons rab hl1, hl2.cons_cons b⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
a b c : List α
⊢ SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b c → SublistForall₂ Rₐ a c

Tactic:
revert a b
    induction c with
    | nil =>
      rintro _ _ h1 h2
      cases h2
      exact h1
    | cons _ _ ih =>
      rintro a b h1 h2
      obtain - | ⟨hbc, tbc⟩ | btc := h2
      · cases h1
        exact SublistForall₂.nil
      · obtain - | ⟨hab, tab⟩ | atb := h1
        · exact SublistForall₂.nil
        · exact SublistForall₂.cons (_root_.trans hab hbc) (ih _ _ tab tbc)
        · exact SublistForall₂.cons_right (ih _ _ atb tbc)
      · exact SublistForall₂.cons_right (ih _ _ h1 btc)

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

Goal state before:
pp: case inl.inl
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length < n
⊢ l₁ ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
insertIdx_of_length_lt hn₂

Goal state after:
case inl.inl
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length < n
⊢ l₁ ~ l₂ ↔ l₁ ~ l₂
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ → (Perm ∘r Forall₂ r) l₁ l₃

pp: case mpr
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Perm ∘r Forall₂ r) l₁ l₃ → (Forall₂ r ∘r Perm) l₁ l₃

Tactic:
· intro h
    rcases h with ⟨l₂, h₁₂, h₂₃⟩
    have : Forall₂ (flip r) l₂ l₁ := h₁₂.flip
    rcases perm_comp_forall₂ h₂₃.symm this with ⟨l', h₁, h₂⟩
    exact ⟨l', h₂.symm, h₁.flip⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Perm ∘r Forall₂ r) l₁ l₃ → (Forall₂ r ∘r Perm) l₁ l₃
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List M
⊢ l[0]?.getD 1 * l.tail.prod = l.prod

Tactic:
cases l

Goal state after:
case nil
M : Type u_4
inst✝ : Monoid M
⊢ [][0]?.getD 1 * [].tail.prod = [].prod

case cons
M : Type u_4
inst✝ : Monoid M
head✝ : M
tail✝ : List M
⊢ (head✝ :: tail✝)[0]?.getD 1 * (head✝ :: tail✝).tail.prod = (head✝ :: tail✝).prod