mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case neg
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : ¬↑i + ↑i + 1 < n + 1 + 1
⊢ ↑i + ↑i + 1 - (n + 1 + 1) = ((↑i + ↑i) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)

Tactic:
rw [Fin.val_mk, not_lt] at h

Goal state after:
case neg
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : n + 1 + 1 ≤ ↑i + ↑i + 1
⊢ ↑i + ↑i + 1 - (n + 1 + 1) = ((↑i + ↑i) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
n : ℕ
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ (if h : ↑i + ↑i + 1 < n + 1 then v ⟨↑i + ↑i + 1, ⋯⟩ else v ⟨↑i + ↑i + 1 - (n + 1), ⋯⟩) = v (i + i + 1)

Tactic:
cases n with

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : (support f).Finite
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r

pp: case neg
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : ¬(support f).Finite
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r

Tactic:
· exact finsum_mul' f r h

Goal state after:
case neg
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : ¬(support f).Finite
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
i : Fin n.succ
h : i ≠ Fin.last n
⊢ ↑((finRotate (n + 1)) i) = ↑i + 1

Tactic:
rw [finRotate_apply]
  have : (i : ℕ) < n := Fin.val_lt_last h
  exact Fin.val_add_one_of_lt this

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ x ^ ⊤ = ⊤

Tactic:
rw [epow_def, if_neg, if_neg, if_neg] <;> grind

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
h : ∑ i ∈ s, Finsupp.single i (f i) = ∑ i ∈ s, Finsupp.single i (g i)
this : ∀ (f : ι → R), f i = (∑ j ∈ s, Finsupp.single j (f j)) i
⊢ (∑ j ∈ s, Finsupp.single j (f j)) i = g i

Tactic:
this g,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
h : ∑ i ∈ s, Finsupp.single i (f i) = ∑ i ∈ s, Finsupp.single i (g i)
this : ∀ (f : ι → R), f i = (∑ j ∈ s, Finsupp.single j (f j)) i
⊢ (∑ j ∈ s, Finsupp.single j (f j)) i = (∑ j ∈ s, Finsupp.single j (g j)) i
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
x : Fin (n + 1)
⊢ f x * ∏ x ∈ map x.succAboveEmb univ, f x = f x * ∏ i, f (x.succAbove i)

Tactic:
Finset.prod_map,

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
x : Fin (n + 1)
⊢ f x * ∏ x_1, f (x.succAboveEmb x_1) = f x * ∏ i, f (x.succAbove i)
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
⊢ ∏ i, f i = (∏ i, f i.castSucc) * f (last n)

Tactic:
by
  simpa [mul_comm] using prod_univ_succAbove f (last n)

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
h : a ≡ b [PMOD p]
⊢ b ≡ a [PMOD p]

Tactic:
modEq_iff_nsmul

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
h : ∃ m n, m • p + a = n • p + b
⊢ ∃ m n, m • p + b = n • p + a
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b c p : M
hab : a ≡ b [PMOD p]
hbc : b ≡ c [PMOD p]
⊢ a ≡ c [PMOD p]

Tactic:
modEq_iff_nsmul

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
a b c p : M
hab : ∃ m n, m • p + a = n • p + b
hbc : ∃ m n, m • p + b = n • p + c
⊢ ∃ m n, m • p + a = n • p + c
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b c d p : M
hab : a ≡ b [PMOD p]
hcd : c ≡ d [PMOD p]
⊢ a + c ≡ b + d [PMOD p]

Tactic:
modEq_iff_nsmul

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
a b c d p : M
hab : ∃ m n, m • p + a = n • p + b
hcd : ∃ m n, m • p + c = n • p + d
⊢ ∃ m n, m • p + (a + c) = n • p + (b + d)
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
n : ℕ
h : a ≡ b [PMOD p]
⊢ n • a ≡ n • b [PMOD n • p]

Tactic:
modEq_iff_nsmul

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
n : ℕ
h : ∃ m n, m • p + a = n • p + b
⊢ ∃ m n_1, m • n • p + n • a = n_1 • n • p + n • b
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
h : a ≡ b [PMOD p]
⊢ f a ≡ f b [PMOD f p]

Tactic:
modEq_iff_nsmul

Goal state after:
M : Type u_1
inst✝³ : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
h : ∃ m n, m • p + a = n • p + b
⊢ ∃ m n, m • f p + f a = n • f p + f b
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
h : a ≡ b [PMOD p]
hadd : a + c ≡ b + d [PMOD p]
⊢ c ≡ d [PMOD p]

Tactic:
modEq_iff_nsmul

Goal state after:
M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
h : ∃ m n, m • p + a = n • p + b
hadd : ∃ m n, m • p + (a + c) = n • p + (b + d)
⊢ ∃ m n, m • p + c = n • p + d
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case h
M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
⊢ n • p + (b + d) + l • p = (n + k) • p + d + a

Tactic:
← add_assoc,

Goal state after:
case h
M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
⊢ n • p + b + d + l • p = (n + k) • p + d + a
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ a ≡ b [PMOD p] ↔ ∃ m, m • p = b - a

Tactic:
modEq_iff_nsmul

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ (∃ m n, m • p + a = n • p + b) ↔ ∃ m, m • p = b - a
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ (∏ i, ∏ j with i ≤ j.castSucc, f i j) * ∏ i, ∏ j with j.castSucc < i, f i j =
    (∏ i, ∏ j ≥ i, f i.castSucc j) * ∏ i, ∏ j ≤ i, f i.succ j

Tactic:
Fin.prod_univ_castSucc,

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ ((∏ i, ∏ j with i.castSucc ≤ j.castSucc, f i.castSucc j) * ∏ j with last n ≤ j.castSucc, f (last n) j) *
      ∏ i, ∏ j with j.castSucc < i, f i j =
    (∏ i, ∏ j ≥ i, f i.castSucc j) * ∏ i, ∏ j ≤ i, f i.succ j
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v) l = ↑x
this✝ : ↑(↑hv.linearCombinationEquiv l) = (Finsupp.linearCombination R v) l
this : ↑hv.linearCombinationEquiv l = x
⊢ hv.repr x = l

Tactic:
← LinearEquiv.symm_apply_apply hv.linearCombinationEquiv l

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v) l = ↑x
this✝ : ↑(↑hv.linearCombinationEquiv l) = (Finsupp.linearCombination R v) l
this : ↑hv.linearCombinationEquiv l = x
⊢ hv.repr x = hv.linearCombinationEquiv.symm (hv.linearCombinationEquiv l)
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case succ
ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n : Fin (m + 1) → ℕ
f : (i : Fin (m + 1)) → Fin (n i)
⊢ ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i

Tactic:
Fin.prod_univ_castSucc,

Goal state after:
case succ
ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n : Fin (m + 1) → ℕ
f : (i : Fin (m + 1)) → Fin (n i)
⊢ ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < (∏ i, n i.castSucc) * n (Fin.last m)
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h :
  ∀ (s t : Finset ι) (f : ι → R),
    Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
| ∑ i ∈ s with g i ≤ f i, (if g i ≤ f i then f i - g i else g i - f i) • v i +
    (∑ i ∈ s with g i ≤ f i, g i • v i + ∑ i ∈ s with f i < g i, f i • v i)

Tactic:
← add_assoc,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h :
  ∀ (s t : Finset ι) (f : ι → R),
    Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
| ∑ i ∈ s with g i ≤ f i, (if g i ≤ f i then f i - g i else g i - f i) • v i + ∑ i ∈ s with g i ≤ f i, g i • v i +
    ∑ i ∈ s with f i < g i, f i • v i
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: n : ℕ
inst✝ : Fintype (ZMod n)
⊢ Fintype.card (ZMod n) = n

Tactic:
cases n with

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : α → Type u_3
inst✝¹ : Fintype α
inst✝ : ∀ (a : α), Finite (β a)
⊢ Nat.card (Sigma β) = ∑ a, Nat.card (β a)

Tactic:
let _ (a : α) : Fintype (β a) := Fintype.ofFinite (β a)
  simp_rw [Nat.card_eq_fintype_card, Fintype.card_sigma]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
⊢ ¬LinearIndependent R v ↔ ∃ s t f, Disjoint s t ∧ ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i ∧ ∃ i ∈ s, 0 < f i

Tactic:
by
  simp only [linearIndependent_iffₒₛ, pos_iff_ne_zero]
  push +distrib Not
  refine ⟨fun ⟨s, t, f, hst, heq, h⟩ => ?_,
    fun ⟨s, t, f, hst, heq, hi⟩ => ⟨s, t, f, hst, heq, .inl hi⟩⟩
  rcases h with ⟨i, hi, hfi⟩ | ⟨i, hi, hgi⟩
  · exact ⟨s, t, f, hst, heq, i, hi, hfi⟩
  · exact ⟨t, s, f, hst.symm, heq.symm, i, hi, hgi⟩

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
i : G →* L
his : i ∈ s
⊢ g i = 0

Tactic:
let ⟨y, hy⟩ := h2 i his

Goal state after:
G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
i : G →* L
his : i ∈ s
y : G
hy : i y ≠ a y
⊢ g i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
i : G →* L
his : i ∈ s
y : G
hy : i y ≠ a y
h : g i = 0 ∨ i y - a y = 0
⊢ g i = 0

Tactic:
exact h.resolve_right (sub_ne_zero_of_ne hy)

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

Goal state before:
pp: case refine_1.refine_1
α : Type u_1
s : Set α
x : α
hx : x ∈ s
z : α
hne : x ≠ z
hs : s \ {x} = {x, z}
⊢ False

Tactic:
exact (hs.symm.subset (Or.inl rfl)).2 rfl

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

Goal state before:
pp: case refine_1.refine_1
α : Type u_1
s : Set α
x : α
hx : x ∈ s
z w : α
hzw : z ≠ w
hyz : x ≠ z
hyw : x ≠ w
hs : s \ {x} = {x, z, w}
⊢ False

Tactic:
exact (hs.symm.subset (Or.inl rfl)).2 rfl

Goal state after:
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
h : Finite ↑(s ∪ t)
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t

Tactic:
rw [finite_coe_iff, finite_union, ← finite_coe_iff, ← finite_coe_iff] at h

Goal state after:
case inl
α : Type u_1
s t : Set α
h : Finite ↑s ∧ Finite ↑t
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
h : Finite ↑(s ∪ t)
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t

pp: case inr
α : Type u_1
s t : Set α
h : Infinite ↑(s ∪ t)
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t

Tactic:
· rw [finite_coe_iff, finite_union, ← finite_coe_iff, ← finite_coe_iff] at h
    cases h
    rw [← @Nat.cast_le Cardinal, Nat.cast_add, Nat.cast_card, Nat.cast_card, Nat.cast_card]
    exact Cardinal.mk_union_le s t

Goal state after:
case inr
α : Type u_1
s t : Set α
h : Infinite ↑(s ∪ t)
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → MulOneClass (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
⊢ (pi univ fun i ↦ closure (s i)) ≤ closure (univ.pi fun i ↦ s i)

Tactic:
exact pi_le_iff.mpr fun i => map_le_of_le_comap _ <| closure_le.2 fun _x hx =>
          subset_closure <| mem_univ_pi.mpr fun j => by
        by_cases H : j = i
        · subst H
          simpa
        · simpa [H] using hs _

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ univ = ⋃ x, Quotient.out x • ↑H

Tactic:
simp_rw [univ_eq_iUnion_orbit H.op, orbit_eq_out_smul]
  rfl

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ∪ t = univ
⊢ Nat.card α ≤ s.ncard + t.ncard

Tactic:
rw [← ncard_univ, ← h]

Goal state after:
α : Type u_1
s t : Set α
h : s ∪ t = univ
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.ncard = 4 ↔ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
rw [← encard_eq_four, ncard_def]

Goal state after:
α : Type u_1
s : Set α
⊢ s.encard.toNat = 4 ↔ s.encard = 4
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n] i = j
hn_lt_ne : ∀ m < n, succ^[m] i ≠ j
⊢ pred^[n] (succ^[n] i) = i

