mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q : ℚ
⊢ IsSquare q ↔ IsSquare q.num ∧ IsSquare q.den

Tactic:
by
  constructor
  · rintro ⟨qr, rfl⟩
    rw [Rat.mul_self_num, mul_self_den]
    simp only [IsSquare.mul_self, and_self]
  · rintro ⟨⟨nr, hnr⟩, ⟨dr, hdr⟩⟩
    refine ⟨nr / dr, ?_⟩
    rw [div_mul_div_comm, ← Int.cast_mul, ← Nat.cast_mul, ← hnr, ← hdr, num_div_den]

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

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a b : ℕ
⊢ ↑(divNat a b) = ↑a / ↑b

Tactic:
by
  rw [← cast_natCast, ← cast_natCast b, ← cast_div]
  congr
  ext
  apply Rat.mkRat_eq_div

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

Goal state before:
pp: case node
α : Type u
v : α
l r : BinaryTree α
hl : map id l = l
hr : map id r = r
⊢ map id (node v l r) = node v l r

Tactic:
rw [map, hl, hr, id_eq]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
⊢ ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f (i + k) = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f i

Tactic:
have hf : Monotone fun n => ⨅ i ≥ n, f i := fun n m h => biInf_mono fun i => h.trans

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
hf : Monotone fun n ↦ ⨅ i, ⨅ (_ : i ≥ n), f i
⊢ ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f (i + k) = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f i
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : SupSet α
p q : Prop
f₁ : p → α
f₂ : q → α
pq : p ↔ q
f : ∀ (x : q), f₁ ⋯ = f₂ x
⊢ iSup f₁ = iSup f₂

Tactic:
obtain rfl := propext pq
  congr with x
  apply f

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : Unique ι
f : ι → α
⊢ ⨆ i, f i = f default

Tactic:
simp only [congr_arg f (Unique.eq_default _), iSup_const]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
g : ((i : ι) → κ i) → ι
⊢ ∃ a, ∀ (b : κ a), ∃ f, ∃ (h : a = g f), h ▸ b = f (g f)

Tactic:
by_contra! h

Goal state after:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
g : ((i : ι) → κ i) → ι
h : ∀ (a : ι), ∃ b, ∀ (f : (i : ι) → κ i) (h : a = g f), h ▸ b ≠ f (g f)
⊢ False
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : OrderBot α
x y : ↑(Iic a)
⊢ Disjoint x y ∧ Codisjoint x y ↔ Disjoint ↑x ↑y ∧ ↑x ⊔ ↑y = a

Tactic:
Iic.disjoint_iff,

Goal state after:
α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : OrderBot α
x y : ↑(Iic a)
⊢ Disjoint ↑x ↑y ∧ Codisjoint x y ↔ Disjoint ↑x ↑y ∧ ↑x ⊔ ↑y = a
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
simp only [inf_iSup_eq]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ι a b = Ι b a

Tactic:
simp only [uIoc, min_comm a b, max_comm a b]

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

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

Tactic:
rw [pa.out]

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : Lattice α
inst✝ : IsOrderedRing α
a : α
na : ℕ
pa : IsInt a (Int.negOfNat na)
⊢ IsNat |↑(Int.negOfNat na)| na
Module: Mathlib.Tactic.NormNum.Abs

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

Tactic:
exact Nat.cast_nonneg' num

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

Goal state before:
pp: case inl
m n : ℕ
hn : 1 < n
⊢ n ! = m ! ↔ n = m

pp: case inr
m n : ℕ
hm : 1 < m
⊢ n ! = m ! ↔ n = m

Tactic:
· exact factorial_inj hn

Goal state after:
case inr
m n : ℕ
hm : 1 < m
⊢ n ! = m ! ↔ n = m
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
h : 0 < n
⊢ (n - 1)! * n.ascFactorial k = (n + k - 1)!

Tactic:
by
  rw [Nat.sub_add_comm h, Nat.sub_one]
  nth_rw 2 [Nat.eq_add_of_sub_eq h rfl]
  rw [Nat.sub_one, factorial_mul_ascFactorial]

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

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

Tactic:
rw [descFactorial_eq_zero_iff_lt.mpr (show n < m by lia)]

Goal state after:
case neg
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: a b : ℕ+
⊢ a - b ≤ a

Tactic:
← coe_le_coe,

Goal state after:
a b : ℕ+
⊢ ↑(a - b) ≤ ↑a
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: a b : ℕ+
hab : a < b
⊢ a ≤ b - 1

Tactic:
← coe_le_coe,

Goal state after:
a b : ℕ+
hab : a < b
⊢ ↑a ≤ ↑(b - 1)
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 < n
a b : α
hab : a < b
⊢ (fun x ↦ x ^ n) a < (fun x ↦ x ^ n) b

Tactic:
rw [← one_lt_div', ← div_zpow]; exact one_lt_zpow (one_lt_div'.2 hab) hn

Goal state after:
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
⊢ -↑k ∈ s

Tactic:
simpa [s] using inv_le_inv' hk

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

Goal state before:
pp: case below
R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
n : ℤ
hn : ↑n < x
⊢ ∃ n, ↑n ≤ x

Tactic:
exact ⟨n, hn.le⟩

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

Goal state before:
pp: case above
R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
n : ℤ
hn : x < ↑n
⊢ ∃ n, x ≤ ↑n

Tactic:
exact ⟨n, hn.le⟩

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 : K
n : ℤ
h : x < ↑n
⊢ ∃ n, x < ↑n

Tactic:
refine ⟨n.toNat, h.trans_le ?_⟩

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 : ℤ
h : x < ↑n
⊢ ↑n ≤ ↑n.toNat
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
h : l[0]? = l.getLast?
⊢ l.reverse.tail.Nodup ↔ l.tail.Nodup

Tactic:
by
  induction l with
  | nil => simp
  | cons a l ih =>
    by_cases hl : l = []
    · simp_all
    · simp_all only [List.tail_reverse, List.nodup_reverse,
        List.dropLast_cons_of_ne_nil hl, List.tail_cons]
      simp only [length_cons, Nat.zero_lt_succ, getElem?_eq_getElem,
        Nat.add_one_sub_one, Nat.lt_add_one, Option.some.injEq, List.getElem_cons,
        show l.length ≠ 0 by aesop, ↓reduceDIte, getLast?_eq_getElem?] at h
      rw [h,
        show l.Nodup = (l.dropLast ++ [l.getLast hl]).Nodup by
          simp [List.dropLast_eq_take],
        List.nodup_append_comm]
      simp [List.getLast_eq_getElem]

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

Goal state before:
pp: α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ : α
b₁ : β
left✝ : b₁ ∈ l₂
h₁ : (a₁, b₁) ∈ (fun a ↦ map (Prod.mk a) l₂) a₁
n : a₁ ≠ a₁
h₂ : (a₁, b₁) ∈ (fun a ↦ map (Prod.mk a) l₂) a₁
mb₂ : b₁ ∈ l₂
⊢ False

Tactic:
exact n rfl

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

Goal state before:
pp: α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ : α
b₁ : σ a₁
left✝ : b₁ ∈ l₂ a₁
h₁ : ⟨a₁, b₁⟩ ∈ (fun a ↦ map (Sigma.mk a) (l₂ a)) a₁
n : a₁ ≠ a₁
h₂ : ⟨a₁, b₁⟩ ∈ (fun a ↦ map (Sigma.mk a) (l₂ a)) a₁
mb₂ : b₁ ∈ l₂ a₁
⊢ False

Tactic:
exact n rfl

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

Goal state before:
pp: α : Type u
β : Type v
l : List α
f : α → Option β
h : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : f a = some b
b' : β
bm' : f a' = some b'
e : b = b'
⊢ b ∈ f a

Tactic:
exact bm

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

Goal state before:
pp: case neg
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (s.erase x) = (map f s).erase (f x)
hxy : ¬y = x
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)

Tactic:
rw [s.erase_cons_tail hxy, map_cons, map_cons, (s.map f).erase_cons_tail (hf.ne hxy), ih]

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
p : α → Prop
inst✝ : DecidableEq α
⊢ (∀ (x : α), x ∈ l₁ ∪ l₂ → p x) ↔ (∀ (x : α), x ∈ l₁ → p x) ∧ ∀ (x : α), x ∈ l₂ → p x

Tactic:
simp only [mem_union_iff, or_imp, forall_and]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s ∩ t + u = (s + u) ∩ (t + u)

Tactic:
by_contra! h

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : s ∩ t + u ≠ (s + u) ∩ (t + u)
⊢ False
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
s t₁ t₂ : Finset α
h₁ : Disjoint s t₁
h₂ : Disjoint s t₂
⊢ s.disjUnion t₁ h₁ = s.disjUnion t₂ h₂ ↔ t₁ = t₂

Tactic:
simp [← val_inj, Multiset.add_right_inj]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x✝ : f a × ((i : α) → i ∈ s → f i)
⊢ consPiProd f has (prodPiCons f has x✝) = x✝

Tactic:
ext _ hi

Goal state after:
case fst
α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x✝ : f a × ((i : α) → i ∈ s → f i)
⊢ (consPiProd f has (prodPiCons f has x✝)).1 = x✝.1

case snd
α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x✝¹ : f a × ((i : α) → i ∈ s → f i)
x✝ : α
hi : x✝ ∈ s
⊢ (consPiProd f has (prodPiCons f has x✝¹)).2 x✝ hi = x✝¹.2 x✝ hi
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ b : α
f✝ : α → β
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x✝ : f a × ((i : α) → i ∈ s → f i)
⊢ insertPiProd f (prodPiInsert f x✝) = x✝

Tactic:
ext _ hi

Goal state after:
case fst
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ b : α
f✝ : α → β
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x✝ : f a × ((i : α) → i ∈ s → f i)
⊢ (insertPiProd f (prodPiInsert f x✝)).1 = x✝.1

case snd
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ b : α
f✝ : α → β
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x✝¹ : f a × ((i : α) → i ∈ s → f i)
x✝ : α
hi : x✝ ∈ s
⊢ (insertPiProd f (prodPiInsert f x✝¹)).2 x✝ hi = x✝¹.2 x✝ hi
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
a : α
⊢ a ∈ s.toFinset ↔ a ∈ s

Tactic:
simp [toFinset]

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

Goal state before:
pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.rev ≤ i.castSucc
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

Tactic:
succAbove_of_le_castSucc _ _ h,

Goal state after:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.rev ≤ i.castSucc
⊢ i.succ = (p.succAbove i.rev).rev
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i.rev ≤ p.castSucc
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev

Tactic:
rw [predAbove_of_le_castSucc _ _ h, rev_castPred,
      predAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)), pred_inj, rev_rev]

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ i.succ ≤ p ∨ p < i.succ

Tactic:
← castSucc_lt_iff_succ_le

Goal state after:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ i.castSucc < p ∨ p < i.succ
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
β : Type u_1
l : List α
f : α → β
⊢ map f (ofFn fun i ↦ l[↑i]) = map f l

Tactic:
ofFn_getElem

Goal state after:
α : Type u
β : Type u_1
l : List α
f : α → β
⊢ map f l = map f l
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
n : ℕ
a : α
f : Fin n → α
⊢ ofFn (Fin.cons a f) = a :: ofFn f

Tactic:
by
  rw [ofFn_succ]
  rfl

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

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.succ ≤ i
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ

Tactic:
rwa [succAbove_of_castSucc_lt _ _ h, succAbove_succ_of_le, succ_castSucc]

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

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

Tactic:
succAbove_of_le_castSucc _ _ h,

Goal state after:
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ i.castSucc.succAbove j.castSucc = j.succ.castSucc
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ (last (n + 1)).pred ⋯ = last n

Tactic:
pred_last

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ last n = last n
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
hs : 1 < #s
a : α
this✝ : Nonempty α
this : ∀ b ∈ s, b = a
⊢ False

Tactic:
exact hs.not_ge (card_le_one_iff_subset_singleton.2 ⟨a, subset_singleton_iff'.2 this⟩)

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
inst✝ : DecidableEq α
h : #s = n + 1
a : α
has : a ∈ s
⊢ #(s.erase a) = n

Tactic:
by
      simp only [h, card_erase_of_mem has, Nat.add_sub_cancel_right]

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

Goal state before:
pp: case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ append u v (natAdd m r) = (v ∘ Fin.cast ⋯) (natAdd m r)

Tactic:
· rw [append_right, Function.comp_apply]
    refine congr_arg v (Fin.ext ?_)
    simp [hu]

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

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ (i.castPred ⋯).predAbove (i.succAbove j) = j

Tactic:
succAbove_of_le_castSucc _ _ h,

Goal state after:
case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ (i.castPred ⋯).predAbove j.succ = j
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ (i.succAbove j).succAbove (j.predAbove i) = i

Tactic:
succAbove_of_le_castSucc _ _ h,

Goal state after:
case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ j.succ.succAbove (j.predAbove i) = i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case cast.last
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
i : Fin n
h : snoc x x₀ i.castSucc = snoc x x₀ (last n)
⊢ i.castSucc = last n

Tactic:
simp only [snoc_castSucc, snoc_last] at h

Goal state after:
case cast.last
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
i : Fin n
h : x i = x₀
⊢ i.castSucc = last n
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case last.cast
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
j : Fin n
h : snoc x x₀ (last n) = snoc x x₀ j.castSucc
⊢ last n = j.castSucc

Tactic:
simp only [snoc_castSucc, snoc_last] at h

Goal state after:
case last.cast
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
j : Fin n
h : x₀ = x j
⊢ last n = j.castSucc
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
w : ∀ (s : Finset ι), #s ≤ n
i : Infinite ι
s : Finset ι
c : #s = n + 1
⊢ False

Tactic:
specialize w s

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
i : Infinite ι
s : Finset ι
w : #s ≤ n
c : #s = n + 1
⊢ False
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
L : List α
a b : α
⊢ count a (orderedInsert r b L) = count a L + if b = a then 1 else 0

Tactic:
rw [(L.perm_orderedInsert r b).count_eq, count_cons]
  simp

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

Goal state before:
pp: α : Type u
s t : Set α
hs : s.Infinite
ht : t.Finite
⊢ ∃ a ∈ s, a ∉ t

Tactic:
by_contra! h

Goal state after:
α : Type u
s t : Set α
hs : s.Infinite
ht : t.Finite
h : ∀ a ∈ s, a ∈ t
⊢ False
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
inst✝ : Infinite α
hs : s.Finite
⊢ ∃ a, a ∉ s

Tactic:
by_contra! h

Goal state after:
α : Type u
s : Set α
inst✝ : Infinite α
hs : s.Finite
h : ∀ (a : α), a ∈ s
⊢ False
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Bool
h : ∃ i, p i = true
⊢ find? p = some (Fin.find (fun x ↦ p x = true) h)

Tactic:
simp_rw [find?_eq_dite, h, dite_true]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha : a ∈ l
hlast : R (l.getLast ⋯) (l.getLast ⋯)
⊢ R a (l.getLast ⋯)

Tactic:
by
  rw [← dropLast_concat_getLast (ne_nil_of_mem ha), mem_append, List.mem_singleton] at ha
  exact ha.elim h₁.rel_dropLast_getLast (· ▸ hlast)

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

Goal state before:
pp: case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ ∀ (a' : List ℕ), a' ∈ map (map fun x ↦ a + x) l.ranges → (range a).Disjoint a'

pp: case cons.right
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise Disjoint (map (map fun x ↦ a + x) l.ranges)

Tactic:
· intro s hs
      obtain ⟨s', _, rfl⟩ := mem_map.mp hs
      intro u hu
      rw [mem_map]
      rw [mem_range] at hu
      lia

Goal state after:
case cons.right
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise Disjoint (map (map fun x ↦ a + x) l.ranges)
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Multiset M
⊢ foldl (fun x y ↦ y * x) 1 s = foldl (fun x1 x2 ↦ x1 * x2) 1 s

Tactic:
simp [mul_comm]

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

Goal state before:
pp: case refine_2
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n.succ ≠ 0 ∧ a ∈ s
⊢ a ∈ n • s ∨ a ∈ s

Tactic:
exact Or.inr h.2

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

Goal state before:
pp: case inl
α : Type u
l l' : List α
n : ℕ
hl : 0 = l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

pp: case inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Tactic:
· rw [eq_nil_of_length_eq_zero hl.symm, rotate_nil]

Goal state after:
case inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: ι : Type u_2
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
s : Multiset ι
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
g : ι → M
⊢ (map (fun i ↦ f (g i)) s).prod = f (map g s).prod

Tactic:
convert! (s.map g).prod_hom f

Goal state after:
ι : Type u_2
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
s : Multiset ι
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
g : ι → M
⊢ map (fun i ↦ f (g i)) s = map (⇑f) (map g s)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
⊢ [] ~r l ↔ [] = l

Tactic:
isRotated_comm,

Goal state after:
α : Type u
l : List α
⊢ l ~r [] ↔ [] = l
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
x : α
⊢ [x] ~r l ↔ [x] = l

Tactic:
isRotated_comm,

Goal state after:
α : Type u
l : List α
x : α
⊢ l ~r [x] ↔ [x] = l
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case succ
n : ℕ
IH : n.multichoose 1 = n
⊢ (n + 1).multichoose 1 = n + 1

Tactic:
simp [multichoose_succ_succ n 0, IH]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : InvolutiveInv α
s✝ t : Set α
a : α
s : Set α
⊢ s⁻¹⁻¹ = s

Tactic:
simp only [← inv_preimage, preimage_preimage, inv_inv, preimage_id']

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
M' : Type u_5
N' : Type u_6
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
f : M →* N
g : M' →* N'
⊢ comap (f.prodMap g) ⊥ = comap (f.prodMap g) (⊥.prod ⊥)

Tactic:
bot_prod_bot

Goal state after:
M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
M' : Type u_5
N' : Type u_6
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
f : M →* N
g : M' →* N'
⊢ comap (f.prodMap g) ⊥ = comap (f.prodMap g) ⊥
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: A : Type u_2
inst✝ : AddGroup A
x : A
⊢ ⇑Multiplicative.ofAdd.symm '' ↑(Subgroup.zpowers (Multiplicative.ofAdd x)) = ↑(AddSubgroup.zmultiples x)

Tactic:
exact ofMul_image_zpowers_eq_zmultiples_ofMul

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
a : α
⊢ a • sᶜ = (a • s)ᶜ

Tactic:
simp_rw [Set.compl_eq_univ_sdiff, smul_set_sdiff, smul_set_univ]

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
N : Type u_5
inst✝² : Group N
G' : Type u_8
N' : Type u_9
inst✝¹ : Group G'
inst✝ : Group N'
f : G →* N
g : G' →* N'
⊢ comap (f.prodMap g) ⊥ = comap (f.prodMap g) (⊥.prod ⊥)

Tactic:
bot_prod_bot

Goal state after:
G : Type u_1
inst✝³ : Group G
N : Type u_5
inst✝² : Group N
G' : Type u_8
N' : Type u_9
inst✝¹ : Group G'
inst✝ : Group N'
f : G →* N
g : G' →* N'
⊢ comap (f.prodMap g) ⊥ = comap (f.prodMap g) ⊥
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case pos
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
hl_empty : l = []
⊢ f (a * l.prod) ≤ f a * (map f l).prod

pp: case neg
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
hl_empty : ¬l = []
⊢ f (a * l.prod) ≤ f a * (map f l).prod

Tactic:
· simp [hl_empty]

Goal state after:
case neg
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
hl_empty : ¬l = []
⊢ f (a * l.prod) ≤ f a * (map f l).prod