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

Goal state before:
pp: case refine_1
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
x✝ : ∃ c, ∑ i, c i • v ↑i = x
c : ↥s → R
hc : ∑ i, c i • v ↑i = x
⊢ ∃ c, ∑ i ∈ s, c i • v i = x

Tactic:
refine ⟨fun i ↦ if h : i ∈ s then c ⟨i, h⟩ else 0, ?_⟩

Goal state after:
case refine_1
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
x✝ : ∃ c, ∑ i, c i • v ↑i = x
c : ↥s → R
hc : ∑ i, c i • v ↑i = x
⊢ ∑ i ∈ s, (fun i ↦ if h : i ∈ s then c ⟨i, h⟩ else 0) i • v i = x
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
x y : α
u : Fin 0 → α
⊢ {x} ∪ Set.range (vecCons y u) = {x, y}

Tactic:
range_cons_empty,

Goal state after:
α : Type u
x y : α
u : Fin 0 → α
⊢ {x} ∪ {y} = {x, y}
Module: Mathlib.Algebra.BigOperators.Finprod

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

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

Tactic:
· exact mul_finsum' f r h

Goal state after:
case neg
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : ¬(support f).Finite
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
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✝ : Fintype ι
⊢ ¬LinearIndependent R v ↔ ∃ f g, ∑ i, f i • v i = ∑ i, g i • v i ∧ ∃ i, f i ≠ g i

Tactic:
by
  simpa using not_iff_not.2 Fintype.linearIndependent_iffₛ

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a : Fin n
⊢ ∏ i ≤ Fin.cast h a, f i = ∏ i ≤ a, f (Fin.cast h i)

Tactic:
simp [← map_finCongr_Iic]

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 ∈ Ioc a.castSucc b.castSucc, f i = ∏ i ∈ Ioc a b, f i.castSucc

Tactic:
simp [← map_castSuccEmb_Ioc]

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

Tactic:
rintro ⟨k, hk⟩

Goal state after:
case mp
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ ∃ i, i < n ∧ ∃ m, a - b = (m * ↑n + ↑i) • p
Module: Mathlib.Algebra.BigOperators.Fin

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

Tactic:
simp only [Finset.prod_mul_distrib]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
x : ↥(span R (range v))
hx : ↑x = v i
⊢ (Finsupp.linearCombination R v) (Finsupp.single i 1) = ↑x

Tactic:
simp [Finsupp.linearCombination_single, hx]

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c d : ℕ
h : c ≤ a ↔ d ≤ b
hab : a ≡ b [MOD n]
hcd : c ≡ d [MOD n]
⊢ a - c ≡ b - d [MOD n]

Tactic:
by
  obtain hac | hca := lt_or_ge a c
  · rw [Nat.sub_eq_zero_of_le hac.le, Nat.sub_eq_zero_of_le ((lt_iff_lt_of_le_iff_le h).1 hac).le]
  rw [modEq_iff_dvd, Int.natCast_sub hca, Int.natCast_sub <| h.1 hca, sub_sub_sub_comm]
  exact Int.dvd_sub hab.dvd hcd.dvd

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n a✝ b✝ c d : ℕ
co : n.Coprime m
a b : ℕ
⊢ a ≡ b [MOD n.gcd m]

Tactic:
by convert! @modEq_one a b

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

Goal state before:
pp: case succ
m : ℕ
ih : ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
⊢ ↑(finSigmaFinEquiv ⟨⟨iv, hi⟩, j⟩) = ∑ i, n (Fin.castLE ⋯ i) + ↑⟨⟨iv, hi⟩, j⟩.snd

Tactic:
rw [finSigmaFinEquiv]

Goal state after:
case succ
m : ℕ
ih : ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
⊢ ↑((Trans.trans
          (Trans.trans
            (Trans.trans
              (Trans.trans finSumFinEquiv.sigmaCongrLeft.symm
                (Equiv.sumSigmaDistrib fun a ↦ Fin (n (finSumFinEquiv a))))
              (finSigmaFinEquiv.sumCongr (Equiv.uniqueSigma fun i ↦ Fin (n (finSumFinEquiv (Sum.inr i))))))
            finSumFinEquiv)
          (finCongr ⋯))
        ⟨⟨iv, hi⟩, j⟩) =
    ∑ i, n (Fin.castLE ⋯ i) + ↑⟨⟨iv, hi⟩, j⟩.snd
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j with ↑j < i, f j
h : ¬i < (ofFn f).length
⊢ take i (ofFn f) = take i.succ (ofFn f)

Tactic:
have : length (ofFn f) ≤ i := not_lt.mp h

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j with ↑j < i, f j
h : ¬i < (ofFn f).length
this : (ofFn f).length ≤ i
⊢ take i (ofFn f) = take i.succ (ofFn f)
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj : Disjoint (span R (v '' s)) (span R (v '' t))
a✝ : Nontrivial R
⊢ Disjoint (span R (range fun x ↦ v ↑x)) (span R (range fun x ↦ v ↑x))

Tactic:
by rwa [← image_eq_range, ← image_eq_range]

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

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

Tactic:
by
        congrm ∑ i ∈ insert a s, ?_ - ∑ i ∈ insert a s, ?_
        · rw [mul_assoc]
        · rw [mul_assoc, mul_left_comm]

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

Goal state before:
pp: case h₁
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
⊢ ∀ (i : { s // LinearIndepOn R id s }), #↑↑i ≤ 1

pp: case h₂
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
⊢ ∀ w < 1, ∃ i, w < #↑↑i

Tactic:
· have := Module.subsingleton R M
    simp [Set.subsingleton_of_subsingleton]

Goal state after:
case h₂
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
⊢ ∀ w < 1, ∃ i, w < #↑↑i
Module: Mathlib.Algebra.EuclideanDomain.Int

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ a.natAbs ≤ (a * b).natAbs

Tactic:
rw [← mul_one a.natAbs, Int.natAbs_mul]

Goal state after:
a b : ℤ
b0 : b ≠ 0
⊢ a.natAbs * 1 ≤ a.natAbs * b.natAbs
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : (s ∩ t).Finite
⊢ s.encard ≤ t.encard ↔ (s \ t).encard ≤ (t \ s).encard

Tactic:
by
  rw [← encard_sdiff_add_encard_inter s t, ← encard_sdiff_add_encard_inter t s, inter_comm t s,
    ENat.add_le_add_iff_right h.encard_lt_top.ne]

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
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
f g : ι → R
⊢ ∑ i ∈ s, f i • v i - ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, f i = g i

Tactic:
← Finset.sum_sub_distrib

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
f g : ι → R
⊢ ∑ x ∈ s, (f x • v x - g x • v x) = 0 → ∀ i ∈ s, f i = g i
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
hfin : s.Finite
h : s.ncard ≤ k
⊢ s.encard = ↑s.ncard

Tactic:
by rw [hfin.cast_ncard_eq]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ ∑ x ∈ (b.repr c).support, ∑ x_1 ∈ (b.repr d).support, (b.repr c) x • (b.repr d) x_1 • (z * (b x * b x_1)) =
    ∑ x ∈ (b.repr d).support, ∑ x_1 ∈ (b.repr c).support, (b.repr d) x • (b.repr c) x_1 • (z * b x_1 * b x)

Tactic:
(h.2 _ _).1,

Goal state after:
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ ∑ x ∈ (b.repr c).support, ∑ x_1 ∈ (b.repr d).support, (b.repr c) x • (b.repr d) x_1 • (z * b x * b x_1) =
    ∑ x ∈ (b.repr d).support, ∑ x_1 ∈ (b.repr c).support, (b.repr d) x • (b.repr c) x_1 • (z * b x_1 * b x)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard

Tactic:
by
  obtain (h | h) := (s ∪ t).finite_or_infinite
  · to_encard_tac
    rw [h.cast_ncard_eq, (h.subset subset_union_left).cast_ncard_eq,
      (h.subset subset_union_right).cast_ncard_eq]
    apply encard_union_le
  rw [h.ncard]
  apply zero_le

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

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n ≤ t.ncard
ht : t.Infinite
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

pp: case inr
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n ≤ t.ncard
ht : t.Finite
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Tactic:
· rw [ht.ncard, Nat.le_zero, ← ht.ncard] at hnt
    exact ⟨t, hst, Subset.rfl, hnt.symm⟩

Goal state after:
case inr
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n ≤ t.ncard
ht : t.Finite
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr
α : Type u_1
t : Set α
n : ℕ
hnt : n ≤ t.ncard
ht : t.Finite
s : Finset α
hst : ↑s ⊆ t
hsn : (↑s).ncard ≤ n
⊢ ∃ u, ↑s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Tactic:
lift t to Finset α using ht

Goal state after:
case inr
α : Type u_1
n : ℕ
s : Finset α
hsn : (↑s).ncard ≤ n
t : Finset α
hnt : n ≤ (↑t).ncard
hst : ↑s ⊆ ↑t
⊢ ∃ u, ↑s ⊆ u ∧ u ⊆ ↑t ∧ u.ncard = n
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrder α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Icc (a + 1) b = Ioc a b

Tactic:
by
  simpa [succ_eq_add_one] using Icc_succ_left_eq_Ioc a b

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
ι : Type v
inst✝² : Finite ι
motive : (N : Type u) → [inst : AddCommMonoid N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommMonoid N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
h : ∀ (i : ι), motive (M i)
⊢ motive' ((i : ι) → M i)

Tactic:
cases nonempty_fintype ι
  revert M
  refine Fintype.induction_empty_option
    (fun α β _ e h M _ _ hM ↦ equiv' (LinearEquiv.piCongrLeft R M e) <| h _ fun i ↦ hM _)
    (fun M _ _ _ ↦ equiv default unit) (fun α _ h M _ _ hn ↦ ?_) ι
  exact equiv' (LinearEquiv.piOptionEquivProd R).symm <| prod (hn _) (h _ fun i ↦ hn i)

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: ι : Type v
inst✝³ : Finite ι
R : Type u_1
inst✝² : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
h : ∀ (i : ι), motive (M i)
⊢ motive' ((i : ι) → M i)

Tactic:
cases nonempty_fintype ι
  revert M
  refine Fintype.induction_empty_option
    (fun α β _ e h M _ _ hM ↦ equiv' (LinearEquiv.piCongrLeft R M e) <| h _ fun i ↦ hM _)
    (fun M _ _ _ ↦ equiv default unit) (fun α _ h M _ _ hn ↦ ?_) ι
  exact equiv' (LinearEquiv.piOptionEquivProd R).symm <| prod (hn _) (h _ fun i ↦ hn i)

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp.left
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 (inl R M M₂) p₁ ≤ q

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 ⟨hx, zero_mem p₂⟩

Goal state after:
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
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
⊢ (f.prod g).range = f.range.prod g.range

Tactic:
refine le_antisymm (f.range_prod_le g) ?_
  simp only [SetLike.le_def, prod_apply, mem_range, mem_prod, exists_imp, and_imp,
    Prod.forall, Function.prod_apply]
  rintro _ _ x rfl y rfl
  -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specify `(f := f)`
  simp only [Prod.mk_inj, ← sub_mem_ker_iff (f := f)]
  have : y - x ∈ ker f ⊔ ker g := by simp only [h, mem_top]
  rcases mem_sup.1 this with ⟨x', hx', y', hy', H⟩
  refine ⟨x' + x, ?_, ?_⟩
  · rwa [add_sub_cancel_right]
  · simp [← eq_sub_iff_add_eq.1 H, map_add, mem_ker.mp hy']

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 : IsGLB (Set.Ioi i) k
⊢ IsGLB (Set.Ioc i j) k

Tactic:
simp_rw [IsGLB, IsGreatest, mem_upperBounds, mem_lowerBounds] at h ⊢
  refine ⟨fun x hx ↦ h.1 x hx.1, fun x hx ↦ h.2 x ?_⟩
  intro y hy
  rcases le_or_gt y j with h_le | h_lt
  · exact hx y ⟨hy, h_le⟩
  · exact le_trans (hx j ⟨hij_lt, le_rfl⟩) h_lt.le

Goal state after:
Module: Mathlib.Data.List.NatAntidiagonal

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

Tactic:
by
  simp only [antidiagonal, range_succ_eq_map, map_cons, Nat.add_succ_sub_one,
    Nat.add_zero, id, Nat.sub_zero, map_map, Prod.map_apply]
  apply congr rfl (congr rfl _)
  ext; simp

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

Goal state before:
pp: α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d = (a - b) * c + b * (c - d)

Tactic:
rw [sub_mul, mul_sub]

Goal state after:
α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d = a * c - b * c + (b * c - b * d)
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
n : ℕ
⊢ (x - y) ^ n = ∑ m ∈ range (n + 1), (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)

Tactic:
rw [sub_eq_add_neg, add_pow]

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
n : ℕ
⊢ ∑ m ∈ range (n + 1), x ^ m * (-y) ^ (n - m) * ↑(n.choose m) =
    ∑ m ∈ range (n + 1), (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)
Module: Mathlib.RingTheory.Ideal.Span

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

Tactic:
span_pair_right_mul_add

Goal state after:
α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, y} = span {x, y}
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:
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.Data.Nat.Choose.Sum

Goal state before:
pp: n k : ℕ
⊢ ∑ i ∈ range (n + 1), k.multichoose i = (n + k).choose k

Tactic:
by
  cases k with
  | zero => simp [Finset.sum_range_succ']
  | succ k => grind [multichoose_eq, choose_symm_of_eq_add, sum_range_add_choose]

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

Goal state before:
pp: α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ↑s → ℕ
⊢ span (range fun x ↦ ↑x ^ n x) = ⊤

Tactic:
have ⟨t, hts, mem⟩ := Submodule.mem_span_finite_of_mem_span ((eq_top_iff_one _).mp hs)

Goal state after:
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ↑s → ℕ
t : Finset α
hts : ↑t ⊆ s
mem : 1 ∈ Submodule.span α ↑t
⊢ span (range fun x ↦ ↑x ^ n x) = ⊤
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CommSemiring α
ι : Type u_5
f : ι → α
s : Finset ι
I : Ideal α
i : ι
hi : i ∈ s
hfi : f i ∈ I
⊢ ∏ i ∈ s, f i ∈ I

Tactic:
classical
  rw [Finset.prod_eq_prod_sdiff_singleton_mul hi]
  exact Ideal.mul_mem_left _ _ hfi

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_5
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ f ⋯.choose y = Pi.single x 1 y

pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_5
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ 0 • ⋯.choose = 0

Tactic:
(s (Finsupp.single x 1)).choose_spec,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_5
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ (Finsupp.single x 1) y = Pi.single x 1 y

R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_5
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ 0 • ⋯.choose = 0
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: M : Type u_5
inst✝³ : AddCommMonoid M
X : Type u_6
Y : Type u_7
Z : Type u_8
inst✝² : Finite X
inst✝¹ : Finite Y
inst✝ : Finite Z
g : Y → Z
f : X → Y
⊢ map (g ∘ f) = map g ∘ map f

Tactic:
by
  ext s
  simp [map, Finsupp.mapDomain_comp]

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

Goal state before:
pp: α : Type u
f : Filter α
p : α → Prop
h : ∀ (s : Set α), ∀ᶠ (x : α) in f, x ∈ s → p x
⊢ ∀ᶠ (x : α) in f, p x

Tactic:
filter_upwards [h univ] with _ pa using pa (by simp)

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

Goal state before:
pp: α : Type u_6
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
⊢ 𝓟 {⊤} = pure ⊤

Tactic:
principal_singleton

Goal state after:
α : Type u_6
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
⊢ pure ⊤ = pure ⊤
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : α → Filter β
s✝ s : Set β
⊢ (s ∈ f.bind fun x ↦ g x ⊓ 𝓟 s✝) ↔ s ∈ f.bind g ⊓ 𝓟 s✝

Tactic:
by simp only [mem_bind, mem_inf_principal]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: case mp.a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
s'' : Finset M
hs'' : span R ↑s'' = span R s
s' : Finset M
hs's : ↑s' ⊆ s
hss' : ↑s'' ⊆ ↑(span R ↑s')
⊢ span R s ≤ span R ↑s'

pp: case a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
s'' : Finset M
hs'' : span R ↑s'' = span R s
s' : Finset M
hs's : ↑s' ⊆ s
hss' : ↑s'' ⊆ ↑(span R ↑s')
⊢ span R ↑s' ≤ span R s

Tactic:
· rwa [← hs'', span_le]

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
s'' : Finset M
hs'' : span R ↑s'' = span R s
s' : Finset M
hs's : ↑s' ⊆ s
hss' : ↑s'' ⊆ ↑(span R ↑s')
⊢ span R ↑s' ≤ span R s
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: case refine_1
α : Type u
inst✝ : Preorder α
h : cof α = 1
⊢ ∃ x, IsTop x

Tactic:
obtain ⟨s, hs, hs'⟩ := exists_cof_eq α
    rw [h, mk_set_eq_one_iff] at hs'
    obtain ⟨t, rfl⟩ := hs'
    use t
    rwa [isCofinal_singleton_iff] at hs

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
⊢ s.FG ↔ IsCompactElement s

Tactic:
have supr_rw : ∀ t : Finset M, ⨆ x ∈ t, sp x = ⨆ x ∈ (↑t : Set M), sp x := fun t => by rfl

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
⊢ s.FG ↔ IsCompactElement s
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulReflectLE α β
h : -a • b₂ ≤ -a • b₁
ha : a < 0
⊢ b₂ ≤ b₁

Tactic:
exact le_of_smul_le_smul_of_pos_left h <| neg_pos.2 ha

Goal state after: