mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : (s ∩ mulSupport (f ∘ g)).Finite
hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y
this : ∏ᶠ (i : β) (_ : i ∈ s), f (g i) = ∏ i ∈ hs.toFinset, f (g i)
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)

Tactic:
this,

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : (s ∩ mulSupport (f ∘ g)).Finite
hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y
this : ∏ᶠ (i : β) (_ : i ∈ s), f (g i) = ∏ i ∈ hs.toFinset, f (g i)
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ i ∈ hs.toFinset, f (g i)
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : Fin n
h : i ≤ m.castSucc
⊢ (finSuccEquiv' i) m.succ = some m

Tactic:
← Fin.succAbove_of_le_castSucc _ _ h,

Goal state after:
n : ℕ
i : Fin (n + 1)
m : Fin n
h : i ≤ m.castSucc
⊢ (finSuccEquiv' i) (i.succAbove m) = some m
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u_1
h : 0 = 0 + 0
⊢ vecAlt0 h ![] = ![]

Tactic:
by
  simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: α : Type u_1
h : 0 = 0 + 0
⊢ vecAlt1 h ![] = ![]

Tactic:
by
  simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: case pos
ι : Type u_3
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CharZero R
f : ι → ℕ
hf : HasFiniteMulSupport f
⊢ ↑(∏ᶠ (x : ι), f x) = ∏ᶠ (x : ι), ↑(f x)

pp: case neg
ι : Type u_3
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CharZero R
f : ι → ℕ
hf : ¬HasFiniteMulSupport f
⊢ ↑(∏ᶠ (x : ι), f x) = ∏ᶠ (x : ι), ↑(f x)

Tactic:
· exact map_finprod (Nat.castRingHom R) hf

Goal state after:
case neg
ι : Type u_3
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CharZero R
f : ι → ℕ
hf : ¬HasFiniteMulSupport f
⊢ ↑(∏ᶠ (x : ι), f x) = ∏ᶠ (x : ι), ↑(f x)
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
⊢ (a ^ (c - b + b) - 1) % (a ^ b - 1) = a ^ ((c - b) % b) - 1

Tactic:
this,

Goal state after:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
⊢ (a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ LinearIndepOn R v s ↔ Injective ⇑(Finsupp.linearCombinationOn ι M R v s)

Tactic:
rw [← linearIndependent_restrict_iff]

Goal state after:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ LinearIndependent (ι := ↑s) R (s.domRestrict v) ↔ Injective ⇑(Finsupp.linearCombinationOn ι M R v s)
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ (k * n + m).gcd n = 1 ↔ m.gcd n = 1

Tactic:
gcd_mul_right_add_left

Goal state after:
m n k : ℕ
⊢ m.gcd n = 1 ↔ m.gcd n = 1
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b : ℕ
h : n ≤ a
⊢ a - n + n ≡ b [MOD n] ↔ a ≡ b [MOD n]

Tactic:
Nat.sub_add_cancel h

Goal state after:
n a b : ℕ
h : n ≤ a
⊢ a ≡ b [MOD n] ↔ a ≡ b [MOD n]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b : ℕ
h : n ≤ b
⊢ a ≡ b - n + n [MOD n] ↔ a ≡ b [MOD n]

Tactic:
Nat.sub_add_cancel h

Goal state after:
n a b : ℕ
h : n ≤ b
⊢ a ≡ b [MOD n] ↔ a ≡ b [MOD n]
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R), ∀ y ∈ span R (range v), c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x, g x.succ • v x = 0
this : g 0 = 0
⊢ g j = 0

Tactic:
this,

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R), ∀ y ∈ span R (range v), c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : 0 • x + ∑ x, g x.succ • v x = 0
this : g 0 = 0
⊢ g j = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_2.inr
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : ∀ x ∈ span R (v '' range Sum.inl), ∀ y ∈ span R (v '' range Sum.inr), x = y → x = 0
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
this :
  ∑ i ∈ s.preimage Sum.inl ⋯, (fun x ↦ g x • v x) (Sum.inl i) =
    -∑ i ∈ s.preimage Sum.inr ⋯, (fun x ↦ g x • v x) (Sum.inr i)
A : ∑ c ∈ s.preimage Sum.inl ⋯, (fun x ↦ g x • v x) (Sum.inl c) = 0
i : ι'
hi : Sum.inr i ∈ s
⊢ g (Sum.inr i) = 0

Tactic:
this,

Goal state after:
case refine_2.inr
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : ∀ x ∈ span R (v '' range Sum.inl), ∀ y ∈ span R (v '' range Sum.inr), x = y → x = 0
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
this :
  ∑ i ∈ s.preimage Sum.inl ⋯, (fun x ↦ g x • v x) (Sum.inl i) =
    -∑ i ∈ s.preimage Sum.inr ⋯, (fun x ↦ g x • v x) (Sum.inr i)
A : -∑ i ∈ s.preimage Sum.inr ⋯, (fun x ↦ g x • v x) (Sum.inr i) = 0
i : ι'
hi : Sum.inr i ∈ s
⊢ g (Sum.inr i) = 0
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case inr.inl
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Finite α
⊢ card (α → β) = card β ^ card α

Tactic:
rcases finite_or_infinite β
    · let := Fintype.ofFinite α
      let := Fintype.ofFinite β
      simp
    · simp only [card_eq_top_of_infinite]
      rw [top_epow]
      rwa [card_ne_zero_iff_nonempty]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : Cardinal.{w}
h : lift.{v, w} c < lift.{w, v} (Module.rank R M)
c' : Cardinal.{v}
hc' : c' < Module.rank R M
hcc' : lift.{w, v} c' = lift.{v, w} c
⊢ ?m.41 < iSup ?m.43

Tactic:
simpa [← hcc', Module.rank_def] using h

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
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝ : ∃ x x_1, ∃ (_ : ∑ i ∈ x, x_1 i • v i = ∑ i ∈ xᶜ, x_1 i • v i), ∃ x, ¬x_1 x = 0
t : Finset ι
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i
i : ι
hfi : ¬f i = 0
⊢ ∃ t f, ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
by_cases hi' : i ∈ t

Goal state after:
case pos
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝ : ∃ x x_1, ∃ (_ : ∑ i ∈ x, x_1 i • v i = ∑ i ∈ xᶜ, x_1 i • v i), ∃ x, ¬x_1 x = 0
t : Finset ι
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i
i : ι
hfi : ¬f i = 0
hi' : i ∈ t
⊢ ∃ t f, ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i ∧ ∃ i ∈ t, f i ≠ 0

case neg
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝ : ∃ x x_1, ∃ (_ : ∑ i ∈ x, x_1 i • v i = ∑ i ∈ xᶜ, x_1 i • v i), ∃ x, ¬x_1 x = 0
t : Finset ι
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i
i : ι
hfi : ¬f i = 0
hi' : i ∉ t
⊢ ∃ t f, ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i ∧ ∃ i ∈ t, f i ≠ 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.encard ≠ 0
⊢ s.Nonempty

Tactic:
by
  rwa [nonempty_iff_ne_empty, Ne, ← encard_eq_zero]

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
inst✝ : DecidableEq ι
s : Finset ι
x✝ : ∃ x, ∃ (_ : x ⊆ s), ∃ x_1, ∃ (_ : ∑ i ∈ x, x_1 i • v i = ∑ i ∈ s \ x, x_1 i • v i), ∃ x, ∃ (_ : x ∈ s), ¬x_1 x = 0
t : Finset ι
hst : t ⊆ s
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i
i : ι
hi : i ∈ s
hfi : ¬f i = 0
⊢ ∃ t ⊆ s, ∃ f, ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
by_cases hi' : i ∈ t

Goal state after:
case pos
ι : 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
inst✝ : DecidableEq ι
s : Finset ι
x✝ : ∃ x, ∃ (_ : x ⊆ s), ∃ x_1, ∃ (_ : ∑ i ∈ x, x_1 i • v i = ∑ i ∈ s \ x, x_1 i • v i), ∃ x, ∃ (_ : x ∈ s), ¬x_1 x = 0
t : Finset ι
hst : t ⊆ s
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i
i : ι
hi : i ∈ s
hfi : ¬f i = 0
hi' : i ∈ t
⊢ ∃ t ⊆ s, ∃ f, ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i ∧ ∃ i ∈ t, f i ≠ 0

case neg
ι : 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
inst✝ : DecidableEq ι
s : Finset ι
x✝ : ∃ x, ∃ (_ : x ⊆ s), ∃ x_1, ∃ (_ : ∑ i ∈ x, x_1 i • v i = ∑ i ∈ s \ x, x_1 i • v i), ∃ x, ∃ (_ : x ∈ s), ¬x_1 x = 0
t : Finset ι
hst : t ⊆ s
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i
i : ι
hi : i ∈ s
hfi : ¬f i = 0
hi' : i ∉ t
⊢ ∃ t ⊆ s, ∃ f, ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i ∧ ∃ i ∈ t, f i ≠ 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
v : ι → M
inst✝ : Fintype ι
⊢ LinearIndependent R v ↔ ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0

Tactic:
refine
    ⟨fun H g => by simpa using linearIndependent_iff'.1 H Finset.univ g, fun H =>
      linearIndependent_iff''.2 fun s g hg hs i => H _ ?_ _⟩
  rw [← hs]
  refine (Finset.sum_subset (Finset.subset_univ _) fun i _ hi => ?_).symm
  rw [hg i hi, zero_smul]

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
L : α ⧸ s
⊢ { x // ↑x = L } ≃ ↑{x | ↑x = ↑(Quotient.out L)}

Tactic:
change
          (_root_.Subtype fun x : α => Quotient.mk'' x = L) ≃
            _root_.Subtype fun x : α => Quotient.mk'' x = Quotient.mk'' _

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
L : α ⧸ s
⊢ { x // Quotient.mk'' x = L } ≃ { x // Quotient.mk'' x = Quotient.mk'' (Quotient.out L) }
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Add α
x : α
v : Fin n → α
w : Fin n.succ → α
⊢ vecCons x v + w = vecCons (x + vecHead w) (v + vecTail w)

Tactic:
by
  ext i; refine i.cases ?_ ?_ <;> simp [vecHead, vecTail]

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
⊢ v + vecCons y w = vecCons (vecHead v + y) (vecTail v + w)

Tactic:
by
  ext i; refine i.cases ?_ ?_ <;> simp [vecHead, vecTail]

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
⊢ vecCons x v - w = vecCons (x - vecHead w) (v - vecTail w)

Tactic:
by
  ext i; refine i.cases ?_ ?_ <;> simp [vecHead, vecTail]

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
⊢ v - vecCons y w = vecCons (vecHead v - y) (vecTail v - w)

Tactic:
by
  ext i; refine i.cases ?_ ?_ <;> simp [vecHead, vecTail]

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ φ.ker
a b : G
h : φ.rangeRestrict a = φ.rangeRestrict b
⊢ (leftRel φ.ker) a b

Tactic:
by
      rw [leftRel_apply, ← ker_rangeRestrict, mem_ker, φ.rangeRestrict.map_mul, ← h,
        φ.rangeRestrict.map_inv, inv_mul_cancel]

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
hn : s.Nonempty
he : Even s.ncard
⊢ 1 < s.ncard

Tactic:
← Set.ncard_pos hs

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
hn : 0 < s.ncard
he : Even s.ncard
⊢ 1 < s.ncard
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
⊢ a ≤ x ∧ x < succ b ↔ a ≤ x ∧ x ≤ b

Tactic:
lt_succ_iff_of_not_isMax hb

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
⊢ a ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
⊢ a < x ∧ x < succ b ↔ a < x ∧ x ≤ b

Tactic:
lt_succ_iff_of_not_isMax hb

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
⊢ a < x ∧ x ≤ b ↔ a < x ∧ x ≤ b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (pred a) b = Icc a b

Tactic:
ext x; rw [mem_Ioc, mem_Icc, pred_lt_iff_of_not_isMin ha]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (pred a) (pred b) = Ico a b

Tactic:
rw [Ioc_pred_right_eq_Ioo, Ioo_pred_left_eq_Ioc_of_not_isMin ha]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ insert a (Ioc a b) = Ioc (pred a) b

Tactic:
Ioc_pred_left_of_not_isMin ha,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ insert a (Ioc a b) = Icc a b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
x : α
⊢ x < succ b ↔ x ≤ b

Tactic:
lt_succ_iff_of_not_isMax hb

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
x : α
⊢ x ≤ b ↔ x ≤ b
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this✝ : Fintype ι
this : x = ∑ i, x (Sum.inl i) • single (Sum.inl i) 1
⊢ ∑ i, x (Sum.inl i) • single (Sum.inl i) 1 ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)

Tactic:
exact sum_mem <| fun i _ ↦ SMulMemClass.smul_mem _ <| subset_span <| Set.mem_range_self i

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x : ↥(snd R M M₂)
⊢ (fun n ↦ ⟨(0, n), ⋯⟩) ((fun x ↦ (↑x).2) x) = x

Tactic:
by aesop (add norm simp Submodule.snd)

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp.right
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : p₁.prod p₂ ≤ q
⊢ map (inr R M M₂) p₂ ≤ q

Tactic:
rintro _ ⟨x, hx, rfl⟩
      apply h
      exact ⟨zero_mem p₁, hx⟩

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : LinearOrder α
f : ι → α
i : ι
⊢ ∃ j ≤ i, (partialSups f) i = f j

Tactic:
by
  obtain ⟨j, hj_mem, hj_le⟩ : ∃ j ∈ Finset.Iic i, ∀ k ∈ Finset.Iic i, f k ≤ f j :=
    Finset.exists_max_image _ _ ⟨i, Finset.mem_Iic.mpr le_rfl⟩
  simp only [Finset.mem_Iic] at hj_mem hj_le
  use j, hj_mem
  apply le_antisymm
  · exact partialSups_le _ _ _ fun k hk => hj_le k hk
  · exact le_partialSups_of_le f hj_mem

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
⊢ (disjointed f i ⊔ (Iio i).sup fun x ↦ (Iic x).sup fun x ↦ disjointed f x) = (partialSups f) i

Tactic:
sup_congr rfl (g := partialSups f)

Goal state after:
case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
⊢ disjointed f i ⊔ (Iio i).sup ⇑(partialSups f) = (partialSups f) i

case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
⊢ ∀ a ∈ Iio i, ((Iic a).sup fun x ↦ disjointed f x) = (partialSups f) a
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
this : Iio (succ i) = Iic i
⊢ f (succ i) \ (Iio (succ i)).sup f ⊔ f i = f (succ i)

Tactic:
this,

Goal state after:
case neg
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
this : Iio (succ i) = Iic i
⊢ f (succ i) \ (Iic i).sup f ⊔ f i = f (succ i)
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 ι
i : ι
hi : hι.some ≤ i
h_nonneg : 0 ≤ toZ hι.some i
⊢ succ^[(toZ hι.some i).toNat] hι.some = i

Tactic:
exact iterate_succ_toZ i hi

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
hf : Monotone f
m✝ n : ι
this : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
m : ι
hm : n ≤ m
ih : (Ioc n m).sup (disjointed f) = f m \ f n
h'm : ¬IsMax m
⊢ f (succ m) \ f m ⊔ f m \ f n = f (succ m) \ f n

Tactic:
exact sdiff_sup_sdiff_cancel (hf (Order.le_succ m)) (hf hm)

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
⊢ toZ hι.some (succ^[n.toNat] hι.some) = n

Tactic:
rw [toZ_iterate_succ]

Goal state after:
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
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ ↑[(n + 1, 0)] + ↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) =
    (n + 1, 0) ::ₘ ↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n))

Tactic:
coe_add,

Goal state after:
n : ℕ
⊢ ↑([(n + 1, 0)] ++ List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) =
    (n + 1, 0) ::ₘ ↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n))
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
n : ℕ
⊢ (toZ ⊥ (succ^[n] ⊥)).toNat = n

Tactic:
rw [toZ_iterate_succ]

Goal state after:
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
n : ℕ
⊢ (↑n).toNat = n
Module: Mathlib.RingTheory.Ideal.Prime

Goal state before:
pp: α : Type u
inst✝¹ : Semiring α
I : Ideal α
inst✝ : I.IsTwoSided
hI : I.IsPrime
x y : α
⊢ x ∈ I ∨ y ∈ I → x * y ∈ I

Tactic:
rintro (h | h)
    exacts [I.mul_mem_right y h, I.mul_mem_left x h]

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

Goal state before:
pp: α : Type u
inst✝² : Semiring α
I : Ideal α
inst✝¹ : I.IsTwoSided
inst✝ : I.IsPrime
x y : α
hx : y ∉ I
⊢ x * y ∈ I ↔ x ∈ I

Tactic:
rw [Ideal.IsPrime.mul_mem_iff_mem_or_mem]

Goal state after:
α : Type u
inst✝² : Semiring α
I : Ideal α
inst✝¹ : I.IsTwoSided
inst✝ : I.IsPrime
x y : α
hx : y ∉ I
⊢ x ∈ I ∨ y ∈ I ↔ x ∈ I

case hI
α : Type u
inst✝² : Semiring α
I : Ideal α
inst✝¹ : I.IsTwoSided
inst✝ : I.IsPrime
x y : α
hx : y ∉ I
⊢ I.IsPrime
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : R
⊢ IsIdempotentElem a ↔ a * a = a

Tactic:
IsIdempotentElem

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
a : R
⊢ a * a = a ↔ a * a = a
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
⊢ IsIdempotentElem a ∧ IsIdempotentElem b

Tactic:
IsIdempotentElem

Goal state after:
R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
⊢ a * a = a ∧ b * b = 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
this : a * b = 0
⊢ Commute a b

Tactic:
this,

Goal state after:
R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : 0 + b * a = 0
this : a * b = 0
⊢ Commute a b
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : Semiring α
P : Ideal α
hmax : ∀ (m : Ideal α), P < m → ¬m.IsMaximal
J : Ideal α
hPJ : P < J
hnonmax : ¬J = ⊤
M : Ideal α
hM1 : M.IsMaximal
hM2 : J ≤ M
⊢ False

Tactic:
exact hmax M (lt_of_lt_of_le hPJ hM2) hM1

Goal state after: