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

Goal state before:
pp: case refine_4.refine_3
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ Coheyting.boundary (𝓟 q.1) ⊔ Coheyting.boundary q.2 ≤ q.2

Tactic:
boundary_principal,

Goal state after:
case refine_4.refine_3
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ ⊥ ⊔ Coheyting.boundary q.2 ≤ q.2
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∑ T ∈ powersetCard (#S - k) S, ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a) =
    ∑ x ∈ powersetCard (#S - k) S ×ˢ S with
      match x with
      | (T, i) => i ∈ T,
      match x with
      | (T, i) => ∏ a ∈ T.erase i, (X - C a)

Tactic:
by
        rw [← sum_finset_product']
        grind

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ (∑ x ∈ powersetCard (#S - (k + 1)) S ×ˢ S with
      match x with
      | (T, i) => i ∉ T,
      match x with
      | (T, i) => ∏ a ∈ T, (X - C a)) =
    ∑ T ∈ powersetCard (#S - (k + 1)) S, ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a)

Tactic:
by
        rw [← sum_finset_product']
        grind

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
p : Finset ι
f : ι → M
⊢ Associates.mk (Multiset.map f p.val).prod = Associates.mk (∏ i ∈ p, f i)

Tactic:
← Finset.prod_eq_multiset_prod

Goal state after:
ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
p : Finset ι
f : ι → M
⊢ Associates.mk (∏ x ∈ p, f x) = Associates.mk (∏ i ∈ p, f i)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Subsingleton Mˣ
x : M
⊢ factors x = normalizedFactors x

Tactic:
unfold normalizedFactors

Goal state after:
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Subsingleton Mˣ
x : M
⊢ factors x = Multiset.map normalize (factors x)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
x✝ : α
⊢ normalize x✝ = (Associates.out ∘ Associates.mk) x✝

Tactic:
rw [Function.comp_apply, Associates.out_mk]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
⊢ normalizedFactors a = normalizedFactors b

Tactic:
unfold normalizedFactors

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
⊢ Multiset.map normalize (factors a) = Multiset.map normalize (factors b)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p x : α
h : x ≠ 0
x✝ : Irreducible p ∧ normalize p = p ∧ p ∣ x
h₁ : Irreducible p
h₂ : normalize p = p
h₃ : p ∣ x
y : α
hy₁ : y ∈ factors x
hy₂ : p ~ᵤ y
⊢ normalize y = p

Tactic:
by
    rwa [← h₂, normalize_eq_normalize_iff_associated, Associated.comm]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
⊢ X.content = 1

Tactic:
rw [← mul_one X, content_X_mul, content_one]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
i : ℕ
hi : i ∈ p.support.erase p.natDegree
⊢ p.coeff i = p.eraseLead.coeff i

Tactic:
rw [Finset.mem_erase] at hi

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
i : ℕ
hi : i ≠ p.natDegree ∧ i ∈ p.support
⊢ p.coeff i = p.eraseLead.coeff i
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p q : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = eval (f i) q
hcard : max p.natDegree q.natDegree < Fintype.card ι
⊢ p - q = 0

Tactic:
apply eq_zero_of_natDegree_lt_card_of_eval_eq_zero _ hf

Goal state after:
case heval
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p q : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = eval (f i) q
hcard : max p.natDegree q.natDegree < Fintype.card ι
⊢ ∀ (i : ι), eval (f i) (p - q) = 0

case hcard
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p q : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = eval (f i) q
hcard : max p.natDegree q.natDegree < Fintype.card ι
⊢ (p - q).natDegree < Fintype.card ι
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ (X - C (f a)) ^ rootMultiplicity a p ∣ ((mapRingHom f) X - (mapRingHom f) (C a)) ^ rootMultiplicity a p

Tactic:
coe_mapRingHom,

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ (X - C (f a)) ^ rootMultiplicity a p ∣ (map f X - map f (C a)) ^ rootMultiplicity a p
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (↑a.degree, a.leadingCoeff) (↑(a.degree + c.degree), (a * c).leadingCoeff)

Tactic:
simp only [Polynomial.leadingCoeff_mul]

Goal state after:
case neg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (↑a.degree, a.leadingCoeff)
    (↑(a.degree + c.degree), a.leadingCoeff * c.leadingCoeff)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
⊢ map f x ∣ map f y ↔ x ∣ y

Tactic:
· classical
    rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq (Associates α)
m p : Associates α
h₁ : m ≠ 0
h₂ : Irreducible p
k : ℕ
⊢ p ^ k ≤ m ↔ k ≤ bcount ⟨p, h₂⟩ m.factors

Tactic:
by
  rcases Associates.exists_non_zero_rep h₁ with ⟨m, hm, rfl⟩
  have := nontrivial_of_ne _ _ hm
  rw [bcount.eq_def, factors_mk, Multiset.le_count_iff_replicate_le, ← factors_le,
    factors_prime_pow, factors_mk, WithTop.coe_le_coe] <;> assumption

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

Goal state before:
pp: K : Type u_1
inst✝ : CommRing K
f : K[X]
a : K
⊢ ?m.57

Tactic:
by apply congrArg derivative <| X_sub_C_mul_divByMonic_eq_sub_modByMonic f a

Goal state after:
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
inst✝ : Nontrivial R
n : ℤ
⊢ IsAlgebraic R ↑n

Tactic:
← map_intCast (algebraMap R A)

Goal state after:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
n : ℤ
⊢ IsAlgebraic R ((algebraMap R A) ↑n)
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.Surjective ⇑f
hg : Function.Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : R[X]
h1 : map (↑f) q ≠ 0
h2 : (aeval (↑g a)) (map (↑f) q) = 0
⊢ (aeval (↑g a)) (map (↑f) q) = 0

Tactic:
h2

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.Surjective ⇑f
hg : Function.Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : R[X]
h1 : map (↑f) q ≠ 0
h2 : (aeval (↑g a)) (map (↑f) q) = 0
⊢ 0 = 0
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case fst
ι✝ : 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 : piLT X i × X i
j : ↑(Iio i)
⊢ ((fun f ↦ (fun j ↦ f ⟨↑j, ⋯⟩, f ⟨i, ⋯⟩)) ((fun f j ↦ if h : ↑j = i then ⋯ ▸ f.2 else f.1 ⟨↑j, ⋯⟩) f)).1 j = f.1 j

pp: case snd
ι✝ : 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 : piLT X i × X i
⊢ ((fun f ↦ (fun j ↦ f ⟨↑j, ⋯⟩, f ⟨i, ⋯⟩)) ((fun f j ↦ if h : ↑j = i then ⋯ ▸ f.2 else f.1 ⟨↑j, ⋯⟩) f)).2 = f.2

Tactic:
exacts [dif_neg j.2.ne, dif_pos rfl]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : Submodule R P
hN : N.FG
x y : ↥N ⊗[R] M
eq : (LinearMap.rTensor M N.subtype) x = (LinearMap.rTensor M N.subtype) y
⊢ ∃ N', N'.FG ∧ ∃ (h : N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y

Tactic:
lift N to {N : Submodule R P // N.FG} using hN

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : { x // x.FG }
x y : ↥↑N ⊗[R] M
eq : (LinearMap.rTensor M (↑N).subtype) x = (LinearMap.rTensor M (↑N).subtype) y
⊢ ∃ N', N'.FG ∧ ∃ (h : ↑N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y
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)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝³ : DecidableEq ι
P : Type u_4
inst✝² : AddCommMonoid P
g✝¹ : (i : ι) → G i →+ P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝¹ j) ((f i j hij) x) = (g✝¹ i) x
G' : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j
g✝ : (i : ι) → G i →+ G' i
hg : ∀ (i j : ι) (h : i ≤ j), (g✝ j).comp (f i j h) = (f' i j h).comp (g✝ i)
i j : ι
h : i ≤ j
g : G i
⊢ ((of G' f' j).comp (g✝ j)) ((f i j h) g) = ((of G' f' i).comp (g✝ i)) g

Tactic:
have eq1 := DFunLike.congr_fun (hg i j h) g
    simp only [AddMonoidHom.coe_comp, Function.comp_apply] at eq1 ⊢
    rw [eq1, of_f]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
q : Q
n : N
⊢ g n ∈ Submodule.comap ((TensorProduct.mk R P Q).flip q) (rTensor Q g).range

Tactic:
exact ⟨n ⊗ₜ[R] q, rfl⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
⊢ (lTensor Q g).range = (lTensor Q g.range.subtype).range

Tactic:
have : g = (Submodule.subtype _).comp g.rangeRestrict := rfl

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ (lTensor Q g).range = (lTensor Q g.range.subtype).range
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case tmul
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
q : Q
n : N
⊢ ∃ a, (rTensor Q g) a = g n ⊗ₜ[R] q

Tactic:
exact ⟨n ⊗ₜ[R] q, rfl⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
⊢ (rTensor Q g).range = (rTensor Q g.range.subtype).range

Tactic:
have : g = (Submodule.subtype _).comp g.rangeRestrict := rfl

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ (rTensor Q g).range = (rTensor Q g.range.subtype).range
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 + h p') ⊗ₜ[R] q ∈ (rTensor Q f).range

Tactic:
← 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: 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
r : R
p : P
q : Q
⊢ h (r • p) ⊗ₜ[R] q - (r • h p) ⊗ₜ[R] q ∈ (rTensor Q f).range

Tactic:
← 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
r : R
p : P
q : Q
⊢ (h (r • p) - r • h p) ⊗ₜ[R] q ∈ (rTensor Q f).range
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
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h ⇑g
y : N ⊗[R] Q
n : N
q : Q
⊢ h (g n) ⊗ₜ[R] q - n ⊗ₜ[R] q ∈ (rTensor Q f).range

Tactic:
← 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
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h ⇑g
y : N ⊗[R] Q
n : N
q : Q
⊢ (h (g n) - n) ⊗ₜ[R] q ∈ (rTensor Q f).range
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a.refine_1
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)))
⊢ ∀ x ∈ ⇑includeRight '' ↑I, ∃ y, (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y = x

Tactic:
intro x
      simp only [includeRight_apply, Set.mem_image, SetLike.mem_coe]
      rintro ⟨y, hy, rfl⟩
      use 1 ⊗ₜ[R] ⟨y, hy⟩
      rfl

Goal state after:
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
s : Set (M ⊗[R] N)
hs : s.Finite
w✝ : Submodule R M
N' : Submodule R N
left✝ : Module.Finite R ↥w✝
hfin : Module.Finite R ↥N'
h : s ⊆ ↑(mapIncl w✝ N').range
⊢ ∃ N', Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.lTensor M N'.subtype).range

Tactic:
refine ⟨N', hfin, ?_⟩

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
s : Set (M ⊗[R] N)
hs : s.Finite
w✝ : Submodule R M
N' : Submodule R N
left✝ : Module.Finite R ↥w✝
hfin : Module.Finite R ↥N'
h : s ⊆ ↑(mapIncl w✝ N').range
⊢ s ⊆ ↑(LinearMap.lTensor M N'.subtype).range
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
S : Type u_4
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : Flat R N
⊢ Injective ⇑(baseChangeHom R S M N)

Tactic:
by
  intro f g h
  ext m
  simpa using Flat.tensorProduct_mk_injective R N S <| LinearMap.congr_fun h (1 ⊗ₜ[R] m)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
⊢ (AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e)) =
    (↑(LinearEquiv.conjAlgEquiv R ↑e)).comp (AlgHom.mulLeftRight R A)

Tactic:
by
  ext <;> simp

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✝¹ : (i : ι) → InvolutiveStar (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
i : ι
x : G i
⊢ star (star ⟦⟨i, x⟩⟧) = ⟦⟨i, x⟩⟧

Tactic:
rw [star_def, star_def, star_star]

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 : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
i : ι
x✝ : G i
⊢ Pow.pow ⟦⟨i, x✝⟩⟧ 0 = 1

Tactic:
Pow.pow,

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✝⁴ : Nonempty ι
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
i : ι
x✝ : G i
⊢ map f f (fun x x_1 ↦ x_1 ^ 0) ⋯ ⟦⟨i, x✝⟩⟧ = 1
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 : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
n : ℕ
i : ι
x : G i
⊢ Pow.pow ⟦⟨i, x⟩⟧ ↑n.succ = Pow.pow ⟦⟨i, x⟩⟧ ↑n * ⟦⟨i, x⟩⟧

Tactic:
Pow.pow,

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✝⁴ : Nonempty ι
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
n : ℕ
i : ι
x : G i
⊢ map f f (fun x x_1 ↦ x_1 ^ ↑n.succ) ⋯ ⟦⟨i, x⟩⟧ = map f f (fun x x_1 ↦ x_1 ^ ↑n) ⋯ ⟦⟨i, x⟩⟧ * ⟦⟨i, x⟩⟧