mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
M : Type u_2
τ : Type u_5
f : σ → τ
inst✝ : AddCommMonoid M
x : σ →₀ M
⊢ degree (mapDomain f x) = degree x

Tactic:
simp [mapDomain, sum]

Goal state after:
σ : Type u_1
M : Type u_2
τ : Type u_5
f : σ → τ
inst✝ : AddCommMonoid M
x : σ →₀ M
⊢ ∑ x_1 ∈ x.support, x x_1 = degree x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
u : αˣ
a✝ : 1 ~ᵤ a → (∀ b ∈ 0, Prime b) → ∃ p, a ~ᵤ p ∧ 0 = {p}
hu : p * ↑u = a
hs : ∀ b ∈ p ::ₘ 0, Prime b
hs0 : True
⊢ a ~ᵤ p ∧ p ::ₘ 0 = {p}

Tactic:
exact ⟨Associated.symm ⟨u, hu⟩, rfl⟩

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

Goal state before:
pp: case succ
α : Type u_5
s : Set α
n : ℕ
ih : n • (fun x ↦ single x 1) '' s = {x | degree x = n ∧ ↑x.support ⊆ s}
⊢ (n + 1) • (fun x ↦ single x 1) '' s = {x | degree x = n + 1 ∧ ↑x.support ⊆ s}

Tactic:
rw [succ_nsmul, ih]

Goal state after:
case succ
α : Type u_5
s : Set α
n : ℕ
ih : n • (fun x ↦ single x 1) '' s = {x | degree x = n ∧ ↑x.support ⊆ s}
⊢ {x | degree x = n ∧ ↑x.support ⊆ s} + (fun x ↦ single x 1) '' s = {x | degree x = n + 1 ∧ ↑x.support ⊆ s}
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
hn : ¬n = 0
⊢ (nthRoots n a).card ≤ n

Tactic:
rw [← Nat.cast_le (α := WithBot ℕ)]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
hn : ¬n = 0
⊢ ↑(nthRoots n a).card ≤ ↑n
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
η a : R
ha : a ≠ 0
hη : η ∈ nthRootsFinset n a
⊢ η ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
hη : 0 ∈ nthRootsFinset n a
⊢ False
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
p : R[X]
hp : p.IsPrimitive
⊢ p ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hp : IsPrimitive 0
⊢ False
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
r : R
q : R[X]
hq : p = C r * q
H : IsUnit q
⊢ r ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
q : R[X]
H : IsUnit q
hq : p = C 0 * q
⊢ False
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ a * c ~ᵤ (Classical.choose ⋯).prod

Tactic:
rw [← b_eq]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ b ~ᵤ (Classical.choose ⋯).prod
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
⊢ (insert p.natDegree (p.support.erase p.natDegree)).gcd p.coeff = gcd p.leadingCoeff p.eraseLead.content

Tactic:
Finset.gcd_insert,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
⊢ gcd (p.coeff p.natDegree) ((p.support.erase p.natDegree).gcd p.coeff) = gcd p.leadingCoeff p.eraseLead.content
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
h : (Multiset.map (fun a ↦ X - C a) s).prod ∣ p
r : R
⊢ (X - C r) ^ count r s ∣ p

Tactic:
← Multiset.prod_replicate,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
s : Multiset R
h : (Multiset.map (fun a ↦ X - C a) s).prod ∣ p
r : R
⊢ (replicate (count r s) (X - C r)).prod ∣ p
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ ↑1! ∈ nonZeroDivisors R

Tactic:
Nat.factorial_one,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ ↑1 ∈ nonZeroDivisors R
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ prod ↑a✝ = 0 ↔ ↑a✝ = ⊤

Tactic:
rw [prod_coe, Multiset.prod_eq_zero_iff, Multiset.mem_map, eq_false WithTop.coe_ne_top,
      iff_false, not_exists]

Goal state after:
case coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ ∀ (x : { a // Irreducible a }), ¬(x ∈ a✝ ∧ ↑x = 0)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
⊢ g ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hdf0 : derivative f ≠ 0
hr : derivative f * 0 = f * r
hg : ¬IsRoot 0 a
⊢ False
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 ∣ map f p

Tactic:
refine _root_.trans ?_ (_root_.map_dvd (mapRingHom f) (pow_rootMultiplicity_dvd p a))

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 ∣ (mapRingHom f) ((X - C a) ^ rootMultiplicity a p)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ (X - C b) ^ count b (Multiset.map (⇑f) p.roots) ∣ map f p

Tactic:
← Multiset.prod_replicate,

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ (replicate (count b (Multiset.map (⇑f) p.roots)) (X - C b)).prod ∣ map f p
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: 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
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (↑a.degree, a.leadingCoeff)
    (if a * c = 0 then ⊤ else ↑(a.degree + c.degree), (a * c).leadingCoeff)

Tactic:
split_ifs with hac

Goal state after:
case pos
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
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (↑a.degree, a.leadingCoeff) (⊤, (a * c).leadingCoeff)

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
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (↑a.degree, a.leadingCoeff) (↑(a.degree + c.degree), (a * c).leadingCoeff)
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
d : ℕ
⊢ UniqueFactorizationMonoid (MvPolynomial σ D)

Tactic:
by
  rw [iff_exists_prime_factors]
  intro a ha; obtain ⟨s, a', rfl⟩ := exists_finset_rename a
  obtain ⟨w, h, u, hw⟩ :=
    iff_exists_prime_factors.1 (uniqueFactorizationMonoid_of_fintype s) a' fun h =>
      ha <| by simp [h]
  exact
    ⟨w.map (rename (↑)), fun b hb =>
      let ⟨b', hb', he⟩ := Multiset.mem_map.1 hb
      he ▸ (prime_rename_iff (σ := σ) ↑s).2 (h b' hb'),
      Units.map (@rename s σ D _ (↑)).toRingHom.toMonoidHom u, by
      rw [Multiset.prod_hom, Units.coe_map, AlgHom.toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe,
        AlgHom.toRingHom_toMonoidHom, MonoidHom.coe_coe, ← map_mul, hw]⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h : a * b = c ^ k
a✝ : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
⊢ c ≠ 0

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
a✝ : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
h : a * b = 0 ^ k
⊢ False
Module: Mathlib.Algebra.Central.End

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∀ (a : End R M), (a ∘ₗ ↑g.symm) ∘ₗ ↑f = (↑g.symm ∘ₗ ↑f) ∘ₗ a) ↔ ∃ α, ⇑f = α • ⇑g

Tactic:
comp_assoc,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∀ (a : End R M), a ∘ₗ ↑g.symm ∘ₗ ↑f = ↑g.symm ∘ₗ ↑f ∘ₗ a) ↔ ∃ α, ⇑f = α • ⇑g
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
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)
inst✝ : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F₁ i → F₂ i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)
i : ι
x : F₁ i
y : F₂ i
⊢ ih i ((f₁ ⟨i, x⟩.fst i ⋯) ⟨i, x⟩.snd) ((f₂ ⟨i, y⟩.fst i ⋯) ⟨i, y⟩.snd) = ih i x y

Tactic:
map_self',

Goal state after:
ι : Type u_1
inst✝⁵ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
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)
inst✝ : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F₁ i → F₂ i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)
i : ι
x : F₁ i
y : F₂ i
⊢ ih i ⟨i, x⟩.snd ((f₂ ⟨i, y⟩.fst i ⋯) ⟨i, y⟩.snd) = ih i x 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)
inst✝⁷ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝⁶ : DecidableEq ι
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
g : (i : ι) → G i →ₗ[R] 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)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
g₁ : (i : ι) → G i →ₗ[R] G' i
g₂ : (i : ι) → G' i →ₗ[R] G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i
hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i
i j : ι
h : i ≤ j
⊢ (g₂ j ∘ₗ f' i j h) ∘ₗ g₁ i = f'' i j h ∘ₗ g₂ i ∘ₗ g₁ i

Tactic:
hg₂ i,

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 ι
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
g : (i : ι) → G i →ₗ[R] 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)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
g₁ : (i : ι) → G i →ₗ[R] G' i
g₂ : (i : ι) → G' i →ₗ[R] G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i
hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i
i j : ι
h : i ≤ j
⊢ (f'' i j h ∘ₗ g₂ i) ∘ₗ g₁ i = f'' i j h ∘ₗ g₂ i ∘ₗ g₁ i
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 ι
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
g : (i : ι) → G i →ₗ[R] 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)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
e : (i : ι) → G i ≃ₗ[R] G' i
he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)
i j : ι
h : i ≤ j
⊢ f' i j h = (f' i j h ∘ₗ ↑(e i)) ∘ₗ ↑(e i).symm

Tactic:
comp_assoc,

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 ι
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
g : (i : ι) → G i →ₗ[R] 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)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
e : (i : ι) → G i ≃ₗ[R] G' i
he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)
i j : ι
h : i ≤ j
⊢ f' i j h = f' i j h ∘ₗ ↑(e i) ∘ₗ ↑(e i).symm
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : 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
j k : ι
h : k ≤ j
t : F j
equiv : (j_1 : ↑(Iio j)) → F ↑j_1 ≃ piLT X ↑j_1
nat : IsNatEquiv f equiv
equivLim : F j ≃ ↑(limit f j)
hi : IsSuccPrelimit j
H : ∀ (x : F j) (l : ↑(Iio j)), ↑(equivLim x) l = f ⋯ x
hj : j ∈ Iic j
hk✝ : k ∈ Iic j
hk : k < j
l : ↑(Iio ↑⟨k, hk✝⟩)
⊢ ↑⟨↑l, ⋯⟩ < ↑⟨k, hk⟩

Tactic:
by exact l.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 ι
G' : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (G' i)
inst✝ : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
e : (i : ι) → G i ≃ₗ[R] G' i
he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)
i✝ : ι
g : G' i✝
i j : ι
h : i ≤ j
⊢ f' i j h = (f' i j h ∘ₗ ↑(e i)) ∘ₗ ↑(e i).symm

Tactic:
comp_assoc,

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 ι
G' : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (G' i)
inst✝ : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
e : (i : ι) → G i ≃ₗ[R] G' i
he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)
i✝ : ι
g : G' i✝
i j : ι
h : i ≤ j
⊢ f' i j h = f' i j h ∘ₗ ↑(e i) ∘ₗ ↑(e i).symm
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
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)
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₂ j).comp (f' i j h)).comp (g₁ i) = (f'' i j h).comp ((g₂ i).comp (g₁ i))

Tactic:
hg₂ i,

Goal state after:
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
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)
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
⊢ ((f'' i j h).comp (g₂ i)).comp (g₁ i) = (f'' i j h).comp ((g₂ i).comp (g₁ i))
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 : g.ker = f.range
hgh : RightInverse h ⇑g
r : R
p : P
q : Q
⊢ h (r • p) - r • h p ∈ f.range

Tactic:
simp only [← hfg, mem_ker, map_sub, map_smul, hgh _, sub_self]

Goal state after:
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 : s = univ
⊢ nilpotencyClass x = 0

Tactic:
change sInf _ = 0; simp [s] at this; simp [this]

Goal state after:
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 ∘ₗ rTensor M f) ↔
    Injective ⇑(rTensor M (↑e ∘ₗ f).range.subtype ∘ₗ rTensor M ↑(LinearEquiv.ofInjective (↑e ∘ₗ f) ⋯))

Tactic:
← rTensor_comp

Goal state after:
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) ⋯)))
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
f g : M →ₗ[R] N
h : (baseChangeHom R S M N) f = (baseChangeHom R S M N) g
⊢ f = g

Tactic:
ext m

Goal state after:
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
f g : M →ₗ[R] N
h : (baseChangeHom R S M N) f = (baseChangeHom R S M N) g
m : M
⊢ f m = g m
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
⊢ ¬IsReduced (C ⊗[R] ↥D)

Tactic:
isReduced_iff,

Goal state after:
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
⊢ ¬∀ (x : C ⊗[R] ↥D), IsNilpotent x → x = 0
Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator

Goal state before:
pp: case cons
ι : Type u_1
κ : Type u_2
β : Type u_4
inst✝ : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih : (↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).mulIndicator f = fun a ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑s).PairwiseDisjoint t ∧ ∀ j ∈ ↑s, Disjoint (t i) (t j)
j : κ
⊢ (⋃ i_1 ∈ cons i s hi, t i_1).mulIndicator f j = ∏ i ∈ cons i s hi, (t i).mulIndicator f j

Tactic:
classical
    rw [prod_cons, cons_eq_insert, set_biUnion_insert, mulIndicator_union_of_notMem_inter, ih hs.1]
    exact (Set.disjoint_iff.mp (Set.disjoint_iUnion₂_right.mpr hs.2) ·)

Goal state after: