mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
⊢ q.prod = (p + factors c).prod

Tactic:
· rw [eqc, Multiset.prod_add]
    congr
    refine associated_iff_eq.mp (factors_prod fun hc => ?_).symm
    refine not_irreducible_zero (hq _ ?_)
    rw [← prod_eq_zero_iff, eqc, hc, mul_zero]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
k : ℕ
⊢ (C r * X ^ k).content = normalize r

Tactic:
← normalize_content,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
k : ℕ
⊢ normalize (C r * X ^ k).content = normalize r
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬X - C t ∣ g
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
⊢ ¬(X - C t) ^ (m - 1 + 1) ∣ C ↑(m - 1 + 1) * (X - C t) ^ (m - 1 + 1 - 1) * g

Tactic:
pow_succ,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬X - C t ∣ g
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
⊢ ¬(X - C t) ^ (m - 1) * (X - C t) ∣ C ↑(m - 1 + 1) * (X - C t) ^ (m - 1 + 1 - 1) * g
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.IsPrimitive ↔ p.content = 1

Tactic:
← normalize_content,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.IsPrimitive ↔ normalize p.content = 1
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.content = 0
⊢ p.primPart.content = 1

Tactic:
← normalize_content,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p.content = 0
⊢ normalize p.primPart.content = 1
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ C ↑(normUnit r) * C ↑(normUnit r)⁻¹ = 1

Tactic:
rw [← map_mul, Units.mul_inv, C_1]

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

Goal state before:
pp: case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
h : p = 0
⊢ rootMultiplicity t 0 = rootMultiplicity t 0 - 1

Tactic:
rootMultiplicity_zero

Goal state after:
case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
h : p = 0
⊢ 0 = 0 - 1
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
p : R[X]
⊢ C ↑(normUnit p.leadingCoeff) * C ↑(normUnit p.leadingCoeff)⁻¹ = 1

Tactic:
rw [← map_mul, Units.mul_inv, C_1]

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 = 0
⊢ False

Tactic:
rw [eq_C_of_degree_le_zero this, hc] at h; simp only [map_zero] at h; contradiction

Goal state after:
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
⊢ (q.primPart * p.primPart).content = 1

Tactic:
← normalize_content,

Goal state after:
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
⊢ normalize (q.primPart * p.primPart).content = 1
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.eraseLead * p.primPart).degree < ↑n

Tactic:
· rw [mul_comm, ← heq, degree_mul, WithBot.add_lt_add_iff_left]
      · apply degree_erase_lt q.primPart_ne_zero
      · rw [Ne, degree_eq_bot]
        apply p.primPart_ne_zero

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

Goal state before:
pp: k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ (p %ₘ (q * C q.leadingCoeff⁻¹)).natDegree < q.natDegree

Tactic:
refine (natDegree_modByMonic_lt p ?_ ?_).trans_le ?_

Goal state after:
case refine_1
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ (q * C q.leadingCoeff⁻¹).Monic

case refine_2
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ q * C q.leadingCoeff⁻¹ ≠ 1

case refine_3
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ (q * C q.leadingCoeff⁻¹).natDegree ≤ q.natDegree
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
⊢ (p * q).content = 1

Tactic:
← normalize_content,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
⊢ normalize (p * q).content = 1
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case neg
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain A
inst✝¹ : IsDomain B
f : A →+* B
inst✝ : DecidablePred fun x ↦ x ∈ f.range
hf : Function.Injective ⇑f
p : A[X]
b : B
h : b ∉ f.range
⊢ 0 = count b (Multiset.map (⇑f) p.roots)

Tactic:
refine (Multiset.count_eq_zero.mpr fun h' ↦ h ?_).symm

Goal state after:
case neg
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain A
inst✝¹ : IsDomain B
f : A →+* B
inst✝ : DecidablePred fun x ↦ x ∈ f.range
hf : Function.Injective ⇑f
p : A[X]
b : B
h : b ∉ f.range
h' : b ∈ Multiset.map (⇑f) p.roots
⊢ b ∈ f.range
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
k : Type y
inst✝³ : Field R
p q : R[X]
inst✝² : Field k
inst✝¹ : DecidableEq R
inst✝ : DecidableEq k
f : R →+* k
x y : R[X]
x✝ : x ≠ 0
ih : EuclideanDomain.gcd (map f (y % x)) (map f x) = map f (EuclideanDomain.gcd (y % x) x)
⊢ EuclideanDomain.gcd (map f y % map f x) (map f x) = map f (EuclideanDomain.gcd x y)

Tactic:
← map_mod,

Goal state after:
R : Type u
k : Type y
inst✝³ : Field R
p q : R[X]
inst✝² : Field k
inst✝¹ : DecidableEq R
inst✝ : DecidableEq k
f : R →+* k
x y : R[X]
x✝ : x ≠ 0
ih : EuclideanDomain.gcd (map f (y % x)) (map f x) = map f (EuclideanDomain.gcd (y % x) x)
⊢ EuclideanDomain.gcd (map f (y % x)) (map f x) = map f (EuclideanDomain.gcd x y)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid

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

Tactic:
rw [← mk_dvd_mk, Associates.quot_out, congr_fun₂ dvd_eq_le, le_inf_iff,
      mk_le_mk_iff_dvd, mk_le_mk_iff_dvd]
    exact ⟨hac, hab⟩

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
⊢ (C a * X ^ n).rootSet S = {0}

Tactic:
by
  rw [C_mul_X_pow_eq_monomial, rootSet_monomial hn ha]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a : Associates α
n : ℕ
h : (a ^ n).factors = n • a.factors
⊢ (a ^ (n + 1)).factors = (n + 1) • a.factors

Tactic:
pow_succ,

Goal state after:
case succ
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a : Associates α
n : ℕ
h : (a ^ n).factors = n • a.factors
⊢ (a ^ n * a).factors = (n + 1) • a.factors
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case pos
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 : p = 0 ∨ q = 0
⊢ p ∣ s ∧ q ∣ s ↔ C (lcm p.content q.content) * r ∣ s

Tactic:
rcases hpq with (hpq | hpq) <;> simp [hpq, hs]

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

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

pp: case neg
F : Type u_1
inst✝ : DivisionSemiring F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : C x = f
hx : ¬x = 0
⊢ False

Tactic:
· rw [← hf, hx, map_zero] at h; exact not_irreducible_zero h

Goal state after:
case neg
F : Type u_1
inst✝ : DivisionSemiring F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : C x = f
hx : ¬x = 0
⊢ False
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case h
α : 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
⊢ a = 1 ^ k

Tactic:
hk0,

Goal state after:
case h
α : 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 ^ 0
a✝ : Nontrivial α
hk0 : k = 0
⊢ a = 1 ^ 0
Module: Mathlib.Algebra.Central.Basic

Goal state before:
pp: K : Type u
inst✝⁴ : CommSemiring K
D D' : Type v
inst✝³ : Semiring D
inst✝² : Algebra K D
h : IsCentral K D
inst✝¹ : Semiring D'
inst✝ : Algebra K D'
e : D ≃ₐ[K] D'
x : D'
hx : x ∈ Subalgebra.center K D'
k : K
hk : (ofId K D).toRingHom k = e.symm x
⊢ (ofId K D').toRingHom k = x

Tactic:
by simpa [ofId] using congr(e $hk)

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_ne : (aeval x) p.divX ≠ 0
⊢ (aeval x) (p.divX * X + C (p.coeff 0)) = (aeval x) p.divX * x + (algebraMap K L) (p.coeff 0)

Tactic:
rw [map_add, map_mul, aeval_X, aeval_C]

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

Goal state before:
pp: σ : Type u
R : Type v
inst✝ : CommSemiring R
s : Set (σ →₀ ℕ)
m : σ →₀ ℕ
r : R
⊢ (monomial m) r ∈ restrictSupport R s ↔ m ∈ s ∨ r = 0

Tactic:
by_cases r = 0 <;> simp [mem_restrictSupport_iff, support_monomial, *]

Goal state after:
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
this : Small.{u, u_2} ↥⊤
⊢ Small.{u, u_2} M

Tactic:
← small_univ_iff

Goal state after:
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
this : Small.{u, u_2} ↥⊤
⊢ Small.{u, u_2} ↑Set.univ
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Small.{u, u_1} R
inst✝ : FiniteType R S
this : Small.{u, u_2} ↥⊤
⊢ Small.{u, u_2} S

Tactic:
← small_univ_iff

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Small.{u, u_1} R
inst✝ : FiniteType R S
this : Small.{u, u_2} ↥⊤
⊢ Small.{u, u_2} ↑Set.univ
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

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

Tactic:
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]

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

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
r : R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
hr : IsNilpotent r
f : F
⊢ f (r ^ Exists.choose hr) = 0

Tactic:
hr.choose_spec,

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
r : R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
hr : IsNilpotent r
f : F
⊢ f 0 = 0
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : N' ⧸ f.range →ₗ[R] N'' := g.range.subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑(f.range.quotEquivOfEq g.ker ⋯)
exact1 : Function.Exact ⇑(lTensor M f) ⇑(lTensor M π)
⊢ Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)

Tactic:
rw [show g = ι.comp π from rfl, lTensor_comp]

Goal state after:
R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : N' ⧸ f.range →ₗ[R] N'' := g.range.subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑(f.range.quotEquivOfEq g.ker ⋯)
exact1 : Function.Exact ⇑(lTensor M f) ⇑(lTensor M π)
⊢ Function.Exact ⇑(lTensor M f) ⇑(lTensor M ι ∘ₗ lTensor M π)
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₁
⊢ Function.Injective ⇑(hf.map hg LinearMap.id i)

Tactic:
have h : hf.map hg LinearMap.id i = hg.equiv ∘ i.lTensor M₁ ∘ hf.equiv.symm :=
    funext fun x ↦ hf.inductionOn x (by simp) (by simp) (fun _ _ hx hy ↦ by simp [hx, hy])
  simpa [h] using Module.Flat.lTensor_preserves_injective_linearMap i hi

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x✝ : (n × n) × n × n
i0 j0 k0 l0 : n
⊢ (mulLeftRightMatrix_inv R n ∘ₗ (mulLeftRight R (Matrix n n R)).toLinearMap)
      (((stdBasis R n n).tensorProduct ((stdBasis R n n).map (opLinearEquiv R))) ((i0, j0), k0, l0)) =
    LinearMap.id (((stdBasis R n n).tensorProduct ((stdBasis R n n).map (opLinearEquiv R))) ((i0, j0), k0, l0))

Tactic:
simp [stdBasis_eq_single, ite_and, Fintype.sum_prod_type,
      mulLeftRight_apply, single, Matrix.mul_apply]

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 : ι) → Monoid (G i)
inst✝² : Monoid 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
⊢ ⟦⟨i, x✝ ^ (n + 1)⟩⟧ = ⟦⟨i, x✝ ^ n⟩⟧ * ⟦⟨i, x✝⟩⟧

Tactic:
pow_succ,

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 : ι) → Monoid (G i)
inst✝² : Monoid 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
⊢ ⟦⟨i, x✝ ^ n * x✝⟩⟧ = ⟦⟨i, x✝ ^ n⟩⟧ * ⟦⟨i, x✝⟩⟧
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
h : #s = #t
⊢ (s ∪ t).dens = (t \ s).dens + t.dens

Tactic:
union_comm s,

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
h : #s = #t
⊢ (t ∪ s).dens = (t \ s).dens + t.dens
Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps

Goal state before:
pp: case i_surj
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := F.intervalGapsWithin h a b
z : α × α
hz : z ∈ F
i : ℕ
hi₁ : i ∈ Set.Iio k
hi₂ : (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) i = z
⊢ ∃ a, ∃ (_ : a ∈ range k), ((p ↑a).2, (p ↑a.succ).1) = z

Tactic:
exact ⟨i, by grind, hi₂⟩

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
e : M₁ ⊗[R] M₂ ≃ₗ[R] M
he : ∀ (x : M₁) (y : M₂), e (x ⊗ₜ[R] y) = (f x) y
this : TensorProduct.lift f = ↑e
⊢ IsTensorProduct f

Tactic:
simpa [IsTensorProduct, this] using e.bijective

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case succ
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
i : M₁ →ₗ[R] M₁
j : M₂ →ₗ[R] M₂
n : ℕ
ih : hf.map hf i j ^ n = hf.map hf (i ^ n) (j ^ n)
⊢ hf.map hf i j ^ (n + 1) = hf.map hf (i ^ (n + 1)) (j ^ (n + 1))

Tactic:
simp only [pow_succ, ih, hf.map_mul]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ (F.intervalGapsWithin h a b ↑j').1

Tactic:
have := hFab (F.intervalGapsWithin_mapsTo h a b (x := j' - 1) (by grind)) |>.right.left

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
this :
  ((fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (j' - 1)).1 ≤
    ((fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (j' - 1)).2
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ (F.intervalGapsWithin h a b ↑j').1
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons
α : Type u_1
x x' : α
xs : List α
ih : x ∉ xs → (map (fun y ↦ s(x, y)) xs).Disjoint xs.sym2
h : x ∉ x' :: xs
⊢ (map (fun y ↦ s(x, y)) (x' :: xs)).Disjoint (x' :: xs).sym2

Tactic:
aesop (add simp mk_mem_sym2_iff, unfold safe List.Disjoint)

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
⊢ (s.sym n).Nonempty ↔ n = 0 ∨ s.Nonempty

Tactic:
by
  contrapose!; exact sym_eq_empty

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: 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
P : Type u_2
Q : Type u_3
inst✝²⁴ : AddCommMonoid P
inst✝²³ : Module R P
inst✝²² : AddCommMonoid Q
inst✝²¹ : Module S Q
inst✝²⁰ : Module R Q
inst✝¹⁹ : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst✝¹⁸ : CommSemiring T
inst✝¹⁷ : Algebra R T
inst✝¹⁶ : Algebra S T
inst✝¹⁵ : IsScalarTower R S T
inst✝¹⁴ : AddCommMonoid O
inst✝¹³ : Module R O
inst✝¹² : Module S O
inst✝¹¹ : Module T O
inst✝¹⁰ : IsScalarTower S T O
inst✝⁹ : IsScalarTower R S O
inst✝⁸ : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst✝⁷ : CommSemiring R'
inst✝⁶ : CommSemiring S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout R S R' S'
x y : S ⊗[R] R'
⊢ ⋯.equiv (x * y) = ⋯.equiv x * ⋯.equiv y

Tactic:
induction x with
    | zero => simp
    | add x y _ _ => simp [*, add_mul]
    | tmul a b =>
      induction y with
      | zero => simp
      | add x y _ _ => simp [*, mul_add]
      | tmul x y => simp [IsBaseChange.equiv_tmul, Algebra.smul_def, mul_mul_mul_comm]

Goal state after: