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

Goal state before:
pp: case map_sInf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
s✝ : Set α
⊢ e (sInf s✝) = ⨅ a ∈ s✝, e a

Tactic:
rfl

Goal state after:
case map_sInf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
s✝ : Set α
⊢ e (sInf s✝) = ⨅ a ∈ s✝, e a
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_top
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := ⋯
⊢ e ⊤ = ⊤

Tactic:
rfl

Goal state after:
case map_top
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := ⋯
⊢ e ⊤ = ⊤
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_bot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := ⋯
⊢ e ⊥ = ⊥

Tactic:
rfl

Goal state after:
case map_bot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := ⋯
⊢ e ⊥ = ⊥
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_compl
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
a✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ

Tactic:
rfl

Goal state after:
case map_compl
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
a✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_himp
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝

Tactic:
rfl

Goal state after:
case map_himp
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_hnot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
a✝ : α
⊢ e (￢a✝) = ￢e a✝

Tactic:
rfl

Goal state after:
case map_hnot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
a✝ : α
⊢ e (￢a✝) = ￢e a✝
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case map_sdiff
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝

Tactic:
rfl

Goal state after:
case map_sdiff
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
h : IsChain r univ
a b : α
this : a ≠ b → r a b ∨ r b a
⊢ ¬r a b → ¬r b a → a = b

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
hf : Function.Injective f
h : ∀ (x y : α), s (f x) (f y) → r x y
c : Set β
hrc : IsChain s c
x✝ : α
ha : x✝ ∈ f ⁻¹' c
y✝ : α
hb : y✝ ∈ f ⁻¹' c
hne : x✝ ≠ y✝
this : (fun x y ↦ s x y ∨ s y x) (f x✝) (f y✝)
⊢ r x✝ y✝ ∨ r y✝ x✝

Tactic:
grind

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
⊢ ⟨a, ⋯⟩ = ⊥

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
⊢ ⟨b, ⋯⟩ = ⊤

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 ≤ r }ˣ
⊢ ↑↑((fun r ↦ { val := ⟨↑r, ⋯⟩, inv := ⟨(↑r)⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ }) ((fun r ↦ ⟨↑↑r, ⋯⟩) r)) = ↑↑r

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : Lattice α
inst✝ : IsOrderedRing α
a : α
na : ℕ
pa : IsNat a na
⊢ ↑na = ↑na

Tactic:
rfl

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

Goal state before:
pp: a b q q' : ℤ
h : IsInt (a / -b) q
hq : -q = q'
⊢ a / b = q'

Tactic:
← hq,

Goal state after:
a b q q' : ℤ
h : IsInt (a / -b) q
hq : -q = q'
⊢ a / b = -q
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: case neg
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ¬∃ a, f a = x
⊢ 1 x = 1

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
k : Set ι
h : mulSupport f ⊆ k
this : range f ⊆ insert 1 (f '' k)
⊢ range f = f '' k ∨ range f = insert 1 (f '' k)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
h : a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
⊢ a ≤ b

Tactic:
rw [← oneLePart_div_leOnePart a, ← oneLePart_div_leOnePart b]

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
h : a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
⊢ a⁺ᵐ / a⁻ᵐ ≤ b⁺ᵐ / b⁻ᵐ
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ * a = a⁺ᵐ * a⁺ᵐ

Tactic:
← mul_mul_div_cancel a⁺ᵐ,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ * a = a⁺ᵐ * ?c * (a⁺ᵐ / ?c)

case c
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ α
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ a / |a|ₘ = (a⁻ᵐ ^ 2)⁻¹

Tactic:
rw [← mabs_div_eq_leOnePart_sq, inv_div]

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

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
⊢ (a ⊔ b)⁻ᵐ = a⁻ᵐ ⊓ b⁻ᵐ

Tactic:
simp [leOnePart, inv_sup, sup_inf_right]

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

Goal state before:
pp: case mpr.refl
⊢ 1! = 1

Tactic:
rfl

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

Goal state before:
pp: case mpr.step.refl
⊢ 0! = 1

Tactic:
rfl

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

Goal state before:
pp: case inr.inl
n : ℕ
hn : 1 < n
h : n ! = n !
⊢ n = n

Tactic:
rfl

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

Goal state before:
pp: case zero
n m : ℕ
h : n ≤ m
⊢ n.ascFactorial 0 ≤ m.ascFactorial 0

Tactic:
rfl

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

Goal state before:
pp: k m n : ℕ
hkm : k ≤ m
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m

Tactic:
by_cases hmn : m ≤ n
  · apply Nat.mul_left_cancel (n - m).factorial_pos
    rw [factorial_mul_descFactorial hmn, show n - m = (n - k) - (m - k) by lia, ← Nat.mul_assoc,
      factorial_mul_descFactorial (show m - k ≤ n - k by lia),
      factorial_mul_descFactorial (le_trans hkm hmn)]
  · rw [descFactorial_eq_zero_iff_lt.mpr (show n < m by lia)]
    by_cases hkn : k ≤ n
    · rw [descFactorial_eq_zero_iff_lt.mpr (show n - k < m - k by lia), Nat.zero_mul]
    · rw [descFactorial_eq_zero_iff_lt.mpr (show n < k by lia), Nat.mul_zero]

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

Goal state before:
pp: case zero
k m : ℕ
h : k ≤ m
⊢ k.descFactorial 0 ≤ m.descFactorial 0

Tactic:
rfl

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

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

Tactic:
by rw [descFactorial_zero, Nat.pow_zero]

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

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

Tactic:
succ_sub_succ

Goal state after:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
succ_sub_succ

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

Goal state before:
pp: n : ℕ
⊢ n.descFactorial 0 ≤ n ^ 0

Tactic:
by rw [descFactorial_zero, Nat.pow_zero]

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

Goal state before:
pp: n : ℕ
⊢ n ! = n.factorialBinarySplitting

Tactic:
simp [factorialBinarySplitting, ← ascFactorial_eq_ascFactorialBinary]

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 + k - 1).descFactorial k

Tactic:
grind

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

Goal state before:
pp: case succ
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n✝ : ℕ
h : 0 < n✝ + 1
⊢ (⟨n✝ + 1, h⟩ + 1).recOn one succ = succ ⟨n✝ + 1, h⟩ (recOn ⟨n✝ + 1, h⟩ one succ)

Tactic:
rfl

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

Goal state before:
pp: case neg
a b : ℕ+
h : ¬b < a
⊢ ↑(toPNat' 0) = 1

Tactic:
rfl

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
n : ℕ
⊢ ⌊a + ↑n⌋ = ⌊a⌋ + ↑n

Tactic:
← Int.cast_natCast,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ ⌊a + ↑↑n⌋ = ⌊a⌋ + ↑n
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
n : ℕ
a : R
⊢ ⌊↑n + a⌋ = ↑n + ⌊a⌋

Tactic:
← Int.cast_natCast,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
n : ℕ
a : R
⊢ ⌊↑↑n + a⌋ = ↑n + ⌊a⌋
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
n : ℕ
⊢ ⌊a - ↑n⌋ = ⌊a⌋ - ↑n

Tactic:
← Int.cast_natCast,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ ⌊a - ↑↑n⌋ = ⌊a⌋ - ↑n
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
⊢ a + b - ↑⌊a + b⌋ - (a - ↑⌊a⌋) - (b - ↑⌊b⌋) = ↑(⌊a⌋ + ⌊b⌋ - ⌊a + b⌋)

Tactic:
grind

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ 0 ≤ (↑n + 1) * (b ^ 2 * (2 * a + b) * a ^ n) + a ^ (n + 1) * b ^ 2

Tactic:
by
          apply_rules [add_nonneg, mul_nonneg, Nat.cast_nonneg, pow_nonneg, zero_le_one]

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

Goal state before:
pp: R : Type u_2
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
⊢ min a b ≠ c

Tactic:
grind

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

Goal state before:
pp: R : Type u_2
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
⊢ max a b ≠ c

Tactic:
grind

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
n : ℕ
⊢ ⌈a + ↑n⌉ = ⌈a⌉ + ↑n

Tactic:
← Int.cast_natCast,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ ⌈a + ↑↑n⌉ = ⌈a⌉ + ↑n
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ ↑(⌊a⌋ + 1) - 1 < a

Tactic:
rw [cast_add, cast_one, add_tsub_cancel_right, ← self_sub_fract a, sub_lt_self_iff]

Goal state after:
case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ 0 < fract a
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 : 0 < n
⊢ R (f x) (f (l + 1 • a))

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.Group.Action.Units

Goal state before:
pp: G : Type u_1
H : Type u_2
M✝ : Type u_3
N : Type u_4
α : Type u_5
M : Type u_6
inst✝ : CommMonoid M
⊢ mulAction'.toSMul = instSMulOfMul

Tactic:
rfl

Goal state after:
G : Type u_1
H : Type u_2
M✝ : Type u_3
N : Type u_4
α : Type u_5
M : Type u_6
inst✝ : CommMonoid M
⊢ mulAction'.toSMul = instSMulOfMul
Module: Mathlib.Algebra.Group.Action.Units

Goal state before:
pp: G : Type u_1
H : Type u_2
M✝ : Type u_3
N : Type u_4
α : Type u_5
M : Type u_6
inst✝ : CommMonoid M
x✝¹ x✝ : Mˣ
⊢ ↑(SMul.smul x✝¹ x✝) = ↑(SMul.smul x✝¹ x✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Group.Action.Units

Goal state before:
pp: M : Type u_6
inst✝ : CommMonoid M
u₁ u₂ : Mˣ
⊢ ↑(u₁ • u₂) = ↑(u₁ * u₂)

Tactic:
rfl

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

Goal state before:
pp: K : Type u_4
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
H : ∀ (x : K), ∃ n, x < ↑n
x y : K
y0 : 0 < y
n : ℕ
h : x / y < ↑n
⊢ x < n • y

Tactic:
rwa [div_lt_iff₀ y0, ← nsmul_eq_mul] at h

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

Goal state before:
pp: K : Type u_4
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
⊢ (∀ (x : K), ∃ n, x < ↑n) → ∀ (x : K), ∃ n, x < ↑n

Tactic:
intro h x

Goal state after:
K : Type u_4
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
h : ∀ (x : K), ∃ n, x < ↑n
x : K
⊢ ∃ n, x < ↑n
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
K : Type u_3
inst✝² : Add G
inst✝¹ : AddZeroClass H
a : G
b : H
inst✝ : DistribSMul K H
c : K
f : G →+c[a, b] H
x : G
⊢ (c • ⇑f) (x + a) = (c • ⇑f) x + c • b

Tactic:
by simp [smul_add]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
H✝ : ∀ (a : α), a ∈ ↑l₁ → p a
⊢ Eq.ndrec (motive := fun s ↦ (∀ (a : α), a ∈ s → p a) → Multiset β) (fun x ↦ ↑(List.pmap f l₁ H₁)) ⋯ H✝ =
    ↑(List.pmap f l₁ H₁)

Tactic:
rfl

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

Goal state before:
pp: case refl
α : Type u_1
s : Multiset α
nodup✝¹ nodup✝ : s.Nodup
⊢ { val := s, nodup := nodup✝¹ } = { val := s, nodup := nodup✝ }

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ (∀ (b : α), b ∈ s → ¬a = b) ↔ ¬a ∈ s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ (∀ (b : α), b ∈ s → ¬b = a) ↔ ¬a ∈ s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ countP (fun a ↦ p ↑a) ↑l.attach = List.countP (fun a ↦ decide (p ↑a)) l.attach

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ List.countP (fun b ↦ decide (b = a)) l = List.countP (fun x ↦ x == a) l

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
H : ∀ (x : α), ¬x ∈ Quot.mk (⇑(isSetoid α)) l
⊢ Quot.mk ⇑(isSetoid α) [] = 0

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
l : List α
d : α
⊢ (range fun n ↦ l[n]?.getD d) = range fun x ↦ l[x]?.getD d

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u
hne : [] ≠ []
hnd : [].Nodup
⊢ [].head hne = [].getLast hne ↔ ∃ x, [] = [x]

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u
head✝ : α
tail✝ : List α
hne : head✝ :: tail✝ ≠ []
hnd : (head✝ :: tail✝).Nodup
⊢ (head✝ :: tail✝).head hne = (head✝ :: tail✝).getLast hne ↔ ∃ x, head✝ :: tail✝ = [x]

Tactic:
grind

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

Goal state before:
pp: α : Type u
l : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
⊢ count x l ≤ 1 ↔ 0 < count x l → count x l = 1

Tactic:
grind

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

Goal state before:
pp: α : Type u
l : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : ∀ (a : α), count a l = 1
a : α
⊢ 1 ≤ count a l

Tactic:
grind

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

Goal state before:
pp: case cons.inl.inl
α : Type u
β : Type v
f : α → β
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
y✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f y✝) ∧ (map f tl).Nodup
h₃ : f y✝ = f y✝
⊢ y✝ = y✝

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
β : Type v
f : α → β
hd : α
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (map f (hd :: tl)).Nodup
⊢ ∀ ⦃x : α⦄, x ∈ hd :: tl → ∀ ⦃y : α⦄, y ∈ hd :: tl → f x = f y → x = y

Tactic:
| cons hd tl ih =>

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

Goal state before:
pp: α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b
h : l.Nodup
⊢ (List.pmap f l H).Nodup

Tactic:
grind

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

Goal state before:
pp: case cons.succ
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
IH : l.Nodup → ∀ (i : ℕ) (h : i < l.length), l.erase l[i] = l.eraseIdx i
hl : (a :: l).Nodup
i : ℕ
h : i + 1 < (a :: l).length
⊢ (a :: l).erase (a :: l)[i + 1] = (a :: l).eraseIdx (i + 1)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
⊢ t.card ≤ s.card

Tactic:
rw [← s.card_map f, ← t.card_map f]

Goal state after:
α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
⊢ (map f t).card ≤ (map f s).card
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset α
t : Multiset γ
f : γ → β
⊢ Rel (flip fun a b ↦ flip r (f a) b) s t ↔ Rel (fun a b ↦ r a (f b)) s t

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
⊢ ([] ++ l₂).dedup = [] ∪ l₂.dedup

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x✝ : List α
⊢ [] <+ []

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ [] ∩ [] = []

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ∩ [] = []
⊢ (head✝ :: tail✝) ∩ [] = []

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
⊢ l₁ ∩ l₂ = [] ↔ l₁.Disjoint l₂

Tactic:
simp only [eq_nil_iff_forall_not_mem, mem_inter_iff, not_and]

Goal state after:
α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
⊢ (∀ (a : α), a ∈ l₁ → ¬a ∈ l₂) ↔ l₁.Disjoint l₂
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
⊢ (∀ (a : α), a ∈ l₁ → ¬a ∈ l₂) ↔ l₁.Disjoint l₂

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ [].bagInter [] = []

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
⊢ [].bagInter (head✝ :: tail✝) = []

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).bagInter [] = []

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u_1
l₁ : List α
a : α
inst✝ : DecidableEq α
l₂ : List α
h : ¬a ∈ []
⊢ [].bagInter (a :: l₂) = [].bagInter l₂

Tactic:
grind

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

Goal state before:
pp: case cons
α : Type u_1
l₁ : List α
a : α
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (l₂ : List α), ¬a ∈ tail✝ → tail✝.bagInter (a :: l₂) = tail✝.bagInter l₂
l₂ : List α
h : ¬a ∈ head✝ :: tail✝
⊢ (head✝ :: tail✝).bagInter (a :: l₂) = (head✝ :: tail✝).bagInter l₂

Tactic:
grind

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

Goal state before:
pp: case case1
α : Type u_1
inst✝ : DecidableEq α
a : α
x✝ : List α
⊢ a ∈ [] ↔ a ∈ [] ∧ a ∈ x✝

Tactic:
grind

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

Goal state before:
pp: case case2
α : Type u_1
inst✝ : DecidableEq α
a : α
t✝ : List α
x✝ : t✝ = [] → False
⊢ a ∈ [] ↔ a ∈ t✝ ∧ a ∈ []

Tactic:
grind

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

Goal state before:
pp: case case3
α : Type u_1
inst✝ : DecidableEq α
a a✝ : α
l₁✝ l₂✝ : List α
x✝ : l₂✝ = [] → False
h✝ : elem a✝ l₂✝ = true
ih1✝ : a ∈ l₁✝.bagInter (l₂✝.erase a✝) ↔ a ∈ l₁✝ ∧ a ∈ l₂✝.erase a✝
⊢ a ∈ a✝ :: l₁✝.bagInter (l₂✝.erase a✝) ↔ a ∈ a✝ :: l₁✝ ∧ a ∈ l₂✝

Tactic:
grind

Goal state after: