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

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : PosMulStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ f a * f b < f (a * c)

Tactic:
mul

Goal state after:
α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : PosMulStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ f a * f b < f a * f c
Module: Mathlib.Algebra.Order.GroupWithZero.Defs

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : MulPosStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ f b * f a < f (c * a)

Tactic:
mul

Goal state after:
α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : MulPosStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ f b * f a < f c * f a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
⊢ a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂

Tactic:
contrapose!
  exact fun h => mul_lt_mul_of_lt_of_lt h.1 h.2

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ a⁻¹ < a ↔ 1 < a

Tactic:
exact inv_lt_self_iff

Goal state after:
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 c : G₀
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ b * c⁻¹
⊢ a * c ≤ b

Tactic:
obtain rfl | hc := hc.eq_or_lt
  · simpa using hb
  · rwa [le_mul_inv_iff₀ hc] at h

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ a⁻¹ ≤ a ↔ 1 ≤ a

Tactic:
inv_le_self_iff

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ 1 ≤ a ↔ 1 ≤ a
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Group α
a : WithZero α
ha : a ≠ 0
⊢ a * a⁻¹ = 1

Tactic:
lift a to α using ha
    norm_cast
    apply mul_inv_cancel

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

Goal state before:
pp: α : Type u
inst✝¹ : Add α
x y z : WithTop α
inst✝ : IsLeftCancelAdd α
hx : x ≠ ⊤
⊢ x + y = x + z ↔ y = z

Tactic:
lift x to α using hx; exact (IsAddLeftRegular.all _).withTop.eq_iff

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

Goal state before:
pp: case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
a✝² a✝¹ a✝ : α
⊢ a✝² + a✝¹ < a✝² + a✝ → a✝¹ < a✝

Tactic:
simpa using lt_of_add_lt_add_left

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 c : α
hb : AddLECancellable b
h : b ≤ a
⊢ c = a - b ↔ a = c + b

Tactic:
hb.eq_tsub_iff_add_eq_of_le h,

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : b ≤ a
⊢ c + b = a ↔ a = c + b
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
inst✝ : Nonempty α
ha : ⊥ ≠ ⊥
⊢ ⊥.unbotA = ⊥.unbot ha

Tactic:
contradiction

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

Goal state before:
pp: case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
a✝² a✝¹ a✝ : α
⊢ a✝² + a✝¹ < a✝² + a✝ → a✝¹ < a✝

Tactic:
simpa using lt_of_add_lt_add_left

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✝ : SemilatticeInf α
x y z : WithTop α
⊢ x ≤ y →
    x ≤ z →
      x ≤
        match y, z with
        | none, none => ⊤
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊓ b)

Tactic:
cases x <;> cases y <;> cases z <;> simp; simpa using le_inf

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

Goal state before:
pp: α : Type u_2
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
⊢ StrictMono Nat.cast

Tactic:
refine strictMono_nat_of_lt_succ fun n => (natCast_mono (Nat.le_succ n)).lt_of_ne fun hn => ?_

Goal state after:
α : Type u_2
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
n : ℕ
hn : ↑n = ↑n.succ
⊢ False
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
x y z : WithBot α
⊢ x ≤ y → x ≤ z → x ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z

Tactic:
cases x <;> cases y <;> cases z <;> simp; simpa using le_inf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
x y z : WithZero α
⊢ x ≤ y → x ≤ z → x ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z

Tactic:
cases x <;> cases y <;> cases z <;> simp; simpa using le_inf

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

Goal state before:
pp: G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hxa : x.log ≤ a
⊢ x ≤ exp a

Tactic:
obtain rfl | hx := eq_or_ne x 0

Goal state after:
case inl
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
hxa : log 0 ≤ a
⊢ 0 ≤ exp a

case inr
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hxa : x.log ≤ a
hx : x ≠ 0
⊢ x ≤ exp a
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hxa : x.log < a
⊢ x < exp a

Tactic:
obtain rfl | hx := eq_or_ne x 0

Goal state after:
case inl
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
hxa : log 0 < a
⊢ 0 < exp a

case inr
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hxa : x.log < a
hx : x ≠ 0
⊢ x < exp a
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hxa : x.log < a
⊢ x < exp a

Tactic:
by
  obtain rfl | hx := eq_or_ne x 0 <;> simp [← log_lt_iff_lt_exp, *]

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

Goal state before:
pp: x : WithZero (Multiplicative ℤ)
y : Multiplicative ℤ
⊢ x < ↑y * exp 1 ↔ x ≤ ↑y

Tactic:
obtain rfl | hx := eq_or_ne x 0

Goal state after:
case inl
y : Multiplicative ℤ
⊢ 0 < ↑y * exp 1 ↔ 0 ≤ ↑y

case inr
x : WithZero (Multiplicative ℤ)
y : Multiplicative ℤ
hx : x ≠ 0
⊢ x < ↑y * exp 1 ↔ x ≤ ↑y
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : Set β
f : β → α
⊢ DirectedOn r (f '' s) ↔ DirectedOn (f ⁻¹'o r) s

Tactic:
simp only [DirectedOn, Set.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, Order.Preimage]

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

Tactic:
by
    contrapose!
    rw [lt_ceil]
    obtain hb | hb := le_or_gt n b
    · obtain ⟨d, rfl⟩ := exists_add_of_le hb
      rw [Nat.cast_add, add_comm n, add_comm (n : R), add_lt_add_iff_right, add_lt_add_iff_right,
        lt_ceil]
    · exact iff_of_true (lt_add_of_nonneg_of_lt ha <| cast_lt.2 hb) (Nat.lt_add_left _ hb)

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s : Set α
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ↔ IsDirectedOrder ↑s

Tactic:
rw [directedOn_iff_directed, IsDirectedOrder]

Goal state after:
α : Type u_1
inst✝ : LE α
s : Set α
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) Subtype.val ↔ IsDirected ↑s fun x1 x2 ↦ x1 ≤ x2
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 using (le_ceil a).trans (le_add_of_nonneg_left zero_le_one)

Goal state after:
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
inst✝ : Invertible (a + b)
⊢ -(1 + 1) + 1 = ⅟b * a + ⅟a * b ↔ -1 + 0 = ⅟b * a + ⅟a * b

Tactic:
neg_add,

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ -1 + -1 + 1 = ⅟b * a + ⅟a * b ↔ -1 + 0 = ⅟b * a + ⅟a * b
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: case inr.inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ a < a + c + b

Tactic:
← hac,

Goal state after:
case inr.inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ a < 0 + b
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
wf : WellFounded r
inst✝ : Nonempty α
h : Relator.RightTotal r
a b : α
ha : ¬r b a
hba : r b a
⊢ False

Tactic:
contradiction

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
wf : WellFounded (Function.swap r)
inst✝ : Nonempty α
h : Relator.LeftTotal r
a b : α
ha : ¬Function.swap r b a
hab : r a b
⊢ False

Tactic:
contradiction

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

Goal state before:
pp: case pos
α : 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

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:
· simp only [h, update_apply]
    aesop

Goal state after:
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
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
heq : ¬a ≤ b
contra : ¬c ≤ d
⊢ False

Tactic:
contradiction

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
x x' : α
h : x = x'
⊢ x = termg 1 x' 0

Tactic:
simp [termg, h]

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

Goal state before:
pp: case neg
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
hl : ¬l = []
⊢ drop l.length (a :: l) = [(a :: l).getLast h]

Tactic:
List.drop_length_cons hl a

Goal state after:
case neg
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
hl : ¬l = []
⊢ [l.getLast hl] = [(a :: l).getLast h]
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : p a = true
⊢ q b = true

Tactic:
rwa [← hpq h₁]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : ¬p a = true
⊢ ¬q b = true

Tactic:
rwa [← hpq h₁]

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

Goal state before:
pp: case nil
M : Type u_4
inst✝¹ : Monoid M
inst✝ : Inhabited M
h : [] ≠ []
⊢ [].headI * [].tail.prod = [].prod

Tactic:
contradiction

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
⊢ zpow' a (m + n) = zpow' a m * zpow' a n

Tactic:
by_cases ha : a = 0
  · simp [zpow', ha]
    by_cases hn : n = 0
    · simp +contextual [hn, zero_zpow]
    · simp +contextual [hn, zero_zpow]
  · simp [zpow', ha, zpow_add₀]

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

Goal state before:
pp: α : Type u
x y : α
x✝ : x ∈ [].getLast?
⊢ x ∈ [y].getLast?

Tactic:
contradiction

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

Goal state before:
pp: α : Type u
l₁ : List α
hl₂ : [] ≠ []
⊢ (l₁ ++ []).getLast? = [].getLast?

Tactic:
contradiction

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : Semiring M
x₁ x₂ X₁ X₂ Y y a : M
h₁ : x₁ = a * X₁
h₂ : x₂ = a * X₂
H_atom : X₁ + X₂ = Y
hy : a * Y = y
⊢ x₁ + x₂ = y

Tactic:
by
  subst h₁ h₂ H_atom hy
  simp [mul_add]

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

Goal state before:
pp: case nil
α : Type u
inst✝ : Inhabited α
t : List α
h : [] ≠ []
⊢ ([] ++ t).head! = [].head!

Tactic:
contradiction

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

Goal state before:
pp: α : Type u
a : α
h : a ∈ [].head?
⊢ a :: [].tail = []

Tactic:
contradiction

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

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
h : [] ≠ []
⊢ [].head! ∈ [].head?

Tactic:
contradiction

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

Goal state after:
case nil
α : Type u_2
i : ℕ
⊢ take (take i (map length [])).sum [].flatten = (take i []).flatten

case cons
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), take (take i (map length tail✝)).sum tail✝.flatten = (take i tail✝).flatten
i : ℕ
⊢ take (take i (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten = (take i (head✝ :: tail✝)).flatten
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

Goal state after:
case nil
α : Type u_2
i : ℕ
⊢ drop (take i (map length [])).sum [].flatten = (drop i []).flatten

case cons
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), drop (take i (map length tail✝)).sum tail✝.flatten = (drop i tail✝).flatten
i : ℕ
⊢ drop (take i (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten = (drop i (head✝ :: tail✝)).flatten
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
hqd : ↑q.den ≠ 0
hrd : ↑r.den ≠ 0
| q.num /. ↑q.den + r.num /. ↑r.den

Tactic:
divInt_add_divInt _ _ hqd hrd

Goal state after:
q r : ℚ
hqd : ↑q.den ≠ 0
hrd : ↑r.den ≠ 0
| (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case mp
qr : ℚ
⊢ IsSquare (qr.num * qr.num) ∧ IsSquare (qr.den * qr.den)

Tactic:
simp only [IsSquare.mul_self, and_self]

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

Goal state before:
pp: q r : ℚ
⊢ (q + r).num * ↑q.den * ↑r.den = (q.num * ↑r.den + r.num * ↑q.den) * ↑(q + r).den

Tactic:
let s := divInt (q.num * r.den + r.num * q.den) (q.den * r.den : ℤ)

Goal state after:
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
⊢ (q + r).num * ↑q.den * ↑r.den = (q.num * ↑r.den + r.num * ↑q.den) * ↑(q + r).den
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
⊢ ↑(divNat a b) = ↑a / ↑b

Tactic:
rcases e : divNat a b with ⟨⟨n, d, h, c⟩, hn⟩
  rw [← Rat.num_nonneg] at hn
  lift n to ℕ using hn
  have hd : (d : α) ≠ 0 := by
    refine fun hd ↦ hb ?_
    have : Rat.divInt a b = _ := congr_arg NNRat.cast e
    obtain ⟨k, rfl⟩ : d ∣ b := by simpa [Int.natCast_dvd_natCast, this] using Rat.den_dvd a b
    simp [*]
  have hb' : b ≠ 0 := by rintro rfl; exact hb Nat.cast_zero
  simp_rw [Rat.mk_eq_divInt, mk_divInt, divNat_inj hb' h] at e
  rw [cast_def]
  dsimp
  rw [Commute.div_eq_div_iff _ hd hb]
  · norm_cast
    rw [e]
  exact b.commute_cast _

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

Goal state before:
pp: n✝¹ num✝ n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsNNRat (NNRat.divNat ↑n✝¹ ↑n✝) num✝ denom✝

Tactic:
by rw [NNRat.divNat_eq_div]; exact ⟨_, h⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a : α
n d : ℕ
⊢ IsNNRat a n.succ d → IsNNRat a⁻¹ d n.succ

Tactic:
by
  rintro ⟨_, rfl⟩
  have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))
  exact ⟨this, by simp⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
a : α
n d : ℕ
⊢ IsRat a (Int.ofNat n.succ) d → IsRat a⁻¹ (Int.ofNat d) n.succ

Tactic:
by
  rintro ⟨_, rfl⟩
  have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))
  exact ⟨this, by simp⟩

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
this : ↑b = 0
⊢ False

Tactic:
contradiction

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
⊢ (if h : p i then f i h else g i h) = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h

Tactic:
split_ifs with h <;> simp [h]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
g : ((i : ι) → κ i) → ι
h : (a : ι) → κ a
hh : ∀ (a : ι) (f : (i : ι) → κ i) (h_1 : a = g f), h_1 ▸ h a ≠ f (g f)
this : ⋯ ▸ h (g h) ≠ h (g h)
⊢ False

Tactic:
contradiction

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

Goal state before:
pp: α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : ⋃ i, Es i = univ
Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
⊢ x ∈ (⋃ i ∈ I, Es i)ᶜ ↔ x ∈ ⋃ i ∈ Iᶜ, Es i

Tactic:
obtain ⟨i, hix⟩ : ∃ i, x ∈ Es i := by simp [← mem_iUnion, Es_union]

Goal state after:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : ⋃ i, Es i = univ
Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
⊢ x ∈ (⋃ i ∈ I, Es i)ᶜ ↔ x ∈ ⋃ i ∈ Iᶜ, Es i
Module: Mathlib.Data.Set.Order

Goal state before:
pp: α : Type u
β : Type v
s : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ AntitoneOn f s ↔ Antitone fun a ↦ f ↑a

Tactic:
by
  simp [Antitone, AntitoneOn]

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
h : a < sSup s
⊢ ∃ b ∈ s, a < b

Tactic:
contrapose! h
  exact csSup_le' h

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s t : Set α
hs : BddAbove s
ht : BddAbove t
⊢ sSup (s ∪ t) = max (sSup s) (sSup t)

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hne)

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
t : Set α
ht : BddAbove t
hs : BddAbove ∅
⊢ sSup (∅ ∪ t) = max (sSup ∅) (sSup t)

case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s t : Set α
hs : BddAbove s
ht : BddAbove t
hne : s.Nonempty
⊢ sSup (s ∪ t) = max (sSup s) (sSup t)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
ha : none ∈ s
⊢ none ≤ ↑(sSup ((fun a ↦ ↑a) ⁻¹' s))

Tactic:
contradiction

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

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

Tactic:
rw [coe_sSup' hb, sSup_image]

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝¹ : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
⊢ s.Pairwise (r on f) ↔ ∃ z, ∀ (x : α), x ∈ s → r (f x) z

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hne)

Goal state after:
case inl
α : Type u_1
ι : Type u_4
inst✝¹ : Nonempty ι
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
⊢ ∅.Pairwise (r on f) ↔ ∃ z, ∀ (x : α), x ∈ ∅ → r (f x) z

case inr
α : Type u_1
ι : Type u_4
inst✝¹ : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
hne : s.Nonempty
⊢ s.Pairwise (r on f) ↔ ∃ z, ∀ (x : α), x ∈ s → r (f x) z
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: case inr
α : Type u_1
s : Set α
inst✝ : Preorder α
hs : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
x y : α
hx : x ∈ s
hy : y ∈ s
h : ¬x < y
h' : y ≤ x
⊢ y ≤ x

Tactic:
exact h'

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
⊢ f a * f b ≤ f (a * c)

Tactic:
mul

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
⊢ f a * f b ≤ f a * f c