mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: case false
m e : ℕ
⊢ 0 ≤ if false = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)

Tactic:
rw [if_neg (by decide)]
    exact num_nonneg.mp <| Int.natCast_nonneg _

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
this : a ^ m * a ∣ a ^ m * 1
⊢ a ^ m ≠ 0

Tactic:
apply pow_ne_zero m ha₀

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 = n /. ↑d
d0 : ↑d ≠ 0
this : ↑a * ↑d = ↑n * ↑b
⊢ ↑a * (↑b)⁻¹ =
    ↑{ num := n, den := d, den_nz := h, reduced := c }.num / ↑{ num := n, den := d, den_nz := h, reduced := c }.den

Tactic:
eq_div_iff_mul_eq 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 = n /. ↑d
d0 : ↑d ≠ 0
this : ↑a * ↑d = ↑n * ↑b
⊢ ↑a * (↑b)⁻¹ * ↑d = ↑{ num := n, den := d, den_nz := h, reduced := c }.num
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
a : α
b : ℤ
nb ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsNat (a ^ nb)⁻¹ ne
⊢ IsNat (a ^ (-↑nb)) ne

Tactic:
zpow_neg,

Goal state after:
α : Type u_1
inst✝ : DivisionSemiring α
a : α
b : ℤ
nb ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsNat (a ^ nb)⁻¹ ne
⊢ IsNat (a ^ ↑nb)⁻¹ ne
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsInt (a ^ nb)⁻¹ (Int.negOfNat ne)
⊢ IsInt (a ^ (-↑nb)) (Int.negOfNat ne)

Tactic:
zpow_neg,

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsInt (a ^ nb)⁻¹ (Int.negOfNat ne)
⊢ IsInt (a ^ ↑nb)⁻¹ (Int.negOfNat ne)
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
a : α
b : ℤ
nb num den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsNNRat (a ^ nb)⁻¹ num den
⊢ IsNNRat (a ^ (-↑nb)) num den

Tactic:
zpow_neg,

Goal state after:
α : Type u_1
inst✝ : DivisionSemiring α
a : α
b : ℤ
nb num den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsNNRat (a ^ nb)⁻¹ num den
⊢ IsNNRat (a ^ ↑nb)⁻¹ num den
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb : ℕ
num : ℤ
den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsRat (a ^ nb)⁻¹ num den
⊢ IsRat (a ^ (-↑nb)) num den

Tactic:
zpow_neg,

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb : ℕ
num : ℤ
den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsRat (a ^ nb)⁻¹ num den
⊢ IsRat (a ^ ↑nb)⁻¹ num den
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd

Tactic:
exact one_div_pos.2 hgcd

Goal state after:
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:
by
  conv => right; rw [← unionEqSigmaOfDisjoint h |>.symm_apply_apply x]
  rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
h : MonotoneOn f (Ici a)
x✝¹ : α
x✝ : x✝¹ ∈ Ici a
⊢ f x✝¹ ∈ Ici (f a)

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
b : α
h : MonotoneOn f (Iic b)
x✝¹ : α
x✝ : x✝¹ ∈ Iic b
⊢ f x✝¹ ∈ Iic (f b)

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
h : AntitoneOn f (Ici a)
x✝¹ : α
x✝ : x✝¹ ∈ Ici a
⊢ f x✝¹ ∈ Iic (f a)

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
b : α
h : AntitoneOn f (Iic b)
x✝¹ : α
x✝ : x✝¹ ∈ Iic b
⊢ f x✝¹ ∈ Ici (f b)

Tactic:
aesop

Goal state after:
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)) ∈ lowerBounds (upperBounds s)

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

Tactic:
· rintro (⟨⟩ | b) hb
      · exact le_top
      refine coe_le_coe.2 (csSup_le ?_ ?_)
      · rcases hs with ⟨⟨⟩ | b, hb⟩
        · exact absurd hb h₁
        · exact ⟨b, hb⟩
      · intro a ha
        exact coe_le_coe.1 (hb 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)
⊢ ⊤ ∈ lowerBounds (upperBounds s)
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : Std.Refl r
f : β → α
c : Set β
h : IsChain (f ⁻¹'o r) c
x✝¹ x✝ : { a // a ∈ c }
a : β
ha : a ∈ c
b : β
hb : b ∈ c
hab : a = b
⊢ ∃ z, r ((fun x ↦ f ↑x) ⟨a, ha⟩) ((fun x ↦ f ↑x) z) ∧ r ((fun x ↦ f ↑x) ⟨b, hb⟩) ((fun x ↦ f ↑x) z)

Tactic:
simp only [hab, exists_prop, and_self_iff, Subtype.exists]
      exact ⟨b, hb, refl _⟩

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a = b

Tactic:
obtain hab | hab | hab := trichotomous_of r a b

Goal state after:
case inl
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r a b
⊢ a = b

case inr.inl
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a = b
⊢ a = b

case inr.inr
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r b a
⊢ a = b
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:
inv_lt'

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Group α
a b : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
⊢ b⁻¹ < a ∧ 1 < b ↔ b⁻¹ < a ∧ 1 < b
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 1 + 2) < n.descFactorial (k + 1 + 2)

Tactic:
rw [descFactorial_succ, Nat.pow_succ, Nat.mul_comm]

Goal state after:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) * (n - (k + 1 + 1)) ^ (k + 2) < (n - (k + 2)) * n.descFactorial (k + 2)
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: case inr
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑(q ^ (-↑n)) = ↑q ^ (-↑n)

Tactic:
zpow_neg,

Goal state after:
case inr
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑(q ^ ↑n)⁻¹ = (↑q ^ ↑n)⁻¹
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) = ↑y + round x

Tactic:
round_add_natCast,

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

Goal state before:
pp: n : ℕ+
a : ℕ
h : a ∣ ↑n
hzero : a = 0
⊢ False

Tactic:
hzero

Goal state after:
n : ℕ+
a : ℕ
h : 0 ∣ ↑n
hzero : a = 0
⊢ False
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
⊢ ↑⌊a⌋ = a ↔ a ∈ range Int.cast

Tactic:
aesop

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

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
⊢ k * fract x = 1 ↔ ∃ n, k * x = k * ↑n + 1

Tactic:
rw [fract, mul_sub, sub_eq_iff_eq_add']

Goal state after:
R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
⊢ k * x = k * ↑⌊x⌋ + 1 ↔ ∃ n, k * x = k * ↑n + 1
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
⊢ ↑⌈a⌉ = a ↔ a ∈ range Int.cast

Tactic:
aesop

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

Goal state before:
pp: n : ℤ
d : ℕ
⊢ n % ↑d = n - ↑d * ⌊↑n / ↑d⌋

Tactic:
by
  rw [Int.emod_def, Rat.floor_intCast_div_natCast]

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
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
⊢ y ^ (-(m + 1)) < x

Tactic:
zpow_neg,

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
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
⊢ (y ^ (m + 1))⁻¹ < x
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
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
⊢ x ≤ y ^ (-m)

Tactic:
zpow_neg,

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
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
⊢ x ≤ (y ^ m)⁻¹
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a b : R
⊢ Int.cast ⁻¹' Icc a b = Icc ⌈a⌉ ⌊b⌋

Tactic:
ext
  simp [ceil_le, le_floor]

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

Goal state before:
pp: case neg
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsStrictOrderedRing R
a : R
ha : -1 < a
h : a < 0
⊢ ↑⌈a⌉₊ < a + 1

Tactic:
· rw [ceil_eq_zero.mpr h.le, cast_zero]
    exact neg_lt_iff_pos_add.mp ha

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
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
⊢ R (f (l + 1 • a)) (f (l + n • a))

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
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
⊢ R (f (l + n • a)) (f y)

Tactic:
· refine Int.rel_of_forall_rel_succ_of_lt R (f := (f <| l + · • a)) (fun k ↦ ?_) hn
        simp_rw [add_comm k 1, add_zsmul, ← add_assoc, one_zsmul, map_add_zsmul]
        refine hR (k • b) (hf _ ?_ _ ?_ ?_) <;> simpa

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)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
⊢ R (f (l + n • a)) (f y)
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ 1 ≤ count a s ↔ a ∈ s

Tactic:
succ_le_iff,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ 0 < count a s ↔ a ∈ s
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
s : Multiset α
n : ℕ
⊢ (∃ a t, a ::ₘ t = s ∧ t.card = n) → s.card = n + 1

Tactic:
aesop

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

Goal state before:
pp: case empty
α : Type u_1
n : ℕ
⊢ card 0 = n + 1 → ∃ a t, a ::ₘ t = 0 ∧ t.card = n

Tactic:
aesop

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

Goal state before:
pp: case cons
α : Type u_1
a✝¹ : α
s✝ : Multiset α
a✝ : ∀ {n : ℕ}, s✝.card = n + 1 → ∃ a t, a ::ₘ t = s✝ ∧ t.card = n
n : ℕ
⊢ (a✝¹ ::ₘ s✝).card = n + 1 → ∃ a t, a ::ₘ t = a✝¹ ::ₘ s✝ ∧ t.card = n

Tactic:
aesop

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

Goal state before:
pp: α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i j : Fin l.length
hg : (fun i ↦ l[↑i]) i = (fun i ↦ l[↑i]) j
⊢ i = j

Tactic:
obtain ⟨i, hi⟩ := i; obtain ⟨j, hj⟩ := j
      rcases Nat.lt_trichotomy i j with (hij | rfl | hji)
      · exact (h i j hi hj hij hg).elim
      · rfl
      · exact (h j i hj hi hji hg.symm).elim

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

Goal state before:
pp: α : Type u_1
l : List α
x : α
⊢ x ∈ range l.get ↔ x ∈ {x | x ∈ l}

Tactic:
rw [mem_ofPred_eq, mem_iff_get, mem_range]

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

Goal state before:
pp: α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.dropLast.Nodup ↔ l.tail.Nodup)
h : (a :: l)[0]? = (a :: l).getLast?
hl : ¬l = []
⊢ l.length ≠ 0

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
⊢ ∀ (a : β), a ∈ t ↔ a ∈ map (fun x ↦ i ↑x ⋯) s.attach

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ (∀ (a : α), count a s + count a t = max (count a s) (count a t)) ↔ ∀ (a : α), count a s = 0 ∨ count a t = 0

Tactic:
Nat.add_eq_max_iff

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
ha : a ∉ s
a✝ : α
⊢ a✝ ∈ insert a s \ insert b s ↔ a✝ ∈ {a}

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : a ∈ s
ht : a ∉ t
⊢ s.erase a = t ↔ s = insert a t

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
hb : b ∈ s
a✝ : α
⊢ a✝ ∈ s.erase a \ s.erase b ↔ a✝ ∈ {b}

Tactic:
aesop

Goal state after:
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) (t.erase a) ↔ Disjoint s t

Tactic:
← disjoint_erase_comm,

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

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

Tactic:
← disjoint_erase_comm,

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

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

Tactic:
rw [← erase_insert ha, ← disjoint_erase_comm, disjoint_insert_right]
  exact ⟨notMem_erase _ _, hst⟩

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

Goal state before:
pp: α β : Type u_4
h : α = β
s : Finset α
⊢ map (Equiv.cast h).toEmbedding s ≍ s

Tactic:
by
  subst h
  simp

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

Goal state before:
pp: α : Type u_4
a : α
H : {a} = ∅
⊢ False

Tactic:
aesop

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ ↑t ⊆ f '' s → ∃ s', ↑s' ⊆ s ∧ image f s' = t

Tactic:
intro h
    let : CanLift β s (f ∘ (↑)) fun y => y ∈ f '' s := ⟨fun y ⟨x, hxt, hy⟩ => ⟨⟨x, hxt⟩, hy⟩⟩
    lift t to Finset s using h
    refine ⟨t.map (Embedding.subtype _), map_subtype_subset _, ?_⟩
    ext y; simp

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ range ⇑i.succAboveOrderEmb = {i}ᶜ

Tactic:
aesop

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

Goal state before:
pp: n✝ m n : ℕ
⊢ NeZero (1 + n)

Tactic:
rw [Nat.add_comm]

Goal state after:
n✝ m n : ℕ
⊢ NeZero (n + 1)
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin m
j : Fin n
⊢ ↑i * n + n = (↑i + 1) * n

Tactic:
by rw [Nat.add_mul, Nat.one_mul]

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

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
ha : a ≠ last n
⊢ a < (a.castPred ha).succ

Tactic:
lt_succ_castPred_iff,

Goal state after:
n : ℕ
a : Fin (n + 1)
ha : a ≠ last n
⊢ a ≤ a
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case pos
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : j = 0
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j

Tactic:
rw [h]
    rfl

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
⊢ snoc (update p i y) x = update (snoc p x) i.castSucc y

Tactic:
ext j
  cases j using lastCases with
  | cast j => rcases eq_or_ne j i with rfl | hne <;> simp [*]
  | last => simp [Ne.symm]

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

Goal state before:
pp: case succ
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
⊢ (if h : i + 1 < n + 1 then cases a as ⟨i + 1, ⋯⟩ else ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩) ⋯)) =
    cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)

Tactic:
split_ifs with h
    · have : i < n := Nat.lt_of_succ_lt_succ h
      simp [addCases, this]
    · have : ¬i < n := Nat.not_le_of_gt <| Nat.le_of_lt_succ <| Nat.gt_of_not_le h
      simp [addCases, this]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ s_1, (∃ s', ↑s' ⊆ s ∧ Finset.image f s' = s_1) ∧ p ↑s_1) ↔ ∃ s_1, ↑s_1 ⊆ s ∧ p (f '' ↑s_1)

Tactic:
aesop

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

Goal state before:
pp: n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
k : Fin n
⊢ j.succAbove (i.succAbove k) = (j.succAbove i).succAbove ((i.predAbove j).succAbove k)

Tactic:
rw [succAbove_succAbove_succAbove_predAbove]

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

Goal state before:
pp: n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑k = ↑j
⊢ j.contractNth op g k = op (g k.castSucc) (g k.succ)

Tactic:
have : ¬(k : ℕ) < j := not_lt.2 (le_of_eq h.symm)

Goal state after:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑k = ↑j
this : ¬↑k < ↑j
⊢ j.contractNth op g k = op (g k.castSucc) (g k.succ)
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
n : ℕ
a : M
⊢ (replicate n a).prod = a ^ n

Tactic:
by
  simp [replicate, List.prod_replicate]

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

Goal state before:
pp: case empty
M : Type u_3
inst✝ : CommMonoid M
s : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
hs : 0 ≠ ∅
p_s : ∀ (a : M), a ∈ 0 → p a
⊢ p (prod 0)

Tactic:
simp at hs

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ drop (n % (zipWith f l l').length) (zipWith f l l') ++ take (n % (zipWith f l l').length) (zipWith f l l') =
    zipWith f (drop (n % l'.length) l ++ take (n % l'.length) l) (drop (n % l'.length) l' ++ take (n % l'.length) l')

Tactic:
zipWith_append,

Goal state after:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ drop (n % (zipWith f l l').length) (zipWith f l l') ++ take (n % (zipWith f l l').length) (zipWith f l l') =
    zipWith f (drop (n % l'.length) l) (drop (n % l'.length) l') ++
      zipWith f (take (n % l'.length) l) (take (n % l'.length) l')

α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ (drop (n % l'.length) l).length = (drop (n % l'.length) l').length
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
l₁ l₂ : List G
⊢ a / (l₁.alternatingProd * l₂.alternatingProd ^ (-1) ^ l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ (-(-1) ^ l₁.length)

Tactic:
zpow_neg,

Goal state after:
G : Type u_7
inst✝ : CommGroup G
a : G
l₁ l₂ : List G
⊢ a / (l₁.alternatingProd * l₂.alternatingProd ^ (-1) ^ l₁.length) =
    a / l₁.alternatingProd * (l₂.alternatingProd ^ (-1) ^ l₁.length)⁻¹
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ l.alternatingProd ^ (-(-1) ^ l.length) * a ^ (-1) ^ l.length = (a / l.alternatingProd) ^ (- -(-1) ^ l.length)

Tactic:
zpow_neg,

Goal state after:
G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ (l.alternatingProd ^ (-1) ^ l.length)⁻¹ * a ^ (-1) ^ l.length = ((a / l.alternatingProd) ^ (-1) ^ l.length)⁻¹⁻¹
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
⊢ (n • s).dedup = s.dedup

Tactic:
by ext a; by_cases h : a ∈ s <;> simp [h, hn]

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

Goal state before:
pp: M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
s : Multiset M
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
l : List M
⊢ (map ⇑f ⟦l⟧).prod = f (prod ⟦l⟧)

Tactic:
by simp only [l.prod_hom f, quot_mk_to_coe, map_coe, prod_coe]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
a : α
⊢ (insert a s).biUnion t = t a ∪ s.biUnion t

Tactic:
aesop

Goal state after: