mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬p.content = 0
⊢ ↑(normUnit p.content) = ↑1

Tactic:
apply mul_left_cancel₀ hp0

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬p.content = 0
⊢ p.content * ↑(normUnit p.content) = p.content * ↑1
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ r ∣ p.content → ∀ (i : ℕ), r ∣ p.coeff i

Tactic:
intro h i

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : r ∣ p.content
i : ℕ
⊢ r ∣ p.coeff i
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case pos.refine_1
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * c' * a' = p * a

Tactic:
rw [mul_assoc, ha']

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : NormalizedGCDMonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ⇑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : eval₂ f s (C p.content * p.primPart) = 0
⊢ eval₂ f s p.primPart = 0

Tactic:
eval₂_mul,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : NormalizedGCDMonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ⇑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : eval₂ f s (C p.content) * eval₂ f s p.primPart = 0
⊢ eval₂ f s p.primPart = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite

Goal state before:
pp: case mp
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
x : M
⊢ (∃ a, a.1 ≤ normalizedFactors y ∧ ↑a.2 * a.1.prod = x) → x ∣ y

Tactic:
rintro ⟨s, hs, rfl⟩
    rw [(unit_associated_one.mul_right s.fst.prod).dvd_iff_dvd_left, one_mul,
      ← (prod_normalizedFactors hy).dvd_iff_dvd_right]
    exact Multiset.prod_dvd_prod_of_le hs

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
s : Multiset R
⊢ (Multiset.map (fun a ↦ X - C a) s).prod ∣ p ↔ s ≤ p.roots

Tactic:
classical exact
  ⟨fun h =>
    Multiset.le_iff_count.2 fun r => by
      rw [count_roots, le_rootMultiplicity_iff hp, ← Multiset.prod_replicate, ←
        Multiset.map_replicate fun a => X - C a, ← Multiset.filter_eq]
      exact (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map <| s.filter_le _).trans h,
    fun h =>
    (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map h).trans p.prod_multiset_X_sub_C_dvd⟩

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

Goal state before:
pp: 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.degree = ⊥

Tactic:
degree_eq_bot

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
⊢ ¬q.primPart = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: 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.degree = ⊥

Tactic:
degree_eq_bot

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 = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : NormalizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ a ∣ (Associates.mk c ⊓ Associates.mk b).out

Tactic:
rw [dvd_out_iff, le_inf_iff, mk_le_mk_iff_dvd, mk_le_mk_iff_dvd]

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : NormalizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ a ∣ c ∧ a ∣ b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

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

Tactic:
exact factors_one

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

Goal state before:
pp: case neg.inl
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hz : p.count a.factors = 0
⊢ p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors

Tactic:
tauto

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : ¬C (lcm p.content q.content) = 0
a✝ : Nontrivial R
⊢ (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    (p.content ∣ s.content ∧ q.content ∣ s.content) ∧ p.primPart ∣ s.primPart ∧ q.primPart ∣ s.primPart

Tactic:
tauto

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
x : k
⊢ (algebraMap K D) ((algebraMap k K) x) = (algebraMap k D) x

Tactic:
by simp [algebraMap_eq_smul_one, smul_assoc]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
hinj : Function.Injective ⇑(algebraMap R S)
x : A
A_alg : IsAlgebraic R x
p : R[X]
hp₁ : p ≠ 0
hp₂ : (aeval x) p = 0
⊢ ¬p.degree = ⊥

Tactic:
degree_eq_bot

Goal state after:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
hinj : Function.Injective ⇑(algebraMap R S)
x : A
A_alg : IsAlgebraic R x
p : R[X]
hp₁ : p ≠ 0
hp₂ : (aeval x) p = 0
⊢ ¬p = 0
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
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst✝⁶ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)
inst✝⁵ : DirectedSystem F₁ fun x1 x2 x3 ↦ ⇑(f₁ x1 x2 x3)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst✝⁴ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)
inst✝³ : DirectedSystem F₂ fun x1 x2 x3 ↦ ⇑(f₂ x1 x2 x3)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
x✝² y✝ z✝ : (i : ι) × F i
x✝¹ : ∃ i, ∃ (hx : x✝².fst ≤ i) (hy : y✝.fst ≤ i), (f x✝².fst i hx) x✝².snd = (f y✝.fst i hy) y✝.snd
x✝ : ∃ i, ∃ (hx : y✝.fst ≤ i) (hy : z✝.fst ≤ i), (f y✝.fst i hx) y✝.snd = (f z✝.fst i hy) z✝.snd
j : ι
hx : x✝².fst ≤ j
w✝¹ : y✝.fst ≤ j
jeq : (f x✝².fst j hx) x✝².snd = (f y✝.fst j w✝¹) y✝.snd
k : ι
w✝ : y✝.fst ≤ k
hz : z✝.fst ≤ k
keq : (f y✝.fst k w✝) y✝.snd = (f z✝.fst k hz) z✝.snd
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ (f x✝².fst i ⋯) x✝².snd = (f z✝.fst i ⋯) z✝.snd

Tactic:
rw [← map_map' _ hx hji, ← map_map' _ hz hki, jeq, ← keq, map_map', map_map']

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case 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
k : ι
hk : k ∈ Iic i⁺
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : i⁺ ∈ Iic i⁺
h : k ≤ i⁺
x : F i⁺
⊢ (piEquivSucc equiv e hi ⟨k, hk⟩) (f h x) = piLTProj h ((piEquivSucc equiv e hi ⟨i⁺, hj⟩) x)

pp: case inr
ι : 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
j k : ι
hj✝ : j ∈ Iic i⁺
hk : k ∈ Iic i⁺
h : k ≤ j
x : F j
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : j ≤ i
⊢ (piEquivSucc equiv e hi ⟨k, hk⟩) (f h x) = piLTProj h ((piEquivSucc equiv e hi ⟨j, hj✝⟩) x)

Tactic:
· obtain rfl | hk := le_succ_iff_eq_or_le.mp hk
    · simp [InverseSystem.map_self]
    · funext l
      rw [piEquivSucc, piSplitLE_lt (lt_succ hk),
        ← InverseSystem.map_map (f := f) hk (le_succ i), ← H, piLTProj, nat le_rfl]
      simp [piSplitLE_lt (l.2.trans_le hk)]

Goal state after:
case inr
ι : 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
j k : ι
hj✝ : j ∈ Iic i⁺
hk : k ∈ Iic i⁺
h : k ≤ j
x : F j
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : j ≤ i
⊢ (piEquivSucc equiv e hi ⟨k, hk⟩) (f h x) = piLTProj h ((piEquivSucc equiv e hi ⟨j, hj✝⟩) x)
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
inst✝¹ : Small.{u, u_1} R
inst✝ : Module.Finite R M
⊢ Small.{u, u_2} M

Tactic:
by
  have : Small.{u} (⊤ : Submodule R M) :=
    FG.small _ (Module.finite_def.mp inferInstance)
  rwa [← small_univ_iff]

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

Goal state before:
pp: σ : Type u
R : Type v
inst✝¹ : CommSemiring R
p m : ℕ
inst✝ : Finite σ
N : ℕ
this : Finite ↑{f | ∀ (a : σ), f a ≤ N}
⊢ Finite ↑{s | (s.sum fun x e ↦ e) ≤ N}

Tactic:
Set.finite_coe_iff

Goal state after:
σ : Type u
R : Type v
inst✝¹ : CommSemiring R
p m : ℕ
inst✝ : Finite σ
N : ℕ
this : {f | ∀ (a : σ), f a ≤ N}.Finite
⊢ {s | (s.sum fun x e ↦ e) ≤ N}.Finite
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
⊢ Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) =
    Submodule.restrictScalars R (Ideal.map includeRight (RingHom.ker g))

Tactic:
have : (RingHom.ker (map (AlgHom.id R A) g)).restrictScalars R =
    LinearMap.ker (LinearMap.lTensor A (AlgHom.toLinearMap g)) := rfl

Goal state after:
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
⊢ Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) =
    Submodule.restrictScalars R (Ideal.map includeRight (RingHom.ker g))
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
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
h : s ⊆ ↑(mapIncl M' N').range
hM : Submodule.map M₁.subtype M' ≤ M₁
hN : Submodule.map N₁.subtype N' ≤ N₁
⊢ s ⊆ ↑(map (inclusion hM) (inclusion hN)).range

Tactic:
rw [mapIncl,
    show M'.subtype = inclusion hM ∘ₗ M₁.subtype.submoduleMap M' by ext; simp,
    show N'.subtype = inclusion hN ∘ₗ N₁.subtype.submoduleMap N' by ext; simp,
    map_comp] at h

Goal state after:
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
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
hM : Submodule.map M₁.subtype M' ≤ M₁
hN : Submodule.map N₁.subtype N' ≤ N₁
h : s ⊆ ↑(map (inclusion hM) (inclusion hN) ∘ₗ map (M₁.subtype.submoduleMap M') (N₁.subtype.submoduleMap N')).range
⊢ s ⊆ ↑(map (inclusion hM) (inclusion hN)).range
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
s : Set ℕ := {k | x ^ k = 0}
this : {k | x ^ k = 0} = univ
⊢ sInf {k | x ^ k = 0} = 0

Tactic:
simp [this]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
F : Type u_3
inst✝² : FunLike F R S
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ⇑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ x = 0

Tactic:
apply hf

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
F : Type u_3
inst✝² : FunLike F R S
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ⇑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ f x = f 0
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N✝ : Type u_1
P✝ : Type u_2
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✝ : Flat R M
f : N✝ →ₗ[R] P✝
hf : Injective ⇑f
N : Submodule R N✝
P : Submodule R P✝
Nfg : N.FG
Pfg : P.FG
le : N ≤ comap f P
⊢ Injective ⇑(rTensor M (f.restrict le))

Tactic:
← Finite.iff_fg

Goal state after:
R : Type u
M : Type v
N✝ : Type u_1
P✝ : Type u_2
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✝ : Flat R M
f : N✝ →ₗ[R] P✝
hf : Injective ⇑f
N : Submodule R N✝
P : Submodule R P✝
Nfg : Module.Finite R ↥N
Pfg : Module.Finite R ↥P
le : N ≤ comap f P
⊢ Injective ⇑(rTensor M (f.restrict le))
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : (i : ι) → FunLike (H i) (G i) C
inst✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : Monoid R
inst✝¹ : (i : ι) → MulAction R (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
i : ι
x✝ : G i
⊢ ⟦⟨i, 1 • x✝⟩⟧ = ⟦⟨i, x✝⟩⟧

Tactic:
one_smul

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : (i : ι) → FunLike (H i) (G i) C
inst✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : Monoid R
inst✝¹ : (i : ι) → MulAction R (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
i : ι
x✝ : G i
⊢ ⟦⟨i, x✝⟩⟧ = ⟦⟨i, x✝⟩⟧
Module: Mathlib.RingTheory.Flat.Basic

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
M₁ : Type u_5
M₂ : Type u_6
N₂ : Type u_8
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : M₁ →ₗ[R] N₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₂ →ₗ[R] N₂
hi : Function.Injective ⇑i
inst✝ : Module.Flat R M₁
h : ⇑(hf.map hg LinearMap.id i) = ⇑hg.equiv ∘ ⇑(LinearMap.lTensor M₁ i) ∘ ⇑hf.equiv.symm
⊢ Function.Injective ⇑(hf.map hg LinearMap.id i)

Tactic:
simpa [h] using Module.Flat.lTensor_preserves_injective_linearMap i hi

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

Goal state before:
pp: R : Type u_1
C : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring C
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Module.Flat R C
h : ∀ (B : Subalgebra R A), B.FG → IsReduced (C ⊗[R] ↥B)
h_contra : ¬IsReduced (C ⊗[R] A)
D : Subalgebra R A
h_inj : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id C C) D.val)
z : C ⊗[R] ↥D
hx :
  (Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z ≠ 0 ∧
    IsNilpotent ((Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z)
hD : D.FG ∧ (Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z ∈ Subalgebra.baseChange C D
h_notReduced : ¬IsReduced (C ⊗[R] ↥D)
⊢ False

Tactic:
tauto

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

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁸ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁷ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁶ : (i : ι) → FunLike (H i) (G i) C
inst✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : Nonempty ι
inst✝² : (i : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝ : ∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)
i : ι
x✝ : G i
⊢ ⟦⟨i, x✝⟩⟧ * 0 = 0

Tactic:
simp_rw [zero_def i, mul_def, mul_zero]

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

Goal state before:
pp: ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → GroupWithZero (G i)
inst✝² : GroupWithZero C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidWithZeroHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
x✝ y✝ : DirectLimit G f
i : ι
x y : G i
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h (⟦⟨i, x⟩⟧ / ⟦⟨i, y⟩⟧) =
    DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, x⟩⟧ / DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, y⟩⟧

Tactic:
simp_rw [div₀_def, lift_def, map_div₀ (g i)]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommSemiring M
inst✝² : Module ℚ≥0 M
inst✝¹ : IsScalarTower ℚ≥0 M M
inst✝ : SMulCommClass ℚ≥0 M M
s : Finset ι
f : ι → M
n : ℕ
⊢ (↑(#s))⁻¹ ^ n • ∑ p ∈ Fintype.piFinset fun _i ↦ s, ∏ i, f (p i) =
    (↑(#(Fintype.piFinset fun x ↦ s)))⁻¹ • ∑ i ∈ Fintype.piFinset fun x ↦ s, ∏ i_1, f (i i_1)

Tactic:
Fintype.card_piFinset_const,

Goal state after:
ι : Type u_1
M : Type u_4
inst✝³ : CommSemiring M
inst✝² : Module ℚ≥0 M
inst✝¹ : IsScalarTower ℚ≥0 M M
inst✝ : SMulCommClass ℚ≥0 M M
s : Finset ι
f : ι → M
n : ℕ
⊢ (↑(#s))⁻¹ ^ n • ∑ p ∈ Fintype.piFinset fun _i ↦ s, ∏ i, f (p i) =
    (↑(#s ^ n))⁻¹ • ∑ i ∈ Fintype.piFinset fun x ↦ s, ∏ i_1, f (i i_1)
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → f a ≡ 0 [ZMOD n]
hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [ZMOD n]
⊢ ∑ x ∈ s, f x ≡ f a [ZMOD n]

Tactic:
by
  simp only [← modEq_natAbs (n := n), ← ZMod.intCast_eq_intCast_iff, cast_zero, cast_sum] at *
  apply Finset.sum_eq_single <;> assumption

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

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
m : M
hm : m ∈ t
⊢ #({a ∈ ht.toFinset | f a = m}) = Nat.card ↑{a | f a = m}

Tactic:
· rw [Nat.card_eq_card_finite_toFinset (hb _ (by aesop))]
    suffices {a | f a = m} ⊆ ht.toFinset from
      congr_arg (Finset.card ·) (Finset.ext_iff.mpr fun a ↦ by simpa using fun h ↦ this h)
    intro _ h
    simp_all

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case e'_2
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 u_3
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
x : M
hF : ∀ (s : S) (m : M), (h.lift g) (s • f m) = s • g m
⊢ f x = 1 • f x

Tactic:
one_smul

Goal state after:
case e'_2
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 u_3
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
x : M
hF : ∀ (s : S) (m : M), (h.lift g) (s • f m) = s • g m
⊢ f x = f x
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case e'_3
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 u_3
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
x : M
hF : ∀ (s : S) (m : M), (h.lift g) (s • f m) = s • g m
⊢ g x = 1 • g x

Tactic:
one_smul

Goal state after:
case e'_3
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 u_3
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
x : M
hF : ∀ (s : S) (m : M), (h.lift g) (s • f m) = s • g m
⊢ g x = g x