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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : (C R n).comp ((2 * X).comp (Polynomial.C ⅟2 * X)) = (2 * T R n).comp (Polynomial.C ⅟2 * X)
⊢ C R n = 2 * (T R n).comp (Polynomial.C ⅟2 * X)

Tactic:
mul_comp,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this :
  (C R n).comp (comp 2 (Polynomial.C ⅟2 * X) * X.comp (Polynomial.C ⅟2 * X)) =
    comp 2 (Polynomial.C ⅟2 * X) * (T R n).comp (Polynomial.C ⅟2 * X)
⊢ C R n = 2 * (T R n).comp (Polynomial.C ⅟2 * X)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (S R (↑n + 1)).comp (2 * X) = U R (↑n + 1)
ih2 : (S R ↑n).comp (2 * X) = U R ↑n
⊢ (X * S R (↑n + 1)).comp (2 * X) - (S R ↑n).comp (2 * X) = 2 * X * U R (↑n + 1) - U R ↑n

Tactic:
mul_comp,

Goal state after:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (S R (↑n + 1)).comp (2 * X) = U R (↑n + 1)
ih2 : (S R ↑n).comp (2 * X) = U R ↑n
⊢ X.comp (2 * X) * (S R (↑n + 1)).comp (2 * X) - (S R ↑n).comp (2 * X) = 2 * X * U R (↑n + 1) - U R ↑n
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (S R (-↑n)).comp (2 * X) = U R (-↑n)
ih2 : (S R (-↑n + 1)).comp (2 * X) = U R (-↑n + 1)
⊢ (X * S R (-↑n)).comp (2 * X) - (S R (-↑n + 1)).comp (2 * X) = 2 * X * U R (-↑n) - U R (-↑n + 1)

Tactic:
mul_comp,

Goal state after:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (S R (-↑n)).comp (2 * X) = U R (-↑n)
ih2 : (S R (-↑n + 1)).comp (2 * X) = U R (-↑n + 1)
⊢ X.comp (2 * X) * (S R (-↑n)).comp (2 * X) - (S R (-↑n + 1)).comp (2 * X) = 2 * X * U R (-↑n) - U R (-↑n + 1)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : (S R n).comp ((2 * X).comp (Polynomial.C ⅟2 * X)) = (U R n).comp (Polynomial.C ⅟2 * X)
⊢ S R n = (U R n).comp (Polynomial.C ⅟2 * X)

Tactic:
mul_comp,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : (S R n).comp (comp 2 (Polynomial.C ⅟2 * X) * X.comp (Polynomial.C ⅟2 * X)) = (U R n).comp (Polynomial.C ⅟2 * X)
⊢ S R n = (U R n).comp (Polynomial.C ⅟2 * X)
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 + ↑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

Tactic:
this,

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 + ↑n • LinearMap.smulRight (f - g) x + (LinearMap.smulRight (f - g) x + 0) =
    LinearMap.id + ↑(n + 1) • LinearMap.smulRight (f - g) x
Module: Mathlib.LinearAlgebra.Matrix.BaseChange

Goal state before:
pp: m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : m) (j : n), A i j ∈ K
i : n
j : m
⊢ B i j ∈ K

Tactic:
by
  cases nonempty_fintype m
  let A' : Matrix m m K := of fun i j ↦ ⟨A.submatrix id e i j, h_mem i (e j)⟩
  have hA' : A'.map K.subtype = A.submatrix id e := rfl
  have hA : IsUnit A' := by
    have h_unit : IsUnit (A.submatrix id e) :=
      .of_mul_eq_one (B.submatrix e id) (by simpa)
    have h_det : (A.submatrix id e).det = K.subtype A'.det := by
      simp [A', K.subtype.map_det, map, submatrix]
    simpa [isUnit_iff_isUnit_det, h_det] using! h_unit
  obtain ⟨B', hB⟩ := isUnit_iff_exists_inv.mp hA
  suffices (B'.submatrix e.symm id).map K.subtype = B by simp [← this]
  replace hB : A * (B'.submatrix e.symm id).map K.subtype = 1 := by
    replace hB := congr_arg (fun C ↦ C.map K.subtype) hB
    simp_rw [Matrix.map_mul] at hB
    rw [hA', ← e.symm_symm, ← submatrix_id_mul_left] at hB
    simpa using! hB
  classical
  simpa [← Matrix.mul_assoc, (mul_eq_one_comm_of_equiv e).mp hAB] using! congr_arg (B * ·) hB

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : (range ⇑r).Finite
h_two : ∀ (i : ι), (c i) (r i) = 2
h_mapsTo : ∀ (i : ι), MapsTo (⇑(preReflection (r i) (c i))) (range ⇑r) (range ⇑r)
i j : ι
hij : (span R (range ⇑r)).subtype.dualMap (c i) = (span R (range ⇑r)).subtype.dualMap (c j)
this : ∀ (k : ι), (c i) (r k) = (c j) (r k)
⊢ (c i) (r j) = 2

Tactic:
this,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : (range ⇑r).Finite
h_two : ∀ (i : ι), (c i) (r i) = 2
h_mapsTo : ∀ (i : ι), MapsTo (⇑(preReflection (r i) (c i))) (range ⇑r) (range ⇑r)
i j : ι
hij : (span R (range ⇑r)).subtype.dualMap (c i) = (span R (range ⇑r)).subtype.dualMap (c j)
this : ∀ (k : ι), (c i) (r k) = (c j) (r k)
⊢ (c j) (r j) = 2
Module: Mathlib.LinearAlgebra.Span.TensorProduct

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
p : Submodule R M
inst✝¹ : Algebra.IsEpi R A
inst✝ : Module.Flat R A
f : A ⊗[R] ↥(span A ↑p) →ₗ[A] ↥(span A ↑p) :=
  AlgebraTensorModule.lift (restrictScalarsₗ R A (↥(span A ↑p)) (↥(span A ↑p)) A ∘ₗ lsmul A ↥(span A ↑p))
g : A ⊗[R] ↥p →ₗ[R] A ⊗[R] ↥(span A ↑p) := lTensor A (inclusionSpan A p)
hf : Injective ⇑f
hg : Injective ⇑g
this : ↑R (tensorToSpan A p) = ↑R f ∘ₗ g
⊢ Injective ⇑(↑R (tensorToSpan A p))

Tactic:
this,

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
p : Submodule R M
inst✝¹ : Algebra.IsEpi R A
inst✝ : Module.Flat R A
f : A ⊗[R] ↥(span A ↑p) →ₗ[A] ↥(span A ↑p) :=
  AlgebraTensorModule.lift (restrictScalarsₗ R A (↥(span A ↑p)) (↥(span A ↑p)) A ∘ₗ lsmul A ↥(span A ↑p))
g : A ⊗[R] ↥p →ₗ[R] A ⊗[R] ↥(span A ↑p) := lTensor A (inclusionSpan A p)
hf : Injective ⇑f
hg : Injective ⇑g
this : ↑R (tensorToSpan A p) = ↑R f ∘ₗ g
⊢ Injective ⇑(↑R f ∘ₗ g)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℤ
m : ℕ
ih1 : C R (-↑m * n) = (C R (-↑m)).comp (C R n)
ih2 : C R ((-↑m + 1) * n) = (C R (-↑m + 1)).comp (C R n)
⊢ C R ((-↑m - 1) * n) = (C R (-↑m - 1)).comp (C R n)

Tactic:
have h₁ := C_mul_C R ((-m) * n) n
    have h₂ := congr_arg (comp · (C R n)) <| C_add_two R (-m - 1)
    simp only [sub_comp, mul_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + C R n * ih1

Goal state after:
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s✝ : Set (Submodule R M)
hs : sSupIndep s✝ ∧ sSup s✝ = ⊤ ∧ ∀ m ∈ s✝, IsSimpleModule R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 : IsNoetherian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
tfae_3_to_5 : IsArtinian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
x✝ : ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
s : Set (Submodule R M)
fin : s.Finite
left✝ : sSupIndep s
sSup_eq_top : sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ IsNoetherian R M ∧ IsArtinian R M

Tactic:
rw [← isNoetherian_top_iff, ← Submodule.topEquiv.isArtinian_iff,
      ← sSup_eq_top, sSup_eq_iSup, ← iSup_subtype'']
    rw [SetCoe.forall'] at simple
    have := fin.to_subtype
    exact ⟨isNoetherian_iSup, isArtinian_iSup⟩

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
h : Function.Surjective ⇑(algebraMap S R)
⊢ length S M = length R M

Tactic:
by
  have : RingHomSurjective (algebraMap S R) := ⟨h⟩
  let f : M →ₛₗ[algebraMap S R] M := ⟨AddHom.id M, by simp⟩
  rw [Module.length, Module.length, WithBot.unbot_inj,
    Order.krullDim_eq_of_orderIso (Submodule.orderIsoMapComapOfBijective f Function.bijective_id)]

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : length R N = ⊤
this : length R M = ⊤
⊢ length R M = ⊤ + length R P

Tactic:
this,

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : length R N = ⊤
this : length R M = ⊤
⊢ ⊤ = ⊤ + length R P
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : length R P = ⊤
this : length R M = ⊤
⊢ length R M = length R N + ⊤

Tactic:
this,

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : length R P = ⊤
this : length R M = ⊤
⊢ ⊤ = length R N + ⊤
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
⊢ [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE

Tactic:
tfae_have 4 → 1
  | ⟨h⟩ => by
    rw [isNoetherianRing_iff, isNoetherian_iff_fg_wellFounded]
    refine ⟨RelEmbedding.wellFounded ?_ h⟩
    have : ∀ I : { J : Ideal R // J.FG }, ∃ x : R, (I : Ideal R) = Ideal.span {x} :=
      fun ⟨I, hI⟩ => (IsBezout.isPrincipal_of_FG I hI).1
    choose f hf using this
    exact
      { toFun := f
        inj' := fun x y e => by ext1; rw [hf, hf, e]
        map_rel_iff' := by
          dsimp
          intro a b
          rw [← Ideal.span_singleton_lt_span_singleton, ← hf, ← hf]
          rfl }

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
tfae_4_to_1 : WfDvdMonoid R → IsNoetherianRing R
⊢ [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE
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
hv : v.Integers O
x : O
⊢ 0 < v ((algebraMap O F) x) ↔ x ≠ 0

Tactic:
rw [← not_le]
  refine not_congr ?_
  simp [map_eq_zero_iff _ hv.hom_inj]

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
hv : v.Integers O
x : F
⊢ ∃ a, x = (algebraMap O F) a ∨ x⁻¹ = (algebraMap O F) a

Tactic:
by
  rcases val_le_one_or_val_inv_le_one v x with h | h <;>
  obtain ⟨a, ha⟩ := exists_of_le_one hv h
  exacts [⟨a, Or.inl ha.symm⟩, ⟨a, Or.inr ha.symm⟩]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : AdicCompletion I M
a : ℕ → M
ha : ∀ (n : ℕ), Submodule.Quotient.mk (a n) = ↑x n
m n : ℕ
hmn : m ≤ n
⊢ a m ≡ a n [SMOD I ^ m • ⊤]

Tactic:
rw [SModEq.def, ha m, ← mkQ_apply,
      ← factor_mk (Submodule.smul_mono_left (Ideal.pow_le_pow_right hmn)) (a n),
      mkQ_apply, ha n, x.property hmn]

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

Goal state before:
pp: case h.right
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := ⋯
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x := ⋯
x : R
hx : x ≠ 0
⊢ Associated (Multiset.replicate (Classical.choose ⋯) p).prod x

Tactic:
rw [Multiset.prod_replicate]
      exact Classical.choose_spec (spec.2 hx)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
t :
  map j.polynomialQuotientEquivQuotientPolynomial.toRingHom ⊥.jacobson =
    map j.polynomialQuotientEquivQuotientPolynomial.toRingHom ⊥
⊢ Function.Bijective ⇑j.polynomialQuotientEquivQuotientPolynomial.toRingHom

Tactic:
exact RingEquiv.bijective (polynomialQuotientEquivQuotientPolynomial j)

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

Goal state before:
pp: R✝ : Type u
inst✝⁵ : CommRing R✝
inst✝⁴ : IsDomain R✝
inst✝³ : IsDiscreteValuationRing R✝
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
I J : Ideal R
⊢ { toFun := fun I ↦ OrderDual.toDual ((addVal R) (generator I)),
          invFun := fun n ↦ ENat.recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) (OrderDual.ofDual n), left_inv := ⋯,
          right_inv := ⋯ }
        I ≤
      { toFun := fun I ↦ OrderDual.toDual ((addVal R) (generator I)),
          invFun := fun n ↦ ENat.recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) (OrderDual.ofDual n), left_inv := ⋯,
          right_inv := ⋯ }
        J ↔
    I ≤ J

Tactic:
simp [addVal_le_iff_dvd, ← span_singleton_le_span_singleton]

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

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O K
v : Valuation K Γ₀
hv : v.Integers O
this✝ : IsDomain O := Function.Injective.isDomain (algebraMap O K) hv.hom_inj
inst✝ : IsDiscreteValuationRing O
ϖ : O
h : Irreducible ϖ
n : ℕ
this : v ((algebraMap O K) ϖ) ^ n = v ((algebraMap O K) (ϖ ^ n))
⊢ ↑(maximalIdeal O ^ n) = {y | v ((algebraMap O K) y) ≤ v ((algebraMap O K) ϖ) ^ n}

Tactic:
this,

Goal state after:
K : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O K
v : Valuation K Γ₀
hv : v.Integers O
this✝ : IsDomain O := Function.Injective.isDomain (algebraMap O K) hv.hom_inj
inst✝ : IsDiscreteValuationRing O
ϖ : O
h : Irreducible ϖ
n : ℕ
this : v ((algebraMap O K) ϖ) ^ n = v ((algebraMap O K) (ϖ ^ n))
⊢ ↑(maximalIdeal O ^ n) = {y | v ((algebraMap O K) y) ≤ v ((algebraMap O K) (ϖ ^ n))}
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝ : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors Sₘ hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → (comap (algebraMap S Sₘ) I).IsMaximal
hϕ' : comap (algebraMap S Sₘ) ⊥ = ⊥
hRₘ : IsJacobsonRing Rₘ
hSₘ : IsJacobsonRing Sₘ
⊢ ⊥.jacobson ≤ comap (algebraMap S Sₘ) ⊥

Tactic:
rw [← hSₘ.out isRadical_bot, comap_jacobson]

Goal state after:
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝ : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors Sₘ hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → (comap (algebraMap S Sₘ) I).IsMaximal
hϕ' : comap (algebraMap S Sₘ) ⊥ = ⊥
hRₘ : IsJacobsonRing Rₘ
hSₘ : IsJacobsonRing Sₘ
⊢ ⊥.jacobson ≤ sInf (comap (algebraMap S Sₘ) '' {J | ⊥ ≤ J ∧ J.IsMaximal})
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: K : Type u_1
L : Type u_2
A : Type u_3
inst✝⁸ : CommRing K
inst✝⁷ : DivisionRing L
inst✝⁶ : CommRing A
inst✝⁵ : IsJacobsonRing K
inst✝⁴ : IsNoetherianRing K
inst✝³ : Nontrivial A
inst✝² : Algebra K L
inst✝¹ : Algebra K A
inst✝ : Algebra.FiniteType K A
f : L →ₐ[K] A
⊢ Module.Finite K L

Tactic:
obtain ⟨m, hm⟩ := Ideal.exists_maximal A
  let := Ideal.Quotient.field m
  have := finite_of_finite_type_of_isJacobsonRing K (A ⧸ m)
  exact Module.Finite.of_injective ((Ideal.Quotient.mkₐ K m).comp f).toLinearMap
    (RingHom.injective _)

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

Goal state before:
pp: case hp
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
K : Type u_7
L : Type u_8
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module L M
inst✝⁶ : Module L N
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
Q : RootPairing ι L M N
inst✝¹ : Q.IsRootSystem
inst✝ : Q.IsValuedIn K
⊢ ∀ x ∈ Q.rootSpan K, ∀ y ∈ Q.corootSpan K, (Q.toLinearMap x) y ∈ (algebraMap K L).range

Tactic:
exact Q.toLinearMap_apply_apply_mem_range_algebraMap K

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
S : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : Algebra S R
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : Module S N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : N
hx : x ∈ (P.PolarizationIn S).range
⊢ x ∈ P.corootSpan S

Tactic:
obtain ⟨y, hy⟩ := hx

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
S : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : Algebra S R
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : Module S N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : N
y : ↥(P.rootSpan S)
hy : (P.PolarizationIn S) y = x
⊢ x ∈ P.corootSpan S
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
S : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : Algebra S R
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : Module S N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : N
y : ↥(P.rootSpan S)
hy : (P.PolarizationIn S) y = x
⊢ x ∈ P.corootSpan S

Tactic:
PolarizationIn_apply

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
S : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : Algebra S R
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : Module S N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : N
y : ↥(P.rootSpan S)
hy : ∑ i, (P.coroot'In S i) y • P.coroot i = x
⊢ x ∈ P.corootSpan S
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
S : Type u_5
inst✝⁸ : CommRing S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower S R M
inst✝³ : Module S N
inst✝² : IsScalarTower S R N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
i : ι
hP :
  (P.PolarizationIn S) (P.rootSpanMem S i) =
    ∑ j, P.pairingIn S i ((P.reflectionPerm i) j) • P.coroot ((P.reflectionPerm i) j)
⊢ ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) • P.coroot i =
    (P.PolarizationIn S) (P.rootSpanMem S i) +
      ∑ j, P.pairingIn S i ((P.reflectionPerm i) j) • P.coroot ((P.reflectionPerm i) j)

Tactic:
PolarizationIn_apply

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
S : Type u_5
inst✝⁸ : CommRing S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower S R M
inst✝³ : Module S N
inst✝² : IsScalarTower S R N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
i : ι
hP :
  (P.PolarizationIn S) (P.rootSpanMem S i) =
    ∑ j, P.pairingIn S i ((P.reflectionPerm i) j) • P.coroot ((P.reflectionPerm i) j)
⊢ ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) • P.coroot i =
    ∑ i_1, (P.coroot'In S i_1) (P.rootSpanMem S i) • P.coroot i_1 +
      ∑ j, P.pairingIn S i ((P.reflectionPerm i) j) • P.coroot ((P.reflectionPerm i) j)