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

Goal state before:
pp: case pos
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
⊢ length R M = length R N + length R P

Tactic:
by_cases hN : IsFiniteLength R N
    · obtain ⟨s, hs₁, hs₂⟩ := isFiniteLength_iff_exists_compositionSeries.mp hP
      obtain ⟨t, ht₁, ht₂⟩ := isFiniteLength_iff_exists_compositionSeries.mp hN
      let s' : CompositionSeries (Submodule R M) :=
        s.map ⟨Submodule.comap g, Submodule.comap_covBy_of_surjective hg⟩
      let t' : CompositionSeries (Submodule R M) :=
        t.map ⟨Submodule.map f, Submodule.map_covBy_of_injective hf⟩
      have hfg : Submodule.map f ⊤ = Submodule.comap g ⊥ := by
        rw [Submodule.map_top, Submodule.comap_bot, LinearMap.exact_iff.mp H]
      let r := t'.smash s' (by simpa [s', t', hs₁, ht₂] using hfg)
      rw [← Module.length_compositionSeries s hs₁ hs₂,
        ← Module.length_compositionSeries t ht₁ ht₂,
        ← Module.length_compositionSeries r
          (by simpa [r, t', ht₁, -Submodule.map_bot] using Submodule.map_bot f)
          (by simpa [r, s', hs₂, -Submodule.comap_top] using Submodule.comap_top g)]
      simp_rw [r, RelSeries.smash_length, Nat.cast_add, s', t', RelSeries.map_length]
    · have := mt (IsFiniteLength.of_injective · hf) hN
      rw [← Module.length_ne_top_iff, ne_eq, not_not] at hN this
      rw [hN, this, top_add]

Goal state after:
Module: Mathlib.RingTheory.Bezout

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

Tactic:
tfae_have 1 → 2
  | _ => inferInstance

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
⊢ [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE
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
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
hf : Function.Injective ⇑f
⊢ length R N ≤ length R M

Tactic:
Module.length_eq_add_of_exact f (LinearMap.range f).mkQ hf
    (Submodule.mkQ_surjective _) (LinearMap.exact_map_mkQ_range f)

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
hf : Function.Injective ⇑f
⊢ length R N ≤ length R N + length R (M ⧸ f.range)
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case inl
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : (algebraMap A K) ya ≠ 0
this : (algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ Quotient.mk'' ((algebraMap A K) xa / (algebraMap A K) ya + (algebraMap A K) xb / (algebraMap A K) yb) ≤
    max (Quotient.mk'' ((algebraMap A K) xa / (algebraMap A K) ya))
      (Quotient.mk'' ((algebraMap A K) xb / (algebraMap A K) yb))

Tactic:
apply le_trans _ (le_max_left _ _)
      use c + 1
      rw [Algebra.smul_def]
      field_simp
      simp only [← map_mul, ← map_add]
      congr 1; linear_combination h

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
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
n : ℕ
⊢ Submodule.map f (I ^ n • ⊤) ≤ I ^ n • ⊤

Tactic:
by
      rw [map_smul'']
      exact smul_mono le_rfl le_top

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
H : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b : R
⊢ a ∣ b ∨ b ∣ a

Tactic:
have := H.total (Ideal.span {a}) (Ideal.span {b})

Goal state after:
R : Type u_1
inst✝ : CommRing R
H : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b : R
this : Ideal.span {a} ≤ Ideal.span {b} ∨ Ideal.span {b} ≤ Ideal.span {a}
⊢ a ∣ b ∨ b ∣ a
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
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
⊢ 0 ∈ {f | IsAdicCauchy I M f}

Tactic:
intro _ _ _
    rfl

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

Goal state before:
pp: case h.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
Q : Ideal R
hQ1 : Q ≠ ⊥
hQ2 : Q.IsPrime
⊢ Q = maximalIdeal R

Tactic:
obtain ⟨q, rfl⟩ := (IsPrincipalIdealRing.principal Q).1

Goal state after:
case h.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : R ∙ q ≠ ⊥
hQ2 : IsPrime (R ∙ q)
⊢ R ∙ q = maximalIdeal R
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ n) p
this : Irreducible (ϖ ^ n)
⊢ Associated p ϖ

Tactic:
rcases lt_trichotomy n 1 with (H | rfl | H)

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ n) p
this : Irreducible (ϖ ^ n)
H : n < 1
⊢ Associated p ϖ

case inr.inl
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
hn : Associated (ϖ ^ 1) p
this : Irreducible (ϖ ^ 1)
⊢ Associated p ϖ

case inr.inr
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ n) p
this : Irreducible (ϖ ^ n)
H : 1 < n
⊢ Associated p ϖ
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
f : AdicCauchySequence I M
k : ℕ
h : ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, ↑f m ∈ I ^ l • ⊤
n m : ℕ
hnm : m ≥ n + k
l : ℕ
hnl : l ≥ n + k
hl : ↑f m ∈ I ^ l • ⊤
⊢ Submodule.Quotient.mk (↑f n) = 0 n

Tactic:
← AdicCauchySequence.mk_eq_mk (show n ≤ m by lia)

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : AdicCauchySequence I M
k : ℕ
h : ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, ↑f m ∈ I ^ l • ⊤
n m : ℕ
hnm : m ≥ n + k
l : ℕ
hnl : l ≥ n + k
hl : ↑f m ∈ I ^ l • ⊤
⊢ Submodule.Quotient.mk (↑f m) = 0 n
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ IsJacobsonRing R ↔ ∀ (P : Ideal R), P.IsPrime → P.jacobson = P

Tactic:
by
  refine isJacobsonRing_iff.trans ⟨fun h I hI => h I hI.isRadical, ?_⟩
  refine fun h I hI ↦ le_antisymm (fun x hx ↦ ?_) (fun x hx ↦ mem_sInf.mpr fun _ hJ ↦ hJ.left hx)
  rw [← hI.radical, radical_eq_sInf I, mem_sInf]
  intro P hP
  rw [Set.mem_ofPred_eq] at hP
  rw [jacobson, mem_sInf] at hx
  rw [← h P hP.right, jacobson, mem_sInf]
  exact fun J hJ => hx ⟨le_trans hP.left hJ.left, hJ.right⟩

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

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'✝ : P'.IsPrime
hP' : (under R P').IsPrime
hPM : Disjoint ↑(powers y) ↑(under R P')
hP : (under R P').jacobson = under R P'
x : R
hx : x ∈ sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}
J : Ideal R
hJ : J ∈ {J | Ideal.comap (algebraMap R S) P' ≤ J ∧ J.IsMaximal}
h : y ∈ J
⊢ x * y ∈ J

Tactic:
exact J.mul_mem_left x h

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 ϖ✝
⊢ ↑(maximalIdeal O) = ↑(span {ϖ✝})

Tactic:
← h.maximalIdeal_eq

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 ϖ✝
⊢ ↑(maximalIdeal O) = ↑(maximalIdeal O)
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) = ↑(span {ϖ} ^ n)

Tactic:
← h.maximalIdeal_eq

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) = ↑(maximalIdeal O ^ n)
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : Associates R
⊢ Associates.mk (Quot.out x) ∈ (Associates R)⁰ ↔
    ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out x))) ∈ (Ideal R)⁰

Tactic:
mk_mem_nonZeroDivisors_associates,

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ IsJacobsonRing R[X] ↔ IsJacobsonRing R

Tactic:
refine ⟨?_, isJacobsonRing_polynomial_of_isJacobsonRing⟩
  intro H
  exact isJacobsonRing_of_surjective ⟨eval₂RingHom (RingHom.id _) 1, fun x =>
    ⟨C x, by simp only [coe_eval₂RingHom, RingHom.id_apply, eval₂_C]⟩⟩

Goal state after:
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:
← LinearMap.coe_comp,

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.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
S : Type u_7
inst✝ : CommRing S
f : S →+* R
x : S
⊢ x ∈ (comap f v).supp ↔ x ∈ Ideal.comap f v.supp

Tactic:
rw [mem_supp_iff, Ideal.mem_comap, mem_supp_iff, comap_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
⊢ P.IsReduced ↔ ∀ (i j : ι), i ≠ j → ¬LinearIndependent R ![P.root i, P.root j] → P.root i = -P.root j

Tactic:
isReduced_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
⊢ (∀ (i j : ι), ¬LinearIndependent R ![P.root i, P.root j] → P.root i = P.root j ∨ P.root i = -P.root j) ↔
    ∀ (i j : ι), i ≠ j → ¬LinearIndependent R ![P.root i, P.root j] → P.root i = -P.root j
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 ι
⊢ (P.posRootForm S).posForm = P.RootFormIn S

Tactic:
by
  ext
  apply FaithfulSMul.algebraMap_injective S R
  simp only [algebraMap_posRootForm_posForm, algebraMap_rootFormIn]

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

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✝⁶ : Finite ι
inst✝⁵ : P.IsRootSystem
k : Type u_5
inst✝⁴ : Field k
inst✝³ : CharZero k
inst✝² : Module k M
inst✝¹ : Module k N
p : M →ₗ[k] N →ₗ[k] k
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hs : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hsp : span k (range ⇑root) = ⊤
⊢ ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p (root i)))) (range ⇑coroot) (range ⇑coroot)

Tactic:
by
    rintro i - ⟨j, rfl⟩
    use RootPairing.equiv_of_mapsTo p root coroot i hs hp j
    refine (coroot_eq_coreflection_of_root_eq_of_span_eq_top p root coroot hp hs hsp ?_)
    rw [equiv_of_mapsTo_apply, (exist_eq_reflection_of_mapsTo p root coroot i j hs).choose_spec]

Goal state after:
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
inst✝¹ : P.IsRootSystem
inst✝ : NeZero 2
s : Set ι
h : LinearIndepOn R (⇑P.root) s
⊢ LinearIndepOn R (⇑P.coroot) s

Tactic:
by
  obtain ⟨f, hf⟩ : ∃ f : s → Rˣ, ∀ i : s, P.coroot i = f i • P.PolarizationEquiv (P.root i) :=
    ⟨fun i ↦ Units.mk0 (2 / P.RootForm (P.root i) (P.root i))
      (by simp [two_ne_zero, IsAnisotropic.rootForm_root_ne_zero]),
     fun i ↦ by simp [coroot_eq_polarizationEquiv_apply_root]⟩
  have : s.domRestrict P.coroot = P.PolarizationEquiv.toLinearMap ∘ (f • s.domRestrict P.root) := by
    ext; simp [hf, polarizationEquiv_apply]
  rw [← linearIndependent_restrict_iff, this,
    LinearMap.linearIndependent_iff_of_injOn _ P.PolarizationEquiv.injective.injOn]
  simpa

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid P
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h : (Q₁.prod Q₂).Anisotropic
⊢ Q₁.Anisotropic ∧ Q₂.Anisotropic

Tactic:
Anisotropic,

Goal state after:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid P
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h : ∀ (x : M₁ × M₂), (Q₁.prod Q₂) x = 0 → x = 0
⊢ Q₁.Anisotropic ∧ Q₂.Anisotropic
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : (pi Q).Anisotropic
⊢ ∀ (i : ι), (Q i).Anisotropic

Tactic:
Anisotropic,

Goal state after:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), (pi Q) x = 0 → x = 0
⊢ ∀ (i : ι), (Q i).Anisotropic
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

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✝ : P.IsRootSystem
x : M
⊢ x = 0 ↔ ∀ (i : ι), (P.coroot' i) x = 0

Tactic:
by
  refine ⟨fun h ↦ by simp [h], fun h ↦ ?_⟩
  replace h : x ∈ ⨅ i, ker (P.coroot' i) := by aesop
  simpa [← P.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot'] using h

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case inr
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α✝ β✝ α : Weight K (↥H) L
hα : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
h : β = α
⊢ (rootSystem H).root ⟨α, hα⟩ = (rootSystem H).root ⟨β, hβ⟩ ∨ (rootSystem H).root ⟨α, hα⟩ = -(rootSystem H).root ⟨β, hβ⟩

Tactic:
left; ext x; simpa using DFunLike.congr_fun h.symm x

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

Goal state before:
pp: case refine_1
ι : 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✝² : Module K M
inst✝¹ : Module K N
inst✝ : Nontrivial M
P : RootPairing ι K M N
h : P.IsIrreducible
x✝ : ↥P.invtRootSubmodule
q : Submodule K M
hq : q ∈ P.invtRootSubmodule
⊢ q = ⊥ ∨ q = ⊤

Tactic:
rw [mem_invtRootSubmodule_iff] at hq

Goal state after:
case refine_1
ι : 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✝² : Module K M
inst✝¹ : Module K N
inst✝ : Nontrivial M
P : RootPairing ι K M N
h : P.IsIrreducible
x✝ : ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
⊢ q = ⊥ ∨ q = ⊤
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₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ Bijective ⇑(↑f).coweightMap

Tactic:
refine bijective_iff_has_inverse.mpr ?_
      use f.inv.coweightMap
      constructor
      · refine leftInverse_iff_comp.mpr ?_
        simp only [← @LinearMap.coe_comp]
        rw [← Hom.coweightMap_mul, f.val_inv, Hom.coweightMap_one, LinearMap.id_coe]
      · refine rightInverse_iff_comp.mpr ?_
        simp only [← @LinearMap.coe_comp]
        rw [← Hom.coweightMap_mul, f.inv_val, Hom.coweightMap_one, LinearMap.id_coe]

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

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
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsAddTorsionFree M
inst✝ : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : ↑z * t = 1
ht : ↑z • P.coroot i ∈ range ⇑P.coroot
w : ℤ
hw : ↑w * ↑z = 1
⊢ ↑z * ↑w = 1

Tactic:
simpa [mul_mul_mul_comm _ t, mul_comm t, mul_comm _ (z : R), hz] using congr_arg₂ (· * ·) hz hw

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

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
B : P.InvariantForm
len_eq : (B.form (P.root i)) (P.root i) = (B.form (P.root j)) (P.root j)
ne : i ≠ j
ne' : P.root i ≠ -P.root j
this : Module.IsReflexive R M
⊢ (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ {(0, 0), (1, 1), (-1, -1)}

Tactic:
have := P.pairingIn_pairingIn_mem_set_of_length_eq len_eq

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
B : P.InvariantForm
len_eq : (B.form (P.root i)) (P.root i) = (B.form (P.root j)) (P.root j)
ne : i ≠ j
ne' : P.root i ≠ -P.root j
this✝ : Module.IsReflexive R M
this : (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ {(0, 0), (1, 1), (-1, -1), (2, 2), (-2, -2)}
⊢ (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ {(0, 0), (1, 1), (-1, -1)}
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

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✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
h : (algebraMap ℤ R) (P.coxeterWeightIn ℤ i j) = 0
⊢ P.pairingIn ℤ i j = 0

Tactic:
algebraMap_coxeterWeightIn,

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✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
h : P.coxeterWeight i j = 0
⊢ P.pairingIn ℤ i j = 0
Module: Mathlib.LinearAlgebra.RootSystem.Base

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
b : P.Base
inst✝ : CharZero R
f : ι → ℤ
hf : ∑ j ∈ b.support, f j • P.root j ∈ range ⇑P.root
hf₀ : Function.support f ⊆ ↑b.support
⊢ ¬0 ≤ f ↔ f < 0

Tactic:
replace hf : ∑ j ∈ b.support, (-f) j • P.root j ∈ range P.root := by
    rw [← neg_mem_range_root_iff]; simpa

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
b : P.Base
inst✝ : CharZero R
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf : ∑ j ∈ b.support, (-f) j • P.root j ∈ range ⇑P.root
⊢ ¬0 ≤ f ↔ f < 0