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

Goal state before:
pp: α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LE α
inst✝ : MulLeftReflectLE α
a b : α
h : a * b ≤ a
⊢ a * b ≤ a * 1

Tactic:
simpa only [mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : MulLeftReflectLT α
a b : α
h : a < a * b
⊢ a * 1 < a * b

Tactic:
simpa only [mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : MulLeftReflectLT α
a b : α
h : a * b < a
⊢ a * b < a * 1

Tactic:
simpa only [mul_one]

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

Goal state before:
pp: α : Type u_1
s : Ring α
⊢ ∀ (a : α), -a + a = 0

Tactic:
simp [neg_add_cancel]

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

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
⊢ 0 ≤ a ^ 2

Tactic:
obtain ha | ha := le_or_gt 0 a

Goal state after:
case inl
R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
ha : 0 ≤ a
⊢ 0 ≤ a ^ 2

case inr
R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
ha : a < 0
⊢ 0 ≤ a ^ 2
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
ha : 1 ≤ a
k : ℕ
⊢ 1 ≤ a ^ (k + 1)

Tactic:
rw [pow_succ]
    exact one_le_mul (one_le_pow_of_le ha k) ha

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

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
a b : M
hab : a ≤ b
k : ℕ
⊢ a ^ (k + 1) ≤ b ^ (k + 1)

Tactic:
rw [pow_succ, pow_succ]

Goal state after:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
a b : M
hab : a ≤ b
k : ℕ
⊢ a ^ k * a ≤ b ^ k * 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 ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ (a ⊓ c ⊓ c))) =
    (b ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))

Tactic:
inf_right_idem,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ (a ⊓ c))) =
    (b ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case H1
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    ↑b % ↑a = ↑x * s + ↑y * t →
      ↑a = ↑x * s' + ↑y * t' →
        ↑((b % a).xgcdAux s t a s' t').1 =
          ↑x * ((b % a).xgcdAux s t a s' t').2.1 + ↑y * ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : ↑a = ↑x * s + ↑y * t
p' : ↑b = ↑x * s' + ↑y * t'
k : ℤ
⊢ ↑b - ↑a * k = ↑x * (s' - k * s) + ↑y * (t' - k * t)

Tactic:
rw [p, p', Int.mul_sub, sub_add_eq_add_sub, Int.mul_sub, Int.add_mul, mul_comm k t,
      mul_comm k s, ← mul_assoc, ← mul_assoc, add_comm (x * s * k), ← add_sub_assoc, sub_sub]

Goal state after:
Module: Mathlib.Data.Int.GCD

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

Tactic:
← Nat.mul_div_cancel' (m.gcd_dvd_left n),

Goal state after:
case left
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ a ^ (m.gcd n * (m / m.gcd n)) = 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : ↑y ^ n = 1
hm : ↑y ^ (m + 1) = 1
⊢ ↑y ^ (m + 1).gcd n = 1

Tactic:
rw [← Units.val_pow_eq_pow_val, ← Units.val_one (α := M), ← zpow_natCast, ← Units.ext_iff] at *

Goal state after:
case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : y ^ ↑n = 1
hm : y ^ ↑(m + 1) = 1
⊢ y ^ ↑((m + 1).gcd n) = 1
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 c : α
h : c ≤ b
⊢ a - c ≤ b - c ↔ a ≤ b

Tactic:
by
  rw [tsub_le_iff_right, tsub_add_cancel_of_le h]

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

Goal state before:
pp: case none.none
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
⊢ ↑a + none ≤ ↑a + none → none ≤ none

pp: case none.some
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
c : α
⊢ ↑a + none ≤ ↑a + Option.some c → none ≤ Option.some c

pp: case some.none
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b : α
⊢ ↑a + Option.some b ≤ ↑a + none → Option.some b ≤ none

pp: case some.some
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b c : α
⊢ ↑a + Option.some b ≤ ↑a + Option.some c → Option.some b ≤ Option.some c

Tactic:
· simp [none_eq_bot]

Goal state after:
case none.some
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
c : α
⊢ ↑a + none ≤ ↑a + Option.some c → none ≤ Option.some c

case some.none
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b : α
⊢ ↑a + Option.some b ≤ ↑a + none → Option.some b ≤ none

case some.some
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b c : α
⊢ ↑a + Option.some b ≤ ↑a + Option.some c → Option.some b ≤ Option.some c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case none.some
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
c : α
⊢ ↑a + none ≤ ↑a + Option.some c → none ≤ Option.some c

pp: case some.none
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b : α
⊢ ↑a + Option.some b ≤ ↑a + none → Option.some b ≤ none

pp: case some.some
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b c : α
⊢ ↑a + Option.some b ≤ ↑a + Option.some c → Option.some b ≤ Option.some c

Tactic:
· simp [none_eq_bot]

Goal state after:
case some.none
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b : α
⊢ ↑a + Option.some b ≤ ↑a + none → Option.some b ≤ none

case some.some
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b c : α
⊢ ↑a + Option.some b ≤ ↑a + Option.some c → Option.some b ≤ Option.some c
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ
⊢ n ≤ Nat.find h ↔ ∀ (m : ℕ), m < n → ¬p m

Tactic:
by
  simp only [← not_lt, find_lt_iff, not_exists, not_and]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a b : WithBot α
⊢ map (⇑f) (a + b) = map (⇑f) a + map (⇑f) b

Tactic:
induction a
  · exact (bot_add _).symm
  · induction b
    · exact (add_bot _).symm
    · rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]
      rfl

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

Goal state before:
pp: α : Type u_3
a : WithZero (Multiplicative α)
h : a ≠ 0
b : α
k : toAdd (unzero h) = b
⊢ a = ↑(ofAdd b)

Tactic:
by subst k; exact (coe_unzero h).symm

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
⊢ n + 1 ≤ ⌈a⌉₊ ↔ n < ⌈a⌉₊

Tactic:
Nat.add_one_le_iff

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
⊢ n < ⌈a⌉₊ ↔ n < ⌈a⌉₊
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
⊢ (a + b) ^ 2 ≤ 2 * (a ^ 2 + b ^ 2)

Tactic:
calc
    (a + b) ^ 2 = a ^ 2 + b ^ 2 + (a * b + b * a) := by
        simp_rw [pow_succ', pow_zero, mul_one, add_mul, mul_add, add_comm (b * a), add_add_add_comm]
    _ ≤ a ^ 2 + b ^ 2 + (a * a + b * b) := add_le_add_right ?_ _
    _ = _ := by simp_rw [pow_succ', pow_zero, mul_one, two_mul]

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
⊢ a * b + b * a ≤ a * a + b * b
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : NeZero 2
a : K
⊢ a / 2 + a / 2 = a

Tactic:
← add_div,

Goal state after:
K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : NeZero 2
a : K
⊢ (a + a) / 2 = a
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a b c : K
⊢ a / c + -b / c = (a - b) / c

Tactic:
← add_div,

Goal state after:
K : Type u_1
inst✝ : DivisionRing K
a b c : K
⊢ (a + -b) / c = (a - b) / c
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝ : DivisionRing K
a : K
ha : a ≠ 0
⊢ a ^ 2 = 1 ↔ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
sq_eq_one_iff

Goal state after:
case inr
K : Type u_1
inst✝ : DivisionRing K
a : K
ha : a ≠ 0
⊢ a = 1 ∨ a = -1 ↔ a = -1 ∨ a = 0 ∨ a = 1
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: u v : ℤ
⊢ u * v = 1 ↔ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1

Tactic:
refine ⟨eq_one_or_neg_one_of_mul_eq_one', fun h ↦ Or.elim h (fun H ↦ ?_) fun H ↦ ?_⟩ <;>
    obtain ⟨rfl, rfl⟩ := H <;> rfl

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a : K
⊢ a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
inv_eq_self₀

Goal state after:
K : Type u_1
inst✝ : DivisionRing K
a : K
⊢ a = -1 ∨ a = 0 ∨ a = 1 ↔ a = -1 ∨ a = 0 ∨ a = 1
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
⊢ StrictAntiOn f (insert a s) ↔ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s

Tactic:
by
  rw [strictAntiOn_insert_iff]
  have : ∀ b ∈ s, a < b → f b < f a := by
    intro b hb hab
    cases (ha _ hb).not_gt hab
  tauto

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

Goal state before:
pp: case inr
α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
this : φ (ψ y) ≤ φ (ψ x)
⊢ ψ x ≤ ψ y

Tactic:
rw [φψs.eq ys, φψs.eq xs] at this

Goal state after:
case inr
α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
this : y ≤ x
⊢ ψ x ≤ ψ y
Module: Mathlib.Data.Set.NAry

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

Tactic:
image2_union_right,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
b : β
⊢ image2 f s {b} ∪ image2 f s t = (fun a ↦ f a b) '' s ∪ image2 f s t
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
n : ℕ
⊢ a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n

Tactic:
by
  rcases eq_or_ne n 0 with rfl | hn <;> simp [pow_eq_pow_iff_of_ne_zero, *]

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

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

Tactic:
← Ico_sdiff_left,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a < b
⊢ Ico a b \ (Ico a b \ {a}) = {a}
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
hab : a < b
⊢ Ioo a b ∪ {a} = Ico a b

Tactic:
← Ico_sdiff_left,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
hab : a < b
⊢ Ico a b \ {a} ∪ {a} = Ico a b
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case pos
α : 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
⊢ Icc a b ⊆ s

Tactic:
← Ico_sdiff_left,

Goal state after:
case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ico a b \ {a} ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ Icc a b ⊆ s
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:
← Ico_sdiff_left,

Goal state after:
case neg.refine_2
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ico a b \ {a} ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ Ico a b ⊆ s
Module: Mathlib.Order.Hom.Set

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

Tactic:
range_eq,

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

Goal state before:
pp: case neg
α : 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
⊢ s ⊆ Ioo a b

Tactic:
← Ico_sdiff_left,

Goal state after:
case neg
α : 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
⊢ s ⊆ Ico a b \ {a}
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ a / 3 + a / 3 + a / 3 = a

Tactic:
← add_div,

Goal state after:
α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ (a + a) / 3 + a / 3 = a
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ (a + a) / 3 + a / 3 = a

Tactic:
← add_div,

Goal state after:
α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ (a + a + a) / 3 = a
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
ha : 0 ≤ 0
hs : IsBot b
hb : b ≤ b + b
⊢ IsBot 0

Tactic:
rw [le_add_iff_nonneg_right] at hb

Goal state after:
case inr.inl
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
ha : 0 ≤ 0
hs : IsBot b
hb : 0 ≤ b
⊢ IsBot 0
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
h : 0 < a
b c : α
hc₀ : 0 < c
hc : b * c < a
⊢ b < c⁻¹ * a

Tactic:
rwa [← div_eq_inv_mul, lt_div_iff₀ hc₀]

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

Goal state before:
pp: case mpr.slnil
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ [] → SublistForall₂ R l₁ []

Tactic:
intro l₁ hl1
      rw [forall₂_nil_right_iff.1 hl1]
      exact SublistForall₂.nil

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ l ⊆ [a, b] ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l

Tactic:
trans ∀ c, c ∈ l → c = b ∨ c = a

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ l ⊆ [a, b] ↔ ∀ (c : α), c ∈ l → c = b ∨ c = a

α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ (∀ (c : α), c ∈ l → c = b ∨ c = a) ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : n = 0
⊢ zpow' a (m * 0) = zpow' (zpow' a m) 0

Tactic:
simp [zpow', ha, zpow_ne_zero ]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case nil
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a : α
hf : ∀ (a' : α), a' ≠ a → a' ∈ [] → f a' = 1
⊢ 1 = f a ^ 0

Tactic:
_root_.pow_zero

Goal state after:
case nil
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a : α
hf : ∀ (a' : α), a' ≠ a → a' ∈ [] → f a' = 1
⊢ 1 = 1
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

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

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

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → L.length ≤ L.sum
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ (j :: L).length ≤ j + L.sum

Tactic:
length,

Goal state after:
case cons
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → L.length ≤ L.sum
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ L.length + 1 ≤ j + L.sum
Module: Mathlib.Algebra.Group.Commute.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Semigroup G
a b c : G
h : SemiconjBy a b c
j : G
⊢ (fun x ↦ a * x) ((fun x ↦ b * x) j) = (fun x ↦ c * x) ((fun x ↦ a * x) j)

Tactic:
simp only [← mul_assoc, h.eq]

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

Goal state before:
pp: q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num =
      (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den ∨
    c = 0

Tactic:
or_iff_not_imp_right

Goal state after:
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ ¬c = 0 →
    ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num =
      (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
s : ℚ := ⋯
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
      (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den ∨
    c = 0

Tactic:
or_iff_not_imp_right

Goal state after:
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ ¬c = 0 →
    ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
      (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
Module: Mathlib.Data.Tree.Basic

Goal state before:
pp: case node
α : Type u
m : Type u → Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
v : α
l r : BinaryTree α
hl : traverse pure l = pure l
hr : traverse pure r = pure r
⊢ node <$> pure v <*> pure l <*> pure r = pure (node v l r)

Tactic:
map_pure,

Goal state after:
case node
α : Type u
m : Type u → Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
v : α
l r : BinaryTree α
hl : traverse pure l = pure l
hr : traverse pure r = pure r
⊢ pure (node v) <*> pure l <*> pure r = pure (node v l r)
Module: Mathlib.Data.Tree.Basic

Goal state before:
pp: case node
α : Type u
m : Type u → Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
v : α
l r : BinaryTree α
hl : traverse pure l = pure l
hr : traverse pure r = pure r
⊢ (fun h ↦ h r) <$> node v <$> pure l = pure (node v l r)

Tactic:
map_pure,

Goal state after:
case node
α : Type u
m : Type u → Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
v : α
l r : BinaryTree α
hl : traverse pure l = pure l
hr : traverse pure r = pure r
⊢ (fun h ↦ h r) <$> pure (node v l) = pure (node v l r)
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b₃ b₁ : R
b₂ : ℕ
⊢ a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * (a * b₃)

Tactic:
mul_left_comm

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a b₃ b₁ : R
b₂ : ℕ
⊢ b₁ ^ b₂ * (a * b₃) = b₁ ^ b₂ * (a * b₃)
Module: Mathlib.Data.Set.BooleanAlgebra

Goal state before:
pp: α : Type u_1
⊢ ∀ {ι : Type u_1} {κ : ι → Type u_1} (f : (a : ι) → κ a → Set α), ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
intros; ext; simp [Classical.skolem]

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

Goal state before:
pp: β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : ⋃ i ∈ t, s i = ⊤
x : β
⊢ ∃ i ∈ t, x ∈ s i

Tactic:
by
  have p : x ∈ ⊤ := Set.mem_univ x
  rw [← w, Set.mem_iUnion] at p
  simpa using p

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : PartialOrder ι
f : ι → α
i : ι
⊢ ⨆ j, ⨆ (_ : j ≤ i), f j = (⨆ j, ⨆ (_ : j < i), f j) ⊔ f i

Tactic:
by
  rw [iSup_split_single _ i]
  -- Squeezed for a ~10x speedup, though it's still reasonably fast unsqueezed.
  simp only [le_refl, iSup_pos, iSup_and', lt_iff_le_and_ne, and_comm, sup_comm]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
⊢ ⨅ i, ⨆ j, f i j = ⨅ i, ⨆ b, ↑b

Tactic:
iSup_subtype,

Goal state after:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
⊢ ⨅ i, ⨆ j, f i j = ⨅ i, ⨆ i_1 ∈ range (f i), i_1
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
⊢ ⋃ i, s i = range fun a ↦ ↑a.snd

Tactic:
by
  simp [Set.ext_iff]

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

Goal state before:
pp: β : Type u_2
ι : Sort u_5
s : ι → Set β
⊢ ⋃ i, s i = range fun a ↦ ↑a.snd

Tactic:
by
  simp [Set.ext_iff]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
a : α
s : Set α
⊢ ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s

Tactic:
by
    calc
      _ ≤ ⨆ i : ULift.{u} Bool, ⨅ j : match i with | .up true => PUnit.{u + 1} | .up false => s,
          match i with
          | .up true => a
          | .up false => j := by
        simp only [minAx.iSup_iInf_eq, iSup_ulift, iSup_bool_eq, le_iInf_iff]
        exact fun x ↦ biInf_le _ (x (.up false)).2
      _ = _ := by simp [sInf_eq_iInf', iInf_unique, iSup_bool_eq]

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
p : α → Prop
⊢ (∀ x ∈ ⋃₀ S, p x) ↔ ∀ s ∈ S, ∀ x ∈ s, p x

Tactic:
by
  simp_rw [← iInf_Prop_eq, iInf_sUnion]

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

Goal state before:
pp: case neg.some.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
c : WithTop β
hc : c ∈ s
⊢ c ∈ {⊤}

Tactic:
mem_singleton_iff,

Goal state after:
case neg.some.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
c : WithTop β
hc : c ∈ s
⊢ c = ⊤