Tactic:
cases n with

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a ≤ b
⊢ (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Icc a b, f x

Tactic:
rw [mul_comm, mul_prod_Ico_eq_prod_Icc h]

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inl.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i0 ≤ i
hj : i0 ≤ j
⊢ i ≤ j

pp: case inl.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i0 ≤ i
hj : j < i0
⊢ i ≤ j

pp: case inr.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : i0 ≤ j
⊢ i ≤ j

pp: case inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : j < i0
⊢ i ≤ j

Tactic:
· rw [← iterate_succ_toZ i hi, ← iterate_succ_toZ j hj]
    exact Monotone.monotone_iterate_of_le_map succ_mono (le_succ _) (Int.toNat_le_toNat h_le)

Goal state after:
case inl.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i0 ≤ i
hj : j < i0
⊢ i ≤ j

case inr.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : i0 ≤ j
⊢ i ≤ j

case inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : j < i0
⊢ i ≤ j
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inr
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : i < hι.some
h_neg : toZ hι.some i < 0
⊢ pred^[(-toZ hι.some i).toNat] hι.some = i

Tactic:
exact iterate_pred_toZ i hi

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : 0 ≤ n
⊢ ↑n.toNat = n

Tactic:
exact Int.toNat_of_nonneg hn

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
⊢ toZ hι.some ((fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) n) = n

Tactic:
rcases le_or_gt 0 n with hn | hn
    · simp_rw [if_pos hn]
      rw [toZ_iterate_succ]
      exact Int.toNat_of_nonneg hn
    · simp_rw [if_neg (not_le.mpr hn)]
      rw [toZ_iterate_pred]
      simp only [hn.le, Int.toNat_of_nonneg, Int.neg_nonneg_of_nonpos, Int.neg_neg]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
⊢ ∃ g ≤ f, univ.sup g = univ.sup f ∧ Pairwise (Disjoint on g)

Tactic:
by
  rcases isEmpty_or_nonempty ι with hι | hι
  ·  -- do `ι = ∅` separately since `⊤ : Fin n` isn't defined for `n = 0`
    exact ⟨f, le_rfl, rfl, Subsingleton.pairwise⟩
  let R : ι ≃ Fin _ := equivFin ι
  let f' : Fin _ → α := f ∘ R.symm
  have hf' : f = f' ∘ R := by ext; simp only [Function.comp_apply, Equiv.symm_apply_apply, f']
  refine ⟨disjointed f' ∘ R, ?_, ?_, ?_⟩
  · intro n
    simpa only [hf'] using! disjointed_le f' (R n)
  · simpa only [← sup_image, image_univ_equiv, hf'] using! sup_disjointed f'
  · exact fun i j hij ↦ disjoint_disjointed f' (R.injective.ne hij)

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_4
m n : ℕ
inst✝ : CommGroup M
hmn : m ≤ n
f : ℕ → M
⊢ ∏ i ∈ Icc m n, f (i + 1) / f i = f (n + 1) / f m

Tactic:
rw [← Finset.Ico_add_one_right_eq_Icc, prod_Ico_div]
  omega

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
a b : R
h : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ IsIdempotentElem (a + b - a * b)

Tactic:
simp only [IsIdempotentElem, h.eq, mul_sub, mul_add, sub_mul, add_mul, ha.eq,
    mul_assoc, add_sub_cancel_right, hb.eq, hb.mul_self_mul, add_sub_cancel_left, sub_right_inj]

Goal state after:
R : Type u_1
inst✝ : NonUnitalRing R
a b : R
h : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ a * (b * a) + b * a - b * (a * (b * a)) = b * a
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
⊢ a + a * b + (b * a + b) = a + b

Tactic:
← add_assoc,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
⊢ a + a * b + b * a + b = a + b
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsCancelAdd R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
h : IsIdempotentElem (a + b)
⊢ a + (a * b + (b * a + b)) = a + (0 + b)

Tactic:
← add_assoc,

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsCancelAdd R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
h : IsIdempotentElem (a + b)
⊢ a + a * b + (b * a + b) = a + (0 + b)
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
h : a * b * a = 0
this : a * a * b + a * b * a = 0
⊢ a * b = 0

Tactic:
by rwa [h, add_zero, ha.eq] at this

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
ι : Type u_1
x : ι → α
a : α
⊢ a ∈ range x \ {0} ↔ a ∈ range fun i ↦ x ↑i

Tactic:
simp only [mem_sdiff, mem_range, mem_singleton_iff]

Goal state after:
α : Type u
inst✝ : Semiring α
ι : Type u_1
x : ι → α
a : α
⊢ (∃ y, x y = a) ∧ ¬a = 0 ↔ ∃ y, x ↑y = a
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
y z : α
hz : z ∈ span ↑I
hy : 1 = y * x + z
⊢ z ∈ I

Tactic:
rwa [← span_eq I]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : b ∈ Submodule.span α ↑I
oe : 1 = a • x + b
⊢ y ∈ I

Tactic:
obtain F : y * 1 = y * (a • x + b) := congr_arg (fun g : α => y * g) oe

Goal state after:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : b ∈ Submodule.span α ↑I
oe : 1 = a • x + b
F : y * 1 = y * (a • x + b)
⊢ y ∈ I