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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
⊢ I ≤ ⊥.jacobson

Tactic:
intro x hx
  rw [← Ideal.neg_mem_iff, Ideal.mem_jacobson_bot]
  intro y
  rw [add_comm]
  let f : ℕ → R := fun n => ∑ i ∈ range n, (x * y) ^ i
  have hf : ∀ m n, m ≤ n → f m ≡ f n [SMOD I ^ m • (⊤ : Submodule R R)] := by
    intro m n h
    simp only [f, smul_eq_mul, Ideal.mul_top, SModEq.sub_mem]
    rw [← add_tsub_cancel_of_le h, Finset.sum_range_add, ← sub_sub, sub_self, zero_sub,
      @neg_mem_iff]
    apply Submodule.sum_mem
    intro n _
    rw [mul_pow, pow_add, mul_assoc]
    exact Ideal.mul_mem_right _ (I ^ m) (Ideal.pow_mem_pow hx m)
  obtain ⟨L, hL⟩ := IsPrecomplete.prec toIsPrecomplete @hf
  rw [isUnit_iff_exists_inv]
  use L
  rw [← sub_eq_zero, neg_mul]
  apply IsHausdorff.haus (toIsHausdorff : IsHausdorff I R)
  intro n
  specialize hL n
  rw [SModEq.sub_mem, smul_eq_mul, Ideal.mul_top] at hL ⊢
  rw [sub_zero]
  suffices (1 - x * y) * f n - 1 ∈ I ^ n by
    convert! Ideal.sub_mem _ this (Ideal.mul_mem_left _ (1 + -(x * y)) hL) using 1
    ring
  cases n
  · simp only [Ideal.one_eq_top, pow_zero, mem_top]
  · rw [← neg_sub _ (1 : R), neg_mul, mul_geom_sum, neg_sub, sub_sub, add_comm (_ ^ _), ← sub_sub,
      sub_self, zero_sub, @neg_mem_iff, mul_pow]
    exact Ideal.mul_mem_right _ (I ^ _) (Ideal.pow_mem_pow hx _)

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝¹ : IsJacobsonRing R
inst✝ : Nontrivial R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
hP'_prime : P'.IsPrime
m : R[X]
hmem_P : m ∈ P
hm : ⟨m, hmem_P⟩ ≠ 0
hm' : m ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
a : R ⧸ P' := (map (Ideal.Quotient.mk P') m).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
hp0 : a ≠ 0
hM : 0 ∉ M
M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M
hM' : 0 ∉ M'
⊢ ⊥.IsMaximal

Tactic:
(map_bot.symm :
    (⊥ : Ideal (Localization M')) = Ideal.map (algebraMap (R[X] ⧸ P) (Localization M')) ⊥)

Goal state after:
R : Type u_1
inst✝² : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝¹ : IsJacobsonRing R
inst✝ : Nontrivial R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
hP'_prime : P'.IsPrime
m : R[X]
hmem_P : m ∈ P
hm : ⟨m, hmem_P⟩ ≠ 0
hm' : m ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
a : R ⧸ P' := (map (Ideal.Quotient.mk P') m).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
hp0 : a ≠ 0
hM : 0 ∉ M
M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M
hM' : 0 ∉ M'
⊢ (Ideal.map (algebraMap (R[X] ⧸ P) (Localization M')) ⊥).IsMaximal
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
⊢ [IsPrincipalIdealRing R, ValuationRing R, IsDedekindDomain R,
      IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R,
      Submodule.IsPrincipal (maximalIdeal R), finrank (ResidueField R) (CotangentSpace R) ≤ 1,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n].TFAE

Tactic:
tfae_have 4 → 3 :=
    fun ⟨h₁, h₂⟩ ↦ { h₁ with maximalOfPrime := (h₂ _ · · ▸ maximalIdeal.isMaximal R) }

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
⊢ [IsPrincipalIdealRing R, ValuationRing R, IsDedekindDomain R,
      IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R,
      Submodule.IsPrincipal (maximalIdeal R), finrank (ResidueField R) (CotangentSpace R) ≤ 1,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n].TFAE
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✝¹ : IsBezout R
inst✝ : IsDomain R
htors : torsion R M = ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
⊢ Function.Injective
    (⇑(lift (lsmul R M ∘ₗ Submodule.subtype I)) ∘ ⇑(LinearEquiv.rTensor M (Ideal.isoBaseOfIsPrincipal h)))

Tactic:
← LinearEquiv.coe_toLinearMap,

Goal state after:
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 ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
⊢ Function.Injective
    (⇑(lift (lsmul R M ∘ₗ Submodule.subtype I)) ∘ ⇑↑(LinearEquiv.rTensor M (Ideal.isoBaseOfIsPrincipal h)))
Module: Mathlib.LinearAlgebra.RootSystem.Basic

Goal state before:
pp: case 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
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

pp: case 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
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 : ι
⊢ MapsTo (⇑(preReflection (P₁.root i) (P₁.flip (P₂.coroot i)))) (range ⇑P₁.root) (range ⇑P₁.root)

Tactic:
· exact hr ▸ he ▸ P₂.coroot_root_two i

Goal state after:
case 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
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 : ι
⊢ MapsTo (⇑(preReflection (P₁.root i) (P₁.flip (P₂.coroot i)))) (range ⇑P₁.root) (range ⇑P₁.root)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
⊢ P.RootForm.orthogonal (P.rootSpan R) = LinearMap.ker P.RootForm

Tactic:
by
  rw [← LinearMap.BilinForm.orthogonal_top_eq_ker P.rootForm_symmetric.isRefl]
  refine le_antisymm ?_ (by intro; simp_all)
  rintro x hx y -
  simp only [LinearMap.BilinForm.mem_orthogonal_iff] at hx ⊢
  obtain ⟨u, hu, v, hv, rfl⟩ : ∃ᵉ (u ∈ P.rootSpan R) (v ∈ LinearMap.ker P.RootForm), u + v = y := by
    rw [← Submodule.mem_sup, P.isCompl_rootSpan_ker_rootForm.sup_eq_top]; exact Submodule.mem_top
  simp only [LinearMap.mem_ker] at hv
  simp [hx _ hu, hv]

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✝⁷ : LinearOrder S
inst✝⁶ : IsStrictOrderedRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x y : ↥(P.rootSpan S)
⊢ ((P.posRootForm S).posForm x) y = ∑ i, (P.coroot'In S i) x * (P.coroot'In S i) y

Tactic:
refine (FaithfulSMul.algebraMap_injective S R) ?_
  simp [posRootForm, rootForm_apply_apply]

Goal state after:
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
S : Type u_5
i j : ι
inst✝⁸ : Finite ι
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : IsTorsionFree R M
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
inst✝² : FaithfulSMul S R
inst✝¹ : P.IsValuedIn S
inst✝ : IsTorsionFree R N
⊢ P.pairingIn S i j = -1 ∧ P.pairingIn S j i = -4 ↔ P.root j = -2 • P.root i

Tactic:
← P.pairing_neg_one_neg_four_iff,

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
i j : ι
inst✝⁸ : Finite ι
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : IsTorsionFree R M
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
inst✝² : FaithfulSMul S R
inst✝¹ : P.IsValuedIn S
inst✝ : IsTorsionFree R N
⊢ P.pairingIn S i j = -1 ∧ P.pairingIn S j i = -4 ↔ P.pairing i j = -1 ∧ P.pairing j i = -4
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (Module.Dual R M × Module.Dual R (Module.Dual R M)) ≃ₗ[R] Module.Dual R (Module.Dual R M × M) :=
  LinearEquiv.prodComm R (Module.Dual R M) (Module.Dual R (Module.Dual R M)) ≪≫ₗ
    Module.dualProdDualEquivDual R (Module.Dual R M) M
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
⊢ Function.Injective (⇑e.symm ∘ ⇑(dualProd R M)) ↔ Function.Injective ⇑(Module.Dual.eval R M)

Tactic:
← LinearEquiv.coe_toLinearMap,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (Module.Dual R M × Module.Dual R (Module.Dual R M)) ≃ₗ[R] Module.Dual R (Module.Dual R M × M) :=
  LinearEquiv.prodComm R (Module.Dual R M) (Module.Dual R (Module.Dual R M)) ≪≫ₗ
    Module.dualProdDualEquivDual R (Module.Dual R M) M
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
⊢ Function.Injective (⇑↑e.symm ∘ ⇑(dualProd R M)) ↔ Function.Injective ⇑(Module.Dual.eval R M)
Module: Mathlib.LinearAlgebra.RootSystem.Hom

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
ι₂✝ : Type u_5
M₂✝ : Type u_6
N₂✝ : Type u_7
inst✝¹¹ : AddCommGroup M₂✝
inst✝¹⁰ : Module R M₂✝
inst✝⁹ : AddCommGroup N₂✝
inst✝⁸ : Module R N₂✝
P✝ : RootPairing ι R M N
Q : RootPairing ι₂✝ R M₂✝ N₂✝
ι₁ : Type u_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
g : P₁.Equiv P₂
f : P.Equiv P₁
⊢ Bijective ⇑((↑g).comp ↑f).weightMap

Tactic:
simp only [Hom.comp, LinearMap.coe_comp]

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
ι₂✝ : Type u_5
M₂✝ : Type u_6
N₂✝ : Type u_7
inst✝¹¹ : AddCommGroup M₂✝
inst✝¹⁰ : Module R M₂✝
inst✝⁹ : AddCommGroup N₂✝
inst✝⁸ : Module R N₂✝
P✝ : RootPairing ι R M N
Q : RootPairing ι₂✝ R M₂✝ N₂✝
ι₁ : Type u_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
g : P₁.Equiv P₂
f : P.Equiv P₁
⊢ Bijective (⇑(↑g).weightMap ∘ ⇑(↑f).weightMap)
Module: Mathlib.LinearAlgebra.RootSystem.Hom

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
ι₂✝ : Type u_5
M₂✝ : Type u_6
N₂✝ : Type u_7
inst✝¹¹ : AddCommGroup M₂✝
inst✝¹⁰ : Module R M₂✝
inst✝⁹ : AddCommGroup N₂✝
inst✝⁸ : Module R N₂✝
P✝ : RootPairing ι R M N
Q : RootPairing ι₂✝ R M₂✝ N₂✝
ι₁ : Type u_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
g : P₁.Equiv P₂
f : P.Equiv P₁
⊢ Bijective ⇑((↑g).comp ↑f).coweightMap

Tactic:
simp only [Hom.comp, LinearMap.coe_comp]

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
ι₂✝ : Type u_5
M₂✝ : Type u_6
N₂✝ : Type u_7
inst✝¹¹ : AddCommGroup M₂✝
inst✝¹⁰ : Module R M₂✝
inst✝⁹ : AddCommGroup N₂✝
inst✝⁸ : Module R N₂✝
P✝ : RootPairing ι R M N
Q : RootPairing ι₂✝ R M₂✝ N₂✝
ι₁ : Type u_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
g : P₁.Equiv P₂
f : P.Equiv P₁
⊢ Bijective (⇑(↑f).coweightMap ∘ ⇑(↑g).coweightMap)
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case smul
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
y : k[G]
r : k
x : k[G]
hx : ((ofMulAction k G G).asAlgebraHom x) y = x * y
⊢ ((ofMulAction k G G).asAlgebraHom (r • x)) y = r • x * y

Tactic:
| smul r x hx =>

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

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
htQ : t ∈ Q
k : ι
hk : P.root k ∈ Q
⊢ (P.coroot' k) t = 0

Tactic:
refine LinearMap.mem_ker.mp (span_le.mpr ?_ ht)

Goal state after:
case pos
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
htQ : t ∈ Q
k : ι
hk : P.root k ∈ Q
⊢ ⇑P.root '' {i | P.root i ∉ Q} ⊆ ↑(ker (P.coroot' k))
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Field R
inst✝⁴ : CharZero R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝ : InvolutiveNeg ι := P.indexNeg
this : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
⊢ span ℚ (range v) = span ℚ (range (P.rootSpanMem ℚ))

Tactic:
apply le_antisymm (span_mono fun x i ↦ by aesop) (span_le.mpr ?_)

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Field R
inst✝⁴ : CharZero R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝ : InvolutiveNeg ι := P.indexNeg
this : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
⊢ range (P.rootSpanMem ℚ) ⊆ ↑(span ℚ (range v))
Module: Mathlib.LinearAlgebra.Matrix.BilinearForm

Goal state before:
pp: R₁ : Type u_1
inst✝⁴ : CommSemiring R₁
n : Type u_5
o : Type u_6
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : DecidableEq n
inst✝ : DecidableEq o
M : Matrix n n R₁
P Q : Matrix n o R₁
⊢ BilinForm.toMatrix' ((toBilin' M).comp (toLin' P) (toLin' Q)) = BilinForm.toMatrix' (toBilin' (Pᵀ * M * Q))

Tactic:
simp only [BilinForm.toMatrix'_comp, BilinForm.toMatrix'_toBilin', toMatrix'_toLin']

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
i : ι
hi : i ∈ baseOf (⇑P.root) f
j : ι
hj : j ∈ {i | 0 < g (P.coroot i)}
k : ι
hk : k ∈ {i | 0 < g (P.coroot i)}
contra : P.coroot i = P.coroot j + P.coroot k
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
a : ↑(⇑P.root '' s) → ℕ
ha : ∑ x, a x • ↑x = P.root j
b : ↑(⇑P.root '' s) → ℕ
hb : ∑ x, b x • ↑x = P.root k
ri : ↑(⇑P.root '' s) := ⟨P.root i, ⋯⟩
huv : u • Nat.cast ∘ a + v • Nat.cast ∘ b = Pi.single ri 1
⊢ P.root j = ↑(a ri) • P.root i

Tactic:
have (x : P.root '' s) (hx : x ≠ ri) : a x = 0 := by
      replace huv : u * ↑(a x) + v * ↑(b x) = 0 := by simpa [hx] using congr($huv x)
      suffices u * (a x) = 0 by simpa [hu.ne'] using this
      have : 0 ≤ u * (a x) := by positivity
      have : 0 ≤ v * (b x) := by positivity
      grind

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
i : ι
hi : i ∈ baseOf (⇑P.root) f
j : ι
hj : j ∈ {i | 0 < g (P.coroot i)}
k : ι
hk : k ∈ {i | 0 < g (P.coroot i)}
contra : P.coroot i = P.coroot j + P.coroot k
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
a : ↑(⇑P.root '' s) → ℕ
ha : ∑ x, a x • ↑x = P.root j
b : ↑(⇑P.root '' s) → ℕ
hb : ∑ x, b x • ↑x = P.root k
ri : ↑(⇑P.root '' s) := ⟨P.root i, ⋯⟩
huv : u • Nat.cast ∘ a + v • Nat.cast ∘ b = Pi.single ri 1
this : ∀ (x : ↑(⇑P.root '' s)), x ≠ ri → a x = 0
⊢ P.root j = ↑(a ri) • P.root i
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case refl
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
i✝ : ℕ
h : ∀ j ≥ i✝, abv (f j - f i✝) < 1
R : ℕ → α := Nat.rec (abv (f 0)) fun i c ↦ max c (abv (f i.succ))
hR : R = Nat.rec (abv (f 0)) fun i c ↦ max c (abv (f i.succ))
i : ℕ
hi : ∀ j ≤ i, abv (f j) ≤ R i
⊢ abv (f i.succ) ≤ R i.succ

pp: case step
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
i✝ : ℕ
h : ∀ j ≥ i✝, abv (f j - f i✝) < 1
R : ℕ → α := Nat.rec (abv (f 0)) fun i c ↦ max c (abv (f i.succ))
hR : R = Nat.rec (abv (f 0)) fun i c ↦ max c (abv (f i.succ))
i : ℕ
hi : ∀ j ≤ i, abv (f j) ≤ R i
j : ℕ
hj : j.le i
⊢ abv (f j) ≤ R i.succ

Tactic:
· simp [R]

Goal state after:
case step
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
i✝ : ℕ
h : ∀ j ≥ i✝, abv (f j - f i✝) < 1
R : ℕ → α := Nat.rec (abv (f 0)) fun i c ↦ max c (abv (f i.succ))
hR : R = Nat.rec (abv (f 0)) fun i c ↦ max c (abv (f i.succ))
i : ℕ
hi : ∀ j ≤ i, abv (f j) ≤ R i
j : ℕ
hj : j.le i
⊢ abv (f j) ≤ R i.succ
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
⊢ Nonempty P.Base

Tactic:
by
  let _i : Module ℚ M := Module.compHom M (algebraMap ℚ R)
  obtain ⟨f, hf⟩ : ∃ f : Dual ℚ M, ∀ i, f (P.root i) ≠ 0 :=
    exists_dual_forall_apply_ne_zero P.root <| by simp [P.ne_zero]
  let := P.indexNeg
  exact ⟨Base.mk' P (baseOf P.root (f : M →+ ℚ)) (P.linearIndepOn_root_baseOf f hf)
    (fun i ↦ mem_or_neg_mem_closure_baseOf P.root (f : M →+ ℚ) i (hf i) (by simp))⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
p : Type u_5
A : Matrix m n R
B : Matrix n p R
h : Aᴴ * A * B = 0
⊢ A * B = 0

Tactic:
apply_fun (Bᴴ * ·) at h

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
p : Type u_5
A : Matrix m n R
B : Matrix n p R
h : Bᴴ * (Aᴴ * A * B) = Bᴴ * 0
⊢ A * B = 0
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f g : Cauchy abs
⊢ { cauchy := f * g⁻¹ } = { cauchy := f } * { cauchy := g }⁻¹

Tactic:
ofCauchy_mul,

Goal state after:
f g : Cauchy abs
⊢ { cauchy := f } * { cauchy := g⁻¹ } = { cauchy := f } * { cauchy := g }⁻¹
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero R
i : m
j : n
r : R
⊢ Function.uncurry (Pi.single i (Pi.single j r)) ∘ Prod.swap = Pi.single (j, i) r

Tactic:
Pi.uncurry_single_single

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero R
i : m
j : n
r : R
⊢ Pi.single (i, j) r ∘ Prod.swap = Pi.single (j, i) r
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosSemidef
e : m → n
⊢ (M.submatrix e e).PosSemidef

Tactic:
refine ⟨hM.1.submatrix _, fun x ↦ ?_⟩

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosSemidef
e : m → n
x : m →₀ R
⊢ 0 ≤ x.sum fun i xi ↦ x.sum fun j xj ↦ star xi * M.submatrix e e i j * xj