mathlib-initiative/mathlib-tactics huggingface dataset:
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
b : H
inst✝² : AddCommGroupWithOne G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H 1 b
f : F
n : ℤ
x : G
⊢ f (↑n + x) = f x + n • b

Tactic:
← map_zsmul_add,

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
b : H
inst✝² : AddCommGroupWithOne G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H 1 b
f : F
n : ℤ
x : G
⊢ f (↑n + x) = f (n • 1 + x)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ a + (b - 1) * a = b * a

Tactic:
by rw [sub_one_mul, add_sub_cancel]

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ : P
⊢ (p₁ /ₛ p₂)⁻¹ = p₂ /ₛ p₁

Tactic:
by
  refine inv_eq_of_mul_eq_one_right (smul_right_cancel p₁ ?_)
  rw [sdiv_mul_sdiv_cancel, sdiv_self]

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
v₁ v₂ : G
p : P
⊢ v₁ • p /ₛ v₂ • p = v₁ / v₂

Tactic:
sdiv_smul_eq_sdiv_div,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
v₁ v₂ : G
p : P
⊢ (v₁ • p /ₛ p) / v₂ = v₁ / v₂
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
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ g⁻¹ • ↑m⁻¹ * g • ↑m = 1

Tactic:
by rw [smul_mul_smul_comm, Units.inv_mul, inv_mul_cancel, one_smul]

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
inst✝ : Archimedean K
x y : K
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : x < ↑z / ↑n
zh' : ↑z / ↑n < y
⊢ ∃ q, x < ↑q ∧ ↑q < y

Tactic:
refine ⟨(z : ℚ) / n, ?_, ?_⟩

Goal state after:
case refine_1
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : x < ↑z / ↑n
zh' : ↑z / ↑n < y
⊢ x < ↑(↑z / ↑n)

case refine_2
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : x < ↑z / ↑n
zh' : ↑z / ↑n < y
⊢ ↑(↑z / ↑n) < y
Module: Mathlib.Algebra.Torsor.Basic

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

Tactic:
sdiv_smul_eq_sdiv_div,

Goal state after:
G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
v : G
p₁ p₂ : P
⊢ (v • p₁ /ₛ p₂) / v = p₁ /ₛ p₂
Module: Mathlib.Algebra.Torsor.Basic

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

Tactic:
sdiv_smul_eq_sdiv_div,

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

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

Tactic:
by
    rintro ⟨l⟩ hl
    lift l to List β using hl
    exact ⟨l, map_coe _ _⟩

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.Multiset.MapFold

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

Tactic:
← rel_flip

Goal state after:
α : 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
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ l₃ : List α
h : l₁ <+ l₂
⊢ l₁ ∩ l₃ <+ l₂ ∩ l₃

Tactic:
grind [inter_def]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
⊢ a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂

Tactic:
fun_induction List.bagInter with

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
⊢ count a (l₁.bagInter l₂) = min (count a l₁) (count a l₂)

Tactic:
fun_induction List.bagInter with

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₁.bagInter l₂ <+ l₁

Tactic:
fun_induction List.bagInter with

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
⊢ List.drop n xs ~ ys ∩ List.drop n xs

Tactic:
by
  by_cases h'' : n ≤ xs.length
  · let n' := xs.length - n
    have h₀ : n = xs.length - n' := by rwa [Nat.sub_sub_self]
    have h₁ : xs.drop n = (xs.reverse.take n').reverse := by
      rw [take_reverse, h₀, reverse_reverse]
    rw [h₁]
    apply (reverse_perm _).trans
    rw [inter_reverse]
    apply Perm.take_inter _ _ h'
    apply (reverse_perm _).trans; assumption
  · grind [drop_eq_nil_of_le]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ s ∪ 0 = s

Tactic:
by simp [union_def]

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

Goal state before:
pp: α : Type u_1
a : α
s t : Multiset α
⊢ _root_.Disjoint s (a ::ₘ t) ↔ ¬a ∈ s ∧ _root_.Disjoint s t

Tactic:
rw [_root_.disjoint_comm, disjoint_cons_left]; tauto

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : a ∈ s
⊢ filter p (s.erase a) - filter p t = filter p s - filter p t

Tactic:
(by rw [filter_cons_of_neg _ h] : filter p (erase s a) = filter p (a ::ₘ erase s a)),

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : a ∈ s
⊢ filter p (a ::ₘ s.erase a) - filter p t = filter p s - filter p t
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ sᶜ ≠ univ ↔ s.Nonempty

Tactic:
by
  simp [eq_univ_iff_forall, Finset.Nonempty]

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

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

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
f : α → β
⊢ t ⊆ image f univ ↔ ∃ s', image f s' = t

Tactic:
by simp [subset_image_iff]

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

Goal state before:
pp: n m : ℕ
hmn : m ≤ n
a b : Fin m
⊢ castLE hmn a = castLE hmn b ↔ a = b

Tactic:
by
  simp [Fin.ext_iff]

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

Goal state before:
pp: n : ℕ
motive : Fin n → Prop
h : ∀ (j : Fin n), (∀ (k : Fin n), k < j → motive k) → motive j
i : Fin n
⊢ motive i

Tactic:
by
  obtain ⟨i, hi⟩ := i
  induction i using Nat.strong_induction_on with
  | h j hj => exact h _ (fun ⟨k, hk₁⟩ hk₂ ↦ hj _ hk₂ hk₁)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
⊢ 0 ∉ map { toFun := succ, inj' := ⋯ } univ

Tactic:
simp [map_eq_image]

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

Goal state before:
pp: n : ℕ
⊢ univ = Finset.cons 0 (map { toFun := succ, inj' := ⋯ } univ) ⋯

Tactic:
simp [map_eq_image]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
⊢ last n ∉ map castSuccEmb univ

Tactic:
simp [map_eq_image]

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

Goal state before:
pp: n : ℕ
⊢ univ = Finset.cons (last n) (map castSuccEmb univ) ⋯

Tactic:
simp [map_eq_image]

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
⊢ univ = Finset.cons p (map p.succAboveEmb univ) ⋯

Tactic:
simp [map_eq_image]

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

Goal state before:
pp: α : Type u_1
s : Finset α
hs : 1 < #s
a : α
this : Nonempty α
⊢ ∃ b ∈ s, b ≠ a

Tactic:
by_contra!

Goal state after:
α : Type u_1
s : Finset α
hs : 1 < #s
a : α
this✝ : Nonempty α
this : ∀ b ∈ s, b = a
⊢ False
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i j : Fin (n + 1)
⊢ cons x₀ x i = cons x₀ x j → i = j

Tactic:
cases i using Fin.cases <;> cases j using Fin.cases

Goal state after:
case zero.zero
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
⊢ cons x₀ x 0 = cons x₀ x 0 → 0 = 0

case zero.succ
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i✝ : Fin n
⊢ cons x₀ x 0 = cons x₀ x i✝.succ → 0 = i✝.succ

case succ.zero
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i✝ : Fin n
⊢ cons x₀ x i✝.succ = cons x₀ x 0 → i✝.succ = 0

case succ.succ
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i✝¹ i✝ : Fin n
⊢ cons x₀ x i✝¹.succ = cons x₀ x i✝.succ → i✝¹.succ = i✝.succ
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : Std.Symm r
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ Pairwise (r on f)

Tactic:
rcases exists_seq_of_forall_finset_exists P r h with ⟨f, hf, hf'⟩

Goal state after:
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : Std.Symm r
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ Pairwise (r on f)
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_4
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ (∃! a, p a) ↔ #{x | p x} = 1

Tactic:
rw [Finset.card_eq_one]

Goal state after:
α : Type u_4
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ (∃! a, p a) ↔ ∃ a, {x | p x} = {a}
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case inr
α : Type u_1
p : (s : Finset α) → s.Nonempty → Prop
h₀ : ∀ (a : α), p {a} ⋯
h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯
s : Finset α
hs✝ : s.Nonempty
hs : s.Nontrivial
t : Finset α
ht : t.Nonempty
hts : t ⊂ s
this : #t < #s
⊢ p t ht

Tactic:
exact ht.strong_induction h₀ h₁

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

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

Tactic:
simp [addCases, this]

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

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

Tactic:
simp [addCases, this]

Goal state after:
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ card α = card Unit ↔ ∃ x, ∀ (y : α), y = x

Tactic:
card_eq

Goal state after:
α : Type u_1
inst✝ : Fintype α
⊢ Nonempty (α ≃ Unit) ↔ ∃ x, ∀ (y : α), y = x
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Type u_3
f : Fin (n + 1) → α
⊢ (last n).removeNth f = init f

Tactic:
by
  ext; simp [init, removeNth]

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)
⊢ i.removeNth (j.removeNth m) ≍ (i.predAbove j).removeNth ((j.succAbove i).removeNth m)

Tactic:
apply Function.hfunext rfl

Goal state after:
n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
⊢ ∀ (a a' : Fin n), a ≍ a' → i.removeNth (j.removeNth m) a ≍ (i.predAbove j).removeNth ((j.succAbove i).removeNth m) a'
Module: Mathlib.Data.List.Range

Goal state before:
pp: case cons
a : ℕ
l : List ℕ
hl : map length l.ranges = l
⊢ map (length ∘ map fun x ↦ a + x) l.ranges = l

Tactic:
conv_rhs => rw [← hl]

Goal state after:
case cons
a : ℕ
l : List ℕ
hl : map length l.ranges = l
⊢ map (length ∘ map fun x ↦ a + x) l.ranges = map length l.ranges
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).length
⊢ (l ++ [a]).rotate' n = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)

Tactic:
rotate'_eq_drop_append_take hnl',

Goal state after:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).length
⊢ drop n (l ++ [a]) ++ take n (l ++ [a]) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ m - (drop (n % l.length) l).length < n % l.length

Tactic:
rwa [Nat.sub_lt_iff_lt_add' hm, length_drop, Nat.sub_add_cancel hlt.le]

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

Goal state before:
pp: case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length ≤ (x :: l).reverse.length

pp: case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length < (x :: l).reverse.length

Tactic:
· exact Nat.sub_le _ _

Goal state after:
case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length < (x :: l).reverse.length
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g
a : ↥s
x✝¹ : a ∈ ↑s.attach
b : ↥s
x✝ : b ∈ ↑s.attach
hab : a ≠ b
x : γ
hxa : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) a
hxb : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) b
xa : β
hfa : xa ∈ f ↑a
hga : x ∈ g xa
hfb : xa ∈ f ↑b
hgb : x ∈ g xa
⊢ False

Tactic:
exact disjoint_left.mp (h1 a.prop b.prop <| Subtype.coe_injective.ne hab) hfa hfb

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

Goal state before:
pp: case mp
α : Type u
l l' : List α
⊢ l.reverse ~r l' → l ~r l'.reverse

Tactic:
· intro h
      simpa using h.reverse

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

Goal state before:
pp: case mpr
α : Type u
l l' : List α
⊢ l ~r l'.reverse → l.reverse ~r l'

Tactic:
· intro h
      simpa using h.reverse

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

Goal state before:
pp: s : Multiset ℤ
n : ℤ
⊢ s.sum % n = (map (fun x ↦ x % n) s).sum % n

Tactic:
by
  induction s using Multiset.induction <;> simp [Int.add_emod, *]

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

Goal state before:
pp: α : Type u
x : α
l : List α
⊢ (x :: l).cyclicPermutations.length = l.length + 1

Tactic:
simp [cyclicPermutations_cons]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
⊢ count (a, b) (c :: l).offDiag = count a (c :: l) * count b (c :: l) - if a = b then count a (c :: l) else 0

Tactic:
have H₂ {x y z : α} : count (x, y) (map (·, z) l) = if z = y then count x l else 0 := by
      split_ifs with h
      · rw [h, count_map_of_injective l (·, y) (by simp [Function.Injective])]
      · simp [count_eq_zero, h]

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (x, z)) l) = if z = y then count x l else 0
⊢ count (a, b) (c :: l).offDiag = count a (c :: l) * count b (c :: l) - if a = b then count a (c :: l) else 0
Module: Mathlib.Data.List.OffDiag

Goal state before:

Tactic:
1 + l.count a < l.count a + l.count a := by simpa
    _ ≤ l.count a * l.count a := by
      rw [← Nat.two_mul]
      exact Nat.mul_le_mul_right _ h

Goal state after:
Module: Mathlib.Data.Fintype.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
H : Infinite (α × β)
a : α
b : β
⊢ Nonempty β ∧ Infinite α ∨ Nonempty α ∧ Infinite β

Tactic:
contrapose! H

Goal state after:
α : Type u_1
β : Type u_2
a : α
b : β
H : (Nonempty β → Finite α) ∧ (Nonempty α → Finite β)
⊢ Finite (α × β)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n : ℕ
⊢ n.multichoose 1 = n

Tactic:
by
  induction n with
  | zero => simp
  | succ n IH => simp [multichoose_succ_succ n 0, IH]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : s.Nodup
b₁ : β a
x✝³ : b₁ ∈ t a
b₂ : β a
x✝² : b₂ ∈ t a
neb : b₁ ≠ b₂
f : (a : α) → a ∈ s → β a
x✝¹ : f ∈ s.pi t
g : (a : α) → a ∈ s → β a
x✝ : g ∈ s.pi t
eq : Pi.cons s a b₁ f = Pi.cons s a b₂ g
this : Pi.cons s a b₁ f a ⋯ = Pi.cons s a b₂ g a ⋯
⊢ b₁ = b₂

Tactic:
rwa [Pi.cons_same, Pi.cons_same] at this

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
⊢ ¬(t.Nonempty → s.Finite) ∨ ¬(s.Nonempty → t.Finite)

Tactic:
by_contra!

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
this : (t.Nonempty → s.Finite) ∧ (s.Nonempty → t.Finite)
⊢ False
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: δ : Type u_4
α : Type u_9
β : Type u_10
γ : Type u_11
s : Set α
t : Set β
f : α → Set γ
g : β → Set δ
fst✝ : γ
snd✝ : δ
⊢ (fst✝, snd✝) ∈ ⋃ x ∈ s ×ˢ t, f x.1 ×ˢ g x.2 ↔ (fst✝, snd✝) ∈ (⋃ x ∈ s, f x) ×ˢ ⋃ x ∈ t, g x

Tactic:
simp only [mem_iUnion, mem_prod, exists_prop, Prod.exists]

Goal state after:
δ : Type u_4
α : Type u_9
β : Type u_10
γ : Type u_11
s : Set α
t : Set β
f : α → Set γ
g : β → Set δ
fst✝ : γ
snd✝ : δ
⊢ (∃ a b, (a ∈ s ∧ b ∈ t) ∧ fst✝ ∈ f a ∧ snd✝ ∈ g b) ↔ (∃ i ∈ s, fst✝ ∈ f i) ∧ ∃ i ∈ t, snd✝ ∈ g i
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nontrivial ↥H ↔ H ≠ ⊥

Tactic:
by
  rw [nontrivial_iff_exists_ne_one, ne_eq, eq_bot_iff_forall]
  simp only [ne_eq, not_forall, exists_prop]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Surjective ⇑f
H K : Subgroup G
h : Codisjoint H K
⊢ Codisjoint (map f H) (map f K)

Tactic:
codisjoint_iff,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Surjective ⇑f
H K : Subgroup G
h : Codisjoint H K
⊢ map f H ⊔ map f K = ⊤
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (K ⊓ H).subgroupOf K = H.subgroupOf K

Tactic:
by
  rw [inf_comm, inf_subgroupOf_right]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
⊢ H ⊔ f.ker = ⊤ ⊔ f.ker ↔ Codisjoint H f.ker

Tactic:
codisjoint_iff,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
⊢ H ⊔ f.ker = ⊤ ⊔ f.ker ↔ H ⊔ f.ker = ⊤
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ Codisjoint (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K))

Tactic:
codisjoint_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.subgroupOf (H ⊔ K) ⊔ K.subgroupOf (H ⊔ K) = ⊤
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: M : Type u_5
N : Type u_6
inst✝¹ : CommGroup M
inst✝ : CommGroup N
e : M ≃* N
n : ℕ
⊢ Subgroup.map (↑e) (powMonoidHom n).range = (powMonoidHom n).range

Tactic:
by
  have H : (e : M →* N).comp (powMonoidHom n) = (powMonoidHom n).comp e := by ext : 1; simp
  rw [map_range, H, range_comp, e.range_eq_top, ← range_eq_map]

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

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
x : M × N
⊢ x ∈ s.prod ⊤ ↔ x ∈ comap (MonoidHom.fst M N) s

Tactic:
simp [mem_prod, MonoidHom.coe_fst]

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
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
hf : Surjective ⇑f
H K : Submonoid M
h : Codisjoint H K
⊢ Codisjoint (map f H) (map f K)

Tactic:
codisjoint_iff,

Goal state after:
M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
hf : Surjective ⇑f
H K : Submonoid M
h : Codisjoint H K
⊢ map f H ⊔ map f K = ⊤
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case neg
a b : ℕ
h : ¬a < b
⊢ unpair (a * a + a + b) = (a, b)

Tactic:
show unpair (a * a + a + b) = (a, b)

Goal state after:
case neg
a b : ℕ
h : ¬a < b
⊢ unpair (a * a + a + b) = (a, b)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
K : Subgroup G
x : G × N
⊢ x ∈ K.prod ⊤ ↔ x ∈ comap (MonoidHom.fst G N) K

Tactic:
simp [mem_prod, MonoidHom.coe_fst]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
y : G
hy : map (↑(MulAut.conj y)) H = H
hx : f y ∈ map f (normalizer ↑H)
this : (↑(MulAut.conj (f y))).comp f = f.comp ↑(MulAut.conj y)
⊢ map (↑(MulAut.conj (f y))) (map f H) = map f H

Tactic:
rw [map_map, this, ← map_map, hy]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : LinearOrder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
l : List ι
hl : l ≠ []
f g : ι → M
h : (map f l).prod ≤ (map g l).prod
⊢ ∃ x, x ∈ l ∧ f x ≤ g x

Tactic:
by
  contrapose! h
  exact prod_lt_prod_of_ne_nil hl _ _ h

Goal state after: