mathlib-initiative/mathlib-tactics huggingface dataset:
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:
apply_rules [add_nonneg, mul_nonneg, Nat.cast_nonneg, pow_nonneg, zero_le_one]

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

Goal state before:
pp: case inr
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ 0 < ↑d

Tactic:
Int.natCast_pos

Goal state after:
case inr
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ 0 < d
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
⊢ ⌈1⌉ = 1

Tactic:
← cast_one,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
⊢ ⌈↑1⌉ = 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⌋ + 1 ↔ a ∉ range Int.cast

Tactic:
refine ⟨fun h ht => ?_, fun h => ?_⟩

Goal state after:
case refine_1
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
h : ⌈a⌉ = ⌊a⌋ + 1
ht : a ∈ range Int.cast
⊢ False

case refine_2
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
h : a ∉ range Int.cast
⊢ ⌈a⌉ = ⌊a⌋ + 1
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: case inr
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
x y : G
hxy : (fun x1 x2 ↦ x1 < x2) x y
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
this : ∀ (x y : G), x < y → x ∈ Ico l (l + a) → R (f x) (f y)
hx : x ∉ Ico l (l + a)
m : ℤ
hm : x - m • a ∈ Ico l (l + a)
⊢ R (f x) (f y)

Tactic:
suffices R (f (x - m • a)) (f (y - m • a)) by simpa using hR (m • b) this

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

Goal state before:
pp: case neg
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 : y < 1
y_pos : 0 < y
⊢ ∃ n, y ^ n < x

Tactic:
rcases pow_unbounded_of_one_lt x⁻¹ ((one_lt_inv₀ y_pos).2 hy) with ⟨q, hq⟩

Goal state after:
case neg
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 : y < 1
y_pos : 0 < y
q : ℕ
hq : x⁻¹ < y⁻¹ ^ q
⊢ ∃ n, y ^ n < x
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : Ring S
inst✝⁴ : LinearOrder S
inst✝³ : FloorRing R
inst✝² : FloorRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
⊢ fract (f a) = f (fract a)

Tactic:
fract,

Goal state after:
F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : Ring S
inst✝⁴ : LinearOrder S
inst✝³ : FloorRing R
inst✝² : FloorRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
⊢ f a - ↑⌊f a⌋ = f (a - ↑⌊a⌋)
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs ⊆ ys
⊢ (xs ++ ys).dedup = ys.dedup

Tactic:
List.dedup_append,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs ⊆ ys
⊢ xs ∪ ys.dedup = ys.dedup
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
⊢ (xs ++ ys).dedup = xs.dedup ++ ys.dedup

Tactic:
List.dedup_append,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
⊢ xs ∪ ys.dedup = xs.dedup ++ ys.dedup
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
⊢ a ∈ s.toList ↔ a ∈ s

Tactic:
by
  rw [← mem_coe, coe_toList]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ count a (filter p s) = 0

Tactic:
by
  simp [h]

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

Goal state before:
pp: α : Type u_1
motive : List α → Sort u_2
x : α
xs : List α
nil : motive []
append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])
⊢ reverseRec nil append_singleton (xs ++ [x]) = append_singleton xs x (reverseRec nil append_singleton xs)

Tactic:
by
  grind [reverseRec, cases List]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
x✝ : s.Nodup ∧ t.Nodup
h₁ : s.Nodup
h₂ : t.Nodup
a : α
⊢ count a (s ∪ t) ≤ 1

Tactic:
by
      rw [count_union]
      exact max_le (nodup_iff_count_le_one.1 h₁ a) (nodup_iff_count_le_one.1 h₂ a)

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

Goal state before:
pp: α : Type u_1
s : Multiset α
p : { a // a ∈ s } → Prop
inst✝¹ : DecidableEq α
inst✝ : DecidablePred p
⊢ map val (filter p s.attach) = map val (map (Subtype.map id ⋯) (filter (fun x ↦ ∃ h, p ⟨x, h⟩) s).attach)

Tactic:
map_filter' _ Subtype.val_injective

Goal state after:
α : Type u_1
s : Multiset α
p : { a // a ∈ s } → Prop
inst✝¹ : DecidableEq α
inst✝ : DecidablePred p
⊢ filter (fun b ↦ ∃ a, p a ∧ ↑a = b) (map val s.attach) =
    map val (map (Subtype.map id ⋯) (filter (fun x ↦ ∃ h, p ⟨x, h⟩) s).attach)
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
hs : s.Nontrivial
⊢ s ≠ {a}

Tactic:
rintro rfl; exact not_nontrivial_singleton hs

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

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ (piFinsetUnion α h) (f, g) ⟨i, hi'⟩ = f ⟨i, hi⟩

Tactic:
simp_rw [piFinsetUnion, sumPiEquivProdPi, piCongrLeft, piCongrLeft', trans_apply, coe_fn_symm_mk]

Goal state after:
ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ ⋯ ▸ Sum.rec f g ((Finset.union s t h).symm ⟨i, hi'⟩) = f ⟨i, hi⟩
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ (piFinsetUnion α h) (f, g) ⟨i, hi'⟩ = g ⟨i, hi⟩

Tactic:
simp_rw [piFinsetUnion, sumPiEquivProdPi, piCongrLeft, piCongrLeft', trans_apply, coe_fn_symm_mk]

Goal state after:
ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ ⋯ ▸ Sum.rec f g ((Finset.union s t h).symm ⟨i, hi'⟩) = g ⟨i, hi⟩
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c✝ : β
c : α → β
p : β → Prop
inst✝ : CanLift β α c p
val✝ : Multiset β
l : List β
hd : l.Nodup
hl : ∀ x ∈ { val := Quot.mk (⇑(List.isSetoid β)) l, nodup := hd }, p x
⊢ ∃ y, image c y = { val := Quot.mk (⇑(List.isSetoid β)) l, nodup := hd }

Tactic:
lift l to List α using hl

Goal state after:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c✝ : β
c : α → β
p : β → Prop
inst✝ : CanLift β α c p
val✝ : Multiset β
l : List α
hd : (List.map c l).Nodup
⊢ ∃ y, image c y = { val := Quot.mk (⇑(List.isSetoid β)) (List.map c l), nodup := hd }
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case succ
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ range (k + 1 + 1) \ {0} = image Nat.succ (range (k + 1))

Tactic:
| succ k hk =>

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

Goal state before:
pp: case isFalse
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑↑u - ↑↑v + ↑n = (↑↑u - ↑↑v) % ↑n

Tactic:
· rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt] <;> omega

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

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

Tactic:
Nat.div_add_mod'

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

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ a.succ < b.succ ↔ a < b

Tactic:
succ_lt_succ_iff

Goal state after:
n : ℕ
a b : Fin n
⊢ a < b ↔ a < b
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin n.succ
hi : i ∈ Set.range castSucc
⊢ ↑((Equiv.ofInjective castSucc ⋯).symm ⟨i, hi⟩) = ↑i

Tactic:
by
  rw [← val_castSucc]
  exact congr_arg val (Equiv.apply_ofInjective_symm _ _)

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

Goal state before:
pp: α : Type u
m : ℕ
f : Fin m → α
⊢ ofFn f = ofFn fun i ↦ f (id i)

Tactic:
id

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

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

Tactic:
rw [succ_castPred_eq_castPred_succ ha, lt_castPred_succ_iff]

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

Goal state before:
pp: n : ℕ
⊢ Set.range succ = {0}ᶜ

Tactic:
rw [← succAbove_zero, range_succAbove]

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
⊢ ofFn f = map f (finRange n)

Tactic:
rw [← ofFn_id, map_ofFn, Function.comp_id]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
j : Fin (n + 1)
h : j ≠ 0
⊢ (predAbove 0 j).succ = j

Tactic:
by
  simp [h]

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

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : i = 0
⊢ predAbove 0 0 = 0

Tactic:
predAbove_right_zero

Goal state after:
case pos
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : i = 0
⊢ 0 = 0
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α✝ : Fin (n + 1) → Sort u
x✝ : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ i.succ
i : Fin n
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
motive : {n : ℕ} → (Fin n → α) → Sort v
elim0 : motive Fin.elim0
cons : {n : ℕ} → (x₀ : α) → (x : Fin n → α) → motive x → motive (Fin.cons x₀ x)
x : Fin 0 → α
⊢ motive x

Tactic:
convert! elim0

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

Tactic:
rw [predAbove_of_le_castSucc _ _ h, succAbove_of_le_castSucc _ _ h, predAbove_of_castSucc_lt,
      pred_succ]

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

Goal state before:
pp: m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
⊢ append (append a b) c = append a (append b c) ∘ Fin.cast ⋯

Tactic:
by
  ext i
  rw [Function.comp_apply]
  refine Fin.addCases (fun l => ?_) (fun r => ?_) i
  · rw [append_left]
    refine Fin.addCases (fun ll => ?_) (fun lr => ?_) l
    · rw [append_left]
      simp [castAdd_castAdd]
    · rw [append_right]
      simp [castAdd_natAdd]
  · rw [append_right]
    simp [← natAdd_natAdd]

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

Goal state before:
pp: n : ℕ
β : Sort u_2
q : Fin (n + 2) → β
i : Fin n
⊢ tail (init q) i = init (tail q) i

Tactic:
simp [tail, init]

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

Goal state before:
pp: m n : ℕ
α✝ : Fin (n + 1) → Sort u_1
x✝ : α✝ (last n)
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ i.castSucc
i : Fin n
y : α✝ i.castSucc
z : α✝ (last n)
α : Sort u_2
motive : {n : ℕ} → (Fin n → α) → Sort u_3
elim0 : motive Fin.elim0
snoc : {n : ℕ} → (x : Fin n → α) → (x₀ : α) → motive x → motive (Fin.snoc x x₀)
x : Fin 0 → α
⊢ motive x

Tactic:
convert! elim0

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

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
⊢ Injective (natEmbeddingAux α)

Tactic:
rintro m n h

Goal state after:
α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
⊢ m = n
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : Std.Refl r
x : α
xs : List α
⊢ (orderedInsert r x xs).erase x = xs

Tactic:
induction xs <;> grind [Std.Refl]

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

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : r x a
h✝ : ¬r x b
⊢ x :: a :: as <+ b :: orderedInsert r x bs

Tactic:
have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : r x a
h✝ : ¬r x b
ih : orderedInsert r x (a :: as) <+ orderedInsert r x bs
⊢ x :: a :: as <+ b :: orderedInsert r x bs
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬r x b
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs

Tactic:
have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬r x b
ih : orderedInsert r x (a :: as) <+ orderedInsert r x bs
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h0 : ¬p 0
⊢ p (Fin.find (fun k ↦ p k.succ) ⋯).succ ∧ ∀ (i : Fin n), i.succ < (Fin.find (fun k ↦ p k.succ) ⋯).succ → ¬p i.succ

Tactic:
succ_lt_succ_iff

Goal state after:
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h0 : ¬p 0
⊢ p (Fin.find (fun k ↦ p k.succ) ⋯).succ ∧ ∀ (i : Fin n), i < Fin.find (fun k ↦ p k.succ) ⋯ → ¬p i.succ
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
inst✝ : Trans R R R
hl : IsChain R l₂
h : l₁ <+ l₂
⊢ IsChain R l₁

Tactic:
rw [isChain_iff_pairwise] at hl ⊢

Goal state after:
α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
inst✝ : Trans R R R
hl : Pairwise R l₂
h : l₁ <+ l₂
⊢ Pairwise R l₁
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons.cons.inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun x1 x2 ↦ x1 > x2) (a' :: as)
hmas : b :: bs < a' :: as
⊢ b ≤ a'

pp: case cons.cons.inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun x1 x2 ↦ x1 > x2) (a' :: as)
hmas : b :: bs = a' :: as
⊢ b ≤ a'

Tactic:
· exact head_le_of_lt hmas

Goal state after:
case cons.cons.inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun x1 x2 ↦ x1 > x2) (a' :: as)
hmas : b :: bs = a' :: as
⊢ b ≤ a'
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: l : List ℕ
n : ℕ
⊢ (∃ s, s ∈ l.ranges ∧ n ∈ s) ↔ n < l.sum

Tactic:
rw [← mem_range, ← ranges_flatten, mem_flatten]

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

Goal state before:
pp: l : List ℤ
h : l.prod = -1
⊢ -1 ∈ l

Tactic:
obtain ⟨x, h₁, h₂⟩ := exists_mem_ne_one_of_prod_ne_one (ne_of_eq_of_ne h (by decide))

Goal state after:
l : List ℤ
h : l.prod = -1
x : ℤ
h₁ : x ∈ l
h₂ : x ≠ 1
⊢ -1 ∈ l
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l l' : List α
h : l ~r l'
⊢ l' ~r l

Tactic:
obtain ⟨n, rfl⟩ := h

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ l.rotate n ~r l
Module: Mathlib.Data.List.Rotate

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

Tactic:
obtain ⟨n, rfl⟩ := h

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ l.reverse ~r (l.rotate n).reverse
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l l' : List α
h : l ~r l'
⊢ ∃ n, n ≤ l.length ∧ l.rotate n = l'

Tactic:
obtain ⟨n, rfl⟩ := h

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ ∃ n_1, n_1 ≤ l.length ∧ l.rotate n_1 = l.rotate n
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset β
t : Finset α
f : α → Finset β
hf : (↑t).PairwiseDisjoint f
⊢ Disjoint s (t.disjiUnion f hf) ↔ ∀ i ∈ t, Disjoint s (f i)

Tactic:
simpa only [_root_.disjoint_comm] using disjoint_disjiUnion_left t f hf s

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

Goal state before:
pp: α : Type u
β : Type u_1
l₁ l₂ : List α
h : l₁ ~r l₂
f : α → β
⊢ List.map f l₁ ~r List.map f l₂

Tactic:
obtain ⟨n, rfl⟩ := h

Goal state after:
α : Type u
β : Type u_1
l₁ : List α
f : α → β
n : ℕ
⊢ List.map f l₁ ~r List.map f (l₁.rotate n)
Module: Mathlib.Data.Fintype.Prod

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

Tactic:
refine
    ⟨fun H => ?_, fun H =>
      H.elim (and_imp.2 <| @Prod.infinite_of_left α β) (and_imp.2 <| @Prod.infinite_of_right α β)⟩
  rw [and_comm]
  rcases Infinite.nonempty (α × β) with ⟨a, b⟩
  contrapose! H; have := H.1 ⟨b⟩; have := H.2 ⟨a⟩
  infer_instance

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

Goal state before:
pp: case mk
α : Type u_1
val✝ : Multiset α
s : List α
hs : Nodup (Quot.mk (⇑(List.isSetoid α)) s)
⊢ #{ val := Quot.mk (⇑(List.isSetoid α)) s, nodup := hs }.offDiag =
    #{ val := Quot.mk (⇑(List.isSetoid α)) s, nodup := hs } ^ 2 -
      #{ val := Quot.mk (⇑(List.isSetoid α)) s, nodup := hs }

Tactic:
apply List.length_offDiag

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
hs : Fintype ↑s
ht : Fintype ↑t
⊢ Fintype ↑(image2 f s t)

Tactic:
rw [← image_prod]
  apply Set.fintypeImage

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
⊢ IsConj 1 a ↔ a = 1

Tactic:
refine ⟨fun ⟨c, h⟩ => ?_, fun h => by rw [h]⟩
  rw [SemiconjBy, mul_one] at h
  exact c.isUnit.mul_eq_right.mp h.symm

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ⇑f
⊢ Function.Surjective (map f)

Tactic:
by
  intro b
  obtain ⟨b, rfl⟩ := ConjClasses.mk_surjective b
  obtain ⟨a, rfl⟩ := hf b
  exact ⟨ConjClasses.mk a, rfl⟩

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
s : Set α
⊢ ⇑f '' (fun x ↦ x⁻¹) '' s = (fun x ↦ x⁻¹) '' ⇑f '' s

Tactic:
exact image_comm (map_inv _)

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

Goal state before:
pp: case a.mul.inl.inl
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
y : 1 ∈ closure s
hx : 1 = 1 ∨ 1 ∈ Subsemigroup.closure s
hy✝ : 1 ∈ closure s
hy : 1 = 1 ∨ 1 ∈ Subsemigroup.closure s
⊢ 1 * 1 ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
simp_all [mul_mem]

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

Goal state before:
pp: case a.mul.inl.inr
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x hx✝ : M
hy✝¹ : hx✝ ∈ closure s
hy✝ : hx✝ = 1 ∨ hx✝ ∈ Subsemigroup.closure s
y : 1 ∈ closure s
hx : 1 = 1 ∨ 1 ∈ Subsemigroup.closure s
hy : hx✝ ∈ Subsemigroup.closure s
⊢ 1 * hx✝ ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
simp_all [mul_mem]

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

Goal state before:
pp: case a.mul.inr.inl
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x✝ x : M
y : x ∈ closure s
hx✝ : x = 1 ∨ x ∈ Subsemigroup.closure s
hx : x ∈ Subsemigroup.closure s
hy✝ : 1 ∈ closure s
hy : 1 = 1 ∨ 1 ∈ Subsemigroup.closure s
⊢ x * 1 ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
simp_all [mul_mem]

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

Goal state before:
pp: case a.mul.inr.inr
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x✝ x hx✝¹ : M
y : x ∈ closure s
hy✝¹ : hx✝¹ ∈ closure s
hx✝ : x = 1 ∨ x ∈ Subsemigroup.closure s
hy✝ : hx✝¹ = 1 ∨ hx✝¹ ∈ Subsemigroup.closure s
hx : x ∈ Subsemigroup.closure s
hy : hx✝¹ ∈ Subsemigroup.closure s
⊢ x * hx✝¹ ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
simp_all [mul_mem]

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

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ x ^ ↑n ∈ K

Tactic:
rw [zpow_natCast]

Goal state after:
M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ x ^ n ∈ K
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ x ^ n ∈ K

Tactic:
exact pow_mem hx n

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : ∀ (h : G), h * g ∈ S ↔ g * h ∈ S
n : G
⊢ n ∈ S ↔ g * n * g⁻¹ ∈ S

Tactic:
rw [mul_assoc, ← h, inv_mul_cancel_right]

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
M : Type u_7
inst✝ : MulOneClass M
f : G →* G'
g : G' →* M
⊢ g.comp f = 1 → f.range ≤ g.ker

Tactic:
by rintro h _ ⟨y, rfl⟩; exact DFunLike.congr_fun h y

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s
h : G
hh : h ∈ H
⊢ closure (⇑↑(MulAut.conj h) '' s) ≤ closure s

Tactic:
simpa using! hH h hh

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
φ : G₂ →* G₃
⊢ (fun g ↦ f.liftOfRightInverseAux f_inv hf ↑g ⋯) ((fun φ ↦ ⟨φ.comp f, ⋯⟩) φ) = φ

Tactic:
by
    ext b
    simp [liftOfRightInverseAux, hf b]

Goal state after: