mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
⊢ (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (b : β), b ∈ t → ∀ (x : α), x ∈ s → x ∈ (fun a ↦ f a b) ⁻¹' u

Tactic:
mem_preimage,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
⊢ (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (b : β), b ∈ t → ∀ (x : α), x ∈ s → f x b ∈ u
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
h : a ^ 2 ≤ b ^ 2
hb : 0 ≤ b
⊢ |a| ≤ b

Tactic:
rwa [← abs_of_nonneg hb, ← sq_le_sq]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
hc : IsCofinalFor s t
a : α
hat : a ∈ t
⊢ ∃ b ∈ t, a ≤ b

Tactic:
exact ⟨a, hat, le_rfl⟩

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

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

Tactic:
rw [Subsingleton.elim f.dual]

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

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

Tactic:
rw [Subsingleton.elim f.dual]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ici a ∩ Iic b ∩ (Iic c ∩ Ici b) = {b}

Tactic:
inter_inter_inter_comm,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ici a ∩ Iic c ∩ (Iic b ∩ Ici b) = {b}
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: γ : Type u_3
inst✝ : LinearOrder γ
i : γ
⊢ ∃ j, IsLUB (Iio i) j

Tactic:
by_cases! h_exists_lt : ∃ j, j ∈ upperBounds (Iio i) ∧ j < i

Goal state after:
case pos
γ : Type u_3
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ∃ j ∈ upperBounds (Iio i), j < i
⊢ ∃ j, IsLUB (Iio i) j

case neg
γ : Type u_3
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ∀ j ∈ upperBounds (Iio i), i ≤ j
⊢ ∃ j, IsLUB (Iio i) j
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
n : ℕ
x a k a' : α
h : a + k = a'
⊢ term n x a + k = term n x a'

Tactic:
simp [h.symm, term, add_assoc]

Goal state after:
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n d : ℕ
inst✝¹ : Semiring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ e

Tactic:
rw [eq, of_decide_eq_true h]

Goal state after:
A : Type u_1
e : A
n d : ℕ
inst✝¹ : Semiring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ ↑0 * ⅟↑d
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝¹ : Ring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ e

Tactic:
rw [eq, of_decide_eq_true h]

Goal state after:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝¹ : Ring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ ↑0 * ⅟↑d
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : c < a
hab : ¬a ≤ b
⊢ AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Icc a b)

Tactic:
simp [hab, Set.Subsingleton.antitoneOn]

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

Goal state before:
pp: case neg
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : b < c
hab : ¬a ≤ b
⊢ AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Icc a b)

Tactic:
simp [hab, Set.Subsingleton.antitoneOn]

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

Goal state before:
pp: case e'_5
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
x✝ : α
⊢ x✝ = x✝ - 0

Tactic:
exact (sub_zero _).symm

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

Goal state before:
pp: case e'_5
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : 0 < a
x✝ : α
⊢ x✝ = x✝ - 0

Tactic:
exact (sub_zero _).symm

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

Goal state before:
pp: case e'_5
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
x✝ : α
⊢ x✝ = x✝ - 0

Tactic:
exact (sub_zero _).symm

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

Goal state before:
pp: case inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b

Tactic:
simp [hb, hb.not_gt, one_le_div_of_neg]

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

Goal state before:
pp: case mpr
α : Type u_1
a b : List α
⊢ a = b → Forall₂ (fun x1 x2 ↦ x1 = x2) a b

Tactic:
rintro rfl
    exact forall₂_refl _

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

Goal state before:
pp: α : Type u
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
hk : n + k + 1 < (l.insertIdx n x).length
⊢ (l.insertIdx n x).get ⟨n + k + 1, hk⟩ = l.get ⟨n + k, hk'⟩

Tactic:
simp [getElem_insertIdx_add_succ, hk']

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : SublistForall₂ R l₁ l₂
⊢ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂

Tactic:
induction h with
    | nil => exact ⟨nil, Forall₂.nil, nil_sublist _⟩
    | @cons a b l1 l2 rab _ ih =>
      obtain ⟨l, hl1, hl2⟩ := ih
      exact ⟨b :: l, Forall₂.cons rab hl1, hl2.cons_cons b⟩
    | cons_right _ ih =>
      obtain ⟨l, hl1, hl2⟩ := ih
      exact ⟨l, hl1, hl2.trans (Sublist.cons _ (Sublist.refl _))⟩

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

Goal state before:
pp: case hab
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ |q| ≤ B + 1

Tactic:
exact add_sub_cancel r q ▸ (abs_add_le ..).trans (add_le_add hr hqr.1)

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List M
i : ℕ
hlen : i < l.length
hcomm : ∀ (a' : M), a' ∈ take i l → Commute l[i] a'
⊢ ((l.eraseIdx i).insertIdx i l[i]).prod = l.prod

Tactic:
insertIdx_eraseIdx_getElem hlen

Goal state after:
M : Type u_4
inst✝ : Monoid M
l : List M
i : ℕ
hlen : i < l.length
hcomm : ∀ (a' : M), a' ∈ take i l → Commute l[i] a'
⊢ l.prod = l.prod
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case neg
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
hn : ¬n < L.length
⊢ (take n L).prod * 1 * (drop (n + 1) L).prod = L.prod * 1

Tactic:
simp (disch := grind) [take_of_length_le, drop_eq_nil_of_le]

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

Goal state before:
pp: case cons.none
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
ha : f a = none
h : filterMap f (a :: l) = map g (a :: l)
⊢ ∀ (x : α), x ∈ a :: l → f x = some (g x)

Tactic:
have : (filterMap f l).length = l.length + 1 := by grind

Goal state after:
case cons.none
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
ha : f a = none
h : filterMap f (a :: l) = map g (a :: l)
this : (filterMap f l).length = l.length + 1
⊢ ∀ (x : α), x ∈ a :: l → f x = some (g x)
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ SMul.smul (↑x✝¹.succ) x✝ = SMul.smul (↑x✝¹) x✝ + x✝

Tactic:
SMul.smul

Goal state after:
q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ ↑↑x✝¹.succ * x✝ = ↑↑x✝¹ * x✝ + x✝
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ SMul.smul (Int.negSucc x✝¹) x✝ = -SMul.smul (↑x✝¹.succ) x✝

Tactic:
SMul.smul

Goal state after:
q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ ↑(Int.negSucc x✝¹) * x✝ = -(↑↑x✝¹.succ * x✝)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ (l.erase a).length + 1 = l.length

Tactic:
by
  rw [erase_eq_eraseP, length_eraseP_add_one h BEq.rfl]

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

Goal state before:
pp: a : ℚ
⊢ a.num ≤ 0 ↔ a ≤ 0

Tactic:
simp +instances [Int.le_iff_lt_or_eq, instLE, Rat.blt]

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:
rw [d0, zero_mul] at this

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
⊢ False
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: case a
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMaxOrder ι
f : ι → α
j : ι
⊢ f j ≤ ⨆ i, ⨆ j, ⨆ (_ : j < i), f j

Tactic:
obtain ⟨i, jlt⟩ := exists_gt j

Goal state after:
case a
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMaxOrder ι
f : ι → α
j i : ι
jlt : j < i
⊢ f j ≤ ⨆ i, ⨆ j, ⨆ (_ : j < i), f j
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ range fun x ↦ ↑(f x i)) → ∃ i, x ∈ C i

Tactic:
rintro ⟨y, i, rfl⟩
    exact ⟨i, (f i y).2⟩

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

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLattice α
⊢ sSup ∅ = ⊥

Tactic:
rw [sSup_eq (by simp) (OrderTop.bddAbove _), Set.preimage_empty, _root_.sSup_empty, coe_bot]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : Frame α
a : α
f : ι → α
⊢ a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i

Tactic:
by
  simpa only [inf_comm] using iSup_inf_eq f a

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

Goal state before:
pp: α : Type u_1
p q r : α → α → Prop
a b : α
c : { x // p a x ∧ q x b }
h : ∀ {x : α}, r x ↑c → q x b
x✝ : α
⊢ x✝ ∈ {x | p a x ∧ q x b} ∩ {y | r y ↑c} ↔ x✝ ∈ {y | p a y ∧ r y ↑c}

Tactic:
simp +contextual [h]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
⊢ sSup s = sSup t

Tactic:
have Bt : BddAbove t := by
      rcases B with ⟨b, hb⟩ | hB
      · refine ⟨b, fun y hy ↦ ?_⟩
        rcases ht y hy with ⟨x, hx, hyx⟩
        exact hyx.trans (hb hx)
      · exact hB

Goal state after:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
⊢ sSup s = sSup t
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
⊢ IsAntichain (fun x1 x2 ↦ r ↑x1 ↑x2) univ ↔ IsAntichain r s

Tactic:
by
  simpa using isAntichain_preimage_subtypeVal s univ

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻ᵐ = if a < 1 then a⁻¹ else 1

Tactic:
by
  grind [leOnePart_eq_ite, inv_one]

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

Goal state before:
pp: n k : ℕ
⊢ (n + k)! * (n + 1 + k) = (n + k + 1) * (n + k)!

Tactic:
Nat.mul_comm,

Goal state after:
n k : ℕ
⊢ (n + 1 + k) * (n + k)! = (n + k + 1) * (n + k)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n ^ k * n ≤ n.ascFactorial (k + 1)

Tactic:
Nat.mul_comm,

Goal state after:
n k : ℕ
⊢ n * n ^ k ≤ n.ascFactorial (k + 1)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1 + k) * (n + 1).ascFactorial k ≤ (n + (k + 1)) ^ k * (n + (k + 1))

Tactic:
Nat.mul_comm,

Goal state after:
n k : ℕ
⊢ (n + 1).ascFactorial k * (n + 1 + k) ≤ (n + (k + 1)) ^ k * (n + (k + 1))
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
x✝ : 2 ≤ k + 2
⊢ (n + 1).ascFactorial (k + 2) < (n + (k + 2)) ^ (k + 1) * (n + (k + 2))

Tactic:
Nat.mul_comm,

Goal state after:
n k : ℕ
x✝ : 2 ≤ k + 2
⊢ (n + 1).ascFactorial (k + 2) < (n + (k + 2)) * (n + (k + 2)) ^ (k + 1)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : 2 ≤ k + 2
⊢ (n - (k + 1)) * n.descFactorial (k + 1) < n * n ^ (k + 1)

Tactic:
Nat.mul_comm,

Goal state after:
n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : 2 ≤ k + 2
⊢ n.descFactorial (k + 1) * (n - (k + 1)) < n * n ^ (k + 1)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case succ
n : ℕ
⊢ 2 ^ (n + 1) * (n + 1)! ≤ (2 * (n + 1))!

Tactic:
Nat.mul_comm,

Goal state after:
case succ
n : ℕ
⊢ (n + 1)! * 2 ^ (n + 1) ≤ (2 * (n + 1))!
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
hx' : 2 * x ∉ range Int.cast
⊢ (⌊2 * x⌋ + 1) / 2 = ⌈2 * x⌉ / 2

Tactic:
(ceil_eq_floor_add_one_iff_notMem _).mpr hx'

Goal state after:
case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
hx' : 2 * x ∉ range Int.cast
⊢ (⌊2 * x⌋ + 1) / 2 = (⌊2 * x⌋ + 1) / 2
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case mp
k m : ℕ+
⊢ ↑m % ↑k = 0 → m.mod k = k

Tactic:
intro h
    apply PNat.eq
    rw [mod_coe, if_pos h]

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
ha : Surjective fun x ↦ 1 ^ x
⊢ False

pp: case inr.inr
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a
⊢ False

Tactic:
· rcases exists_ne (1 : α) with ⟨b, hb⟩
    simpa [hb.symm] using ha b

Goal state after:
case inr.inr
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a
⊢ False
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr.refine_2
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑(m % n) / ↑n < 1

Tactic:
simpa only [div_lt_one hn', Nat.cast_lt] using m.mod_lt hn

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

Goal state before:
pp: R : Type u_3
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
r : R
n : ℤ
d : ℕ
res : ℤ
hres : round (↑n / ↑d) = res
⊢ IsRat r n d → IsInt (round r) res

Tactic:
rintro ⟨inv, rfl⟩
  subst res
  constructor
  rw [invOf_eq_inv, ← div_eq_mul_inv]
  norm_cast

Goal state after:
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
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
hR : CovariantClass H H (fun x y ↦ y + x) R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
x y : G
hxy : (fun x1 x2 ↦ x1 < x2) x y
⊢ R (f x) (f y)

Tactic:
replace hR := hR.elim

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
x y : G
hxy : (fun x1 x2 ↦ x1 < x2) x y
hR : Covariant H H (fun x y ↦ y + x) R
⊢ R (f x) (f y)
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case inr.inr
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
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
· rcases lt_or_ge a 1 with ha₁ | ha₁
      · refine ⟨0, ?_⟩
        rw [zpow_zero]
        exact ⟨ha₁, hb₁⟩
      · have : b⁻¹ < a⁻¹ * c := by rwa [lt_inv_mul_iff₀' ha, inv_mul_lt_iff₀ hb₀]
        obtain ⟨n, hn₁, hn₂⟩ :=
          exists_pow_btwn_of_lt_mul this (inv_pos_of_pos ha) (inv_le_one_of_one_le₀ ha₁) hc₀ hc₁
        refine ⟨-n, ?_, ?_⟩
        · rwa [lt_inv_comm₀ (pow_pos hc₀ n) ha, ← zpow_natCast, ← zpow_neg] at hn₂
        · rwa [inv_lt_comm₀ hb₀ (pow_pos hc₀ n), ← zpow_natCast, ← zpow_neg] at hn₁

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₁ /ₛ p₂) • p₃ = (p₃ /ₛ p₂) • p₁

Tactic:
← @sdiv_eq_one_iff_eq G,

Goal state after:
G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₁ /ₛ p₂) • p₃ /ₛ (p₃ /ₛ p₂) • p₁ = 1
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ count a ↑l = List.count a l

Tactic:
by
  simp_rw [count, List.count, coe_countP (a = ·) l, @eq_comm _ a]
  rfl

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

Goal state before:
pp: α : Type u
β : Type v
l₁ : List α
f : α → List β
⊢ (Pairwise (fun a b ↦ (f a).Disjoint (f b)) l₁ ∧ ∀ (l : List β) (x : α), f x = l → x ∈ l₁ → l.Nodup) ↔
    Pairwise (Disjoint on f) l₁ ∧ ∀ (x : α), x ∈ l₁ → (f x).Nodup

Tactic:
show (∀ (l : List β) (x : α), f x = l → x ∈ l₁ → Nodup l) ↔ ∀ x : α, x ∈ l₁ → Nodup (f x)
      from forall_comm.trans <| forall_congr' fun _ => forall_eq'

Goal state after:
α : Type u
β : Type v
l₁ : List α
f : α → List β
⊢ (Pairwise (fun a b ↦ (f a).Disjoint (f b)) l₁ ∧ ∀ (x : α), x ∈ l₁ → (f x).Nodup) ↔
    Pairwise (Disjoint on f) l₁ ∧ ∀ (x : α), x ∈ l₁ → (f x).Nodup
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
a : α
h : ¬a ∈ l
h' : l.Nodup
⊢ (l ++ [a]).Nodup

Tactic:
exact h'.append (nodup_singleton _) (disjoint_singleton.2 h)

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ map f s = b ::ₘ t → ∃ a, a ∈ s ∧ f a = b ∧ map f (s.erase a) = t

Tactic:
intro h
    have : b ∈ s.map f := by
      rw [h]
      exact mem_cons_self _ _
    obtain ⟨a, h1, rfl⟩ := mem_map.mp this
    obtain ⟨u, rfl⟩ := exists_cons_of_mem h1
    rw [map_cons, cons_inj_right] at h
    refine ⟨a, mem_cons_self _ _, rfl, ?_⟩
    rw [Multiset.erase_cons_head, h]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : x ∈ xs
⊢ (f x :: map f xs).dedup = map f xs.dedup

Tactic:
dedup_cons_of_mem (mem_map_of_mem h),

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : x ∈ xs
⊢ (map f xs).dedup = map f xs.dedup
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : t ⊆ s
⊢ (s + t).dedup = s.dedup

Tactic:
by
  rw [s.add_comm, Subset.dedup_add_right h]

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

Goal state before:
pp: α : Type u_1
a : α
m : Multiset α
⊢ m.toList = [a] ↔ m = {a}

Tactic:
← perm_singleton,

Goal state after:
α : Type u_1
a : α
m : Multiset α
⊢ m.toList ~ [a] ↔ m = {a}
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a b : List α
p✝ : a ≈ b
hp : ∃! a, a ∈ ⟦b⟧ ∧ p a
all_equal : ∀ (x y : { t // t ∈ b ∧ p t }), x = y
⊢ Eq.ndrec (motive := fun x ↦ (∃! a, a ∈ x ∧ p a) → { a // a ∈ x ∧ p a }) (fun ex_unique ↦ List.chooseX p a ⋯) ⋯ hp =
    List.chooseX p b ⋯

Tactic:
by
        apply all_equal

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + s ∩ t ∪ (t + s ∩ t) ≤ s + t

Tactic:
refine union_le (Multiset.add_le_add_left inter_le_right) ?_

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ t + s ∩ t ≤ s + t
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ count y (replicate n x ∩ s) = count y (replicate (min n (count x s)) x)

Tactic:
rw [count_inter, count_replicate, count_replicate]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
⊢ insert a s ⊆ insert a t ↔ s ⊆ t

Tactic:
simp_rw [← coe_subset]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
⊢ ↑(insert a s) ⊆ ↑(insert a t) ↔ ↑s ⊆ ↑t
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
⊢ Disjoint s ((insert a t).erase a) ↔ Disjoint s t

Tactic:
erase_insert ha

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
⊢ Disjoint s t ↔ Disjoint s t
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
⊢ Disjoint ((insert a s).erase a) t ↔ Disjoint s t

Tactic:
erase_insert ha

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
⊢ Disjoint s t ↔ Disjoint s t
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ insert a (insert a s)ᶜ = sᶜ

Tactic:
compl_insert,

Goal state after:
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ insert a (sᶜ.erase a) = sᶜ
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ (if n ≤ ↑a % n + ↑b % n then ↑a % n + ↑b % n - n else ↑a % n + ↑b % n) = if n ≤ ↑a + ↑b then ↑a + ↑b - n else ↑a + ↑b

Tactic:
Nat.mod_eq_of_lt (show ↑a < n from a.2),

Goal state after:
n : ℕ
a b : Fin n
⊢ (if n ≤ ↑a + ↑b % n then ↑a + ↑b % n - n else ↑a + ↑b % n) = if n ≤ ↑a + ↑b then ↑a + ↑b - n else ↑a + ↑b
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ ((m - ↑i / n - 1) * n + (n - (↑i % n + 1))) % n = n - (↑i % n + 1)

Tactic:
Nat.mul_comm,

Goal state after:
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (n * (m - ↑i / n - 1) + (n - (↑i % n + 1))) % n = n - (↑i % n + 1)
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ ↑(last n - i) = ↑i.rev

Tactic:
coe_sub_iff_le.2 i.le_last,

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ ↑(last n) - ↑i = ↑i.rev