mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ {-1} + {1} = {-1, 1}

Tactic:
rfl

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

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : T
⊢ ↑∅ = ∅

Tactic:
Finset.coe_empty

Goal state after:
S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : T
⊢ ∅ = ∅
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
⊢ ↑m ! * eval t ((⇑derivative)^[0] (p /ₘ (X - C t) ^ m)) = ↑m ! * eval t (p /ₘ (X - C t) ^ m)

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hroot : ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t
hnzd : ↑n ! ∈ nonZeroDivisors R
⊢ n < rootMultiplicity t p

Tactic:
by_contra! h'
  replace hroot := hroot _ h'
  simp only [IsRoot, eval_iterate_derivative_rootMultiplicity] at hroot
  obtain ⟨q, hq⟩ : ((rootMultiplicity t p)! : R) ∣ n ! := by gcongr
  rw [hq, mul_mem_nonZeroDivisors] at hnzd
  rw [nsmul_eq_mul, mul_left_mem_nonZeroDivisors_eq_zero_iff hnzd.1] at hroot
  exact eval_divByMonic_pow_rootMultiplicity_ne_zero t h hroot

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
p : Associates α
hp : Irreducible p
l : Multiset { a // Irreducible a }
⊢ BfactorSetMem ⟨p, hp⟩ ↑l ↔ l.Mem ⟨p, hp⟩

Tactic:
rfl

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

Goal state before:
pp: case top.top
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
h : prod ⊤ = prod ⊤
⊢ ⊤ = ⊤

Tactic:
rfl

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hirr : Irreducible p
x : R
hx : x ∈ p.roots
⊢ p.roots.card ≤ 1

Tactic:
convert! p.card_roots'

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hirr : Irreducible p
x : R
hx : x ∈ p.roots
⊢ 1 = p.natDegree
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ gcd (q.primPart * p.primPart).eraseLead.content q.primPart.leadingCoeff *
      gcd (q.primPart * p.primPart).eraseLead.content p.primPart.leadingCoeff ∣
    1

Tactic:
rw [content_mul_aux, (ih ..).gcd_eq_left, content_primPart, mul_one, gcd_comm, ←
      content_eq_gcd_leadingCoeff_content_eraseLead, content_primPart, one_mul,
      mul_comm q.primPart, content_mul_aux, (ih ..).gcd_eq_left, content_primPart, mul_one,
      gcd_comm, ← content_eq_gcd_leadingCoeff_content_eraseLead, content_primPart]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ (p.primPart.eraseLead * q.primPart).degree < ↑n

R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ (q.primPart.eraseLead * p.primPart).degree < ↑n
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 : Associates α
ha : a ≠ 0
hb : b ≠ 0
sa sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α) (a : Irreducible p), Multiset.count ⟨p, a⟩ sa = Multiset.count ⟨p, a⟩ sb
h_sa : a.factors = ↑sa
h_sb : b.factors = ↑sb
a✝ : { p // Irreducible p }
⊢ Multiset.count a✝ sa = Multiset.count a✝ sb

Tactic:
grind

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
⊢ ((monomial n) a).rootSet S = {0}

Tactic:
classical
  rw [rootSet, aroots_monomial ha,
    Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton, Finset.coe_singleton]

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

Goal state before:
pp: R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
⊢ ((↑u).coeff n)⁻¹ = (↑u⁻¹).coeff n

Tactic:
rw [eq_C_of_degree_eq_zero (degree_coe_units u), eq_C_of_degree_eq_zero (degree_coe_units u⁻¹),
    coeff_C, coeff_C, inv_eq_one_div]

Goal state after:
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
⊢ (1 / if n = 0 then (↑u).coeff 0 else 0) = if n = 0 then (↑u⁻¹).coeff 0 else 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
⊢ p.factors.prod = FactorSet.prod ↑{⟨p, hp⟩}

Tactic:
rw [factors_prod, FactorSet.prod.eq_def]

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
⊢ p =
    match ↑{⟨p, hp⟩} with
    | none => 0
    | some s => (Multiset.map Subtype.val s).prod
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 p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ (Associates.mk p).count (Associates.mk a).factors ≠ 0 ↔ p ∣ a

Tactic:
by
  rw [← Associates.mk_le_mk_iff_dvd]
  refine
    ⟨fun h =>
      Associates.le_of_count_ne_zero (Associates.mk_ne_zero.mpr ha0)
        (Associates.irreducible_mk.mpr hp) h,
      fun h => ?_⟩
  rw [← pow_one (Associates.mk p),
    Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero.mpr ha0)
      (Associates.irreducible_mk.mpr hp)] at h
  exact (zero_lt_one.trans_le h).ne'

Goal state after:
Module: Mathlib.Algebra.AlgebraicCard

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : CharZero A
⊢ {x | IsAlgebraic R x}.Infinite

Tactic:
let := MulActionWithZero.nontrivial R A
  exact infinite_of_injective_forall_mem Nat.cast_injective isAlgebraic_natCast

Goal state after:
Module: Mathlib.Algebra.AlgebraicCard

Goal state before:
pp: R A : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
⊢ #{ x // IsAlgebraic R x } ≤ max #R ℵ₀

Tactic:
rw [← lift_id #_, ← lift_id #R]

Goal state after:
R A : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
⊢ lift.{u, u} #{ x // IsAlgebraic R x } ≤ max (lift.{u, u} #R) ℵ₀
Module: Mathlib.Algebra.Central.Basic

Goal state before:
pp: k : Type u_1
K : Type u_2
D : Type u_3
inst✝⁸ : Field k
inst✝⁷ : Field K
inst✝⁶ : Ring D
inst✝⁵ : Nontrivial D
inst✝⁴ : Algebra k K
inst✝³ : Algebra K D
inst✝² : Algebra k D
inst✝¹ : IsScalarTower k K D
inst✝ : IsCentral k D
this : IsCentral K D
x : K
H : (algebraMap K D) x ∈ ↑(Subalgebra.center K D)
⊢ ↑(Subalgebra.center K D) = ↑(Subalgebra.center k D)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Central.Basic

Goal state before:
pp: k : Type u_1
K : Type u_2
D : Type u_3
inst✝⁸ : Field k
inst✝⁷ : Field K
inst✝⁶ : Ring D
inst✝⁵ : Nontrivial D
inst✝⁴ : Algebra k K
inst✝³ : Algebra K D
inst✝² : Algebra k D
inst✝¹ : IsScalarTower k K D
inst✝ : IsCentral k D
this : IsCentral K D
x : K
H : (algebraMap K D) x ∈ ↑(Subalgebra.center K D)
⊢ ∃ a, (algebraMap k K) a = x

Tactic:
show (Subalgebra.center K D : Set D) = Subalgebra.center k D by rfl

Goal state after:
k : Type u_1
K : Type u_2
D : Type u_3
inst✝⁸ : Field k
inst✝⁷ : Field K
inst✝⁶ : Ring D
inst✝⁵ : Nontrivial D
inst✝⁴ : Algebra k K
inst✝³ : Algebra K D
inst✝² : Algebra k D
inst✝¹ : IsScalarTower k K D
inst✝ : IsCentral k D
this : IsCentral K D
x : K
H : (algebraMap K D) x ∈ ↑(Subalgebra.center k D)
⊢ ∃ a, (algebraMap k K) a = x
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsAlgebraic (↥⊥) S
x✝ : R
⊢ ((algebraMap (↥⊥) S).comp ↑(algebraMap R ↥⊥)) x✝ = ((↑(RingHom.id S)).comp (algebraMap R S)) x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ S⁰
p : R[X]
hp0 : p ≠ 0
q : R[X]
hp : (aeval s) q * (aeval s) (X ^ rootMultiplicity 0 p) = 0
hpq : p = q * X ^ rootMultiplicity 0 p
hq : ¬q.coeff 0 = 0
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0

Tactic:
aeval_X_pow

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ S⁰
p : R[X]
hp0 : p ≠ 0
q : R[X]
hp : (aeval s) q * s ^ rootMultiplicity 0 p = 0
hpq : p = q * X ^ rootMultiplicity 0 p
hq : ¬q.coeff 0 = 0
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0
Module: Mathlib.Algebra.Colimit.Finiteness

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq (Submodule R M)
x : M
⊢ x ∈ {x}

Tactic:
rfl

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
⊢ (((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)) 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)

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_6
inst✝ : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : ↑(limit piLTProj i)
k l : ↑(Iio i)
hl : ↑l < ↑k
⊢ (piLTLim hi).symm f l = ↑((piLTLim hi).toFun ((piLTLim hi).invFun f)) k ⟨↑l, hl⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι✝ : Type u_1
inst✝² : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝¹ : PartialOrder ι
inst✝ : DecidableEq ι
f : (j : ↑(Iic i)) → X ↑j
⊢ (fun f j ↦ if h : ↑j = i then ⋯ ▸ f.2 else f.1 ⟨↑j, ⋯⟩) ((fun f ↦ (fun j ↦ f ⟨↑j, ⋯⟩, f ⟨i, ⋯⟩)) f) = f

Tactic:
grind

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✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z✝ : DirectLimit G f
ind : ι
z : DirectSum ι G
p q : DirectSum ι fun i ↦ G i
x✝¹ : ∃ i x, (of R ι G f i) x = Quotient.mk'' p
x✝ : ∃ i x, (of R ι G f i) x = Quotient.mk'' q
i : ι
x : G i
ihx : (of R ι G f i) x = Quotient.mk'' p
j : ι
y : G j
ihy : (of R ι G f j) y = Quotient.mk'' q
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ Quotient.mk'' p + Quotient.mk'' q = Quotient.mk'' (p + q)

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case inl.inl
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equiv : (j : ↑(Iic i)) → F ↑j ≃ piLT X ↑j
e : F i⁺ ≃ F i × X i
hi : ¬IsMax i
inst✝ : InverseSystem f
H : ∀ (x : F i⁺), (e x).1 = f ⋯ x
nat : IsNatEquiv f equiv
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : i⁺ ∈ Iic i⁺
x : F i⁺
hk : i⁺ ∈ Iic i⁺
h : i⁺ ≤ i⁺
⊢ (piEquivSucc equiv e hi ⟨i⁺, hk⟩) (f h x) = piLTProj h ((piEquivSucc equiv e hi ⟨i⁺, hj⟩) x)

Tactic:
simp [InverseSystem.map_self]

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case inl.inl
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝¹ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝ : InverseSystem f
k : ι
h : k ≤ k
t : F k
equiv : (j : ↑(Iio k)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
equivLim : F k ≃ ↑(limit f k)
hi : IsSuccPrelimit k
H : ∀ (x : F k) (l : ↑(Iio k)), ↑(equivLim x) l = f ⋯ x
hj hk : k ∈ Iic k
⊢ (piEquivLim nat equivLim hi ⟨k, hk⟩) (f h t) = piLTProj h ((piEquivLim nat equivLim hi ⟨k, hj⟩) t)

Tactic:
simp [InverseSystem.map_self]

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

Goal state before:
pp: σ : Type u
R : Type v
inst✝ : CommSemiring R
m : ℕ
p : MvPolynomial σ R
⊢ p ∈ restrictTotalDegree σ R m ↔ ∀ b ∈ p.support, (b.sum fun x e ↦ e) ≤ m

Tactic:
rfl

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

Goal state before:
pp: σ : Type u
R : Type v
inst✝ : CommSemiring R
p : MvPolynomial σ R
n : ℕ
⊢ ↑p.coeff.support ⊆ {n_1 | ∀ (i : σ), n_1 i ≤ n} ↔ ∀ s ∈ p.support, ∀ (i : σ), s i ≤ n

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
N : Submodule R M
⊢ (lTensor Q N.mkQ).ker = (lTensor Q N.subtype).range

Tactic:
rw [← exact_iff]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
N : Submodule R M
⊢ Exact ⇑(lTensor Q N.subtype) ⇑(lTensor Q N.mkQ)
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
N : Submodule R M
⊢ (rTensor Q N.mkQ).ker = (rTensor Q N.subtype).range

Tactic:
rw [← exact_iff]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
N : Submodule R M
⊢ Exact ⇑(rTensor Q N.subtype) ⇑(rTensor Q N.mkQ)
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
hx : x ∈ ↑(Submodule.restrictScalars R (map includeLeft I))
⊢ ∃ y, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y = x

Tactic:
Ideal.map,

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 (span (⇑includeLeft '' ↑I)))
⊢ ∃ y, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y = x
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case h
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 (Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)))
y : A
hy : y ∈ I
⊢ (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) (⟨y, hy⟩ ⊗ₜ[R] 1) = y ⊗ₜ[R] 1

Tactic:
rfl

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

Goal state before:
pp: case h
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 (Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)))
a : A
b : B
x : ↥(Submodule.restrictScalars R I)
y : B
⊢ (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) ((a • x) ⊗ₜ[R] (b * y)) =
    a ⊗ₜ[R] b * (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) (x ⊗ₜ[R] y)

Tactic:
rfl

Goal state after:
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
hx : x ∈ ↑(Submodule.restrictScalars R (map includeRight I))
⊢ ∃ y, (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y = x

Tactic:
Ideal.map,

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 (span (⇑includeRight '' ↑I)))
⊢ ∃ y, (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y = x
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case h
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 (Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)))
y : B
hy : y ∈ I
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) (1 ⊗ₜ[R] ⟨y, hy⟩) = 1 ⊗ₜ[R] y

Tactic:
rfl

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

Goal state before:
pp: case h
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 (Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)))
a : A
b : B
x : A
y : ↥(Submodule.restrictScalars R I)
⊢ (a * x) ⊗ₜ[R] ↑(b • y) = (a * x) ⊗ₜ[R] (b * ↑y)

Tactic:
rfl

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 B
⊢ Submodule.restrictScalars R (map includeRight I) = (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype).range

Tactic:
rw [← SetLike.coe_set_eq]
  apply le_antisymm
  · intro x hx
    simp only [SetLike.mem_coe, LinearMap.mem_range]
    rw [Ideal.map, ← submodule_span_eq] at hx
    refine Submodule.span_induction ?_ ?_ ?_ ?_ hx
    · intro x
      simp only [includeRight_apply, Set.mem_image, SetLike.mem_coe]
      rintro ⟨y, hy, rfl⟩
      use 1 ⊗ₜ[R] ⟨y, hy⟩
      rfl
    · use 0
      simp only [map_zero]
    · rintro x y - - ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩
      use x + y
      simp only [map_add]
    · rintro a x - ⟨x, hx, rfl⟩
      induction a with
      | zero =>
        use 0
        simp only [map_zero, smul_eq_mul, zero_mul]
      | tmul a b =>
        induction x with
        | zero =>
          use 0
          simp only [map_zero, smul_eq_mul, mul_zero]
        | tmul x y =>
          use (a * x) ⊗ₜ[R] (b • y)
          simp only [LinearMap.lTensor_tmul, Submodule.coe_subtype, smul_eq_mul, tmul_mul_tmul]
          rfl
        | add x y hx hy =>
          obtain ⟨x', hx'⟩ := hx
          obtain ⟨y', hy'⟩ := hy
          use x' + y'
          simp only [map_add, hx', smul_add, hy']
      | add a b ha hb =>
        obtain ⟨x', ha'⟩ := ha
        obtain ⟨y', hb'⟩ := hb
        use x' + y'
        simp only [map_add, ha', add_smul, hb']
  · rintro x ⟨y, rfl⟩
    induction y with
    | zero =>
        rw [map_zero]
        apply zero_mem
    | tmul a b =>
        simp only [LinearMap.lTensor_tmul, Submodule.coe_subtype]
        suffices a ⊗ₜ[R] (b : B) = (a ⊗ₜ[R] (1 : B)) * ((1 : A) ⊗ₜ[R] (b : B)) by
          rw [this]
          simp only [Submodule.coe_restrictScalars, SetLike.mem_coe]
          apply Ideal.mul_mem_left
          -- Note: adding `includeRight` as a hint fixes a timeout https://github.com/leanprover-community/mathlib4/pull/8386
          apply Ideal.mem_map_of_mem includeRight
          exact Submodule.coe_mem b
        simp only [Algebra.TensorProduct.tmul_mul_tmul,
          mul_one, one_mul]
    | add x y hx hy =>
        rw [map_add]
        apply Submodule.add_mem _ hx hy

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

Goal state before:
pp: R : Type u_4
inst✝⁶ : CommRing R
A : Type u_6
C : Type u_8
D : Type u_9
inst✝⁵ : Ring A
inst✝⁴ : Ring C
inst✝³ : Ring D
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective ⇑g
this : Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) = (LinearMap.lTensor A g.toLinearMap).ker
⊢ (LinearMap.lTensor A g.toLinearMap.ker.subtype).range =
    (LinearMap.lTensor A (Submodule.restrictScalars R (RingHom.ker g)).subtype).range

Tactic:
rfl

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
inst✝⁹ : Ring A
inst✝⁸ : Ring B
inst✝⁷ : Ring C
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra R C
inst✝³ : Algebra S A
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Surjective ⇑f
this :
  Submodule.restrictScalars R (RingHom.ker (map f (AlgHom.id R C))) =
    (LinearMap.rTensor C (AlgHom.restrictScalars R f).toLinearMap).ker
⊢ (LinearMap.rTensor C (AlgHom.restrictScalars R f).toLinearMap.ker.subtype).range =
    (LinearMap.rTensor C (Submodule.restrictScalars R (RingHom.ker f)).subtype).range

Tactic:
rfl

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
inst✝¹¹ : Ring A
inst✝¹⁰ : Ring B
inst✝⁹ : Ring C
inst✝⁸ : Ring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : Algebra S A
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id S A) g)
⊢ Ideal.map (↑includeLeft) (RingHom.ker f) = Ideal.map (↑(includeLeft.comp (AlgHom.id R A))) (RingHom.ker f)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Central.TensorProduct

Goal state before:
pp: K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
x : B ⊗[K] C
hx : ∃ x_1, (∀ (b : C), b * x_1 = x_1 * b) ∧ includeRight x_1 = x
⊢ ∀ (b : B ⊗[K] C), b * x = x * b

Tactic:
obtain ⟨c, hc0, rfl⟩ := hx

Goal state after:
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
c : C
hc0 : ∀ (b : C), b * c = c * b
⊢ ∀ (b : B ⊗[K] C), b * includeRight c = includeRight c * b
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : N →ₗ[R] P
hf : Injective ⇑f
e : P ≃ₗ[R] Q
⊢ Injective ⇑(rTensor M (↑e ∘ₗ f)) ↔
    Injective ⇑(rTensor M ((↑e ∘ₗ f).range.subtype ∘ₗ ↑(LinearEquiv.ofInjective (↑e ∘ₗ f) ⋯)))

Tactic:
rfl

Goal state after: