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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
⊢ a + -a = 0

Tactic:
by simp [ha, add_neg_cancel_of_ne_top]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
h : a + b = 0
⊢ -a = b

Tactic:
have ha : a ≠ ⊤ := by rintro rfl; simp at h
    exact left_neg_eq_right_neg (a := a) (by simp [neg_add_cancel_of_ne_top, *]) h

Goal state after:
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:
simp only [← succ_le_iff, le_find_iff, succ_le_succ_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Mul α
inst✝ : MulLeftMono α
⊢ MulLeftMono (WithZero α)

Tactic:
refine ⟨fun a b c hbc => ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a✝ b✝ : α
inst✝¹ : Mul α
inst✝ : MulLeftMono α
a b c : WithZero α
hbc : b ≤ c
⊢ a * b ≤ a * c
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
⊢ AddLeftMono (WithZero α)

Tactic:
refine ⟨fun a b c hbc => ?_⟩

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a b c : WithZero α
hbc : b ≤ c
⊢ a + b ≤ a + c
Module: Mathlib.Algebra.Order.Floor.Semiring

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

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

Tactic:
simp only [← pow_succ, ← two_mul, ← mul_assoc]

Goal state after:
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))
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
c n : ℤ
x a : α
n' : ℤ
a' : α
h₁ : c * n = n'
h₂ : smulg c a = a'
⊢ smulg c (termg n x a) = termg n' x a'

Tactic:
by
  simp [h₂.symm, h₁.symm, termg, smulg, zsmul_add, mul_zsmul]

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
⊢ ∃ b' ∈ Set.Ico 0 b, c < a * b'

Tactic:
have hb : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha
  simp_rw [mul_comm a] at h ⊢
  exact exists_lt_mul_left_of_nonneg hb.le hc h

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

Goal state before:
pp: case inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab✝¹ : d < a * b
hd : 0 ≤ d
a' : α
ha' : a' ∈ Set.Ico 0 a
d_ab✝ : d < a' * b
b' : α
hb' : b' ∈ Set.Ico 0 b
d_ab : d < a' * b'
⊢ d ≤ c

Tactic:
exact d_ab.le.trans (h a' ha'.1 ha'.2 b' hb'.1 hb'.2)

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ |1 / a| = 1 / |a|

Tactic:
abs_div,

Goal state after:
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ |1| / |a| = 1 / |a|
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case e_tail
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
ih : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ tail✝¹ = tail✝

Tactic:
· apply ih; simpa using hl

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

Goal state before:
pp: α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
⊢ map f l₁ ⊆ map f l₂ ↔ l₁ ⊆ l₂

Tactic:
refine ⟨?_, map_subset f⟩

Goal state after:
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
⊢ map f l₁ ⊆ map f l₂ → l₁ ⊆ l₂
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
⊢ (map f []).prod = f a ^ count a []

Tactic:
rw [map_nil, prod_nil, count_nil, _root_.pow_zero]

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

Goal state before:
pp: L : List ℕ
⊢ L.tail.sum = L.sum - L.headI

Tactic:
rw [← headI_add_tail_sum L, add_comm, Nat.add_sub_cancel_right]

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

Goal state before:
pp: α : Type u
l₁ l₂ l : List α
p : l₁ ~ l₂
⊢ l₁.Disjoint l ↔ l₂.Disjoint l

Tactic:
by
  simp_rw [List.disjoint_left, p.mem_iff]

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

Goal state before:
pp: q : ℚ≥0
⊢ ↑q.num / ↑q.den = q

Tactic:
ext1
  rw [coe_div, coe_natCast, coe_natCast, num, ← Int.cast_natCast]
  exact (cast_def _).symm

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

Goal state before:
pp: h : nil ≠ nil
⊢ node () nil.left nil.right = nil

Tactic:
trivial

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
a✝ b✝ c✝ : PUnit
⊢ a✝ ≤ b✝ ⇨ c✝ ↔ min a✝ b✝ ≤ c✝

Tactic:
trivial

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
a✝ : PUnit
⊢ a✝ ⇨ ⊥ = a✝ᶜ

Tactic:
trivial

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
a✝ b✝ c✝ : PUnit
⊢ a✝ \ b✝ ≤ c✝ ↔ a✝ ≤ max b✝ c✝

Tactic:
trivial

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
a✝ : PUnit
⊢ ⊤ \ a✝ = ￢a✝

Tactic:
trivial

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : Unique ι
f : ι → α
⊢ ⨆ i, f i = f default

Tactic:
by
  simp only [congr_arg f (Unique.eq_default _), iSup_const]

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
β : α → Type u_9
inst✝ : (i : α) → CompleteLattice (β i)
x✝¹ : Set ((i : α) → β i)
x✝ : α
⊢ IsLUB (eval x✝ '' x✝¹) (sSup x✝¹ x✝)

Tactic:
rw [sSup_apply_eq_sSup_image]

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
β : α → Type u_9
inst✝ : (i : α) → CompleteLattice (β i)
x✝¹ : Set ((i : α) → β i)
x✝ : α
⊢ IsLUB (eval x✝ '' x✝¹) (sSup (eval x✝ '' x✝¹))
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
h : ∃ x, rhs < x ∧ x < lhs
⊢ lhs ≤ rhs

Tactic:
then

Goal state after:
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
h : ∃ x, rhs < x ∧ x < lhs
⊢ lhs ≤ rhs
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : ↑(⋃ i, t i)
| ↑((unionEqSigmaOfDisjoint h) x).snd = ↑x

Tactic:
right; rw [← unionEqSigmaOfDisjoint h |>.symm_apply_apply x]

Goal state after:
α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : ↑(⋃ i, t i)
| ↑((unionEqSigmaOfDisjoint h).symm ((unionEqSigmaOfDisjoint h) x))
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → ConditionallyCompleteLattice (α i)
x✝¹ : Set ((i : ι) → α i)
hn : x✝¹.Nonempty
hb : BddAbove x✝¹
x✝ : ι
⊢ IsLUB (eval x✝ '' x✝¹) (sSup x✝¹ x✝)

Tactic:
rw [sSup_apply_eq_sSup_image]

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → ConditionallyCompleteLattice (α i)
x✝¹ : Set ((i : ι) → α i)
hn : x✝¹.Nonempty
hb : BddAbove x✝¹
x✝ : ι
⊢ IsLUB (eval x✝ '' x✝¹) (sSup (eval x✝ '' x✝¹))
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

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

pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ⊤ ∈ upperBounds s

Tactic:
· rintro (⟨⟩ | a) ha
      · contradiction
      apply coe_le_coe.2
      exact le_csSup h₂ ha

Goal state after:
case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ⊤ ∈ upperBounds s
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s)) ∈ lowerBounds s

Tactic:
rintro (⟨⟩ | a) ha
      · exact le_top
      refine coe_le_coe.2 (csInf_le ?_ ha)
      rcases hs with ⟨⟨⟩ | b, hb⟩
      · exfalso
        apply h
        intro c hc
        rw [mem_singleton_iff, ← top_le_iff]
        exact hb hc
      use b
      intro c hc
      exact coe_le_coe.1 (hb hc)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : ∅ ⊆ t
h : ∀ y ∈ t, ∃ x ∈ ∅, x ≤ y
⊢ t = ∅

Tactic:
by simpa [Set.eq_empty_iff_forall_notMem] using h

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : ∅ ⊆ t
h : ∀ y ∈ t, ∃ x ∈ ∅, x ≤ y
⊢ sInf (f '' ∅) = sInf (f '' t)

pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ sInf (f '' s) = sInf (f '' t)

Tactic:
· obtain rfl : t = ∅ := by simpa [Set.eq_empty_iff_forall_notMem] using h
    rfl

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ sInf (f '' s) = sInf (f '' t)
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : Set ι
f : ι → α
hs : s.PairwiseDisjoint f
g : ι → ι
hg : f ∘ g ≤ f
⊢ (g '' s).PairwiseDisjoint f

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ h
  exact (hs ha hb <| ne_of_apply_ne _ h).mono (hg a) (hg b)

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
h : ∃ t, IsChain r s ∧ SuperChain r s t
⊢ IsChain r (SuccChain r s)

Tactic:
then

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
h : ∃ t, IsChain r s ∧ SuperChain r s t
⊢ IsChain r (SuccChain r s)
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
h : ∃ t, IsChain r s ∧ SuperChain r s t
⊢ s ⊆ SuccChain r s

Tactic:
then

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
h : ∃ t, IsChain r s ∧ SuperChain r s t
⊢ s ⊆ SuccChain r s
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
ht : t.Nonempty
h_bdd : BddAbove t
⊢ sSup (Subtype.val '' t) ∈ s

Tactic:
obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
h_bdd : BddAbove t
c : ↑s
hct : c ∈ t
⊢ sSup (Subtype.val '' t) ∈ s
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
ht : t.Nonempty
h_bdd : BddBelow t
⊢ sInf (Subtype.val '' t) ∈ s

Tactic:
obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
h_bdd : BddBelow t
c : ↑s
hct : c ∈ t
⊢ sInf (Subtype.val '' t) ∈ s
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ ⟨↑r, ⋯⟩ * ⟨(↑r)⁻¹, ⋯⟩ = 1

Tactic:
ext; simp [r.2.ne']

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ ⟨(↑r)⁻¹, ⋯⟩ * ⟨↑r, ⋯⟩ = 1

Tactic:
ext; simp [r.2.ne']

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f g : ι → M
x✝ : mulSupport f = mulSupport g ∧ ∀ (x : ι), x ∈ mulSupport f → f x = g x
h₁ : mulSupport f = mulSupport g
h₂ : ∀ (x : ι), x ∈ mulSupport f → f x = g x
x : ι
hx : x ∈ mulSupport f
⊢ f x = g x

Tactic:
then

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : One M
f g : ι → M
x✝ : mulSupport f = mulSupport g ∧ ∀ (x : ι), x ∈ mulSupport f → f x = g x
h₁ : mulSupport f = mulSupport g
h₂ : ∀ (x : ι), x ∈ mulSupport f → f x = g x
x : ι
hx : x ∈ mulSupport f
⊢ f x = g x
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ round x = ⌊x + 1 / 2⌋

Tactic:
← cast_mul_floor_div_cancel_of_pos two_pos,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ round x = ⌊↑2 * (x + 1 / 2)⌋ / 2
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case mp
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
z : ℤ
hz : -x = ↑z
⊢ ∃ z, x = ↑z

Tactic:
use -z

Goal state after:
case h
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
z : ℤ
hz : -x = ↑z
⊢ x = ↑(-z)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case mpr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
z : ℤ
hz : x = ↑z
⊢ ∃ z, -x = ↑z

Tactic:
use -z

Goal state after:
case h
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
z : ℤ
hz : x = ↑z
⊢ -x = ↑(-z)
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : ℚ
⊢ ↑(fract x) = fract ↑x

Tactic:
by
  simp only [fract, cast_sub, cast_intCast, floor_cast]

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
a : R
inst✝ : IsOrderedRing R
z : ℤ
⊢ ⌈-a⌉ ≤ z ↔ -⌊a⌋ ≤ z

Tactic:
by rw [neg_le, ceil_le, le_floor, Int.cast_neg, neg_le]

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

Goal state before:
pp: case e'_4
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this : 0 < a - 1
⊢ 1 / (1 - a⁻¹) = (a - 1)⁻¹ + 1

Tactic:
field

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
x y z : α
xz : x ≠ z
⊢ x ≠ y ∨ y ≠ z

Tactic:
exact not_and_or.1 <| mt (fun h ↦ h.1.trans h.2) xz

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∪ t + s ∩ t = s + t

Tactic:
apply _root_.le_antisymm

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∪ t + s ∩ t ≤ s + t

case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t ≤ s ∪ t + s ∩ t
Module: Mathlib.Data.Finset.Empty

Goal state before:
pp: α : Type u_1
a : α
⊢ ¬a ∈ ∅

Tactic:
by
  simp only [mem_def, empty_val, notMem_zero, not_false_iff]

Goal state after:
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
x✝ : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : ¬a ∈ s
⊢ s ≤ t

Tactic:
exact l

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
⊢ cons a s hs ⊆ cons a t ht ↔ s ⊆ t

Tactic:
rwa [← coe_subset, coe_cons, coe_cons, Set.insert_subset_insert_iff, coe_subset]

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ l.toFinset.Nonempty ↔ l ≠ []

Tactic:
by
  simp [Finset.nonempty_iff_ne_empty]

Goal state after:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ (s.erase a)ᶜ ↔ a✝ ∈ insert a sᶜ

Tactic:
simp only [or_iff_not_imp_left, mem_insert, not_and, mem_compl, mem_erase]

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

Goal state before:
pp: k l : ℕ
h : k = l
a b : Fin k
hab : Fin.cast h a = Fin.cast h b
⊢ a = b

Tactic:
by simpa [← val_eq_val] using hab

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

Goal state before:
pp: case inr
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
this : ∀ ⦃i j : Fin (n + 1)⦄, i.predAbove = j.predAbove → i < j → i = j
h : j ≤ i
⊢ i = j

pp: n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
h : i < j
⊢ i = j

Tactic:
· obtain h | rfl := h.lt_or_eq
    · exact (this hij.symm h).symm
    · rfl

Goal state after:
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
h : i < j
⊢ i = j
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin n.succ
hi : i ∈ Set.range castSucc
⊢ ↑((Equiv.ofInjective castSucc ⋯).symm ⟨i, hi⟩) = ↑i

Tactic:
rw [← val_castSucc]
  exact congr_arg val (Equiv.apply_ofInjective_symm _ _)

Goal state after:
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
this✝ : image f s = t
this : #(image f s) = #t
⊢ Set.InjOn f ↑s

Tactic:
have : #(s.image f) ≤ #s := card_image_le

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
this✝¹ : image f s = t
this✝ : #(image f s) = #t
this : #(image f s) ≤ #s
⊢ Set.InjOn f ↑s
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
m n : ℕ
a : Fin m → α
b : Fin n → α
⊢ ofFn (Fin.append a b) = ofFn a ++ ofFn b

Tactic:
simp_rw [ofFn_add]

Goal state after:
α : Type u
m n : ℕ
a : Fin m → α
b : Fin n → α
⊢ ((ofFn fun i ↦ Fin.append a b (Fin.castLE ⋯ i)) ++ ofFn fun i ↦ Fin.append a b (Fin.natAdd m i)) = ofFn a ++ ofFn b
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
m n : ℕ
f : Fin (m * n) → α
⊢ ofFn f = (ofFn fun i ↦ ofFn fun j ↦ f ⟨↑i * n + ↑j, ⋯⟩).flatten

Tactic:
induction m with

Goal state after:
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ #(filter p s ∪ {a ∈ s | ¬p a}) = #s

Tactic:
filter_union_filter_not_eq

Goal state after:
α : Type u_1
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ #s = #s
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
⊢ ∀ k < #t, n ≤ k → (∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k + 1) → ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k

Tactic:
intro k _ hnk ⟨u, hu₁, hu₂, hu₃⟩

Goal state after:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: α : Type u_1
l : List α
x : α
h : x ∈+ x :: l
⊢ x ∈ l

Tactic:
obtain h | h := h

Goal state after:
case cons_mem
α : Type u_1
l : List α
x : α
h : x ∈ l
⊢ x ∈ l

case cons_duplicate
α : Type u_1
l : List α
x : α
h : x ∈+ l
⊢ x ∈ l
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: P : (α : Type u_4) → [Fintype α] → Prop
α : Type u_4
inst✝ : Fintype α
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
⊢ P α

Tactic:
obtain ⟨n, hn⟩ : ∃ n, Fintype.card α = n := ⟨Fintype.card α, rfl⟩

Goal state after:
P : (α : Type u_4) → [Fintype α] → Prop
α : Type u_4
inst✝ : Fintype α
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
hn : card α = n
⊢ P α
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ card { i // ↑i < m } = m

Tactic:
by
  conv_rhs => rw [← Fintype.card_fin m]
  apply Fintype.card_congr
  exact { toFun := fun ⟨⟨i, _⟩, hi⟩ ↦ ⟨i, hi⟩
          invFun := fun ⟨i, hi⟩ ↦ ⟨⟨i, lt_of_lt_of_le hi h⟩, hi⟩ }

Goal state after:
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
hsn : Fintype.card α = #s
⊢ ∃ f, map f univ = s

Tactic:
obtain ⟨f : α ↪ β, hf⟩ := exists_of_card_le_finset (Nat.le_of_eq hsn)

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
hsn : Fintype.card α = #s
f : α ↪ β
hf : Set.range ⇑f ⊆ ↑s
⊢ ∃ f, map f univ = s
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
j : Fin (n + 1 + 1)
⊢ i.succ.insertNth x (cons a p) j = cons a (i.insertNth x p) j

Tactic:
cases j using Fin.succAboveCases i.succ with

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : a = b
⊢ R a b

Tactic:
then

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : a = b
⊢ R a b