mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
n : ℕ
⊢ (∃ f g, ∑ i, f i • ↑(g i) = m) → ∃ x, (∀ (i : Fin n), (x i).2 ∈ s) ∧ ∑ i, (x i).1 • (x i).2 = m

Tactic:
rintro ⟨f, g, rfl⟩
    exact ⟨fun i ↦ (f i, g i), fun i ↦ (g i).2, rfl⟩

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

Goal state before:
pp: α : 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
⊢ ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y

Tactic:
simpa only [hs.mem_toFinset]

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

Goal state before:
pp: m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
⊢ vecAppend ho u v i = if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩

Tactic:
vecAppend,

Goal state after:
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
⊢ (Fin.append u v ∘ Fin.cast ho) i = if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg
α : 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 fun x ↦ f (g x)).Finite
⊢ (g '' (s ∩ mulSupport (f ∘ g))).Infinite

Tactic:
infinite_image_iff hg

Goal state after:
case neg
α : 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 fun x ↦ f (g x)).Finite
⊢ (s ∩ mulSupport (f ∘ g)).Infinite
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n✝ n : ℕ
inst✝ : NeZero n
a : ℤ
⊢ a / ↑n * ↑n + ↑(a.natMod ↑n % n) = a

Tactic:
natCast_mod,

Goal state after:
m n✝ n : ℕ
inst✝ : NeZero n
a : ℤ
⊢ a / ↑n * ↑n + ↑(a.natMod ↑n) % ↑n = a
Module: Mathlib.Algebra.Group.Fin.Basic

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

Tactic:
rw [← rev_lt_rev, Iff.comm, ← rev_lt_rev, rev_add, lt_sub_iff, rev_rev]

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
hi : i ≠ 0
⊢ ↑(i - 1) = ↑i - 1

Tactic:
Fin.val_sub_one_of_ne_zero

Goal state after:
n : ℕ
inst✝ : NeZero n
i : Fin n
hi : i ≠ 0
⊢ ↑i - 1 = ↑i - 1

n : ℕ
inst✝ : NeZero n
i : Fin n
hi : i ≠ 0
⊢ i ≠ 0
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
k i : Fin n
⊢ (fun i ↦ i - k) ((fun i ↦ i + k) i) = i

Tactic:
have := NeZero.of_pos k.pos

Goal state after:
n : ℕ
k i : Fin n
this : NeZero n
⊢ (fun i ↦ i - k) ((fun i ↦ i + k) i) = i
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
k i : Fin n
⊢ (fun i ↦ i + k) ((fun i ↦ i - k) i) = i

Tactic:
have := NeZero.of_pos k.pos

Goal state after:
n : ℕ
k i : Fin n
this : NeZero n
⊢ (fun i ↦ i + k) ((fun i ↦ i - k) i) = i
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:
by
  rw [modEq_iff_nsmul] at *
  rcases hab with ⟨m, n, hab⟩
  rcases hbc with ⟨k, l, hbc⟩
  use k + m, n + l
  rw [add_nsmul, add_assoc, hab, add_nsmul, add_assoc, ← hbc, add_left_comm]

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

Goal state before:
pp: case mpr
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
⊢ (∀ (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i) →
    ∀ (f g : ↑↑s → R), ∑ i, f i • v ↑i = ∑ i, g i • v ↑i → ∀ (i : ↑↑s), f i = g i

Tactic:
· rintro hv f g hfg i
    simpa using hv (fun j ↦ if hj : j ∈ s then f ⟨j, hj⟩ else 0)
      (fun j ↦ if hj : j ∈ s then g ⟨j, hj⟩ else 0) (by simpa +contextual [← s.sum_attach]) i

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

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

Tactic:
simp [← map_castSuccEmb_Ioo]

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

Goal state before:
pp: case inl
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ g k.castSucc = j.contractNth (fun x1 x2 ↦ x1 * x2) g k

pp: case inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ k.castSucc < j

pp: case inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ k.castSucc.castSucc < j.succ

Tactic:
contractNth_apply_of_lt

Goal state after:
case inl
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ g k.castSucc = g k.castSucc

case inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ ↑k < ↑j

case inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ k.castSucc < j

case inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ k.castSucc.castSucc < j.succ
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n a b c d : ℕ
h : a ≡ b [MOD n.gcd 0]
hn : ¬n = 0
hm : m = 0
⊢ b ≡ a [MOD n] ∧ b ≡ b [MOD m]

Tactic:
gcd_zero_right

Goal state after:
m n a b c d : ℕ
h : a ≡ b [MOD n]
hn : ¬n = 0
hm : m = 0
⊢ b ≡ a [MOD n] ∧ b ≡ b [MOD m]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b m n : ℕ
hmn : m.Coprime n
h : ↑m ∣ ↑b - ↑a ∧ ↑n ∣ ↑b - ↑a
⊢ a ≡ b [MOD m * n]

Tactic:
← Int.dvd_natAbs,

Goal state after:
a b m n : ℕ
hmn : m.Coprime n
h : ↑m ∣ ↑(↑b - ↑a).natAbs ∧ ↑n ∣ ↑b - ↑a
⊢ a ≡ b [MOD m * n]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b m n : ℕ
hmn : m.Coprime n
h : m ∣ (↑b - ↑a).natAbs ∧ ↑n ∣ ↑b - ↑a
⊢ a ≡ b [MOD m * n]

Tactic:
← Int.dvd_natAbs,

Goal state after:
a b m n : ℕ
hmn : m.Coprime n
h : m ∣ (↑b - ↑a).natAbs ∧ ↑n ∣ ↑(↑b - ↑a).natAbs
⊢ a ≡ b [MOD m * n]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b m n : ℕ
hmn : m.Coprime n
h : m ∣ (↑b - ↑a).natAbs ∧ n ∣ (↑b - ↑a).natAbs
⊢ ↑(m * n) ∣ ↑b - ↑a

Tactic:
← Int.dvd_natAbs,

Goal state after:
a b m n : ℕ
hmn : m.Coprime n
h : m ∣ (↑b - ↑a).natAbs ∧ n ∣ (↑b - ↑a).natAbs
⊢ ↑(m * n) ∣ ↑(↑b - ↑a).natAbs
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ card α = ↑(Fintype.card α)

Tactic:
simp [card]

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ card α < ⊤

Tactic:
simp [card]

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

Goal state before:
pp: α : Type u_3
⊢ card α = 0 ↔ #α = 0

Tactic:
simp [card]

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

Goal state before:
pp: α : Type u_3
⊢ card α ≤ 1 ↔ #α ≤ 1

Tactic:
simp [card]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (↑s).encard = ↑s.card

Tactic:
rw [Finite.encard_eq_coe_toFinset_card (Finset.finite_toSet s)]

Goal state after:
α : Type u_1
s : Finset α
⊢ ↑⋯.toFinset.card = ↑s.card
Module: Mathlib.Data.Set.Card

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

Tactic:
rwa [nonempty_iff_ne_empty, Ne, ← encard_eq_zero]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * (y⁻¹ * (y * x⁻¹)) ∈ s ↔ z * y⁻¹ ∈ s

Tactic:
← mul_assoc

Goal state after:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * y⁻¹ * (y * x⁻¹) ∈ s ↔ z * y⁻¹ ∈ s
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : IsTorsionFree R S
b : Basis ι S M
m : M
h✝ : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
i : ι
x✝ : i ∈ (b.repr m).support
w✝ : R
h : (algebraMap R S) w✝ = (b.repr m) i
⊢ w✝ • b i ∈ span R (range ⇑b)

Tactic:
exact smul_mem _ _ (subset_span (Set.mem_range_self i))

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x x✝ : α
⊢ x✝ ∈ orbitRel.Quotient.orbit ↑x ↔ x✝ ∈ x • ↑s

Tactic:
rw [orbitRel.Quotient.mem_orbit]

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x x✝ : α
⊢ Quotient.mk'' x✝ = ↑x ↔ x✝ ∈ x • ↑s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
b : ↥t
⊢ (fun a ↦ (Quotient.map' id ⋯ a, Quotient.map' (fun g ↦ ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a))
      ((fun a ↦ Quotient.map' (fun b ↦ f a.1 * ↑b) ⋯ a.2) (Quotient.mk'' a, Quotient.mk'' b)) =
    (Quotient.mk'' a, Quotient.mk'' b)

Tactic:
have key : Quotient.mk'' (f (Quotient.mk'' a) * b) = Quotient.mk'' a :=
      (QuotientGroup.mk_mul_of_mem (f a) b.2).trans (hf a)

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
b : ↥t
key : Quotient.mk'' (f (Quotient.mk'' a) * ↑b) = Quotient.mk'' a
⊢ (fun a ↦ (Quotient.map' id ⋯ a, Quotient.map' (fun g ↦ ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a))
      ((fun a ↦ Quotient.map' (fun b ↦ f a.1 * ↑b) ⋯ a.2) (Quotient.mk'' a, Quotient.mk'' b)) =
    (Quotient.mk'' a, Quotient.mk'' b)
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (j : Fin (n + 1)) → Group (α j)
i : Fin (n + 1)
x y : α i
p : (j : Fin n) → α (i.succAbove j)
⊢ i.insertNth (x / y) (p / p) = Pi.mulSingle i (x / y)

Tactic:
← insertNth_one_right,

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (j : Fin (n + 1)) → Group (α j)
i : Fin (n + 1)
x y : α i
p : (j : Fin n) → α (i.succAbove j)
⊢ i.insertNth (x / y) (p / p) = i.insertNth (x / y) 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.ncard = 1
hft : Fintype ↑s
⊢ ∃ a, s = {a}

Tactic:
simp_rw [ncard_eq_toFinset_card', @Finset.card_eq_one _ (toFinset s)] at h

Goal state after:
α : Type u_1
s : Set α
hft : Fintype ↑s
h : ∃ a, s.toFinset = {a}
⊢ ∃ a, s = {a}
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 : Submodule R M
⊢ map p.mkQ p = ⊥

Tactic:
rw [eq_bot_iff, map_le_iff_le_comap, comap_bot, ker_mkQ]

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
S : Type u_3
inst✝¹⁵ : Semiring R
inst✝¹⁴ : Semiring S
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M₃
inst✝¹⁰ : AddCommMonoid M₄
inst✝⁹ : AddCommMonoid M₅
inst✝⁸ : AddCommMonoid M₆
inst✝⁷ : Module R M
inst✝⁶ : Module R M₂
inst✝⁵ : Module R M₃
inst✝⁴ : Module R M₄
inst✝³ : Module R M₅
inst✝² : Module R M₆
f✝ : M →ₗ[R] M₂
inst✝¹ : Module S M₃
inst✝ : SMulCommClass R S M₃
f : M × M₂ →ₗ[R] M₃
⊢ (fun f ↦ f.1.coprod f.2) ((fun f ↦ (f ∘ₗ inl R M M₂, f ∘ₗ inr R M M₂)) f) = f

Tactic:
by simp only [← comp_coprod, comp_id, coprod_inl_inr]

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' : Submodule R M
H : p ≤ p'
x : M
⊢ (factor H ∘ₗ p.mkQ) x = p'.mkQ x

Tactic:
rw [LinearMap.comp_apply, factor_mk]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_3
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
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
⊢ (codRestrict (⨅ i ∈ J, (proj i).ker) (pi fun i ↦ if h : i ∈ I then proj ⟨i, h⟩ else 0) ⋯ ∘ₗ
      pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) =
    id

Tactic:
ext1 ⟨b, hb⟩

Goal state after:
case refine_3
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
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb : b ∈ ⨅ i ∈ J, (proj i).ker
⊢ (codRestrict (⨅ i ∈ J, (proj i).ker) (pi fun i ↦ if h : i ∈ I then proj ⟨i, h⟩ else 0) ⋯ ∘ₗ
        pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype)
      ⟨b, hb⟩ =
    id ⟨b, hb⟩
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
q : Submodule R M₂
⊢ map (snd R M M₂) (p.prod q) = q

Tactic:
ext x; simp [(⟨0, zero_mem _⟩ : ∃ x, x ∈ p)]

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

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
⊢ (∀ x ∈ Set.Ioc i j, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioc i j, x ≤ x_1) → x ≤ k

Tactic:
refine ⟨fun x hx ↦ h.1 x hx.1, fun x hx ↦ h.2 x ?_⟩

Goal state after:
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
⊢ ∀ x_1 ∈ Set.Ioi i, x ≤ x_1
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
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
⊢ pred^[(-toZ i0 i).toNat] i0 ≤ pred^[(-toZ i0 j).toNat] i0

Tactic:
refine Monotone.antitone_iterate_of_map_le pred_mono (pred_le _) (Int.toNat_le_toNat ?_)

Goal state after:
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
⊢ -toZ i0 j ≤ -toZ i0 i
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
h2 : q * (p * q) = p * q
⊢ Commute p q

Tactic:
← mul_assoc

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
h1 : q * p * q = q * p
h2 : q * p * q = p * q
⊢ Commute p q
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ I ≠ ⊤ ↔ ∃ M, M.IsMaximal ∧ I ≤ M

Tactic:
by
  refine ⟨exists_le_maximal I, ?_⟩
  contrapose!
  rintro rfl _ hMmax
  rw [top_le_iff]
  exact IsMaximal.ne_top hMmax

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

Goal state before:
pp: case refine_1.inl
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
c : Set (Ideal α)
hc : c ⊆ {p | Disjoint ↑p ↑S}
hc' : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
x : Ideal α
hx : x ∈ c
h✝ : IsEmpty ↑c
⊢ ∃ ub ∈ {p | Disjoint ↑p ↑S}, ∀ z ∈ c, z ≤ ub

Tactic:
exact ⟨I, disjoint, fun J hJ ↦ isEmptyElim (⟨J, hJ⟩ : c)⟩

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

Goal state before:
pp: n : ℕ
h : ¬n = 0
⊢ ∑ i ∈ range (n + 1), (n - i) * n.choose i + ∑ i ∈ range (n + 1), i * n.choose i = ∑ i ∈ range (n + 1), n * n.choose i

Tactic:
by
      rw [← sum_add_distrib]
      congr! 1 with _ h'
      rw [← add_mul, Nat.sub_add_cancel (mem_range_succ_iff.mp h')]

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

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) =
    a ^ (n + 1) * (a ^ (c - (n + 1)) * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c)) + 0

Tactic:
← mul_assoc

Goal state after:
case pos
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) =
    a ^ (n + 1) * a ^ (c - (n + 1)) * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) + 0
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case right
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
⊢ x ∉ I → x ∈ J → 1 ∈ J

Tactic:
hxnI

Goal state after:
case right
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : x ∉ I
⊢ x ∈ J → 1 ∈ J
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case h
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : c ≤ n
this : (s.card + 1) * n + 1 - c = s.card * n + 1 + (n - c)
⊢ a ^ c * (s.sum ^ (n - c) * ↑(((s.card + 1) * n + 1).choose c) * s.sum ^ (s.card * n + 1)) ∈
    span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset

Tactic:
← mul_assoc

Goal state after:
case h
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : c ≤ n
this : (s.card + 1) * n + 1 - c = s.card * n + 1 + (n - c)
⊢ a ^ c * s.sum ^ (n - c) * ↑(((s.card + 1) * n + 1).choose c) * s.sum ^ (s.card * n + 1) ∈
    span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
⊢ x ∈ (mapRange.linearMap f).range → x ∈ submodule fun x ↦ f.range

Tactic:
rintro ⟨y, hy⟩
    simp [← hy]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : α → β
f : Filter α
g : Filter β
i : γ → α
h : range i ∈ f
⊢ (map m ∘ map i) (comap i f) ≤ g ↔ Tendsto m f g

Tactic:
simp only [(· ∘ ·), map_comap_of_mem h, Tendsto]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter (α ⊕ β)
⊢ map inl (comap inl l) ⊔ map inr (comap inr l) = l

Tactic:
rw [← comap_sumElim_eq, Sum.elim_inl_inr, comap_id]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
⊢ MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 t)) ↔ MapsTo m s t

Tactic:
map_mapsTo_Iic_iff_tendsto,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
⊢ Tendsto m (𝓟 s) (𝓟 t) ↔ MapsTo m s t
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
⊢ (comap Prod.snd f).NeBot ↔ Nonempty α ∧ f.NeBot

Tactic:
rcases isEmpty_or_nonempty α with hα | hα
  · rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]; simp
  · simp [comap_neBot_iff_frequently, hα]

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

Goal state before:
pp: α : Type u_3
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : NoMaxOrder α
a : α
this : Nonempty α
⊢ atTop.HasBasis (fun x ↦ a < x) Ioi

Tactic:
refine atTop_basis_Ioi.to_hasBasis (fun b _ ↦ ?_) fun b _ ↦ ⟨b, trivial, Subset.rfl⟩

Goal state after:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : NoMaxOrder α
a : α
this : Nonempty α
b : α
x✝ : True
⊢ ∃ i', a < i' ∧ Ioi i' ⊆ Ioi b
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
⊢ atTop = comap Subtype.val atTop

Tactic:
by
  rcases isEmpty_or_nonempty (Ioi a) with h | ⟨⟨b, hb⟩⟩
  · subsingleton
  · rw [← map_val_atTop_of_Ici_subset (Ici_subset_Ioi.2 hb), comap_map Subtype.coe_injective]

Goal state after:
Module: Mathlib.Algebra.Module.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring R
e✝ e : α ≃ β
inst✝¹ : AddCommMonoid β
inst✝ : Module R β
this : AddCommMonoid α := e.addCommMonoid
module : Module R α := Equiv.module R e
r : R
x : α
⊢ e.addEquiv.toFun (r • x) = (RingHom.id R) r • e.addEquiv.toFun x

Tactic:
apply e.symm.injective

Goal state after:
R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring R
e✝ e : α ≃ β
inst✝¹ : AddCommMonoid β
inst✝ : Module R β
this : AddCommMonoid α := ⋯
module : Module R α := ⋯
r : R
x : α
⊢ e.symm (e.addEquiv.toFun (r • x)) = e.symm ((RingHom.id R) r • e.addEquiv.toFun x)
Module: Mathlib.Algebra.Module.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : Semiring R
A : Type ?u.8
inst✝⁴ : Semiring A
inst✝³ : Module R A
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
inst✝ : Module A β
e : α ≃+ β
⊢ ∀ (x y : A) (b : α), (x * y) • b = x • y • b

Tactic:
by simp [Equiv.smul_def, mul_smul]

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : ⋃ i ∈ s, Iio i = univ
⊢ IsCofinal s

Tactic:
by
    rw [isCofinal_iff_iUnion_Iic_eq_univ, ← univ_subset_iff, ← hs]
    gcongr
    exact Iio_subset_Iic_self

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

Goal state before:
pp: α : Type u
inst✝ : Preorder α
c : Cardinal.{max u v}
⊢ c ≤ lift.{v, u} (cof α) ↔ ∀ (s : Set α), IsCofinal s → c ≤ lift.{v, u} #↑s

Tactic:
rw [cof, lift_iInf, le_ciInf_iff']
  simp

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b✝ b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosReflectLT α β
inst✝ : SMulPosReflectLT α γ
b : β × γ
hb : 0 ≤ b
_a₁ _a₂ : α
h₁ : (_a₁ • b).1 < (_a₂ • b).1
h₂ : (_a₁ • b).2 ≤ (_a₂ • b).2
⊢ _a₁ < _a₂

pp: case inr
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b✝ b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosReflectLT α β
inst✝ : SMulPosReflectLT α γ
b : β × γ
hb : 0 ≤ b
_a₁ _a₂ : α
h₁ : (_a₁ • b).1 ≤ (_a₂ • b).1
h₂ : (_a₁ • b).2 < (_a₂ • b).2
⊢ _a₁ < _a₂

Tactic:
· exact lt_of_smul_lt_smul_right h₁ hb.1

Goal state after:
case inr
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b✝ b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosReflectLT α β
inst✝ : SMulPosReflectLT α γ
b : β × γ
hb : 0 ≤ b
_a₁ _a₂ : α
h₁ : (_a₁ • b).1 ≤ (_a₂ • b).1
h₂ : (_a₁ • b).2 < (_a₂ • b).2
⊢ _a₁ < _a₂