mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case e'_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
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 =
    ∑ i ∈ s, f i • v i

Tactic:
← Finset.sum_filter_add_sum_filter_not s (fun i => g i ≤ f i),

Goal state after:
case e'_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
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 =
    ∑ i ∈ s with g i ≤ f i, f i • v i + ∑ i ∈ s with ¬g i ≤ f i, f i • v i
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case e'_3
ι : 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) =
    ∑ i ∈ s, g i • v i

Tactic:
← Finset.sum_filter_add_sum_filter_not s (fun i => g i ≤ f i),

Goal state after:
case e'_3
ι : 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) =
    ∑ i ∈ s with g i ≤ f i, g i • v i + ∑ i ∈ s with ¬g i ≤ f i, g i • v i
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite β
f : α → β
hf : Injective f
⊢ Nat.card α ≤ Nat.card β

Tactic:
by
  simpa using! toNat_le_toNat (lift_mk_le_lift_mk_of_injective hf) (by simp)

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

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
g h : G
L : List G
⊢ g * h⁻¹ * ∏ i, L[i] ^ (-1) ^ ↑i = ∏ i, (g :: h :: L)[i] ^ (-1) ^ ↑i

Tactic:
Fin.prod_univ_succ,

Goal state after:
G : Type u_3
inst✝ : DivisionCommMonoid G
g h : G
L : List G
⊢ g * h⁻¹ * ∏ i, L[i] ^ (-1) ^ ↑i = (g :: h :: L)[0] ^ (-1) ^ ↑0 * ∏ i, (g :: h :: L)[i.succ] ^ (-1) ^ ↑i.succ
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
g h : G
L : List G
⊢ g * h⁻¹ * ∏ i, L[i] ^ (-1) ^ ↑i = (g :: h :: L)[0] ^ (-1) ^ ↑0 * ∏ i, (g :: h :: L)[i.succ] ^ (-1) ^ ↑i.succ

Tactic:
Fin.prod_univ_succ,

Goal state after:
G : Type u_3
inst✝ : DivisionCommMonoid G
g h : G
L : List G
⊢ g * h⁻¹ * ∏ i, L[i] ^ (-1) ^ ↑i =
    (g :: h :: L)[0] ^ (-1) ^ ↑0 *
      ((g :: h :: L)[Fin.succ 0] ^ (-1) ^ ↑(Fin.succ 0) * ∏ i, (g :: h :: L)[i.succ.succ] ^ (-1) ^ ↑i.succ.succ)
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α

Tactic:
by
  have := Fintype.ofFinite α
  rw [Nat.card_pi, Finset.prod_const, Finset.card_univ, ← Nat.card_eq_fintype_card]

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

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Finite
this : Fintype ↑s
⊢ ENat.card ↑s = ↑h.toFinset.card

Tactic:
ENat.card_eq_coe_fintype_card,

Goal state after:
α : Type u_1
s : Set α
h : s.Finite
this : Fintype ↑s
⊢ ↑(Fintype.card ↑s) = ↑h.toFinset.card
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
e : α
⊢ ENat.card ↑{e} = 1

Tactic:
ENat.card_eq_coe_fintype_card,

Goal state after:
α : Type u_1
e : α
⊢ ↑(Fintype.card ↑{e}) = 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : Disjoint s t
⊢ (s ∪ t).encard = s.encard + t.encard

Tactic:
classical
  unfold encard
  simp [ENat.card_congr (Equiv.Set.union h)]

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
hst : (t \ s).encard + s.encard = s.encard + 1
⊢ ∃ a, t = insert a s

Tactic:
add_comm _ 1,

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
hst : (t \ s).encard + s.encard = 1 + s.encard
⊢ ∃ a, t = insert a s
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mp
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
h : ∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0
i : ι
h_in_span : v i ∈ span K (v '' (univ \ {i}))
⊢ False

Tactic:
apply one_ne_zero (h i 1 (by simp [h_in_span]))

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

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s : Set ι
⊢ LinearIndepOn K v s ↔ ∀ i ∈ s, v i ∉ span K (v '' (s \ {i}))

Tactic:
by
  rw [LinearIndepOn, linearIndependent_iff_notMem_span, ← Function.comp_def]
  simp_rw [Set.image_comp]
  simp [Set.image_sdiff Subtype.val_injective]

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ 1 < Nat.card α ↔ Nontrivial α

Tactic:
by
  have := Fintype.ofFinite α
  simp only [Nat.card_eq_fintype_card, Fintype.one_lt_card_iff_nontrivial]

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

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

Tactic:
rw [← @Nat.cast_le Cardinal, Nat.cast_add, Nat.cast_card, Nat.cast_card, Nat.cast_card]

Goal state after:
case inl.intro
α : Type u_1
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ Cardinal.mk ↑(s ∪ t) ≤ Cardinal.mk ↑s + Cardinal.mk ↑t
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
⊢ Nat.card ↑s < Nat.card ↑t

Tactic:
have : Fintype t := Finite.fintype ht

Goal state after:
α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
this : Fintype ↑t
⊢ Nat.card ↑s < Nat.card ↑t
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
s : Set α
⊢ s.ncard ≤ (insert a s).ncard

Tactic:
classical
  refine
    s.finite_or_infinite.elim (fun h ↦ ?_) (fun h ↦ by (rw [h.ncard]; exact Nat.zero_le _))
  rw [ncard_insert_eq_ite h]; split_ifs <;> simp

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

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun i ↦ f ↑i ⋯
x : α
⊢ x ∈ s ↔ x ∈ f' '' univ

Tactic:
simp only [image_univ, mem_range]

Goal state after:
α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun i ↦ f ↑i ⋯
x : α
⊢ x ∈ s ↔ ∃ y, f' y = x
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
h : ∀ (g : α), g • ↑s = op g • ↑s
a : α
ha : a ∈ s
g : α
⊢ g * a * g⁻¹ ∈ ↑s

Tactic:
rw [← mem_rightCoset_iff, ← h]; exact mem_leftCoset g ha

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

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
hns : n ≤ s.ncard
⊢ ∃ t ⊆ s, t.ncard = n

Tactic:
by
  simpa using exists_subsuperset_card_eq s.empty_subset (by simp) hns

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

Goal state before:
pp: G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H✝ : Type v
inst✝¹ : Group H✝
M : Type x
inst✝ : Monoid M
φ✝ : G →* H✝
H N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
y : G
hy : y ∈ H ⊔ N
⊢ ∃ a, φ a = Quotient.mk'' ⟨y, hy⟩

Tactic:
← SetLike.mem_coe

Goal state after:
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H✝ : Type v
inst✝¹ : Group H✝
M : Type x
inst✝ : Monoid M
φ✝ : G →* H✝
H N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
y : G
hy✝ : y ∈ H ⊔ N
hy : y ∈ ↑(H ⊔ N)
⊢ ∃ a, φ a = Quotient.mk'' ⟨y, hy✝⟩
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Nonempty α
hs : s.Finite
⊢ hs.toFinset.card ≤ 1 ↔ ∃ x, s ⊆ {x}

Tactic:
Finset.card_le_one_iff_subset_singleton,

Goal state after:
α : Type u_1
s : Set α
inst✝ : Nonempty α
hs : s.Finite
⊢ (∃ x, hs.toFinset ⊆ {x}) ↔ ∃ x, s ⊆ {x}
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: ι : Type u_1
A : ι → Type u_2
inst✝ : (i : ι) → CommGroup (A i)
n : ℕ
φ : ((i : ι) → A i) →* (i : ι) → A i ⧸ (powMonoidHom n).range :=
  { toFun := fun x x_1 ↦ ↑(x x_1), map_one' := ⋯, map_mul' := ⋯ }
y : (i : ι) → A i ⧸ (powMonoidHom n).range
⊢ (φ fun i ↦ Quotient.out (y i)) = y

Tactic:
simp [φ]

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
⊢ Subsingleton (RingCon R) ↔ Subsingleton R

Tactic:
simp_rw [← not_nontrivial_iff_subsingleton, nontrivial_iff]

Goal state after:
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y = y * (x * z)

Tactic:
rw [hxz, mul_one]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' p'' : Submodule R M
H1 : p ≤ p'
H2 : p' ≤ p''
x : M ⧸ p
⊢ (factor H2) ((factor H1) x) = (factor ⋯) x

Tactic:
rw [← comp_apply]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' p'' : Submodule R M
H1 : p ≤ p'
H2 : p' ≤ p''
x : M ⧸ p
⊢ (factor H2 ∘ₗ factor H1) x = (factor ⋯) x
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
⊢ ↑(insert b (Icc a (pred b))) = ↑(Icc a b)

Tactic:
simpa using Set.insert_Icc_pred_right_eq_Icc h

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

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_2
inst✝² : Finite ι
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ a ≤ ⨆ i, f i ⊔ a

Tactic:
exact le_ciSup_of_le (Classical.arbitrary ι) le_sup_right

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

Goal state before:
pp: case e_s
G : Type u_4
inst✝ : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
⊢ ∀ (a : ℕ), a ∈ Ico n m ↔ a ∈ {k ∈ range m | n ≤ k}

Tactic:
simp only [mem_Ico, mem_filter, mem_range, *]

Goal state after:
case e_s
G : Type u_4
inst✝ : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
⊢ ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ disjointed f (succ i) = f (succ i) \ (partialSups f) i

Tactic:
by
  rw [disjointed_apply, partialSups_apply, sup'_eq_sup]
  congr 2 with m
  simpa only [mem_Iio, mem_Iic] using lt_succ_iff_of_not_isMax hi

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝¹ : Monoid A
inst✝ : HasMulAntidiagonal A
n k l : A
h : (k, l) ∈ mulAntidiagonal n
⊢ (fun x ↦ ⟨x.1 * x.2, ⟨x, ⋯⟩⟩) ((fun x ↦ ↑x.snd) ⟨n, ⟨(k, l), h⟩⟩) = ⟨n, ⟨(k, l), h⟩⟩

Tactic:
rw [mem_mulAntidiagonal] at h

Goal state after:
A : Type u_1
inst✝¹ : Monoid A
inst✝ : HasMulAntidiagonal A
n k l : A
h✝ : (k, l) ∈ mulAntidiagonal n
h : (k, l).1 * (k, l).2 = n
⊢ (fun x ↦ ⟨x.1 * x.2, ⟨x, ⋯⟩⟩) ((fun x ↦ ↑x.snd) ⟨n, ⟨(k, l), h✝⟩⟩) = ⟨n, ⟨(k, l), h✝⟩⟩
Module: Mathlib.Order.Disjointed

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

Tactic:
induction hm using Succ.rec with

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

Goal state before:
pp: case pos
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
hn_max : IsMax (succ^[↑n] ⊥)
⊢ ↑n ≤ (toZ ⊥ (succ^[↑n] ⊥)).toNat

Tactic:
rw [← isTop_iff_isMax, isTop_iff_eq_top] at hn_max

Goal state after:
case pos
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
hn_max : succ^[↑n] ⊥ = ⊤
⊢ ↑n ≤ (toZ ⊥ (succ^[↑n] ⊥)).toNat
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case neg
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
hn_max : ¬IsMax (succ^[↑n] ⊥)
⊢ ↑n ≤ (toZ ⊥ (succ^[↑n] ⊥)).toNat

Tactic:
· rw [toZ_iterate_succ_of_not_isMax _ hn_max]
      simp only [Int.toNat_natCast, le_refl]

Goal state after:
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
| b

Tactic:
rw [← one_mul b, ← add, add_mul, mul, zero_add]

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

Tactic:
nsmul_zero

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
⊢ (1 + 1) • (a * b * a) = 0
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
h1 : q * (p * q + q * p - p) = q * p
h2 : (p * q + q * p - p) * q = p * q
⊢ Commute p q

Tactic:
simp_rw [mul_sub, mul_add, ← mul_assoc, hq.eq, add_sub_cancel_right] at h1

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
h2 : (p * q + q * p - p) * q = p * q
h1 : q * p * q = q * p
⊢ Commute p q
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
b₁ b₂ : α
h₁ : b₁ ≠ 0
h₂ : ¬IsUnit b₂
h : span {b₁} ≤ span {b₁ * b₂}
⊢ b₁ * b₂ ∣ b₁ * 1

Tactic:
rwa [mul_one, ← Ideal.span_singleton_le_span_singleton]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
⊢ ∑ m ∈ range (2 * n + 1), (2 * n).choose m ≤ ∑ x ∈ range (2 * n + 1), (2 * n).choose (2 * n / 2)

Tactic:
gcongr; apply choose_le_middle

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

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x - z * y, y} = span {x, y}

Tactic:
rw [mul_comm, span_pair_sub_right_mul]

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
s₁ : α
hs₁ : s₁ ∈ S
i₁ : α
hi₁ : i₁ ∈ I
r₁ : α
hr₁ : i₁ + x * r₁ = s₁
s₂ : α
hs₂ : s₂ ∈ S
i₂ : α
hi₂ : i₂ ∈ I
r₂ : α
hr₂ : i₂ + y * r₂ = s₂
⊢ (i₁ + x * r₁) * i₂ + (i₁ * (y * r₂) + x * y * (r₁ * r₂)) = (i₁ + x * r₁) * s₂

Tactic:
← hr₂

Goal state after:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
s₁ : α
hs₁ : s₁ ∈ S
i₁ : α
hi₁ : i₁ ∈ I
r₁ : α
hr₁ : i₁ + x * r₁ = s₁
s₂ : α
hs₂ : s₂ ∈ S
i₂ : α
hi₂ : i₂ ∈ I
r₂ : α
hr₂ : i₂ + y * r₂ = s₂
⊢ (i₁ + x * r₁) * i₂ + (i₁ * (y * r₂) + x * y * (r₁ * r₂)) = (i₁ + x * r₁) * (i₂ + y * r₂)
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
this : 1 ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
⊢ {↑x ^ (n + 1)} ⊆ ↑(span ((fun x ↦ x ^ (n + 1)) '' s))

Tactic:
Set.singleton_subset_iff

Goal state after:
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
this : 1 ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
⊢ ↑x ^ (n + 1) ∈ ↑(span ((fun x ↦ x ^ (n + 1)) '' s))
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq α
x : α
⊢ lcoeFun ∘ₗ lsingle x = LinearMap.single R (fun x ↦ M) x

Tactic:
ext; simp [single_eq_pi_single]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
g : β → α
hfg : LeftInvOn g f s
F : Filter α
hF : F ≤ 𝓟 s
this : g ∘ f =ᶠ[𝓟 s] id
⊢ map (g ∘ f) F = F

Tactic:
map_congr (this.filter_mono hF),

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
g : β → α
hfg : LeftInvOn g f s
F : Filter α
hF : F ≤ 𝓟 s
this : g ∘ f =ᶠ[𝓟 s] id
⊢ map id F = F
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : Disjoint (Ico x₁ x₂) (Ico y₁ y₂)
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂

Tactic:
rw [Ico_disjoint_Ico, min_eq_left (le_of_lt h2.2), le_max_iff] at h

Goal state after:
α : Type v
inst✝ : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
U : Set (Set α)
f : β → α
⊢ generate ((fun x ↦ f ⁻¹' x) '' U) ≤ comap f (generate U)

Tactic:
by
  rw [← map_le_iff_le_comap, le_generate_iff]
  exact fun u hu ↦ mem_generate_of_mem ⟨u, hu, rfl⟩

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

Goal state before:
pp: α : Type u_1
f : Filter α
a : α
⊢ f ≤ pure a ↔ {a} ∈ f

Tactic:
by
  rw [← principal_singleton, le_principal_iff]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
⊢ s.seq t ∈ map (fun g ↦ g a) f

Tactic:
refine sets_of_superset (map (fun g : α → β => g a) f) (image_mem_map hs) ?_

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
⊢ (fun g ↦ g a) '' s ⊆ s.seq t
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
⊢ CommMonoid α

Tactic:
let one := e.one
  let mul := e.mul
  let pow := e.pow ℕ
  apply e.injective.commMonoid _ <;> intros <;> exact e.apply_symm_apply _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
⊢ IsSuccLimit (f a) ↔ IsSuccLimit a

Tactic:
by
  simp [isSuccLimit_iff]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ cof α ≤ 1 ↔ ∃ x, IsTop x

Tactic:
rw [le_iff_lt_or_eq, Cardinal.lt_one_iff, cof_eq_one_iff]
  simp

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ DirSupClosed sᶜ ↔ DirSupInacc s

Tactic:
← dirSupClosedOn_univ,

Goal state after:
α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ DirSupClosedOn univ sᶜ ↔ DirSupInacc s
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupClosed (f i)
⊢ DirSupClosed (⋂₀ range f)

Tactic:
exact DirSupClosed.sInter (by simpa)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ a • b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Tactic:
rw [← neg_nonneg, ← neg_smul, smul_nonneg_iff_pos_imp_nonneg]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < -a → 0 ≤ b) ∧ (0 < b → 0 ≤ -a) ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 ≤ b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ a₁ • b ≤ a₂ • b

Tactic:
by
    simp only [← hf, zero, smul] at *; exact smul_le_smul_of_nonneg_right ha hb

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
y : α
hy✝ : y ∈ Iic (sSup (f ⁻¹' Iic x))
hy : ∃ b ∈ f ⁻¹' Iic x, y < b
⊢ y ∈ f ⁻¹' Iic x

Tactic:
obtain ⟨z, hz, hyz⟩ := hy

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
y : α
hy : y ∈ Iic (sSup (f ⁻¹' Iic x))
z : α
hz : z ∈ f ⁻¹' Iic x
hyz : y < z
⊢ y ∈ f ⁻¹' Iic x