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

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
⊢ (¬∃ x y, x ≠ y) ↔ IsRightRegular 0

Tactic:
isRightRegular_zero_iff_subsingleton,

Goal state after:
R : Type u_1
inst✝ : MulZeroClass R
⊢ (¬∃ x y, x ≠ y) ↔ Subsingleton R
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
⊢ Injective ⇑(map' f) ↔ Injective ⇑f

Tactic:
simp [Injective, WithZero.forall]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
⊢ 0 ≤ a - a

Tactic:
sub_self_eq_zero_of_ne_top ha

Goal state after:
case inr
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
⊢ 0 ≤ 0
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : b ≤ a
⊢ a - b + b = max a b

Tactic:
rw [max_eq_left h, tsub_add_cancel_of_le h]

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

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
ceil : α → ℤ
gc_ceil_coe : GaloisConnection ceil Int.cast
a : ℤ
z : α
⊢ ↑a ≤ z ↔ ceil (-z) ≤ -a

Tactic:
gc_ceil_coe,

Goal state after:
F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
ceil : α → ℤ
gc_ceil_coe : GaloisConnection ceil Int.cast
a : ℤ
z : α
⊢ ↑a ≤ z ↔ -z ≤ ↑(-a)
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp.coe
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
a b : α
hab : a < b
c : α
hc : ↑a < ↑c ∧ ↑c < ↑b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
exact ⟨c, by simpa using hc⟩

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp.coe
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
a b : α
hab : a < b
c : α
hc : ↑a < ↑c ∧ ↑c < ↑b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
exact ⟨c, by simpa using hc⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ |a| ≤ 1 ↔ a * a ≤ 1

Tactic:
simpa only [abs_one, one_mul] using abs_le_iff_mul_self_le (a := a) (b := 1)

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
o : ↑s ⊕ ↑t
⊢ (fun x ↦ if hp : p ↑x then Sum.inl ⟨↑x, ⋯⟩ else Sum.inr ⟨↑x, ⋯⟩)
      ((fun o ↦
          match o with
          | Sum.inl x => ⟨↑x, ⋯⟩
          | Sum.inr x => ⟨↑x, ⋯⟩)
        o) =
    o

Tactic:
rcases o with (⟨x, h⟩ | ⟨x, h⟩) <;> [simp [hs _ h]; simp [ht _ h]]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
β : Type u_4
inst✝ : Preorder β
s : Set (α × β)
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ IsCofinalFor ((Prod.fst '' s) ×ˢ (Prod.snd '' s)) s

Tactic:
rintro ⟨_, _⟩ ⟨⟨x, hx, rfl⟩, y, hy, rfl⟩

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
β : Type u_4
inst✝ : Preorder β
s : Set (α × β)
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
x : α × β
hx : x ∈ s
y : α × β
hy : y ∈ s
⊢ ∃ b ∈ s, (x.1, y.2) ≤ b
Module: Mathlib.Algebra.Order.Field.Basic

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

Tactic:
simpa using le_inv_comm₀ ha hb

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ a ≤ b / c ↔ b ≤ a * c

Tactic:
rw [← neg_neg c, mul_neg, div_neg, le_neg, div_le_iff₀ (neg_pos.2 hc), neg_mul]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
h1 : a < 0
h2 : -1 < a
this : 1 / a < 1 / -1
⊢ 1 / a < -1

Tactic:
one_div_neg_one_eq_neg_one

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
h1 : a < 0
h2 : -1 < a
this : 1 / a < -1
⊢ 1 / a < -1
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
h1 : a < 0
h2 : -1 ≤ a
this : 1 / a ≤ 1 / -1
⊢ 1 / a ≤ -1

Tactic:
one_div_neg_one_eq_neg_one

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
h1 : a < 0
h2 : -1 ≤ a
this : 1 / a ≤ -1
⊢ 1 / a ≤ -1
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a b c d : α
hc : c ≠ 0
hd : d ≠ 0
⊢ a / c - b / d ≤ 0 ↔ a / c ≤ b / d

Tactic:
sub_nonpos

Goal state after:
α : Type u_2
inst✝² : Field α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a b c d : α
hc : c ≠ 0
hd : d ≠ 0
⊢ a / c ≤ b / d ↔ a / c ≤ b / d
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
n : ℕ
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
⊢ Forall₂ R (take (n + 1) (a✝ :: l₁✝)) (take (n + 1) (b✝ :: l₂✝))

Tactic:
simp [And.intro h₁ h₂, forall₂_take n]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
p : l₁ ~ l₂
⊢ ∀ (b : β), foldr f b l₁ = foldr f b l₂

Tactic:
by
  intro b
  induction p using Perm.recOnSwap' generalizing b with
  | nil => rfl
  | cons _ _ r => simp [r b]
  | swap' _ _ _ r => simp only [foldr_cons]; rw [lcomm.left_comm, r b]
  | trans _ _ r₁ r₂ => exact Eq.trans (r₁ b) (r₂ b)

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

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
he : e ≠ 0
L l l' : NF M
h : L.eval * l.eval = l'.eval
⊢ ((n, e) ::ᵣ L).eval * ((-n, e) ::ᵣ l).eval = l'.eval

Tactic:
mul_eq_eval₂ n (-n) e h

Goal state after:
M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
he : e ≠ 0
L l l' : NF M
h : L.eval * l.eval = l'.eval
⊢ ((n + -n, e) ::ᵣ l').eval = l'.eval
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: q : ℚ
this : ↑q.den ≠ 0
⊢ q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1

Tactic:
rw [divInt_mul_divInt, mul_comm (q.den : ℤ) 1, divInt_mul_right this]

Goal state after:
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x z d : α
h : IsRelPrime (x * d) z
⊢ IsRelPrime x z

Tactic:
exact IsRelPrime.of_mul_left_left h

Goal state after:
Module: Mathlib.Algebra.Group.Commute.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ a⁻¹ * b * a = b

Tactic:
rw [h.inv_left.eq, inv_mul_cancel_right]

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 = ↑d * ↑k
⊢ False

Tactic:
d0,

Goal state after:
α : 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 * ↑k
⊢ False
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
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c } = ↑a / ↑b

Tactic:
rw [mk_eq_divInt] at e

Goal state after:
α : 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 = n /. ↑d
d0 : ↑d ≠ 0
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c } = ↑a / ↑b
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q : ℚ
⊢ (-q)⁻¹ = -q⁻¹

Tactic:
by
  rw [← num_divInt_den q]
  simp only [Rat.neg_divInt, Rat.inv_divInt, Rat.divInt_neg]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
⊢ (compl ∘ u ∘ compl) a ≤ b ↔ a ≤ (compl ∘ l ∘ compl) b

Tactic:
dsimp
  rw [le_compl_iff_le_compl, gc, compl_le_iff_compl_le]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
a b : β
⊢ ⨆ x ∈ {a, b}, f x = f a ⊔ f b

Tactic:
iSup_insert,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
a b : β
⊢ f a ⊔ ⨆ x ∈ {b}, f x = f a ⊔ f b
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
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
⊢ CompleteLattice α

Tactic:
let lattice := e.lattice

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
⊢ CompleteLattice α
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : CompleteBooleanAlgebra α
f g : ι → α
⊢ (⨆ i, f i) ∆ ⨆ i, g i ≤ ⨆ i, f i ∆ g i

Tactic:
simp_rw [symmDiff_le_iff, ← iSup_sup_eq]
  exact ⟨iSup_mono fun i ↦ sup_comm (g i) _ ▸ le_symmDiff_sup_right ..,
    iSup_mono fun i ↦ sup_comm (f i) _ ▸ symmDiff_comm (f i) _ ▸ le_symmDiff_sup_right ..⟩

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)

Tactic:
by_cases BddAbove (s ∪ t)

Goal state after:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
h✝ : BddAbove (s ∪ t)
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)

case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
h✝ : ¬BddAbove (s ∪ t)
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case left
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ sSup s ∈ upperBounds s

Tactic:
change ite _ _ _ ∈ _

Goal state after:
case left
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ (if ⊤ ∈ s then ⊤ else if BddAbove ((fun a ↦ ↑a) ⁻¹' s) then ↑(sSup ((fun a ↦ ↑a) ⁻¹' s)) else ⊤) ∈ upperBounds s
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case right
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ sSup s ∈ lowerBounds (upperBounds s)

Tactic:
change ite _ _ _ ∈ _

Goal state after:
case right
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ (if ⊤ ∈ s then ⊤ else if BddAbove ((fun a ↦ ↑a) ⁻¹' s) then ↑(sSup ((fun a ↦ ↑a) ⁻¹' s)) else ⊤) ∈
    lowerBounds (upperBounds s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case left
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ sInf s ∈ lowerBounds s

Tactic:
change ite _ _ _ ∈ _

Goal state after:
case left
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ (if s ⊆ {⊤} ∨ ¬BddBelow s then ⊤ else ↑(sInf ((fun a ↦ ↑a) ⁻¹' s))) ∈ lowerBounds s
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case right
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ sInf s ∈ upperBounds (lowerBounds s)

Tactic:
change ite _ _ _ ∈ _

Goal state after:
case right
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ (if s ⊆ {⊤} ∨ ¬BddBelow s then ⊤ else ↑(sInf ((fun a ↦ ↑a) ⁻¹' s))) ∈ upperBounds (lowerBounds s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ IsGLB s (sInf s)

Tactic:
exact isGLB_sInf' (OrderBot.bddBelow _)

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 : α
hz : ∀ (x : ι), x ∈ s → r (f x) z
x : ι
hx : x ∈ s
y : ι
hy : y ∈ s
a✝ : x ≠ y
⊢ (r on f) x y

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

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

Goal state before:
pp: case hb
α : Type u_1
inst✝² : DivisionRing α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible ↑den
⊢ 0 ≤ ⅟↑den

Tactic:
simp only [invOf_eq_inv, inv_nonneg, Nat.cast_nonneg]

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Group α
a b : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
⊢ a⁻¹ < b ∧ 1 < b ↔ b⁻¹ < a ∧ 1 < b

Tactic:
by rw [inv_lt']

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

Goal state before:
pp: n : ℕ
⊢ (n + 1 - 0) * (n + 1).descFactorial 0 = (n + 1) * n.descFactorial 0

Tactic:
Nat.sub_zero,

Goal state after:
n : ℕ
⊢ (n + 1) * (n + 1).descFactorial 0 = (n + 1) * n.descFactorial 0
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
q : ℚ≥0
hn : (↑↑q.num / ↑↑q.den).num = ↑q.num
hd : ↑(↑↑q.num / ↑↑q.den).den = ↑q.den
⊢ ↑(↑q.num / ↑q.den).num / ↑(↑q.num / ↑q.den).den = ↑q.num / ↑q.den

Tactic:
simp only [Int.cast_natCast, Nat.cast_inj] at hn hd

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
q : ℚ≥0
hn : (↑q.num / ↑q.den).num = ↑q.num
hd : (↑q.num / ↑q.den).den = q.den
⊢ ↑(↑q.num / ↑q.den).num / ↑(↑q.num / ↑q.den).den = ↑q.num / ↑q.den
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
m : ℤ
a : R
⊢ fract (a + ↑m) = fract a

Tactic:
fract_add_intCast

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
m : ℤ
a : R
⊢ fract a = fract a
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n | a ^ n ≤ g}
k✝ : ℕ
hk✝ : g⁻¹ ≤ a ^ k✝
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
⊢ ∀ n ∈ s, n ≤ ↑k

Tactic:
intro n hn

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n | a ^ n ≤ g}
k✝ : ℕ
hk✝ : g⁻¹ ≤ a ^ k✝
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
n : ℤ
hn : n ∈ s
⊢ n ≤ ↑k
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
this : 0 < (1 - fract q) * ↑q.den
⊢ ↑q.num < ↑q.num + (1 - fract q) * ↑q.den

Tactic:
by
    rw [← sub_lt_iff_lt_add']
    simpa

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
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ Nat.find this < b * c
⊢ False

Tactic:
have hn : Nat.find this ≠ 0 := by
    intro hf
    simp only [hf, pow_zero] at H
    exact (H.trans <| (mul_lt_of_lt_one_right hb₀ hc₁).trans_le hb₁).false

Goal state after:
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ Nat.find this < b * c
hn : Nat.find this ≠ 0
⊢ False
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: α : Type u_1
l₁ l₂ l : List α
h₁ : l ~ l₁
h₂✝ : l <+ l₂
l' : List α
h₂ : l₂ ~ l ++ l'
⊢ ∃ l, l ~ l₂ ∧ l₁ <+ l

Tactic:
exact ⟨l₁ ++ l', (h₂.trans (h₁.append_right _)).symm, (prefix_append _ _).sublist⟩

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

Goal state before:
pp: case neg
α : Type u_1
a b : α
as bs : Multiset α
this✝² : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝¹ : a ∈ b ::ₘ bs
this✝ : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
this : a ::ₘ as = b ::ₘ a ::ₘ cs
⊢ as = b ::ₘ cs

Tactic:
have : a ::ₘ as = a ::ₘ b ::ₘ cs := by rwa [cons_swap]

Goal state after:
case neg
α : Type u_1
a b : α
as bs : Multiset α
this✝³ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝² : a ∈ b ::ₘ bs
this✝¹ : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
this✝ : a ::ₘ as = b ::ₘ a ::ₘ cs
this : a ::ₘ as = a ::ₘ b ::ₘ cs
⊢ as = b ::ₘ cs
Module: Mathlib.Data.Set.List

Goal state before:
pp: α : Type u_1
β : Type u_2
l✝ : List α
c : β → α
p : α → Prop
inst✝ : CanLift α β c p
l : List α
H : ∀ (x : α), x ∈ l → p x
⊢ ∃ y, map c y = l

Tactic:
rw [← Set.mem_range, Set.range_list_map]

Goal state after:
α : Type u_1
β : Type u_2
l✝ : List α
c : β → α
p : α → Prop
inst✝ : CanLift α β c p
l : List α
H : ∀ (x : α), x ∈ l → p x
⊢ l ∈ {l | ∀ (x : α), x ∈ l → x ∈ Set.range c}
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
⊢ l.dedup.tail = l'

Tactic:
by rw [h, tail_cons]

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
⊢ l.dedup = a :: l'

Tactic:
· have := @List.cons_head!_tail α ⟨a⟩ _ (ne_nil_of_mem (mem_dedup.2 h.1))
    have hal : a ∈ l.dedup := mem_dedup.2 h.1
    rw [← this, mem_cons, or_iff_not_imp_right] at hal
    exact this ▸ h.2.2.symm ▸ cons_eq_cons.2 ⟨(hal (h.2.2.symm ▸ h.2.1)).symm, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ (replicate (n + 2) x).dedup = [x]

Tactic:
rw [replicate_succ, dedup_cons_of_mem (mem_replicate.2 ⟨n.succ_ne_zero, rfl⟩),
      replicate_dedup n.succ_ne_zero]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
⊢ count True (map p s) = (filter p s).card

Tactic:
simp only [count_eq_card_filter_eq, eq_iff_iff, true_iff, filter_map, comp_apply, card_map]

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

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ ⋯ ▸ Sum.rec f g ((Finset.union s t h).symm ⟨i, hi'⟩) = f ⟨i, hi⟩

Tactic:
rw! [

Goal state after:
ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ ⋯ ▸ Sum.rec f g ((Finset.union s t h).symm ⟨i, hi'⟩) = f ⟨i, hi⟩
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ ⋯ ▸ Sum.rec f g ((Finset.union s t h).symm ⟨i, hi'⟩) = g ⟨i, hi⟩

Tactic:
rw! [

Goal state after:
ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ ⋯ ▸ Sum.rec f g ((Finset.union s t h).symm ⟨i, hi'⟩) = g ⟨i, hi⟩
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : s.toFinset = t.toFinset
⊢ ↑t.toFinset = t

Tactic:
t.coe_toFinset

Goal state after:
α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : s.toFinset = t.toFinset
⊢ t = t
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
hf : Set.InjOn f (↑s ∪ ↑t)
⊢ ↑(image f (s ∩ t)) = ↑(image f s ∩ image f t)

Tactic:
push_cast
    exact Set.image_inter_on fun a ha b hb => hf (Or.inr ha) <| Or.inl hb

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α ↪ β
s : Finset α
a : α
⊢ map f (s.erase a) = (map f s).erase (f a)

Tactic:
simp_rw [map_eq_image]
  exact s.image_erase f.2 a

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : Fin n
⊢ 0 < a ↔ a ≠ 0

Tactic:
rw [← val_pos_iff, Nat.pos_iff_ne_zero, val_ne_zero_iff]

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
h : a < b
⊢ a + 1 ≤ b

Tactic:
by
  cases n <;> fin_omega

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⊆ t
this : #(t \ s) = #(t \ s ∪ s) - #s
⊢ #(t \ s) = #t - #s

Tactic:
rwa [sdiff_union_of_subset h] at this

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
x✝ : p b = true ∧ ∃ i, f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true
hpb : p b = true
i : Fin n
hfb : f i = b
h : ∀ (j : Fin n), j < i → ¬p (f j) = true
j : ℕ
hj : j < ↑i
⊢ ⟨j, ⋯⟩ < i

Tactic:
simpa using! hj

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

Goal state before:
pp: ι : Type u_4
α : ι → Type u_5
inst✝ : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
h : 1 < #s
⊢ ∃ i, 1 < #(image (fun x ↦ x i) s) ∧ ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s

Tactic:
simp_rw [one_lt_card_iff, Function.ne_iff] at h ⊢

Goal state after:
ι : Type u_4
α : ι → Type u_5
inst✝ : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
h : ∃ a b, a ∈ s ∧ b ∈ s ∧ ∃ a_1, a a_1 ≠ b a_1
⊢ ∃ i, (∃ a b, a ∈ image (fun x ↦ x i) s ∧ b ∈ image (fun x ↦ x i) s ∧ a ≠ b) ∧ ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.Nodup ↔ ∀ (x : α), ¬x ∈+ l

Tactic:
nodup_iff_sublist,

Goal state after:
α : Type u_1
l : List α
⊢ (∀ (a : α), ¬[a, a] <+ l) ↔ ∀ (x : α), ¬x ∈+ l
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ 1 < card α ↔ Nontrivial α

Tactic:
contrapose!; exact card_le_one_iff_subsingleton

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

Goal state before:
pp: case x
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
hi : P p
⊢ P p ∨ ∃ i, P (p.succAbove i)

pp: case p
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
j✝ : Fin n
hi : P (p.succAbove j✝)
⊢ P p ∨ ∃ i, P (p.succAbove i)

Tactic:
· exact .inl hi

Goal state after:
case p
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
j✝ : Fin n
hi : P (p.succAbove j✝)
⊢ P p ∨ ∃ i, P (p.succAbove i)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
⊢ SurjOn f s s ↔ BijOn f s s

Tactic:
by
  refine ⟨fun h ↦ ⟨hm, ?_, h⟩, BijOn.surjOn⟩
  have : Finite s := finite_coe_iff.mpr hs
  exact hm.restrict_inj.mp (Finite.injective_iff_surjective.mpr <| hm.restrict_surjective_iff.mpr h)

Goal state after: