mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
⊢ False

Tactic:
have := pow_mul_divByMonic_rootMultiplicity_eq p a

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) = p
⊢ False
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: K : Type u_1
inst✝ : Field K
p q : K[X]
hpq : p ∣ q
hq : q ≠ 0
h₁ : q.natDegree ≤ p.natDegree
⊢ IsUnit q.leadingCoeff

Tactic:
by rwa [← leadingCoeff_ne_zero, ← isUnit_iff_ne_zero] at hq

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
hp : p.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ q = C q.leadingCoeff * p

Tactic:
rw [mul_comm, ← eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le hp hdvd hdeg]

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

Goal state before:
pp: case mpr
α : Type u_2
f : Filter α
h : f.kerᶜ ∈ f
x : α
⊢ x ∉ f.ker

Tactic:
hx

Goal state after:
case mpr
α : Type u_2
f : Filter α
h : f.kerᶜ ∈ f
x : α
hx : x ∈ f.ker
⊢ False
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case mpr
α : Type u_2
f : Filter α
⊢ f.kerᶜ ∈ f → f.ker = ∅

Tactic:
intro h
    rw [eq_empty_iff_forall_notMem]
    intro x hx
    exact hx f.kerᶜ h hx

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

Goal state before:
pp: case refine_3
α : Type u_2
f : Filter α
⊢ f = 𝓟 (f.ker, Coheyting.boundary f).1 ⊔ (f.ker, Coheyting.boundary f).2

Tactic:
← compl_compl f.ker,

Goal state after:
case refine_3
α : Type u_2
f : Filter α
⊢ f = 𝓟 (f.kerᶜᶜ, Coheyting.boundary f).1 ⊔ (f.kerᶜᶜ, Coheyting.boundary f).2
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inr.inl.refine_1
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c✝ : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hprod : c✝ * s.prod = c✝ * (c * y)
hc : x = c✝ * c
⊢ c✝ ∈ {r | IsUnit r ∨ Prime r}

Tactic:
right; exact ha₂

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
hp0 : 0 < p.degree
⊢ (p - C a).degree = p.degree

Tactic:
rw [sub_eq_add_neg, ← C_neg]; exact degree_add_C hp0

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : ¬a = 0
x : α
⊢ x ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯) → Prime x

Tactic:
hx

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : ¬a = 0
x : α
hx : x ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯)
⊢ Prime x
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case mpr
σ : Type u_1
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : f = 0
⊢ (weight w) 0 = 0

Tactic:
map_zero

Goal state after:
case mpr
σ : Type u_1
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : f = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
h : ¬a = 0
x : α
⊢ x ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯) → normalize x = x

Tactic:
hx

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
h : ¬a = 0
x : α
hx : x ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯)
⊢ normalize x = x
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case h
σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
d : σ →₀ ℕ
hd : (weight w) d ≤ n
x : σ
⊢ (d + (equivFunOnFinite.symm (Function.const σ n) - d)) x = (equivFunOnFinite.symm (Function.const σ n)) x

Tactic:
grw [← le_weight _ (hw x)] at hd

Goal state after:
case h
σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
d : σ →₀ ℕ
x : σ
hd : d x ≤ n
⊢ (d + (equivFunOnFinite.symm (Function.const σ n) - d)) x = (equivFunOnFinite.symm (Function.const σ n)) x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case inr.hg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
x : α
⊢ x ∈ 0 → Irreducible x

Tactic:
hx

Goal state after:
case inr.hg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
x : α
hx : x ∈ 0
⊢ Irreducible x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case hf
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x✝ y : α
hx : x✝ ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
x : α
⊢ x ∈ normalizedFactors x✝ + normalizedFactors y → Irreducible x

Tactic:
hx

Goal state after:
case hf
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x✝ y : α
hx✝ : x✝ ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
x : α
hx : x ∈ normalizedFactors x✝ + normalizedFactors y
⊢ Irreducible x
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_5
s t : Set ℕ
⊢ ⇑degree ⁻¹' (s + t) = ⇑degree ⁻¹' s + ⇑degree ⁻¹' t

Tactic:
by
  refine (Set.preimage_add_preimage_subset ..).antisymm' ?_
  rintro f ⟨m, hm, n, hn, e : m + n = _⟩
  obtain ⟨g, hgf, rfl⟩ := exists_le_degree_eq f m (by grind)
  obtain ⟨f, rfl⟩ := le_iff_exists_add.mp hgf
  exact Set.add_mem_add hm (by simp_all)

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
⊢ (p.comp (C a * X + C b)).roots = Multiset.map (fun x ↦ a⁻¹ʳ * (x - b)) p.roots

Tactic:
conv_rhs => rw [← p.map_roots_comp_C_mul_X_add_C a b ha]
  simp [← mul_assoc, Ring.inverse_mul_cancel a ha]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ factors 1 = 0

Tactic:
rw [← rel_zero_right]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ Rel ?m.19 (factors 1) 0

α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ Type ?u.17

α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ α → ?m.18 → Prop
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case mp
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : 0 < normalizedFactors x
⊢ ¬IsUnit x

Tactic:
hx

Goal state after:
case mp
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx✝ : x ≠ 0
h : 0 < normalizedFactors x
hx : IsUnit x
⊢ False
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : n ∈ p.support
⊢ p.content ∣ p.coeff n

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : n ∉ p.support
⊢ p.content ∣ p.coeff n

Tactic:
· apply Finset.gcd_dvd h

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : n ∉ p.support
⊢ p.content ∣ p.coeff n
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing T
p : T[X]
inst✝⁴ : CommRing S
inst✝³ : Algebra T S
inst✝² : Algebra S R
inst✝¹ : Algebra T R
inst✝ : IsScalarTower T S R
⊢ (map (algebraMap T S) p).aroots R = p.aroots R

Tactic:
rw [aroots_def, aroots_def, map_map, IsScalarTower.algebraMap_eq T S R]

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

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
p : T[X]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
⊢ a ∈ p.aroots S ↔ map (algebraMap T S) p ≠ 0 ∧ (aeval a) p = 0

Tactic:
mem_aroots'

Goal state after:
T : Type w
inst✝³ : CommRing T
p : T[X]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
⊢ map (algebraMap T S) p ≠ 0 ∧ (aeval a) p = 0 ↔ map (algebraMap T S) p ≠ 0 ∧ (aeval a) p = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * ↑u = e.symm a
⊢ e (e.symm a) = a

Tactic:
apply_symm_apply

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * ↑u = e.symm a
⊢ a = a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
p : Associates α
hp : Irreducible p
⊢ BfactorSetMem ⟨p, hp⟩ ⊤

Tactic:
exact trivial

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)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
h : a.factors ≤ b.factors
⊢ p.count a.factors ≤ p.count b.factors

Tactic:
by
  by_cases ha : a = 0
  · simp_all
  obtain ⟨sa, h_sa⟩ := factors_eq_some_iff_ne_zero.mpr ha
  obtain ⟨sb, h_sb⟩ := factors_eq_some_iff_ne_zero.mpr hb
  rw [h_sa, h_sb] at h ⊢
  rw [count_some hp, count_some hp]; rw [WithTop.coe_le_coe] at h
  exact Multiset.count_le_of_le _ h

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

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

Tactic:
obtain ⟨q, hq, hpq⟩ := exists_mem_factors_of_dvd ha0 hp hd

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
⊢ ⟨Associates.mk p, ⋯⟩ ∈ factors' a
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: K : Type u_1
inst✝ : Ring K
f : K[X]
a : K
⊢ (X - C a) * (f /ₘ (X - C a)) + f %ₘ (X - C a) = f

Tactic:
← eq_sub_iff_add_eq',

Goal state after:
K : Type u_1
inst✝ : Ring K
f : K[X]
a : K
⊢ f %ₘ (X - C a) = f - (X - C a) * (f /ₘ (X - C a))
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)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
h : 0 < p.count m.factors
⊢ p ≤ m

Tactic:
rw [← pow_one p]

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
h : 0 < p.count m.factors
⊢ p ^ 1 ≤ m
Module: Mathlib.Algebra.Polynomial.FieldDivision

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

Tactic:
map_zero

Goal state after:
case pos
F : Type u_1
inst✝ : DivisionSemiring F
f : F[X]
H : f.natDegree = 0
x : F
h : Irreducible 0
hf : C x = f
hx : x = 0
⊢ False
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
r : A
f : R[X]
H : ∀ (p : R[X]), (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0 → p = 0
p : R[X]
hp : (Polynomial.aeval f) p = 0
⊢ (Polynomial.aeval r) 0 = 0

Tactic:
map_zero

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
H : ∀ (p : R[X]), (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0 → p = 0
p : R[X]
hp : (Polynomial.aeval f) p = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
S : Type u_1
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
a : S
x✝ : IsAlgebraic R a
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval a) f = 0
⊢ (algebraMap S A) 0 = 0

Tactic:
map_zero

Goal state after:
R : Type u
S : Type u_1
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
a : S
x✝ : IsAlgebraic R a
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval a) f = 0
⊢ 0 = 0
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
B : Type u_2
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
a : A
h : IsAlgebraic R a
p : R[X]
hp : p ≠ 0
ha : (aeval a) p = 0
⊢ f 0 = 0

Tactic:
map_zero

Goal state after:
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
B : Type u_2
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
a : A
h : IsAlgebraic R a
p : R[X]
hp : p ≠ 0
ha : (aeval a) p = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Injective ⇑f
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
p : R[X]
h1 : p ≠ 0
h2 : (aeval a) p = 0
⊢ ↑g 0 = 0

Tactic:
map_zero

Goal state after:
R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Injective ⇑f
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
p : R[X]
h1 : p ≠ 0
h2 : (aeval a) p = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ (↑x)⁻¹ ∈ A

Tactic:
suffices (x⁻¹ : L) = (-p.coeff 0)⁻¹ • aeval x (divX p) by
    rw [this]
    exact A.smul_mem (aeval x _).2 _

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ (↑x)⁻¹ = (-p.coeff 0)⁻¹ • ↑((aeval x) p.divX)
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
ne_zero : p ≠ 0
aeval_eq : ↑((aeval x) p) = 0
⊢ (↑x)⁻¹ ∈ A

Tactic:
Subalgebra.coe_eq_zero

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
ne_zero : p ≠ 0
aeval_eq : (aeval x) p = 0
⊢ (↑x)⁻¹ ∈ A
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
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
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z w : DirectLimit G f
i : ι
x : G i
hx : (of R ι G f i) x = z
j : ι
y : G j
hy : (of R ι G f j) y = w
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ (of R ι G f i) x = z

Tactic:
hx

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
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
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z w : DirectLimit G f
i : ι
x : G i
hx : (of R ι G f i) x = z
j : ι
y : G j
hy : (of R ι G f j) y = w
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ z = z
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
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
inst✝² : DecidableEq ι
inst✝¹ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
i : ι
x y : G i
h : (of R ι G f i) x = (of R ι G f i) y
⊢ ∃ j, ∃ (hij : i ≤ j), (f i j hij) x = (f i j hij) y

Tactic:
by
  have := Nonempty.intro i
  apply_fun linearEquiv _ _ at h
  simp_rw [linearEquiv_of] at h
  have ⟨j, h⟩ := Quotient.exact h
  exact ⟨j, h.1, h.2.2⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
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
inst✝² : DecidableEq ι
inst✝¹ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
i : ι
x : G i
H : (of R ι G f i) x = 0
x✝¹ : ι
x✝ : i ≤ x✝¹
⊢ 0 = (f i x✝¹ x✝) 0

Tactic:
map_zero

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
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
inst✝² : DecidableEq ι
inst✝¹ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
i : ι
x : G i
H : (of R ι G f i) x = 0
x✝¹ : ι
x✝ : i ≤ x✝¹
⊢ 0 = 0
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
s t : Set (σ →₀ ℕ)
x : σ →₀ ℕ
⊢ x ∈ s → ∀ y ∈ t, x + y ∈ (fun x ↦ (monomial x) 1) ⁻¹' ↑(restrictSupport R s * restrictSupport R t)

Tactic:
hx

Goal state after:
case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
s t : Set (σ →₀ ℕ)
x : σ →₀ ℕ
hx : x ∈ s
⊢ ∀ y ∈ t, x + y ∈ (fun x ↦ (monomial x) 1) ⁻¹' ↑(restrictSupport R s * restrictSupport R t)
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
h : P → N
hgh : RightInverse h ⇑g
y : Q ⊗[R] N
⊢ (toFun Q hfg) (Submodule.Quotient.mk y) = (lTensor Q g) y

Tactic:
simp only [lTensor.toFun, Submodule.liftQ_apply]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg✝ : Exact ⇑f ⇑g
hg : Surjective ⇑g
h : P → N
hfg : Exact ⇑f ⇑g
hgh : RightInverse h ⇑g
p p' : P
q : Q
⊢ h (p + p') ⊗ₜ[R] q - (h p ⊗ₜ[R] q + h p' ⊗ₜ[R] q) ∈ (rTensor Q f).range

Tactic:
rw [← TensorProduct.add_tmul, ← TensorProduct.sub_tmul]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg✝ : Exact ⇑f ⇑g
hg : Surjective ⇑g
h : P → N
hfg : Exact ⇑f ⇑g
hgh : RightInverse h ⇑g
p p' : P
q : Q
⊢ (h (p + p') - (h p + h p')) ⊗ₜ[R] q ∈ (rTensor Q f).range
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a
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
x : A ⊗[R] B
⊢ x ∈ ↑(Submodule.restrictScalars R (map includeLeft I)) →
    x ∈ ↑(LinearMap.rTensor B (Submodule.restrictScalars R I).subtype).range

Tactic:
hx

Goal state after:
case a
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
x : A ⊗[R] B
hx : x ∈ ↑(Submodule.restrictScalars R (map includeLeft I))
⊢ x ∈ ↑(LinearMap.rTensor B (Submodule.restrictScalars R I).subtype).range
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
⊢ ∃ S, x = S.sum fun n m ↦ m ⊗ₜ[R] n

Tactic:
obtain ⟨S, h⟩ := exists_finsupp_left (TensorProduct.comm R M N x)
  refine ⟨S, (TensorProduct.comm R M N).injective ?_⟩
  simp_rw [h, Finsupp.sum, map_sum, comm_tmul]

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

Goal state before:
pp: case a.zero
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
⊢ (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) 0 ∈ ↑(Submodule.restrictScalars R (map includeLeft I))

Tactic:
map_zero

Goal state after:
case a.zero
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
⊢ 0 ∈ ↑(Submodule.restrictScalars R (map includeLeft I))
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a
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
x : A ⊗[R] B
⊢ x ∈ ↑(Submodule.restrictScalars R (map includeRight I)) →
    x ∈ ↑(LinearMap.lTensor A (Submodule.restrictScalars R I).subtype).range

Tactic:
hx

Goal state after:
case a
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
x : A ⊗[R] B
hx : x ∈ ↑(Submodule.restrictScalars R (map includeRight I))
⊢ x ∈ ↑(LinearMap.lTensor A (Submodule.restrictScalars R I).subtype).range