mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case succ
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ↑u = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
ih : ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x
this : LinearMap.smulRight (f - g) x ∘ₗ (↑n • LinearMap.smulRight (f - g) x) = 0
⊢ LinearMap.id ∘ₗ LinearMap.id + LinearMap.id ∘ₗ (↑n • LinearMap.smulRight (f - g) x) +
      (LinearMap.smulRight (f - g) x ∘ₗ LinearMap.id +
        LinearMap.smulRight (f - g) x ∘ₗ (↑n • LinearMap.smulRight (f - g) x)) =
    LinearMap.id + ↑(n + 1) • LinearMap.smulRight (f - g) x

Tactic:
LinearMap.comp_id,

Goal state after:
case succ
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ↑u = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
ih : ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x
this : LinearMap.smulRight (f - g) x ∘ₗ (↑n • LinearMap.smulRight (f - g) x) = 0
⊢ LinearMap.id + LinearMap.id ∘ₗ (↑n • LinearMap.smulRight (f - g) x) +
      (LinearMap.smulRight (f - g) x + LinearMap.smulRight (f - g) x ∘ₗ (↑n • LinearMap.smulRight (f - g) x)) =
    LinearMap.id + ↑(n + 1) • LinearMap.smulRight (f - g) x
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: case mem
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁸ : CommRing R
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : Module R M
inst✝¹⁵ : AddCommGroup N
inst✝¹⁴ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝¹³ : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra S R
inst✝⁹ : Module S M
inst✝⁸ : Module S N
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S R N
inst✝⁵ : IsTorsionFree S R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M'
inst✝² : Module S M'
inst✝¹ : AddCommGroup N'
inst✝ : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective ⇑i
hN : span R ↑j.range = ⊤
hp : ∀ (m : M') (n : N'), (p (i m)) (j n) ∈ (algebraMap S R).range
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : f x = 0
n : N
n' : N'
⊢ (p (i x)) (j n') = 0

Tactic:
simpa [f] using LinearMap.congr_fun hx n'

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

Goal state before:
pp: case pos.convert_4
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
j : ℕ
hj : j ≠ p.natDegree
h : j < p.natDegree
⊢ j + 0 < p.natDegree

Tactic:
simpa using h

Goal state after:
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: F : Type u
Γ₀ : Type v
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝² : CommRing O
inst✝¹ : Algebra O F
inst✝ : IsPrincipalIdealRing O
hv : v.Integers O
H : DenselyOrdered ↑(range ⇑v)
I : Ideal O := { carrier := ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
x : O
hx₁ : v ((algebraMap O F) x) < 1
hx : v ((algebraMap O F) x) ∈ upperBounds (Iio 1 ∩ range (⇑v ∘ ⇑(algebraMap O F)))
⊢ ∃ y, v ((algebraMap O F) x) < v y ∧ v y < 1

Tactic:
simpa only [Subtype.exists, Subtype.mk_lt_mk, exists_range_iff, exists_prop]
      using H.dense ⟨v (algebraMap O F x), mem_range_self _⟩ ⟨1, 1, v.map_one⟩ hx₁

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : IsHausdorff I N
f : M →ₗ[R] N
g : Hausdorffification I M →ₗ[R] N
hg : g ∘ₗ of I M = f
x✝ : Hausdorffification I M
x : M
⊢ g ((of I M) x) = (g ∘ₗ of I M) x

Tactic:
LinearMap.comp_apply

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : IsHausdorff I N
f : M →ₗ[R] N
g : Hausdorffification I M →ₗ[R] N
hg : g ∘ₗ of I M = f
x✝ : Hausdorffification I M
x : M
⊢ g ((of I M) x) = g ((of I M) x)
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case neg.inl
𝒪 : Type u
K : Type v
inst✝² : CommRing 𝒪
inst✝¹ : Field K
inst✝ : Algebra 𝒪 K
h : ∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
hinj : Function.Injective ⇑(algebraMap 𝒪 K)
this✝² : IsDomain 𝒪
this✝¹ : FaithfulSMul 𝒪 K
this✝ : IsDomain 𝒪
x : K
a : 𝒪
h0 : ¬a = 0
this : (algebraMap 𝒪 K) a ≠ 0
ha : x = (algebraMap 𝒪 K) a
⊢ ∃ x_1, x * (algebraMap 𝒪 K) ↑x_1.2 = (algebraMap 𝒪 K) x_1.1

Tactic:
exact ⟨⟨a, 1⟩, by simpa⟩

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case neg
𝒪 : Type u
K : Type v
inst✝² : CommRing 𝒪
inst✝¹ : Field K
inst✝ : Algebra 𝒪 K
h : ∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
hinj : Function.Injective ⇑(algebraMap 𝒪 K)
this✝² : IsDomain 𝒪
this✝¹ : FaithfulSMul 𝒪 K
this✝ : IsDomain 𝒪
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K) a ∨ x * (algebraMap 𝒪 K) a = 1
h0 : ¬a = 0
this : (algebraMap 𝒪 K) a ≠ 0
⊢ ∃ x_1, x * (algebraMap 𝒪 K) ↑x_1.2 = (algebraMap 𝒪 K) x_1.1

Tactic:
cases ha with

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ x y : R
h : v x ≠ v y
h' : v (x + y) < max (v x) (v y)
vyx : v y < v x
⊢ False

Tactic:
max_eq_left_of_lt vyx

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ x y : R
h : v x ≠ v y
h' : v (x + y) < v x
vyx : v y < v x
⊢ False
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
⊢ ∃ r ∈ I, r ≠ 0

Tactic:
by
      by_contra! h; apply hI; rw [eq_bot_iff]; exact h

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

Goal state before:
pp: K : Type u_7
inst✝¹ : DivisionRing K
Γ₀ : Type u_8
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
⊢ ∃ x, 1 < v x

Tactic:
obtain ⟨x, h0, h1⟩ := hv.exists_lt_one

Goal state after:
K : Type u_7
inst✝¹ : DivisionRing K
Γ₀ : Type u_8
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
x : K
h0 : x ≠ 0
h1 : v x < 1
⊢ ∃ x, 1 < v x
Module: Mathlib.RingTheory.DedekindDomain.Dvr

Goal state before:
pp: A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
⊢ ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)

Tactic:
rintro ⟨y, hy⟩

Goal state after:
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
y : A
hy : y ∈ M
⊢ IsUnit ((algebraMap A (FractionRing A)) ↑⟨y, hy⟩)
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
r : R
⊢ v₁ r = 0 ↔ v₂ r = 0

Tactic:
have : v₁ r = v₁ 0 ↔ v₂ r = v₂ 0 := h.eq_iff

Goal state after:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
r : R
this : v₁ r = v₁ 0 ↔ v₂ r = v₂ 0
⊢ v₁ r = 0 ↔ v₂ r = 0
Module: Mathlib.RingTheory.DedekindDomain.Dvr

Goal state before:
pp: case refine_4
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
⊢ ∃ y, (algebraMap Aₘ (FractionRing A)) y = x

Tactic:
obtain ⟨⟨y, y_mem⟩, hy⟩ := hx.exists_multiple_integral_of_isLocalization M _

Goal state after:
case refine_4
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A (⟨y, y_mem⟩ • x)
⊢ ∃ y, (algebraMap Aₘ (FractionRing A)) y = x
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x : (ofClass w).ValueGroup₀
⊢ h.valueGroup₀Fun (⋯.valueGroup₀Fun x) = x

Tactic:
obtain _ | ⟨r₁, s₁, hr₁, hs₁, rfl⟩ := x.zero_or_exists_mk
    · simp_all [valueGroup₀Fun_zero]
    rw [valueGroup₀Fun_spec h.symm, valueGroup₀Fun_spec h]

Goal state after:
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x y : Associates R
⊢ ↑((associatesEquivIsPrincipal R) (x * y)) = ↑((associatesEquivIsPrincipal R) x) * ↑((associatesEquivIsPrincipal R) y)

Tactic:
rw [← quot_out x, ← quot_out y]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x y : Associates R
⊢ ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out x) * Associates.mk (Quot.out y))) =
    ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out x))) *
      ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out y)))
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_5
inst✝² : CommRing R
inst✝¹ : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst✝ : P.IsPrime
hP : ∀ (x : R), C x ∈ P → x = 0
⊢ P.jacobson = P

Tactic:
by
  by_cases Pb : P = ⊥
  · exact Pb.symm ▸
      jacobson_bot_polynomial_of_jacobson_bot (hR.out isRadical_bot)
  · rw [jacobson_eq_iff_jacobson_quotient_eq_bot]
    let P' := P.comap (C : R →+* R[X])
    have : P'.IsPrime := comap_isPrime C P
    have hR' : IsJacobsonRing (R ⧸ P') := by infer_instance
    obtain ⟨p, pP, p0⟩ := exists_nonzero_mem_of_ne_bot Pb hP
    let x := (Polynomial.map (Ideal.Quotient.mk P') p).leadingCoeff
    have hx : x ≠ 0 := by rwa [Ne, leadingCoeff_eq_zero]
    let φ : R ⧸ P' →+* R[X] ⧸ P := Ideal.quotientMap P (C : R →+* R[X]) le_rfl
    let hφ : Function.Injective ↑φ := quotientMap_injective
    let Rₘ := Localization.Away x
    let Sₘ := (Localization ((Submonoid.powers x).map φ : Submonoid (R[X] ⧸ P)))
    refine jacobson_bot_of_integral_localization (S := R[X] ⧸ P) (R := R ⧸ P') Rₘ Sₘ _ hφ _ hx ?_
    exact isIntegral_isLocalization_polynomial_quotient P p pP

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
tfae_1_to_2 : IsPrincipalIdealRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → IsPrincipalIdealRing R
tfae_1_to_4 : IsPrincipalIdealRing R → IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_6_iff_5 : finrank (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
⊢ (∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n) → ValuationRing R

Tactic:
rw [ValuationRing.iff_ideal_total]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
tfae_1_to_2 : IsPrincipalIdealRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → IsPrincipalIdealRing R
tfae_1_to_4 : IsPrincipalIdealRing R → IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_6_iff_5 : finrank (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
⊢ (∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n) → Std.Total fun x1 x2 ↦ x1 ≤ x2
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Flat R M
m : M
r : R
hr : r ∈ R⁰
h : ⟨r, hr⟩ • m = 0
⊢ (fun x ↦ r • x) m = (fun x ↦ r • x) 0

Tactic:
simpa using h

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

Goal state before:
pp: case inr
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : torsion R M = ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
⊢ Function.Injective ⇑(lift (lsmul R M ∘ₗ Submodule.subtype I))

Tactic:
have hprinc : I.IsPrincipal := IsBezout.isPrincipal_of_FG I hFG
    have : IsPrincipal.generator I ≠ 0 := by
      rwa [ne_eq, ← IsPrincipal.eq_bot_iff_generator_eq_zero]
    apply Function.Injective.of_comp_right _
      (LinearEquiv.rTensor M (Ideal.isoBaseOfIsPrincipal h)).surjective
    rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.coe_comp, LinearEquiv.coe_rTensor, rTensor,
      lift_comp_map, LinearMap.compl₂_id, LinearMap.comp_assoc,
      Ideal.subtype_isoBaseOfIsPrincipal_eq_mul, LinearMap.lift_lsmul_mul_eq_lsmul_lift_lsmul,
      LinearMap.coe_comp]
    rw [← Submodule.isTorsionFree_iff_torsion_eq_bot] at htors
    refine Function.Injective.comp (LinearMap.lsmul_injective this) ?_
    rw [← Equiv.injective_comp (TensorProduct.lid R M).symm.toEquiv]
    convert! Function.injective_id
    ext
    simp

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case hf.hg
R : Type u
S : Type v
T : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : IsJacobsonRing S
inst✝¹ : Algebra R S
inst✝ : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral
v : S[X] ≃ₐ[R] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := ⋯
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : (S[X] ⧸ Q) ≃ₐ[R] T ⧸ P := ⋯
Q' : Ideal S := ⋯
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := ⋯
h_eq : algebraMap R (T ⧸ P) = w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q')))
⊢ w'.IsIntegral

Tactic:
· suffices w'.toRingHom = Ideal.quotientMap Q (Polynomial.C) le_rfl by
        rw [this]
        rw [isIntegral_quotientMap_iff _]
        apply Polynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing
      rfl

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseChange

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
h : (fun i ↦ ⟨P.root i, ⋯⟩) i = (fun i ↦ ⟨P.root i, ⋯⟩) j
⊢ i = j

Tactic:
simpa using h

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseChange

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
h : (fun i ↦ ⟨P.coroot i, ⋯⟩) i = (fun i ↦ ⟨P.coroot i, ⋯⟩) j
⊢ i = j

Tactic:
simpa using h

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field S
inst✝² : Algebra R S
inst✝¹ : IsJacobsonRing R
inst✝ : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ (algebraMap R S).IsIntegral

Tactic:
rw [← f.comp_algebraMap]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field S
inst✝² : Algebra R S
inst✝¹ : IsJacobsonRing R
inst✝ : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ ((↑f).comp (algebraMap R (MvPolynomial ι R))).IsIntegral
Module: Mathlib.LinearAlgebra.RootSystem.RootPositive

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
⊢ P.pairingIn S j i * B.rootLength i = P.pairingIn S i j * B.rootLength j

Tactic:
simpa only [← (algebraMap_injective S R).eq_iff, algebraMap_pairingIn, map_mul,
    B.algebraMap_rootLength] using! B.toInvariantForm.pairing_mul_eq_pairing_mul_swap i j

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
m : M
⊢ P.Polarization m = 0 ↔ P.RootForm m = 0

Tactic:
← flip_comp_polarization_eq_rootForm

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
m : M
⊢ P.Polarization m = 0 ↔ (P.flip.toLinearMap ∘ₗ P.Polarization) m = 0
Module: Mathlib.LinearAlgebra.RootSystem.Basic

Goal state before:
pp: case hf₁
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc : range ⇑P₁.coroot = range ⇑P₂.coroot
hp : P₁.coroot = P₂.coroot → P₁.reflectionPerm = P₂.reflectionPerm
this : IsAddTorsionFree M
i : ι
⊢ (P₁.flip (P₁.coroot i)) (P₁.root i) = 2

Tactic:
exact P₁.coroot_root_two i

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

Goal state before:
pp: case mpr.mpr
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, v x = 1 ↔ v' x = 1
x : K
⊢ v' x ≤ 1 → v x ≤ 1

Tactic:
· intro hx
      rcases lt_or_eq_of_le hx with hx' | hx'
      · have : v' (1 + x) = 1 := by
          rw [← v'.map_one]
          apply map_add_eq_of_lt_left
          simpa
        rw [← h] at this
        rw [show x = -1 + (1 + x) by simp]
        refine le_trans (v.map_add _ _) ?_
        simp [this]
      · rw [← h] at hx'
        exact le_of_eq hx'

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Basic

Goal state before:
pp: case h.hg₁
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
hP₁ : P₁.IsRootSystem
hP₂ : P₂.IsRootSystem
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
i : ι
⊢ (P₁.flip.toPerfPair (P₁.coroot i)) (P₁.root i) = 2

Tactic:
exact P₁.coroot_root_two i

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.OrzechProperty

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : OrzechProperty R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
ι : Type u_3
inst✝ : Fintype ι
b : ι → M
hc : Fintype.card ι = Set.finrank R (Set.range b)
x✝¹ : ↥(span R (Set.range b))
val✝ : M
property✝ : val✝ ∈ span R (Set.range b)
x✝ : ⟨val✝, property✝⟩ ∈ ⊤
⊢ (span R (Set.range b)).subtype ⟨val✝, property✝⟩ ∈
    ↑(span R (⇑(span R (Set.range b)).subtype '' Set.range fun i ↦ ⟨b i, ⋯⟩))

Tactic:
← Set.range_comp

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : OrzechProperty R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
ι : Type u_3
inst✝ : Fintype ι
b : ι → M
hc : Fintype.card ι = Set.finrank R (Set.range b)
x✝¹ : ↥(span R (Set.range b))
val✝ : M
property✝ : val✝ ∈ span R (Set.range b)
x✝ : ⟨val✝, property✝⟩ ∈ ⊤
⊢ (span R (Set.range b)).subtype ⟨val✝, property✝⟩ ∈
    ↑(span R (Set.range (⇑(span R (Set.range b)).subtype ∘ fun i ↦ ⟨b i, ⋯⟩)))
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
i j : ι
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsTorsionFree R N
h2 : IsSMulRegular R 2
this : IsAddTorsionFree M
⊢ P.pairing i j = 1 ∧ P.pairing j i = 4 ↔ P.root j = 2 • P.root i

Tactic:
have : IsAddTorsionFree N := .of_isTorsionFree R N

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
i j : ι
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsTorsionFree R N
h2 : IsSMulRegular R 2
this✝ : IsAddTorsionFree M
this : IsAddTorsionFree N
⊢ P.pairing i j = 1 ∧ P.pairing j i = 4 ↔ P.root j = 2 • P.root i
Module: Mathlib.Algebra.Module.Submodule.Union

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
inst✝⁴ : Field K
inst✝³ : AddCommGroup M
inst✝² : Module K M
inst✝¹ : Finite ι
inst✝ : Infinite K
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
i : ι
contra : v i = 0
⊢ False

Tactic:
exact hv i contra

Goal state after: