mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ natAdd m '' Ioi i = Ioi (natAdd m i)

Tactic:
rw [← preimage_natAdd_Ioi_natAdd, image_preimage_eq_of_subset]

Goal state after:
n m : ℕ
i : Fin n
⊢ Ioi (natAdd m i) ⊆ range (natAdd m)
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m '' Ioo i j = Ioo (natAdd m i) (natAdd m j)

Tactic:
rw [← preimage_natAdd_Ioo_natAdd, image_preimage_eq_of_subset]

Goal state after:
n m : ℕ
i j : Fin n
⊢ Ioo (natAdd m i) (natAdd m j) ⊆ range (natAdd m)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
s : Set α
hf : (s ∩ mulSupport f).Finite
hg : (s ∩ mulSupport g).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i * g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i

Tactic:
by
  rw [← mulSupport_mulIndicator] at hf hg
  simp only [finprod_mem_def, mulIndicator_mul, finprod_mul_distrib hf hg]

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝ : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R✝ M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
⊢ (fun f i ↦ f (b i)) ((fun f ↦ linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ ↑b.repr) f) = f

Tactic:
ext
    simp

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

Goal state before:
pp: n m : ℕ
⊢ #{i | ↑i < m} = min n m

Tactic:
by
  simp [← card_map valEmbedding, ← filter_filter, exists_iff, map_filter']

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

Goal state before:
pp: case neg
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∉ mulSupport f
⊢ 1 ∣ finprod f

Tactic:
exact one_dvd (finprod f)

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

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n), ¬p k → #{i | p i} ≤ ↑k
h : p j
hc : #{i | p i} ≤ ↑j
q : Fin n → Prop := fun x ↦ ↑x < #{i | p i}
⊢ #(filter p univ) ≤ #(filter q univ)

Tactic:
rw [card_filter_val_lt]

Goal state after:
n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n), ¬p k → #{i | p i} ≤ ↑k
h : p j
hc : #{i | p i} ≤ ↑j
q : Fin n → Prop := fun x ↦ ↑x < #{i | p i}
⊢ #(filter p univ) ≤ min n #{i | p i}
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
⊢ ↑(a - 1) = if a = 0 then n else ↑a - 1

Tactic:
cases n

Goal state after:
case zero
a : Fin (0 + 1)
⊢ ↑(a - 1) = if a = 0 then 0 else ↑a - 1

case succ
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
⊢ ↑(a - 1) = if a = 0 then n✝ + 1 else ↑a - 1
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
k : Fin (n + 1)
⊢ k ≤ k - 1 ↔ k = 0

Tactic:
cases n

Goal state after:
case zero
k : Fin (0 + 1)
⊢ k ≤ k - 1 ↔ k = 0

case succ
n✝ : ℕ
k : Fin (n✝ + 1 + 1)
⊢ k ≤ k - 1 ↔ k = 0
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ (a + b).rev = a.rev - b

Tactic:
cases n

Goal state after:
case zero
a b : Fin 0
⊢ (a + b).rev = a.rev - b

case succ
n✝ : ℕ
a b : Fin (n✝ + 1)
⊢ (a + b).rev = a.rev - b
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
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:
· have H : ¬ (fun i ↦ (f i : R)).HasFiniteMulSupport :=
      fun h ↦ hf <| h.of_comp cast_one cast_injective
    rw [finprod_of_not_hasFiniteMulSupport hf, finprod_of_not_hasFiniteMulSupport H, cast_one]

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

Goal state before:
pp: case h
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
m : ℤ
h : m • p = b - a
⊢ (↑m.toNat - ↑(-m).toNat) • p = b - a

Tactic:
m.toNat_sub_toNat_neg

Goal state after:
case h
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
m : ℤ
h : m • p = b - a
⊢ m • p = b - a
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case mp
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ (∃ m, a - b = m • p) → ∃ i, i < n ∧ ∃ m, a - b = (m * ↑n + ↑i) • p

pp: case mpr
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ (∃ i, i < n ∧ ∃ m, a - b = (m * ↑n + ↑i) • p) → ∃ m, a - b = m • p

Tactic:
· rintro ⟨k, hk⟩
    refine ⟨(k % n).toNat, ?_⟩
    rw [← Int.ofNat_lt, Int.toNat_of_nonneg (Int.emod_nonneg _ (mod_cast hn))]
    refine ⟨?_, k / n, ?_⟩
    · refine Int.emod_lt_of_pos _ ?_
      lia
    · rw [hk, Int.ediv_mul_add_emod]

Goal state after:
case mpr
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ (∃ i, i < n ∧ ∃ m, a - b = (m * ↑n + ↑i) • p) → ∃ m, a - b = m • p
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
⊢ hv.repr x = l

Tactic:
by
  have :
    ↑((LinearIndependent.linearCombinationEquiv hv : (ι →₀ R) →ₗ[R] span R (range v)) l) =
      Finsupp.linearCombination R v l :=
    rfl
  have : (LinearIndependent.linearCombinationEquiv hv : (ι →₀ R) →ₗ[R] span R (range v)) l = x := by
    rw [eq] at this
    exact Subtype.ext_iff.2 this
  rw [← LinearEquiv.symm_apply_apply hv.linearCombinationEquiv l]
  rw [← this]
  rfl

Goal state after:
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 : ℕ
v : Fin m → M
x : M
hli : LinearIndependent R v
x_ortho : ∀ (c : R), ∀ y ∈ span R (range v), c • x + y = 0 → c = 0
⊢ LinearIndependent R (Fin.snoc v x)

Tactic:
Fin.snoc_eq_cons_rotate v x,

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
v : Fin m → M
x : M
hli : LinearIndependent R v
x_ortho : ∀ (c : R), ∀ y ∈ span R (range v), c • x + y = 0 → c = 0
⊢ LinearIndependent R fun i ↦ Fin.cons x v ((finRotate (m + 1)) i)
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:
← Finset.sum_add_distrib

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
| ∑ x ∈ s with g x ≤ f x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + g x • v x) +
    ∑ i ∈ s with f i < g i, f i • v i
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
⊢ ∀ (a : Fin (∏ i, i.elim0)), ⟨∑ i, (↑a / ∏ j, (Fin.castLE ⋯ j).elim0) % i.elim0 * ∏ j, (Fin.castLE ⋯ j).elim0, ⋯⟩ = a

Tactic:
intro a
        have : Subsingleton (Fin (∏ i : Fin 0, i.elim0)) :=
          (finCongr <| prod_empty).subsingleton
        subsingleton

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
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, g i • v i +
    (∑ i ∈ s with f i < g i, (if g i ≤ f i then f i - g i else g i - f i) • v i + ∑ i ∈ s with f i < g i, f i • v i)

Tactic:
← Finset.sum_add_distrib

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, g i • v i +
    ∑ x ∈ s with f x < g x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + f x • v x)
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ℤ
h✝ : ¬0 ≤ x
h : ¬n ∣ x.natAbs
⊢ 0 < ↑n

Tactic:
by have := NeZero.ne n; lia

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ Nat.card ↑(range f) = Nat.card α

Tactic:
← Nat.card_preimage_of_injective hf le_rfl

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ Nat.card ↑(f ⁻¹' range f) = Nat.card α
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: n : ℕ
⊢ Nat.card (ZMod n) = n

Tactic:
cases n

Goal state after:
case zero
⊢ Nat.card (ZMod 0) = 0

case succ
n✝ : ℕ
⊢ Nat.card (ZMod (n✝ + 1)) = n✝ + 1
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: n : ℕ
c : Cardinal.{u_3}
⊢ ↑n = toENat c ↔ ↑n = c

Tactic:
by
  rw [le_antisymm_iff, le_antisymm_iff, Cardinal.toENat_le_natCast, Cardinal.natCast_le_toENat]

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
h✝ : Module.rank R M ≠ 0
h : 1 ≤ Module.rank R M
⊢ ?m.16

Tactic:
one_le_rank_iff

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h✝ : Module.rank R M ≠ 0
h : ∃ f, Injective ⇑f
⊢ ?m.16
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
x✝ : s.Finite ∧ ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
left✝ : s.Finite
n₀ : ℕ
hs : s.encard = ↑n₀
hle : n₀ ≤ k
⊢ s.encard ≤ ↑k

Tactic:
by rwa [hs, Nat.cast_le]

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

Goal state before:
pp: case refine_2
ι : 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 ι
h : ∀ t ⊆ s, ∀ (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i → ∀ i ∈ s, f i = 0
t : Finset ↑↑s
f : ↑↑s → R
heq : ∑ i ∈ t, f i • v ↑i = ∑ i ∈ tᶜ, f i • v ↑i
i : ↑↑s
⊢ f i = 0

Tactic:
specialize h (t.map (Embedding.subtype _)) (Finset.map_subtype_subset _)
      (fun i => if h : i ∈ s then f ⟨i, h⟩ else 0) ?_ i i.2
    · conv =>
        enter [2, 1, 1]
        rw [← s.subtype_map_of_mem (fun x hx => hx), Finset.subtype_eq_univ.2 (fun x hx => hx)]
        change Finset.map (Embedding.subtype (· ∈ (s : Set ι))) _
      rw [← Finset.map_sdiff]
      simpa [Embedding.subtype, ← Finset.compl_eq_univ_sdiff]
    simpa using h

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

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

Tactic:
rintro rfl; exact (hs.symm.subset (Or.inr rfl)).2 rfl

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

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = 0 → l = 0
f : ι →₀ R
hf : f ∈ Finsupp.supported R R s
g : ι →₀ R
hg : g ∈ Finsupp.supported R R s
eq : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
⊢ (Finsupp.linearCombination R v) (f - g) = 0

Tactic:
rw [map_sub, eq, sub_self]

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α = 0 ↔ IsEmpty α

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_eq_zero_iff]

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

Goal state before:
pp: case h.inr
P : Type u_4 → Prop
hbase : ∀ (α : Type u_4) [Finite α] [Subsingleton α], P α
hstep : ∀ (α : Type u_4) [Finite α] [Nontrivial α], (∀ (β : Type u_4) [Finite β], Nat.card β < Nat.card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [Finite α], Nat.card α = m → P α
α : Type u_4
inst✝ : Finite α
hn : Nat.card α = n
hnontriv : Nontrivial α
⊢ P α

Tactic:
apply hstep

Goal state after:
case h.inr
P : Type u_4 → Prop
hbase : ∀ (α : Type u_4) [Finite α] [Subsingleton α], P α
hstep : ∀ (α : Type u_4) [Finite α] [Nontrivial α], (∀ (β : Type u_4) [Finite β], Nat.card β < Nat.card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [Finite α], Nat.card α = m → P α
α : Type u_4
inst✝ : Finite α
hn : Nat.card α = n
hnontriv : Nontrivial α
⊢ ∀ (β : Type u_4) [Finite β], Nat.card β < Nat.card α → P β
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
⊢ ∀ (a₁ a₂ : α),
    (∀ (x : ι), quotientMapOfLE ⋯ (Quotient.mk'' a₁) = quotientMapOfLE ⋯ (Quotient.mk'' a₂)) →
      Quotient.mk'' a₁ = Quotient.mk'' a₂

Tactic:
quotientMapOfLE_apply_mk,

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
⊢ ∀ (a₁ a₂ : α), (∀ (x : ι), ↑a₁ = ↑a₂) → Quotient.mk'' a₁ = Quotient.mk'' a₂
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ sᶜ.ncard = s.ncard + sᶜ.ncard - s.ncard

Tactic:
Nat.add_sub_cancel_left

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ sᶜ.ncard = sᶜ.ncard
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
x : α
⊢ x ∈ Ico (succ a) b ↔ x ∈ Ioo a b

Tactic:
rw [mem_Ico, mem_Ioo, succ_le_iff_of_not_isMax ha]

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : PredOrder α
a b : α
⊢ ↑(Ioc a (pred b)) = ↑(Ioo a b)

Tactic:
by simpa using Set.Ioc_pred_right_eq_Ioo _ _

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a - 1 ≤ b
⊢ insert (a - 1) (Icc a b) = Icc (a - 1) b

Tactic:
simpa [← pred_eq_sub_one] using insert_Icc_left_eq_Icc_pred (pred_eq_sub_one a ▸ h)

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: 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₂
⊢ p₁.prod p₂ = ⊥ ↔ p₁ = ⊥ ∧ p₂ = ⊥

Tactic:
by
  simp only [eq_bot_iff, prod_le_iff, (gc_map_comap _).le_iff_le, comap_bot, ker_inl, ker_inr]

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

Tactic:
refine (ciSup_le fun i ↦ ?_).antisymm (ciSup_mono ?_ <| le_partialSups f)
    · simpa only [partialSups_eq_ciSup_Iic] using ciSup_le fun i ↦ le_ciSup h _
    · rwa [bddAbove_range_partialSups]

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

Goal state before:
pp: ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i ≤ j
⊢ ∃ n, succ^[n] i = j

Tactic:
le_iff_lt_or_eq

Goal state after:
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j ∨ i = j
⊢ ∃ n, succ^[n] i = j
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
⊢ toZ i0 (succ^[n] i0) = ↑n

Tactic:
by_cases hmn : m = n

Goal state after:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : m = n
⊢ toZ i0 (succ^[n] i0) = ↑n

case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : ¬m = n
⊢ toZ i0 (succ^[n] i0) = ↑n
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ j ∈ range n, f (n - 1 - j) = ∏ j ∈ range n, f j

Tactic:
cases n

Goal state after:
case zero
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
⊢ ∏ j ∈ range 0, f (0 - 1 - j) = ∏ j ∈ range 0, f j

case succ
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
n✝ : ℕ
⊢ ∏ j ∈ range (n✝ + 1), f (n✝ + 1 - 1 - j) = ∏ j ∈ range (n✝ + 1), f j
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 * a + a * b * a = 0
⊢ (1 + 1) • (a * b * a) = 0

Tactic:
← two_nsmul

Goal state after:
R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
this : 2 • (a * b * a) = 0
⊢ (1 + 1) • (a * b * a) = 0
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x * (1 - e) ∈ (LinearMap.toSpanSingleton R R e).ker

Tactic:
change x * (1 - e) * e = 0

Goal state after:
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x * (1 - e) * e = 0
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n k : ℕ
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)

Tactic:
by
  rcases lt_or_ge n k with h | h
  · rw [choose_eq_zero_of_lt (by lia), Icc_eq_empty_of_lt h, sum_empty]
  · induction n, h using le_induction with
    | base => simp
    | succ n _ ih =>
      rw [← Ico_insert_right (by lia), sum_insert (by simp), Ico_add_one_right_eq_Icc, ih,
        choose_succ_succ' (n + 1)]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: case zero.succ
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
hf : Surjective ⇑f
hi : Injective ⇑i
heq : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (0 + 1) K
m : ℕ
ih : f.iterateMapComap i m K ≠ f.iterateMapComap i (m + 1) K
⊢ f.iterateMapComap i (m + 1) K ≠ f.iterateMapComap i (m + 1 + 1) K

Tactic:
rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ']
      exact fun H ↦ ih (map_injective_of_injective hi (comap_injective_of_surjective hf H))

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

Goal state before:
pp: case single
ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
R : ι → Type u_6
inst✝ : (i : ι) → Semiring (R i)
i : ι
r : R i
⊢ Pi.single i r ∈ span (range fun i ↦ Pi.single i 1)

Tactic:
rw [show Pi.single i r = Pi.single i r * Pi.single i 1 by simp [← Pi.single_mul_left]]

Goal state after:
case single
ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
R : ι → Type u_6
inst✝ : (i : ι) → Semiring (R i)
i : ι
r : R i
⊢ Pi.single i r * Pi.single i 1 ∈ span (range fun i ↦ Pi.single i 1)
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst✝ : DivisionSemiring K
I✝ I : Ideal K
⊢ ![⊥, ⊤] ((fun I ↦ if I = ⊥ then 0 else 1) I) = I

Tactic:
rcases eq_bot_or_top I with rfl | rfl

Goal state after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst✝ : DivisionSemiring K
I : Ideal K
⊢ ![⊥, ⊤] ((fun I ↦ if I = ⊥ then 0 else 1) ⊥) = ⊥

case inr
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst✝ : DivisionSemiring K
I : Ideal K
⊢ ![⊥, ⊤] ((fun I ↦ if I = ⊥ then 0 else 1) ⊤) = ⊤
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ∀ (p : Ideal R), p ≠ ⊥ → ¬p.IsMaximal
⊢ IsField R

Tactic:
simp only [← bot_lt_iff_ne_bot] at h

Goal state after:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ∀ (p : Ideal R), ⊥ < p → ¬p.IsMaximal
⊢ IsField R
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
x y : α →₀ M
⊢ ⇑(x + y) = ⇑x + ⇑y

Tactic:
ext
    simp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
x : R
y : α →₀ M
⊢ ⇑(x • y) = (RingHom.id R) x • ⇑y

Tactic:
ext
    simp

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

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
⊢ p s

Tactic:
have q_mono : Monotone q := fun a b hab ha ↦
    ⟨mem_of_superset ha.1 hab, fun t hbt ↦ ha.2 _ (hab.trans hbt)⟩

Goal state after:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
⊢ p s
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
a : α
p : α → Prop
⊢ (∃ᶠ (x : α) in pure a, p x) ↔ p a

Tactic:
by
  simp [Filter.Frequently]

Goal state after: