mathlib-initiative/mathlib-tactics huggingface dataset:
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:
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.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b - c
⊢ a ∣ b ↔ a ∣ c

Tactic:
by
  rw [← sub_add_cancel b c, dvd_add_right h]

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

Goal state before:
pp: u v : ℤˣ
⊢ u ≠ v ↔ u = -v

Tactic:
simpa only [Ne, Units.ext_iff] using! isUnit_ne_iff_eq_neg u.isUnit v.isUnit

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

Goal state before:
pp: case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |a ^ (n + 1) - b ^ (n + 1)| ≤ |a - b| * ↑(n + 1) * max |a| |b| ^ (n + 1 - 1)

Tactic:
rw [Nat.add_sub_cancel, pow_sub_pow_eq_sub_mul_geomSum, abs_mul, mul_assoc, Nat.cast_succ]

Goal state after:
case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |a - b| * |geomSum a b n| ≤ |a - b| * ((↑n + 1) * max |a| |b| ^ n)
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
y : ↑(⇑e '' s)
⊢ e.symm ↑y ∈ s

Tactic:
by
      rcases y with ⟨-, ⟨a, ⟨m, rfl⟩⟩⟩
      simpa using m

Goal state after:
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:
by
  rw [← Ico_sdiff_left, sdiff_union_self,
    union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Ico.2 hab)]

Goal state after:
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
⊢ InjOn (Sum.elim f g) (sumEquiv.symm s)

Tactic:
rintro (a₁ | b₁) h₁ (a₂ | b₂) h₂ heq

Goal state after:
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
a₁ : α
h₁ : Sum.inl a₁ ∈ sumEquiv.symm s
a₂ : α
h₂ : Sum.inl a₂ ∈ sumEquiv.symm s
heq : Sum.elim f g (Sum.inl a₁) = Sum.elim f g (Sum.inl a₂)
⊢ Sum.inl a₁ = Sum.inl a₂

case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
a₁ : α
h₁ : Sum.inl a₁ ∈ sumEquiv.symm s
b₂ : β
h₂ : Sum.inr b₂ ∈ sumEquiv.symm s
heq : Sum.elim f g (Sum.inl a₁) = Sum.elim f g (Sum.inr b₂)
⊢ Sum.inl a₁ = Sum.inr b₂

case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
b₁ : β
h₁ : Sum.inr b₁ ∈ sumEquiv.symm s
a₂ : α
h₂ : Sum.inl a₂ ∈ sumEquiv.symm s
heq : Sum.elim f g (Sum.inr b₁) = Sum.elim f g (Sum.inl a₂)
⊢ Sum.inr b₁ = Sum.inl a₂

case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
b₁ : β
h₁ : Sum.inr b₁ ∈ sumEquiv.symm s
b₂ : β
h₂ : Sum.inr b₂ ∈ sumEquiv.symm s
heq : Sum.elim f g (Sum.inr b₁) = Sum.elim f g (Sum.inr b₂)
⊢ Sum.inr b₁ = Sum.inr b₂
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
hs : Nonempty ↑s
ht : Nonempty ↑t
x✝ : α × β
⊢ x✝ ∈ upperBounds (s ×ˢ t) ↔ x✝ ∈ upperBounds s ×ˢ upperBounds t

Tactic:
aesop (add simp [upperBounds, Prod.le_def, forall_and])

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
h : 1 / a < 1 / b
⊢ b < a

Tactic:
by
  simpa using one_div_lt_one_div_of_lt (by simpa) h

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Mul M
inst✝ : One M
l : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
base : ∀ (x : M), x ∈ l → p x
⊢ p l.prod

Tactic:
induction l with
  | nil => simpa
  | cons a l ih =>
    rw [List.prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at base
    exact hom _ _ (base.1) (ih base.2)

Goal state after:
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
⊢ (na.mul ↑db).add ((-nb).mul ↑da) = (↑k).mul nc

Tactic:
rw [show Int.mul (-nb) _ = _ from neg_mul ..]

Goal state after:
α : 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
⊢ (na.mul ↑db).add (-(nb * ↑da)) = (↑k).mul nc
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: α : Type u
n : ℕ
x : α
⊢ Injective fun l ↦ l.insertIdx n x

Tactic:
intro l₁

Goal state after:
α : Type u
n : ℕ
x : α
l₁ : List α
⊢ ∀ ⦃a₂ : List α⦄, (fun l ↦ l.insertIdx n x) l₁ = (fun l ↦ l.insertIdx n x) a₂ → l₁ = a₂
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₁

Goal state after:
case mpr.slnil
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
l₁ : List α
⊢ Forall₂ R l₁ [] → SublistForall₂ R l₁ []
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mpr.cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ (a✝¹ :: l₂✝)

Tactic:
intro l₁

Goal state after:
case mpr.cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
l₁ : List α
⊢ Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ (a✝¹ :: l₂✝)
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mpr.cons_cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ (a✝¹ :: l₁✝) → SublistForall₂ R l₁ (a✝¹ :: l₂✝)

Tactic:
intro l₁

Goal state after:
case mpr.cons_cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
l₁ : List α
⊢ Forall₂ R l₁ (a✝¹ :: l₁✝) → SublistForall₂ R l₁ (a✝¹ :: l₂✝)
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ l1 : List γ
h1 : Forall₂ (fun a c ↦ R a (f c)) l₁ l1
h2 : l1 <+ l₂
⊢ Forall₂ R l₁ (map f l1) ∧ map f l1 <+ map f l₂

Tactic:
simp [h1, h2.map]

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

Goal state before:
pp: case mp
α : Type u_1
a c : List α
⊢ (Perm ∘r Perm) a c → a ~ c

Tactic:
exact fun ⟨b, hab, hba⟩ => Perm.trans hab hba

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

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

Tactic:
rcases o₂ with - | b

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

case none.some
α : Type u_1
b : α
p : none.toList ~ (some b).toList
⊢ none = some b
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case some
α : Type u_1
o₂ : Option α
a : α
p : (some a).toList ~ o₂.toList
⊢ some a = o₂

Tactic:
rcases o₂ with - | b

Goal state after:
case some.none
α : Type u_1
a : α
p : (some a).toList ~ none.toList
⊢ some a = none

case some.some
α : Type u_1
a b : α
p : (some a).toList ~ (some b).toList
⊢ some a = some b
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: ⊢ 0 ≠ 1

Tactic:
rw [ne_comm, ← divInt_one_one, divInt_ne_zero] <;> lia

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

Goal state before:
pp: α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ p x → Forall p l → q x ∧ Forall q l

Tactic:
rw [← and_imp]

Goal state after:
α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ p x ∧ Forall p l → q x ∧ Forall q l
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
hq : q ≠ 0
⊢ (mkRat (↑q.den) q.num).den = q.num

Tactic:
← Rat.mk_eq_mkRat _ _ (num_ne_zero.mpr hq)

Goal state after:
q : ℚ≥0
hq : q ≠ 0
⊢ { num := ↑q.den, den := q.num, den_nz := ⋯, reduced := ?m.26 }.den = q.num

q : ℚ≥0
hq : q ≠ 0
⊢ (↑q.den).natAbs.Coprime q.num
Module: Mathlib.Tactic.NormNum.Inv

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

Tactic:
by
  rintro ⟨_, rfl⟩
  simp only [Int.negOfNat_eq]
  have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))
  generalize Nat.succ n = n at *
  use this; simp only [Int.ofNat_eq_natCast, Int.cast_neg,
    Int.cast_natCast, invOf_eq_inv, inv_neg, neg_mul, mul_inv_rev, inv_inv]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: $u✝ «$u» : Lean.Level
«$α» : Type u
«$sα» : CommSemiring «$α»
«$a» : «$α»
«$b» : ℕ
$expr✝ : «$α»
«$pf» : Nat.rawCast 1 = $expr✝
⊢ «$a» ^ «$b» * Nat.rawCast 1 = «$a» ^ «$b» * $expr✝

Tactic:
by rw [← pf]

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

Goal state before:
pp: case inr
R : Type u
inst✝⁶ : NonUnitalNonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hba : b ≤ a
⊢ (a - b) * c = a * c - b * c

Tactic:
apply h.eq_tsub_of_add_eq
    rw [← add_mul, tsub_add_cancel_of_le hba]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
b c k : ℕ
d e : R
x✝² : b = c * k
x✝¹ : a ^ c = d
x✝ : d ^ k = e
⊢ a ^ b = e

Tactic:
subst_vars; simp [pow_mul]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a a' : R
p : a = a'
e : ℕ
hone : Nat.rawCast 1 = e
⊢ a = a' ^ e * Nat.rawCast 1

Tactic:
by simp [← hone, *]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
a b x✝ : α
h : sInf {c | a ≤ b ⊔ c} ≤ x✝
⊢ a ≤ b ⊔ sInf {c | a ≤ b ⊔ c}

Tactic:
simp [minAx.sup_sInf_eq]

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

Goal state before:
pp: α : Type u_1
s : Set (Set α)
⊢ ⋂₀ s = ⋂ i, ↑i

Tactic:
simp only [← sInter_range, Subtype.range_coe]

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:
simp_rw [← exists_prop, ← iSup_Prop_eq, iSup_sUnion]

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

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

Tactic:
rintro ⟨z, hz⟩ x hx y hy _
    exact @IsTrans.trans α r _ (f x) z (f y) (hz _ hx) (symm <| hz _ hy)

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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α}, b ∈ [[a, c]] → a ≤ c → Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ Ι c b ∪ Ι b a = Ι a c

Tactic:
this _ (le_of_not_ge hac),

Goal state after:
case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α}, b ∈ [[a, c]] → a ≤ c → Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ Ι c a = Ι a c

α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α}, b ∈ [[a, c]] → a ≤ c → Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ b ∈ [[c, a]]
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z = x
⊢ z ∈ s

Tactic:
hz

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z = x
⊢ x ∈ s
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
s : Set α
a : α
inst✝ : Preorder α
⊢ s = {a} → IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s ∧ IsGreatest s a

Tactic:
by
    rintro rfl
    exact ⟨IsAntichain.singleton, isGreatest_singleton⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : Lattice α
inst✝ : IsOrderedRing α
a : α
na : ℕ
pa : IsInt a (Int.negOfNat na)
⊢ IsNat |a| na

Tactic:
rw [pa.out]
  constructor
  simp

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case neg
n k : ℕ
h : ¬n < k
⊢ n.descFactorial k = (n - k + 1).ascFactorialBinary k

Tactic:
rw [← ascFactorial_eq_ascFactorialBinary, ← add_descFactorial_eq_ascFactorial']
    grind

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

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
q : ℚ≥0
⊢ 0 < ↑q.den

Tactic:
simpa only [Int.natCast_pos] using q.den_pos

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

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x - ↑y) = round x - y

Tactic:
rw [sub_eq_add_neg]

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x + -↑y) = round x - y
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: m k : ℕ+
h₀ : 0 = ↑m
hr : ↑m % ↑k = 0
hq : ↑m / ↑k = 0
⊢ False

Tactic:
exact (m.ne_zero h₀.symm).elim

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
inst✝ : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ ↑⌊a⌋ = a - b

Tactic:
hz

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ ↑⌊a⌋ = ↑z
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
b : H
inst✝² : AddMonoidWithOne G
inst✝¹ : AddMonoid H
inst✝ : AddConstMapClass F G H 1 b
f : F
n : ℕ
⊢ f ↑n = f 0 + n • b

Tactic:
simpa using map_add_nat' f 0 n

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
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
this : ↑⌈a⌉ = ↑⌊a⌋ + 1
⊢ fract a = a + 1 - ↑⌈a⌉

Tactic:
by
    rw [this, ← self_sub_fract]
    abel

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

Goal state before:
pp: K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ m, y ^ m ≤ x
⊢ ∃ b, ∀ (m : ℤ), y ^ m ≤ x → m ≤ b

Tactic:
obtain ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy

Goal state after:
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ m, y ^ m ≤ x
M : ℕ
hM : x < y ^ M
⊢ ∃ b, ∀ (m : ℤ), y ^ m ≤ x → m ≤ b
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
h : ¬a ∈ s
⊢ count a s = 0

Tactic:
· exact count_eq_zero_of_notMem h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
hts : t ≤ s
⊢ s - t + t = s

Tactic:
by
  ext a; simp [Nat.sub_add_cancel <| count_le_of_le _ hts]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs₀ bs₁ : Multiset β
h : ∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs'
h₁ : Rel r as₁ bs₁
⊢ ∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs₀ + bs₁ = b ::ₘ bs'

Tactic:
rcases h with ⟨b, bs, hab, h₀, rfl⟩

Goal state after:
case mpr
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs₁ : Multiset β
h₁ : Rel r as₁ bs₁
b : β
bs : Multiset β
hab : r a b
h₀ : Rel r s bs
⊢ ∃ b_1 bs', r a b_1 ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ b ::ₘ bs + bs₁ = b_1 ::ₘ bs'
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h₁ : s ≤ u
h₂ : t ≤ u
⊢ s ∪ t ≤ u

Tactic:
by
  rw [← eq_union_left h₂]; exact union_le_union_right h₁ t

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

Goal state before:
pp: α : Type u_2
s t : Finset α
⊢ Disjoint ↑s ↑t ↔ Disjoint s t

Tactic:
by
  simp only [Finset.disjoint_left, Set.disjoint_left, mem_coe]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
x : Bool
⊢ x ∈ { val := {true, false}, nodup := fintype._proof_1 }

Tactic:
by cases x <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
x : Ordering
⊢ x ∈ { val := {lt, eq, gt}, nodup := fintype._proof_1 }

Tactic:
by cases x <;> simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ map (Embedding.subtype p) univ = map (Embedding.subtype p) (Finset.subtype p univ)

Tactic:
subtype_univ

Goal state after:
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ map (Embedding.subtype p) univ = map (Embedding.subtype p) univ
Module: Mathlib.Data.Fin.Embedding

Goal state before:
pp: n m : ℕ
hmn : n ≤ m
y : Fin m
x✝ : y ∈ Set.range ⇑((addNatEmb (m - n)).trans (finCongr ⋯).toEmbedding)
x : Fin n
hx : ((addNatEmb (m - n)).trans (finCongr ⋯).toEmbedding) x = y
⊢ y ∈ {i | m ≤ ↑i + n}

Tactic:
simp [← hx]; lia

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
k : Fin n
⊢ k = 0 → k ≤ 0

Tactic:
by rintro rfl; exact Nat.le_refl _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : α → β
hi : Set.MapsTo i ↑s ↑t
i_inj : Set.InjOn i ↑s
i_surj : Set.SurjOn i ↑s ↑t
⊢ ∀ b ∈ t, ∃ a, ∃ (_ : a ∈ s), i a = b

Tactic:
by simpa using! i_surj

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
⊢ Injective p.succAbove

Tactic:
by
  rintro i j hij
  unfold succAbove at hij
  split_ifs at hij with hi hj hj
  · exact castSucc_injective _ hij
  · rw [hij] at hi
    cases hj <| Nat.lt_trans j.castSucc_lt_succ hi
  · rw [← hij] at hj
    cases hi <| Nat.lt_trans i.castSucc_lt_succ hj
  · exact succ_injective _ hij

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

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
⊢ P (f n)

Tactic:
induction n using Nat.strong_induction_on with | _ n IH
       =>  _ 

Goal state after:
case h
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ m < n, P (f m)
⊢ P (f n)
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
t : Finset β
inst✝ : DecidableEq β
hf : Set.InjOn f ↑s
hf' : Set.MapsTo f ↑s ↑t
h : #t = #s + 1
⊢ ∃! x, x ∈ t ∧ x ∉ image f s

Tactic:
have : #(t \ s.image f) = 1 := by
    grind [card_sdiff_of_subset hf'.finsetImage_subset, card_image_of_injOn hf]

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
t : Finset β
inst✝ : DecidableEq β
hf : Set.InjOn f ↑s
hf' : Set.MapsTo f ↑s ↑t
h : #t = #s + 1
this : #(t \ image f s) = 1
⊢ ∃! x, x ∈ t ∧ x ∉ image f s
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 2 + 1 ≤ #s ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
le_card_iff_exists_subset_card,

Goal state after:
α : Type u_1
s : Finset α
⊢ (∃ t ⊆ s, #t = 2 + 1) ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 3 + 1 ≤ #s ↔ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
le_card_iff_exists_subset_card,

Goal state after:
α : Type u_1
s : Finset α
⊢ (∃ t ⊆ s, #t = 3 + 1) ↔ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: case refine_1.cons_mem
α : Type u_1
l : List α
x : α
hm : x ∈ l
⊢ x = x ∧ x ∈ l ∨ x ∈+ l

Tactic:
exact Or.inl ⟨rfl, hm⟩

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

Goal state before:
pp: case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : j = i
⊢ init (update q i.castSucc y) j = update (init q) i y j

pp: case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : ¬j = i
⊢ init (update q i.castSucc y) j = update (init q) i y j

Tactic:
· rw [h]
    simp [init]

Goal state after:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : ¬j = i
⊢ init (update q i.castSucc y) j = update (init q) i y j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
β : Sort u_2
q : Fin (n + 2) → β
⊢ tail (init q) = init (tail q)

Tactic:
by
  ext i
  simp [tail, init]

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
hsn : Fintype.card α = #s
f : α ↪ β
hf : Set.range ⇑f ⊆ ↑s
⊢ map f univ = s

Tactic:
apply Finset.eq_of_subset_of_card_le

Goal state after:
case h.h
α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
hsn : Fintype.card α = #s
f : α ↪ β
hf : Set.range ⇑f ⊆ ↑s
⊢ map f univ ⊆ s

case h.h₂
α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
hsn : Fintype.card α = #s
f : α ↪ β
hf : Set.range ⇑f ⊆ ↑s
⊢ #s ≤ #(map f univ)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
h : s.Finite
⊢ ∃ s', ∀ (a : α), a ∈ s' ↔ a ∈ s

Tactic:
by
  cases h.nonempty_fintype
  exact ⟨s.toFinset, fun _ => mem_toFinset⟩

Goal state after: