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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
hv : LinearIndependent R v
w : ι → Rˣ
⊢ LinearIndependent R (w • v)

Tactic:
rw [linearIndependent_iff''ₛ] at hv ⊢

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
w : ι → Rˣ
⊢ ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • (w • v) i = ∑ i ∈ s, g i • (w • v) i → ∀ (i : ι), f i = g i
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr
a b c : ℕ
hb : b > 0
⊢ (a ^ b - 1).gcd (a ^ c - 1) = a ^ b.gcd c - 1

Tactic:
replace hb : c % b < b := mod_lt c hb

Goal state after:
case inr
a b c : ℕ
hb : c % b < b
⊢ (a ^ b - 1).gcd (a ^ c - 1) = a ^ b.gcd c - 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
⊢ (m + n).Coprime m ↔ n.Coprime m

Tactic:
rw [Coprime, Coprime, gcd_self_add_left]

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

Goal state before:
pp: n a b c : ℕ
h : a ≡ b [MOD n]
⊢ a * c ≡ b * c [MOD n * c]

Tactic:
by
  rw [mul_comm a, mul_comm b, mul_comm n]; exact h.mul_left' c

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

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
⊢ Surjective ⇑f

Tactic:
by
  intro i
  let repr : (span R (range (v ∘ f)) : Type _) → ι' →₀ R := (hv.comp f f.injective).repr
  let l := (repr ⟨v i, hss (mem_range_self i)⟩).mapDomain f
  have h_total_l : Finsupp.linearCombination R v l = v i := by
    dsimp only [l]
    rw [Finsupp.linearCombination_mapDomain]
    rw [(hv.comp f f.injective).linearCombination_repr]
  have h_total_eq : Finsupp.linearCombination R v l = Finsupp.linearCombination R v
       (Finsupp.single i 1) := by
    rw [h_total_l, Finsupp.linearCombination_single, one_smul]
  have l_eq : l = _ := hv h_total_eq
  dsimp only [l] at l_eq
  rw [← Finsupp.embDomain_eq_mapDomain] at l_eq
  rcases Finsupp.single_of_embDomain_single (repr ⟨v i, _⟩) f i (1 : R) zero_ne_one.symm l_eq with
    ⟨i', hi'⟩
  use i'
  exact hi'.2

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

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

Tactic:
by
    refine hlr _ (sum_mem fun i _ => ?_) _ (neg_mem <| sum_mem fun i _ => ?_) this
    · exact smul_mem _ _ (subset_span ⟨Sum.inl i, mem_range_self _, rfl⟩)
    · exact smul_mem _ _ (subset_span ⟨Sum.inr i, mem_range_self _, rfl⟩)

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

Goal state before:
pp: case neg
a b c : ℕ
h : ¬c = 0
⊢ (a + b) / c ≤ a / c + b / c + 1

Tactic:
· rw [Nat.add_div (Nat.pos_of_ne_zero h), Nat.add_le_add_iff_left]
    split <;> decide

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

Goal state before:
pp: n : ℕ
⊢ n % 4 = 1 → n % 2 = 1

Tactic:
by
  simpa [ModEq] using @ModEq.of_mul_left 2 n 1 2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
this✝ : Fintype α
this : Fintype β
⊢ Bijective f ↔ Nat.card α = Nat.card β ∧ Surjective f

Tactic:
← and_comm,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
this✝ : Fintype α
this : Fintype β
⊢ Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β
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
hli : LinearIndependent R (Sum.elim (fun x ↦ v ↑x) fun x ↦ v ↑x)
⊢ LinearIndepOn R v (s ∪ t)

Tactic:
have hdj := (hdj.of_span₀ hs.zero_notMem_image).of_image

Goal state after:
ι : 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
hli : LinearIndependent R (Sum.elim (fun x ↦ v ↑x) fun x ↦ v ↑x)
hdj : Disjoint s t
⊢ LinearIndepOn R v (s ∪ t)
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : lift.{w, v} (Module.rank R M) ≤ lift.{v, w} (Module.rank R N)
h' : Module.rank R N < ℵ₀
⊢ finrank R M ≤ finrank R N

Tactic:
by
  simpa only [toNat_lift] using! toNat_le_toNat h (lift_lt_aleph0.mpr h')

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s t r' s' t' : R
⊢ xgcdAux 0 s t r' s' t' = (r', s', t')

Tactic:
unfold xgcdAux
  exact if_pos rfl

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

Goal state before:
pp: α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
⊢ s = t

Tactic:
have hdiff :=
    (ENat.addLECancellable_of_lt_top (ht.subset hst).encard_lt_top).add_le_add_iff_right.mp hts

Goal state after:
α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
hdiff : (t \ s).encard ≤ 0
⊢ s = t
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
⊢ s.ncard = n

Tactic:
by
  let f' : Fin n → α := fun i ↦ f i.val i.is_lt
  suffices himage : s = f' '' Set.univ by
    rw [← Fintype.card_fin n, ← Nat.card_eq_fintype_card, ← Set.ncard_univ, himage]
    exact InjOn.ncard_image <| fun i _hi j _hj h ↦ Fin.ext <| f_inj i.val j.val i.is_lt j.is_lt h
  ext x
  simp only [image_univ, mem_range]
  refine ⟨fun hx ↦ ?_, fun ⟨⟨i, hi⟩, hx⟩ ↦ hx ▸ hf' i hi⟩
  obtain ⟨i, hi, rfl⟩ := hf x hx
  use ⟨i, hi⟩

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 * x⁻¹ ∈ s ↔ z * y⁻¹ ∈ s

Tactic:
← inv_mul_cancel_left y x⁻¹

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: M : Type u_7
R : Type u_8
inst✝⁴ : Ring R
inst✝³ : Nontrivial R
inst✝² : IsAddTorsionFree R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : AddSubgroup M
ι : Type u_9
b : Basis ι R M
h : A = AddSubgroup.closure (range ⇑b)
x : ↥A
i : ι
⊢ ↑(((addSubgroupOfClosure A b h).repr x) i) = (b.repr ↑x) i

Tactic:
suffices Finsupp.mapRange.linearMap (Algebra.linearMap ℤ R) ∘ₗ
      (b.addSubgroupOfClosure A h).repr.toLinearMap =
        ((b.repr : M →ₗ[R] ι →₀ R).restrictScalars ℤ).domRestrict A.toIntSubmodule by
    exact DFunLike.congr_fun (LinearMap.congr_fun this x) i

Goal state after:
M : Type u_7
R : Type u_8
inst✝⁴ : Ring R
inst✝³ : Nontrivial R
inst✝² : IsAddTorsionFree R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : AddSubgroup M
ι : Type u_9
b : Basis ι R M
h : A = AddSubgroup.closure (range ⇑b)
x : ↥A
i : ι
⊢ mapRange.linearMap (Algebra.linearMap ℤ R) ∘ₗ ↑(addSubgroupOfClosure A b h).repr =
    (↑ℤ ↑b.repr).domRestrict (AddSubgroup.toIntSubmodule A)
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
⊢ rightRel (s.prod s') = (rightRel s).prod (rightRel s')

Tactic:
by
  refine Setoid.ext fun x y ↦ ?_
  rw [Setoid.prod_apply]
  simp_rw [rightRel_apply]
  rfl

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
n : ℕ
⊢ {t | t ⊆ s ∧ t.ncard = n}.ncard = s.ncard.choose n

Tactic:
lift s to Finset α using hs
  have h₁ : {t ⊆ (s : Set α) | t.ncard = n} ⊆ range ((↑) : Finset α → Set α) := by
    intro t ht
    rw [Finset.mem_range_coe_iff]
    exact s.finite_toSet.subset ht.1
  have h₂ : (↑) ⁻¹' {t ⊆ (s : Set α) | t.ncard = n} = (s.powersetCard n : Set (Finset α)) := by
    ext t
    simp
  grind [ncard_coe_finset, ncard_preimage_of_injective_subset_range, Finset.card_powersetCard]

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

Goal state before:
pp: G : Type u
inst✝ : Group G
H : Subgroup G
h : Subsingleton (G ⧸ H)
x : G
x✝ : x ∈ ⊤
this : 1 * x ∈ H
⊢ x ∈ H

Tactic:
one_mul

Goal state after:
G : Type u
inst✝ : Group G
H : Subgroup G
h : Subsingleton (G ⧸ H)
x : G
x✝ : x ∈ ⊤
this : x ∈ H
⊢ x ∈ H
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y : M
f✝ f : M →* P
g : P → M
hf : RightInverse g ⇑f
x : P
⊢ (kerLift f) ((toQuotient ∘ g) x) = x

Tactic:
conv_rhs => rw [← hf x]

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y : M
f✝ f : M →* P
g : P → M
hf : RightInverse g ⇑f
x : P
⊢ (kerLift f) ((toQuotient ∘ g) x) = f (g x)
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
⊢ 1 * z = z

Tactic:
one_mul

Goal state after:
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
⊢ z = z
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
⊢ Ici (succ a) = Ioi a

Tactic:
by
  ext x; rw [mem_Ici, mem_Ioi, succ_le_iff_of_not_isMax ha]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' p'' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q✝ : Submodule R₂ M₂
x✝ : ↑(Set.Ici p)
q : Submodule R M
hq : q ∈ Set.Ici p
⊢ ↑((fun p' ↦ ⟨comap p.mkQ p', ⋯⟩) ((fun q ↦ map p.mkQ ↑q) ⟨q, hq⟩)) = ↑⟨q, hq⟩

Tactic:
by simpa [comap_map_mkQ p]

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₂
⊢ map (fst R M M₂) ⊤ = ⊤

Tactic:
← prod_top,

Goal state after:
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₂
⊢ map (fst R M M₂) (⊤.prod ⊤) = ⊤
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₂
⊢ map (snd R M M₂) ⊤ = ⊤

Tactic:
← prod_top,

Goal state after:
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₂
⊢ map (snd R M M₂) (⊤.prod ⊤) = ⊤
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 ≤ b
⊢ insert b (Icc a (b - 1)) = Icc a b

Tactic:
simpa [pred_eq_sub_one] using insert_Icc_pred_right_eq_Icc h

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

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ succ^[(↑(Nat.find ⋯)).toNat] i0 = i

Tactic:
Int.toNat_natCast

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ succ^[Nat.find ⋯] i0 = i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ pred^[(↑(Nat.find ⋯)).toNat] i0 = i

Tactic:
Int.toNat_natCast

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ pred^[Nat.find ⋯] i0 = i
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case e_a.e_s
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
m : ι
⊢ m ∈ Iio (succ i) ↔ m ∈ Iic i

Tactic:
simpa only [mem_Iio, mem_Iic] using lt_succ_iff_of_not_isMax hi

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

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
⊢ Countable ι

Tactic:
by
  rcases isEmpty_or_nonempty ι with _ | hι
  · infer_instance
  · exact Countable.of_equiv _ orderIsoRangeToZOfLinearSuccPredArch.symm.toEquiv

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
y' : α
hy' : y' * y = 1
this : 1 * x ∈ I
⊢ x ∈ I

Tactic:
one_mul

Goal state after:
α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
y' : α
hy' : y' * y = 1
this : x ∈ I
⊢ x ∈ I
Module: Mathlib.RingTheory.Ideal.Defs

Goal state before:
pp: α : Type u
β : Type v
F : Type w
R : Type ?u.7
M : Type ?u.9
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m m' : M
a✝ b✝ : R
h : a✝ ∈ {r | r • m = r • m'}
h' : b✝ ∈ {r | r • m = r • m'}
⊢ a✝ + b✝ ∈ {r | r • m = r • m'}

Tactic:
simpa [add_smul] using congr($h + $h')

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

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y x✝¹ : α
x✝ : ∃ a b, a * (x + y) + b * y = x✝¹
a b : α
h : a * (x + y) + b * y = x✝¹
⊢ a * x + (b + a) * y = x✝¹

Tactic:
rw [add_comm b, add_mul, ← add_assoc, ← mul_add, h]

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

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

Tactic:
rw [add_comm, span_pair_add_left]

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

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

Tactic:
← sum_Icc_choose,

Goal state after:
n k : ℕ
⊢ ∑ i ∈ range (n + 1), (i + k).choose k = ∑ m ∈ Icc k (n + k), m.choose k
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x y : R
⊢ (mk I) x = (mk I) y ↔ x - y ∈ I

Tactic:
by
  rw [← eq_zero_iff_mem, map_sub, sub_eq_zero]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
x✝ : ∃ i, ∃ x_1 ∈ s, ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑⟨i, hi⟩ + a = x
⊢ a - x ∈ I

Tactic:
← Eq,

Goal state after:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
x✝ : ∃ i, ∃ x_1 ∈ s, ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑⟨i, hi⟩ + a = x
⊢ a - (↑⟨i, hi⟩ + a) ∈ I
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 + 1
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) ∈
    span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset

Tactic:
replace h : c ≤ n := Nat.lt_succ_iff.mp h

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
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) ∈
    span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
c : R ⧸ I
m : (ι → R) ⧸ pi fun x ↦ I
c₁ : R
m₁ : ι → R
c₂ : R
⊢ ∀ (b₂ : ι → R),
    (Submodule.quotientRel I) c₁ c₂ →
      (Submodule.quotientRel (pi fun x ↦ I)) m₁ b₂ → Submodule.Quotient.mk (c₁ • m₁) = Submodule.Quotient.mk (c₂ • b₂)

Tactic:
m₂

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
c : R ⧸ I
m : (ι → R) ⧸ pi fun x ↦ I
c₁ : R
m₁ : ι → R
c₂ : R
m₂ : ι → R
⊢ (Submodule.quotientRel I) c₁ c₂ →
    (Submodule.quotientRel (pi fun x ↦ I)) m₁ m₂ → Submodule.Quotient.mk (c₁ • m₁) = Submodule.Quotient.mk (c₂ • m₂)
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)
  refine top_unique ((span_pow_eq_top _ ((eq_top_iff_one _).mpr mem) <|
    t.attach.sup fun x ↦ n ⟨x, hts x.2⟩).ge.trans <| span_le.mpr ?_)
  rintro _ ⟨x, hxt, rfl⟩
  rw [← Nat.sub_add_cancel (Finset.le_sup <| t.mem_attach ⟨x, hxt⟩)]
  simp_rw [pow_add]
  exact mul_mem_left _ _ (subset_span ⟨_, rfl⟩)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
y a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
xy : a ∩ b ⊆ y
⊢ y = (a ∪ y) ∩ (b ∪ y)

Tactic:
← inter_union_distrib_right,

Goal state after:
α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
y a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
xy : a ∩ b ⊆ y
⊢ y = a ∩ b ∪ y
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: 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
I : Type u_6
x : I →₀ M
⊢ x ∈ (mapRange.linearMap f).ker ↔ x ∈ submodule fun x ↦ f.ker

Tactic:
simp [Finsupp.ext_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → β
s : Set α
hf : Injective m
h : m '' s ∈ map m f
⊢ s ∈ f

Tactic:
← preimage_image_eq s hf

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
s : Set α
hf : Injective m
h : m '' s ∈ map m f
⊢ m ⁻¹' m '' s ∈ f
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
h : IsGLB s a
x : α
hx : x ∈ Ioi a
⊢ x ∈ ⋃ i ∈ s, Ioi i

Tactic:
rcases h.exists_between hx with ⟨y, hys, _, hyx⟩
    exact mem_biUnion hys hyx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
s : Set α
g : Filter β
⊢ s ∈ comap m g ↔ kernImage m s ∈ g

Tactic:
mem_comap''

Goal state after:
α : Type u_1
β : Type u_2
m : α → β
s : Set α
g : Filter β
⊢ kernImage m s ∈ g ↔ kernImage m s ∈ g
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
s : Set α
⊢ 𝓟 s ⊓ 𝓟 sᶜ = ⊥

Tactic:
inf_principal,

Goal state after:
α : Type u
s : Set α
⊢ 𝓟 (s ∩ sᶜ) = ⊥
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
l : Filter α
p : α → Prop
⊢ (∃ᶠ (x : α) in l, p x) ↔ (l ⊓ 𝓟 {x | p x}).NeBot

Tactic:
rw [neBot_iff, Ne, inf_principal_eq_bot]; rfl

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : IsCofinal s
x y : α
hy : x < y
⊢ ∃ i ∈ s, x ∈ Iio i

Tactic:
obtain ⟨z, hz, hz'⟩ := hs y

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : IsCofinal s
x y : α
hy : x < y
z : α
hz : z ∈ s
hz' : y ≤ z
⊢ ∃ i ∈ s, x ∈ Iio i
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

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

Tactic:
apply le_antisymm
    · apply (cof_le (s := {t}) _).trans_eq (mk_singleton _)
      rwa [isCofinal_singleton_iff]
    · rw [Cardinal.one_le_iff_ne_zero, cof_ne_zero_iff]
      use t

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

Goal state before:
pp: A : Type u_5
M : Type u_6
inst✝⁶ : Semiring A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module A M
S : Submodule A M
R : Type u_7
inst✝³ : Semiring R
inst✝² : Module R M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
hS : (restrictScalars R S).FG
⊢ S.FG

Tactic:
obtain ⟨s, e⟩ := hS
  refine ⟨s, restrictScalars_injective R _ _ (le_antisymm ?_ ?_)⟩
  · have := span_le.mp e.le
    rwa [restrictScalars_le, span_le]
  · rw [← e]
    exact span_le_restrictScalars ..

Goal state after:
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✝ : PosSMulReflectLT α β
h : a • b₁ < a • b₂
ha : a ≤ 0
⊢ b₂ < b₁

Tactic:
by
  rw [← neg_neg a, neg_smul, neg_smul (-a), neg_lt_neg_iff] at h
  exact lt_of_smul_lt_smul_of_nonneg_left h (neg_nonneg_of_nonpos ha)

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:
by
  rw [← neg_nonneg, ← neg_smul, smul_nonneg_iff_pos_imp_nonneg]; simp only [neg_pos, neg_nonneg]

Goal state after: