mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
⊢ s ∈ f ×ˢ 𝓟 t ↔ {a | ∀ b ∈ t, (a, b) ∈ s} ∈ f

Tactic:
← @exists_mem_subset_iff _ f,

Goal state after:
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
⊢ s ∈ f ×ˢ 𝓟 t ↔ ∃ t_1 ∈ f, t_1 ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
γ : Type u_3
f : Filter α
g : Filter γ
p : α × γ × γ → Prop
⊢ (∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x) → ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.1, x.2, x.2)

Tactic:
by
  intro h
  obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h
  exact (ht.prod_mk hs.diag_of_prod).mono fun x hx => by simp only [hst hx.1 hx.2]

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊔ b) ⊔ b

Tactic:
hnot_le_iff_codisjoint_right,

Goal state after:
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ Codisjoint a (￢(a ⊔ b) ⊔ b)
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢￢a ⊔ ∂ a = a

Tactic:
by
  rw [boundary, sup_inf_left, hnot_sup_self, inf_top_eq, sup_eq_right]
  exact hnot_hnot_le

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

Goal state before:
pp: α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ map (Prod.map (fun x ↦ b) id) ((𝓟 {a}).coprod (𝓟 {i})) = 𝓟 ({b} ×ˢ univ)

Tactic:
by
  rw [principal_coprod_principal, map_principal]
  congr
  ext ⟨b', i'⟩
  constructor
  · rintro ⟨⟨a'', i''⟩, _, h₂, h₃⟩
    simp
  · rintro ⟨h₁, _⟩
    use (a, i')
    simpa using h₁.symm

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

Goal state before:
pp: M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : (a : M₀) → DecidablePred (Associated a)
s : Multiset M₀
n : M₀
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1
⊢ s.prod ∣ n

Tactic:
by
  induction s using Multiset.induction_on generalizing n with
  | empty => simp only [Multiset.prod_zero, one_dvd]
  | cons a s induct =>
    rw [Multiset.prod_cons]
    obtain ⟨k, rfl⟩ : a ∣ n := div a (Multiset.mem_cons_self a s)
    gcongr
    refine induct _ (fun a ha => h a (Multiset.mem_cons_of_mem ha)) (fun b b_in_s => ?_)
      fun a => (Multiset.countP_le_of_le _ (Multiset.le_cons_self _ _)).trans (uniq a)
    have b_div_n := div b (Multiset.mem_cons_of_mem b_in_s)
    have a_prime := h a (Multiset.mem_cons_self a s)
    have b_prime := h b (Multiset.mem_cons_of_mem b_in_s)
    refine (b_prime.dvd_or_dvd b_div_n).resolve_left fun b_div_a => ?_
    have assoc := b_prime.associated_of_dvd a_prime b_div_a
    have := uniq a
    rw [Multiset.countP_cons_of_pos _ (Associated.refl _), Nat.succ_le_succ_iff, ← not_lt,
      Multiset.countP_pos] at this
    exact this ⟨b, b_in_s, assoc.symm⟩

Goal state after:
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
R : Type u_5
inst✝ : Semiring R
⊢ degree = weight fun x ↦ 1

Tactic:
ext d

Goal state after:
σ : Type u_1
R : Type u_5
inst✝ : Semiring R
d : σ
x✝ : R
⊢ (degree.comp (singleAddHom d)) x✝ = ((weight fun x ↦ 1).comp (singleAddHom d)) x✝
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
h0 : x = 0
⊢ normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x

Tactic:
simp [h0, zero_pow n.succ_ne_zero, nsmul_zero]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
b : α
hbmem : b ∈ factors a
hab : a ~ᵤ b
⊢ (factors a).card ≤ {b}.card

Tactic:
by rw [card_factors_of_irreducible ha, Multiset.card_singleton]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
⊢ Rel Associated 0 0

Tactic:
rel_zero_right

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
⊢ 0 = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : x = 0
⊢ Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)

Tactic:
simp [h0, zero_pow n.succ_ne_zero, nsmul_zero]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case mp
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ DvdNotUnit x y → normalizedFactors x < normalizedFactors y

Tactic:
rintro ⟨_, c, hc, rfl⟩
    simp only [hx, right_ne_zero_of_mul hy, normalizedFactors_mul, Ne, not_false_iff,
      lt_add_iff_pos_right, normalizedFactors_pos, hc]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
h₁ : X ^ 2 - C 1 = (X + C 1) * (X - C 1)
h₂ : X ^ 2 - C 1 ≠ 0
⊢ nthRoots 2 1 = {-1, 1}

Tactic:
rw [nthRoots, h₁, roots_mul (h₁ ▸ h₂), roots_X_add_C, roots_X_sub_C]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
h₁ : X ^ 2 - C 1 = (X + C 1) * (X - C 1)
h₂ : X ^ 2 - C 1 ≠ 0
⊢ {-1} + {1} = {-1, 1}
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).support.gcd (C r * p).coeff = p.support.gcd fun x ↦ r * p.coeff x

Tactic:
refine congr (congr rfl ?_) ?_ <;> ext

Goal state after:
case neg.refine_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
a✝ : ℕ
⊢ a✝ ∈ (C r * p).support ↔ a✝ ∈ p.support

case neg.refine_2
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
x✝ : ℕ
⊢ (C r * p).coeff x✝ = r * p.coeff x✝
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).support.gcd (C r * p).coeff = p.support.gcd fun x ↦ r * p.coeff x

Tactic:
refine congr (congr rfl ?_) ?_ <;> ext

Goal state after:
case neg.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
a✝ : ℕ
⊢ a✝ ∈ (C r * p).support ↔ a✝ ∈ p.support

case neg.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
x✝ : ℕ
⊢ (C r * p).coeff x✝ = r * p.coeff x✝
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
hnzd : ↑(rootMultiplicity t p) ∈ nonZeroDivisors R
h : ¬p = 0
g : R[X]
hp : p = (X - C t) ^ rootMultiplicity t p * g
hndvd : ¬X - C t ∣ g
⊢ rootMultiplicity t (derivative p) = rootMultiplicity t p - 1

Tactic:
set m := p.rootMultiplicity t

Goal state after:
case neg
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬X - C t ∣ g
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
⊢ rootMultiplicity t (derivative p) = m - 1
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
| eval t ((⇑derivative)^[m] ((X - C t) ^ rootMultiplicity t p * (p /ₘ (X - C t) ^ rootMultiplicity t p)))

Tactic:
← hm

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
| eval t ((⇑derivative)^[m] ((X - C t) ^ m * (p /ₘ (X - C t) ^ m)))
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: A : Type u_1
inst✝³ : CommRing A
p : A[X]
B : Type u_3
inst✝² : CommRing B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
⊢ (p.rootSet B).ncard ≤ p.natDegree

Tactic:
grw [rootSet, Set.ncard_coe_finset, Multiset.toFinset_card_le]

Goal state after:
A : Type u_1
inst✝³ : CommRing A
p : A[X]
B : Type u_3
inst✝² : CommRing B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
⊢ (p.aroots B).card ≤ p.natDegree
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ ⟨Associates.mk p, ⋯⟩ ∈ factors' a ↔ p ∣ a

Tactic:
constructor
  · rw [← mk_dvd_mk]
    apply dvd_of_mem_factors'
    apply ha0
  · apply mem_factors'_of_dvd ha0 hp

Goal state after:
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case refine_3
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ (q * C q.leadingCoeff⁻¹).natDegree ≤ q.natDegree

Tactic:
· exact natDegree_mul_C_le q q.leadingCoeff⁻¹

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
sC : s.natDegree ≤ 0
⊢ False

Tactic:
rw [eq_C_of_natDegree_le_zero (le_trans hs sC), isPrimitive_iff_content_eq_one, content_C,
        normalize_eq_one] at rprim
      rw [eq_C_of_natDegree_le_zero (le_trans hs sC), ← dvd_content_iff_C_dvd] at rs
      apply rs rprim.dvd

Goal state after:
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
⊢ (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff

Tactic:
by_cases hq : q = 0
  · simp [hq]
  rw [div_def, leadingCoeff_mul, leadingCoeff_C,
    leadingCoeff_divByMonic_of_monic (monic_mul_leadingCoeff_inv hq) _, mul_comm,
    div_eq_mul_inv]
  rwa [degree_mul_leadingCoeff_inv q hq]

Goal state after:
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case e_q
R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : ¬a = 0
⊢ C 1 * (q * C q.leadingCoeff⁻¹) = q * C q.leadingCoeff⁻¹

Tactic:
C.map_one,

Goal state after:
case e_q
R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : ¬a = 0
⊢ 1 * (q * C q.leadingCoeff⁻¹) = q * C q.leadingCoeff⁻¹
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : a ≠ 0
x✝ : p ∣ q
r : R[X]
hr : q = p * r
⊢ q = C 1 * (p * r)

Tactic:
C.map_one,

Goal state after:
R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : a ≠ 0
x✝ : p ∣ q
r : R[X]
hr : q = p * r
⊢ q = 1 * (p * r)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : a ≠ 0
x✝ : p ∣ C a * q
r : R[X]
hr : C a * q = p * r
⊢ q = C 1 * q

Tactic:
C.map_one,

Goal state after:
R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : a ≠ 0
x✝ : p ∣ C a * q
r : R[X]
hr : C a * q = p * r
⊢ q = 1 * q
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case inr
R : Type u
inst✝ : Field R
p₁ p₂ q : R[X]
h : q ∣ p₁ - p₂
hq : q ≠ 0
⊢ q * C q.leadingCoeff⁻¹ ∣ p₁ - p₂

Tactic:
rw [mul_comm]

Goal state after:
case inr
R : Type u
inst✝ : Field R
p₁ p₂ q : R[X]
h : q ∣ p₁ - p₂
hq : q ≠ 0
⊢ C q.leadingCoeff⁻¹ * q ∣ p₁ - p₂
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
F : Type u_1
inst✝ : DivisionSemiring F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : C x = f
hx : ¬x = 0
⊢ False

Tactic:
exact h.1 (hf ▸ isUnit_C.2 (Ne.isUnit hx))

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
k : ℕ
a✝ : Nontrivial α
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count ↑(factors' a0)
⊢ ∃ b, Associates.mk a0 = b ^ k

Tactic:
have hk' : ∀ p, p ∈ factors' a0 → k ∣ (factors' a0).count p := by
    rintro p -
    have pp : p = ⟨p.val, p.2⟩ := by simp only [Subtype.coe_eta]
    rw [pp, ← count_some p.2]
    exact hk p.val p.2

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
k : ℕ
a✝ : Nontrivial α
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count ↑(factors' a0)
hk' : ∀ p ∈ factors' a0, k ∣ Multiset.count p (factors' a0)
⊢ ∃ b, Associates.mk a0 = b ^ k
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
h : Algebra.Transcendental R A
⊢ Function.Injective ⇑(algebraMap R A)

Tactic:
by
  rw [transcendental_iff_not_isAlgebraic] at h
  contrapose h
  exact isAlgebraic_of_not_injective h

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
g : G i
m : M
⊢ (lift
        (Module.DirectLimit.lift R ι G f
          (fun i ↦
            (mk R (G i) M).compr₂ (of R ι (fun _i ↦ G _i ⊗[R] M) (fun _i _j h ↦ LinearMap.rTensor M (f _i _j h)) i))
          ⋯))
      ((of R ι G f i) g ⊗ₜ[R] m) =
    (of R ι (fun x ↦ G x ⊗[R] M) (fun i j h ↦ LinearMap.rTensor M (f i j h)) i) (g ⊗ₜ[R] m)

Tactic:
lift.tmul,

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
g : G i
m : M
⊢ ((Module.DirectLimit.lift R ι G f
          (fun i ↦
            (mk R (G i) M).compr₂ (of R ι (fun _i ↦ G _i ⊗[R] M) (fun _i _j h ↦ LinearMap.rTensor M (f _i _j h)) i))
          ⋯)
        ((of R ι G f i) g))
      m =
    (of R ι (fun x ↦ G x ⊗[R] M) (fun i j h ↦ LinearMap.rTensor M (f i j h)) i) (g ⊗ₜ[R] m)
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
ι : Type u_3
P : ι → Submodule R M
inst✝¹ : Small.{u, u_3} ι
inst✝ : ∀ (i : ι), Small.{u, u_2} ↥(P i)
⊢ Small.{u, u_2} ↥(iSup P)

Tactic:
rw [iSup_eq_range_dfinsupp_lsum]
  apply small_range

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
a : ↥(Submodule.restrictScalars R I)
b : B
this : ↑a ⊗ₜ[R] b = 1 ⊗ₜ[R] b * ↑a ⊗ₜ[R] 1
⊢ 1 ⊗ₜ[R] b * ↑a ⊗ₜ[R] 1 ∈ map includeLeft I

Tactic:
apply Ideal.mul_mem_left

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
a : ↥(Submodule.restrictScalars R I)
b : B
this : ↑a ⊗ₜ[R] b = 1 ⊗ₜ[R] b * ↑a ⊗ₜ[R] 1
⊢ ↑a ⊗ₜ[R] 1 ∈ map includeLeft I
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
a : A
b : ↥(Submodule.restrictScalars R I)
this : a ⊗ₜ[R] ↑b = a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] ↑b
⊢ a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] ↑b ∈ map includeRight I

Tactic:
apply Ideal.mul_mem_left

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
a : A
b : ↥(Submodule.restrictScalars R I)
this : a ⊗ₜ[R] ↑b = a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] ↑b
⊢ 1 ⊗ₜ[R] ↑b ∈ map includeRight I
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝¹ : Zero R
inst✝ : Pow R ℕ
hx : 0 < nilpotencyClass x
⊢ IsNilpotent x

Tactic:
by
  let s : Set ℕ := {k | x ^ k = 0}
  change s.Nonempty
  change 0 < sInf s at hx
  by_contra contra
  simp [not_nonempty_iff_eq_empty.mp contra] at hx

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
⊢ ∑ i ∈ Ico m n, f i • g i =
    f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i -
      ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

Tactic:
have h₁ : (∑ i ∈ Ico (m + 1) n, f i • G i) = ∑ i ∈ Ico m (n - 1), f (i + 1) • G (i + 1) := by
    rw [← Nat.sub_add_cancel (Nat.one_le_of_lt hmn), ← sum_Ico_add']
    simp only [add_tsub_cancel_right]
  have h₂ :
    (∑ i ∈ Ico (m + 1) n, f i • G (i + 1)) =
      (∑ i ∈ Ico m (n - 1), f i • G (i + 1)) + f (n - 1) • G n - f m • G (m + 1) := by
    rw [← sum_Ico_sub_bot _ hmn, ← sum_Ico_succ_sub_top _ (Nat.le_sub_one_of_lt hmn),
      Nat.sub_add_cancel (pos_of_gt hmn), sub_add_cancel]
  rw [sum_eq_sum_Ico_succ_bot hmn]
  conv in (occs := 3) (f _ • g _) => rw [← sum_range_succ_sub_sum g]
  simp_rw [smul_sub, sum_sub_distrib, h₂, h₁]
  conv_lhs => congr; rfl; rw [← add_sub, add_comm, ← add_sub, ← sum_sub_distrib]
  have : ∀ i, f i • G (i + 1) - f (i + 1) • G (i + 1) = -((f (i + 1) - f i) • G (i + 1)) := by
    intro i
    rw [sub_smul]
    abel
  simp_rw [this, sum_neg_distrib, sum_range_succ, smul_add]
  abel

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case tmul
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : Module R M
inst✝¹³ : Module R N
inst✝¹² : Module S N
inst✝¹¹ : IsScalarTower R S N
P : Type u_2
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
A : Type u_4
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra S A
inst✝⁵ : IsScalarTower R S A
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
inst✝² : Module A N
inst✝¹ : IsScalarTower S A N
inst✝ : IsScalarTower R A N
f : M →ₗ[S] N
hf : IsBaseChange A f
e : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] N ⊗[R] P :=
  (AlgebraTensorModule.assoc R S A A M P).symm ≪≫ₗ AlgebraTensorModule.congr hf.equiv (LinearEquiv.refl R P)
x✝ : M
y✝ : P
⊢ e (1 ⊗ₜ[S] (x✝ ⊗ₜ[R] y✝)) = (AlgebraTensorModule.map f LinearMap.id) (x✝ ⊗ₜ[R] y✝)

Tactic:
simp [e, IsBaseChange.equiv_tmul]

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
⊢ (map g s).sym n = map { toFun := Sym.map ⇑g, inj' := ⋯ } (s.sym n)

Tactic:
ext d

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
⊢ d ∈ (map g s).sym n ↔ d ∈ map { toFun := Sym.map ⇑g, inj' := ⋯ } (s.sym n)
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ (s(x, x) :: (map (fun y ↦ s(x, y)) xs ++ xs.sym2)).dedup = (x :: xs).dedup.sym2

Tactic:
rw [dedup_cons_of_notMem hm, List.sym2, map_cons, ← ih, dedup_cons_of_notMem, cons_append,
        List.Disjoint.dedup_append, dedup_map_of_injective]
      · exact (Sym2.mkEmbedding _).injective
      · exact map_mk_disjoint_sym2 x xs hm
      · simp [hm, mem_sym2_iff]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
⊢ ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g

Tactic:
intro Q _ _ _ _ g
    exact ⟨h.lift g, h.lift_comp g, fun g' e => h.algHom_ext' _ _ (e.trans (h.lift_comp g).symm)⟩

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
F : Sym2 α → Sym2 β → γ
a₁ a₂ : α
b₁ b₂ : β
⊢ (fun a₁ a₂ b₁ b₂ ↦ F s(a₁, a₂) s(b₁, b₂)) a₁ a₂ b₁ b₂ = (fun a₁ a₂ b₁ b₂ ↦ F s(a₁, a₂) s(b₁, b₂)) a₂ a₁ b₁ b₂

pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
F : Sym2 α → Sym2 β → γ
a₁ a₂ : α
b₁ b₂ : β
⊢ (fun a₁ a₂ b₁ b₂ ↦ F s(a₁, a₂) s(b₁, b₂)) a₁ a₂ b₁ b₂ = (fun a₁ a₂ b₁ b₂ ↦ F s(a₁, a₂) s(b₁, b₂)) a₁ a₂ b₂ b₁

Tactic:
exacts [congr_arg₂ F eq_swap rfl, congr_arg₂ F rfl eq_swap]

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a b c : α
⊢ Sym2.Mem a s(b, c) → a = b ∨ a = c

Tactic:
rintro ⟨_, h⟩

Goal state after:
α : Type u_1
a b c w✝ : α
h : s(b, c) = s(a, w✝)
⊢ a = b ∨ a = c
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y X' Y' : V
hX : X = X'
hY : Y = Y'
f : X ⟶ Y
f' : X' ⟶ Y'
e : homOfEq f hX hY = f'
⊢ f ≍ f'

Tactic:
by
  subst hX hY
  rw [Quiver.homOfEq_rfl] at e
  rw [e]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_4
R : Type u_1
S : Type v₃
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁹ : CommSemiring R'
inst✝⁸ : CommSemiring S'
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra R S'
inst✝³ : IsScalarTower R R' S'
inst✝² : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
x : S'
⊢ ∀ (n₁ n₂ : S'), f n₁ = g n₁ → f n₂ = g n₂ → f (n₁ + n₂) = g (n₁ + n₂)

Tactic:
· intro s₁ s₂ e₁ e₂
    rw [map_add, map_add, e₁, e₂]

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : Y ≅ Z
⊢ α.symm ≪≫ α ≪≫ β = β

Tactic:
← trans_assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : Y ≅ Z
⊢ (α.symm ≪≫ α) ≪≫ β = β
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : X ≅ Z
⊢ α ≪≫ α.symm ≪≫ β = β

Tactic:
← trans_assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : X ≅ Z
⊢ (α ≪≫ α.symm) ≪≫ β = β
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b : V
p : Path a b
n : ℕ
hp : p.length = n + 1
⊢ ∃ c f q x, p = f.toPath.comp q

Tactic:
by
  induction p generalizing n with
  | nil => simp at hp
  | @cons c d p q h =>
    cases n
    · rw [length_cons, Nat.zero_add, Nat.add_eq_right] at hp
      obtain rfl := eq_of_length_zero p hp
      obtain rfl := eq_nil_of_length_zero p hp
      exact ⟨d, q, nil, rfl, rfl⟩
    · rw [length_cons, Nat.add_right_cancel_iff] at hp
      obtain ⟨x, q'', p'', hl, rfl⟩ := h hp
      exact ⟨x, q'', p''.cons q, by simpa, rfl⟩

Goal state after: