mathlib-initiative/mathlib-tactics huggingface dataset:
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ₘ := ⋯
φ' : Rₘ →+* Sₘ := ⋯
I : Ideal Sₘ
hI : I.IsMaximal
this✝⁴ : (comap (algebraMap S Sₘ) I).IsPrime
this✝³ : (comap φ' I).IsPrime
this✝² : ⊥.IsPrime
hcomm : φ'.comp (algebraMap R Rₘ) = (algebraMap S Sₘ).comp φ
f : R ⧸ comap φ (comap (algebraMap S Sₘ) I) →+* S ⧸ comap (algebraMap S Sₘ) I := ⋯
g : S ⧸ comap (algebraMap S Sₘ) I →+* Sₘ ⧸ I := ⋯
this✝¹ : (comap φ' I).IsMaximal
this✝ : (under R (comap φ' I)).IsMaximal
this : ⊥.IsMaximal
⊢ (g.comp f).IsIntegral

Tactic:
rw [comp_quotientMap_eq_of_comp_eq hcomm]

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ₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
this✝⁴ : (comap (algebraMap S Sₘ) I).IsPrime
this✝³ : (comap φ' I).IsPrime
this✝² : ⊥.IsPrime
hcomm : φ'.comp (algebraMap R Rₘ) = (algebraMap S Sₘ).comp φ
f : R ⧸ comap φ (comap (algebraMap S Sₘ) I) →+* S ⧸ comap (algebraMap S Sₘ) I :=
  quotientMap (comap (algebraMap S Sₘ) I) φ ⋯
g : S ⧸ comap (algebraMap S Sₘ) I →+* Sₘ ⧸ I := quotientMap I (algebraMap S Sₘ) ⋯
this✝¹ : (comap φ' I).IsMaximal
this✝ : (under R (comap φ' I)).IsMaximal
this : ⊥.IsMaximal
⊢ ((quotientMap I φ' ⋯).comp (quotientMap (comap φ' I) (algebraMap R Rₘ) ⋯)).IsIntegral
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) (Associates.mk (Quot.out x * Quot.out y))) =
    ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out x))) *
      ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out y)))

Tactic:
associatesEquivIsPrincipal_apply,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x y : Associates R
⊢ span {Quot.out x * Quot.out y} = span {Quot.out x} * span {Quot.out y}
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ↑((associatesEquivIsPrincipal R) (Associates.mk 0)) = 0

Tactic:
associatesEquivIsPrincipal_apply,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ span {0} = 0
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ↑((associatesEquivIsPrincipal R) (Associates.mk 1)) = 1

Tactic:
associatesEquivIsPrincipal_apply,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ span {1} = 1
Module: Mathlib.RingTheory.Ideal.IsPrincipal

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

Tactic:
associatesEquivIsPrincipal_apply,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : Associates R
⊢ Quot.out x ∈ R⁰ ↔ span {Quot.out x} ∈ (Ideal R)⁰
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝¹ : (Ideal.span {a}).radical = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := (algebraMap R K) b / (algebraMap R K) a
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : (algebraMap R K) a ≠ 0
hx : ¬∀ y ∈ M, x * y ∈ M
this : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤
⊢ ∃ y ∈ maximalIdeal R, b * y = a

Tactic:
Ideal.eq_top_iff_one,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝¹ : (Ideal.span {a}).radical = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := (algebraMap R K) b / (algebraMap R K) a
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : (algebraMap R K) a ≠ 0
hx : ¬∀ y ∈ M, x * y ∈ M
this : 1 ∈ Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M)
⊢ ∃ y ∈ maximalIdeal R, b * y = a
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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_7
inst✝⁶ : CommRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : P.IsValuedIn S
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : NeZero 2
i j : ι
⊢ P.pairingIn S i j = 0 ↔ P.pairingIn S j i = 0

Tactic:
simpa only [← FaithfulSMul.algebraMap_eq_zero_iff S R, algebraMap_pairingIn] using
    P.pairing_eq_zero_iff

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Union

Goal state before:
pp: case insert
ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hj' : ↑s.card < ENat.card K → ⋃ i ∈ s, ↑(p i) ⊂ univ
h₂ : ↑(insert j s).card < ENat.card K
⊢ ⋃ i ∈ insert j s, ↑(p i) ⊂ univ

Tactic:
simp only [ssubset_univ_iff] at hj' ⊢

Goal state after:
case insert
ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
h₂ : ↑(insert j s).card < ENat.card K
hj' : ↑s.card < ENat.card K → ⋃ i ∈ s, ↑(p i) ≠ univ
⊢ ⋃ i ∈ insert j s, ↑(p i) ≠ univ
Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup

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.weylGroupToPerm.range = Subgroup.closure (range P.reflectionPerm)

Tactic:
by
  refine (Subgroup.closure_eq_of_le _ ?_ ?_).symm
  · rintro - ⟨i, rfl⟩
    simp only [MonoidHom.domRestrict_range, Subgroup.coe_map, mem_image, SetLike.mem_coe]
    use Equiv.reflection P i
    refine ⟨reflection_mem_weylGroup P i, by simp⟩
  · rintro fg ⟨⟨w, hw⟩, rfl⟩
    induction hw using Subgroup.closure_induction'' with
    | one =>
      change ((Equiv.indexHom P).domRestrict P.weylGroup) 1 ∈ _
      simp only [map_one, one_mem]
    | mem w' hw' =>
      obtain ⟨i, rfl⟩ := hw'
      simp only [MonoidHom.domRestrict_apply, Equiv.indexHom_apply, Equiv.reflection_indexEquiv]
      simpa only [reflection_mem_weylGroup] using! Subgroup.subset_closure (mem_range_self i)
    | inv_mem w' hw' =>
      obtain ⟨i, rfl⟩ := hw'
      simp only [Equiv.reflection_inv, MonoidHom.domRestrict_apply, Equiv.indexHom_apply,
        Equiv.reflection_indexEquiv]
      simpa only [reflection_mem_weylGroup] using! Subgroup.subset_closure (mem_range_self i)
    | mul w₁ w₂ hw₁ hw₂ h₁ h₂ =>
      simpa only [← Submonoid.mk_mul_mk _ w₁ w₂ hw₁ hw₂, map_mul] using! Subgroup.mul_mem _ h₁ h₂

Goal state after:
Module: Mathlib.RepresentationTheory.Submodule

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
p : Submodule k V
⊢ p ∈ ρ.invtSubmodule ↔ ∀ (g : G), p ∈ Module.End.invtSubmodule (ρ g)

Tactic:
invtSubmodule,

Goal state after:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
p : Submodule k V
⊢ p ∈ ⨅ g, Module.End.invtSubmodule (ρ g) ↔ ∀ (g : G), p ∈ Module.End.invtSubmodule (ρ g)
Module: Mathlib.RepresentationTheory.Submodule

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
p : Submodule k V
hp : ∀ (g : G), ∀ v ∈ p, (ρ g) v ∈ p
v : V
hv : v ∈ p
x : k[G]
⊢ (ρ.asAlgebraHom x) v ∈ p

Tactic:
by
  apply x.induction_on <;> aesop

Goal state after:
Module: Mathlib.RepresentationTheory.Submodule

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
q : Submodule k[G] ρ.asModule
⊢ (Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm (Submodule.restrictScalars k q) ∈ ρ.invtSubmodule

Tactic:
invtSubmodule,

Goal state after:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
q : Submodule k[G] ρ.asModule
⊢ (Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm (Submodule.restrictScalars k q) ∈
    ⨅ g, Module.End.invtSubmodule (ρ g)
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
P : RootPairing ι R M N
⊢ Injective ⇑(weightHom P)

Tactic:
intro f g hfg
  ext x
  · exact LinearMap.congr_fun hfg x
  · refine LinearEquiv.injective P.flip.toPerfPair ?_
    simp_rw [← weight_coweight_transpose_apply]
    exact congrFun (congrArg DFunLike.coe (congrArg LinearMap.dualMap hfg)) (P.flip.toPerfPair x)
  · refine Embedding.injective P.root ?_
    simp_rw [← root_weightMap_apply]
    exact congrFun (congrArg DFunLike.coe hfg) (P.root x)

Goal state after:
Module: Mathlib.Data.Int.ConditionallyCompleteOrder

Goal state before:
pp: s : Set ℤ
inst✝ : DecidablePred fun x ↦ x ∈ s
b : ℤ
Hb : ∀ z ∈ s, z ≤ b
Hinh : ∃ z, z ∈ s
⊢ sSup s = ↑(b.greatestOfBdd Hb Hinh)

Tactic:
have : s.Nonempty ∧ BddAbove s := ⟨Hinh, b, Hb⟩
  simp only [sSup, dif_pos this]
  convert! (coe_greatestOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddAbove s)) Hinh).symm

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnectedLinear

Goal state before:
pp: α : Type u_1
I : Set α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
h' : ∀ x ∈ I, ∀ y ∈ I, Ioo x y ⊆ Iᶜ → Ioo x y = ∅
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : x < y
z : α
hz : z ∈ Ioo x y
hz' : z ∉ I
x' : α
hx' : x ≤ x'
hx'' : Maximal (fun x_1 ↦ x_1 ∈ I ∩ Icc x z) x'
hxz : x' < z
y' : α
hy' : y' ≤ y
hy'' : Minimal (fun x ↦ x ∈ I ∩ Icc z y) y'
hzy : z < y'
h₃ : Ioc x' z ⊆ Iᶜ
h₄ : Ico z y' ⊆ Iᶜ
⊢ Ioo x' y' ⊆ Iᶜ

Tactic:
simp only [← Ioc_union_Ico_eq_Ioo hxz hzy, union_subset_iff, and_true, h₃, h₄]

Goal state after:
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₂
w : P.Autᵐᵒᵖ
t : R
x : N
⊢ w • t • x = t • w • x

Tactic:
change unop (coweightHom P (unop w)) (t • x) = t • unop (coweightHom P (unop w)) x
    simp

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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
B : P.InvariantForm
inst✝ : P.IsIrreducible
i j j' : ι
h₁ : (B.form (P.root j')) (P.root j') = (B.form (P.root j)) (P.root j)
h₂ : (B.form (P.root i)) (P.root j') ≠ 0
this : P.pairingIn ℤ i j' ≠ 0
⊢ (B.form (P.root i)) (P.root i) = (B.form (P.root j)) (P.root j) ∨
    (B.form (P.root i)) (P.root i) = 2 * (B.form (P.root j)) (P.root j) ∨
      (B.form (P.root i)) (P.root i) = 3 * (B.form (P.root j)) (P.root j) ∨
        (B.form (P.root j)) (P.root j) = 2 * (B.form (P.root i)) (P.root i) ∨
          (B.form (P.root j)) (P.root j) = 3 * (B.form (P.root i)) (P.root i)

Tactic:
simp only [← h₁, B.apply_eq_or_aux i j' this]

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
i j k : ι
hi : b.IsPos i
hj : b.IsPos j
hk : P.root k = P.root i + P.root j
⊢ b.IsPos k

Tactic:
rw [isPos_iff] at hi hj ⊢

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
i j k : ι
hi : 0 < b.height i
hj : 0 < b.height j
hk : P.root k = P.root i + P.root j
⊢ 0 < b.height k
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✝ : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
⊢ ∃ j ∈ b.support, 0 < P.pairingIn ℤ j i

Tactic:
by_contra! contra
  suffices P.pairingIn ℤ i i ≤ 0 by simp_all
  obtain ⟨f, hf₀, hf₁, hf₂⟩ := b.exists_root_eq_sum_int i
  replace hf₁ : 0 < f := by
    refine hf₁.resolve_right ?_
    rw [isPos_iff, height_eq_sum hf₂] at h₀
    contrapose! h₀
    exact Finset.sum_nonpos fun i _ ↦ h₀.le i
  have : P.pairingIn ℤ i i = ∑ j ∈ b.support, f j • P.pairingIn ℤ j i :=
    algebraMap_injective ℤ R <| by
      simp_rw [algebraMap_pairingIn, map_sum, ← root_coroot_eq_pairing, hf₂, map_sum, map_zsmul,
        LinearMap.coe_sum, Finset.sum_apply, LinearMap.smul_apply, root_coroot_eq_pairing,
        zsmul_eq_mul, algebraMap_pairingIn]
  rw [this]
  refine Finset.sum_nonpos fun j _ ↦ ?_
  by_cases hj : j ∈ Function.support f
  · exact smul_nonpos_of_nonneg_of_nonpos (hf₁.le j) (contra j (hf₀ hj))
  · simp_all

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

Goal state before:
pp: R₂ : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
inst✝² : IsDomain R₂
inst✝¹ : Free R₂ M₂
inst✝ : Module.Finite R₂ M₂
B : BilinForm R₂ M₂
hB : SeparatingLeft B
ι : Type u_4
b : Basis ι R₂ M₂
this✝¹ : Finite ι
this✝ : Fintype ι
this : DecidableEq ι
⊢ B.Nondegenerate

Tactic:
rwa [← BilinForm.nondegenerate_toMatrix_iff b, Matrix.nondegenerate_iff_det_ne_zero,
    ← Matrix.separatingLeft_iff_det_ne_zero, separatingLeft_toMatrix_iff]

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f1 f2 g1 g2 : CauSeq β abv
hf : f1 ≈ f2
hg : g1 ≈ g2
⊢ f1 * g1 ≈ f2 * g2

Tactic:
by
  simpa only [mul_sub, sub_mul, sub_add_sub_cancel]
    using! add_limZero (mul_limZero_left g1 hf) (mul_limZero_right f2 hg)

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f1 f2 : CauSeq β abv
hf : f1 ≈ f2
n : ℕ
⊢ f1 ^ n ≈ f2 ^ n

Tactic:
by
  induction n with
  | zero => simp only [pow_zero, Setoid.refl]
  | succ n ih => simpa only [pow_succ'] using mul_equiv_mul hf ih

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
K : α
H : ∀ (i : ℕ), |↑f i| < K
i : ℕ
x✝ : i ≥ 0
⊢ ↑f i + 1 ≤ K + 1

Tactic:
add_le_add_iff_right

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
K : α
H : ∀ (i : ℕ), |↑f i| < K
i : ℕ
x✝ : i ≥ 0
⊢ ↑f i ≤ K
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a : ℝ
⊢ a ≤ a

Tactic:
induction a using Real.ind_mk

Goal state after:
case h
x : ℝ
y✝ : CauSeq ℚ abs
⊢ mk y✝ ≤ mk y✝
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b c : ℝ
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
induction a using Real.ind_mk

Goal state after:
case h
x b c : ℝ
y✝ : CauSeq ℚ abs
⊢ mk y✝ ≤ b → b ≤ c → mk y✝ ≤ c
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b : ℝ
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
induction a using Real.ind_mk

Goal state after:
case h
x b : ℝ
y✝ : CauSeq ℚ abs
⊢ mk y✝ < b ↔ mk y✝ ≤ b ∧ ¬b ≤ mk y✝
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b : ℝ
⊢ a ≤ b → b ≤ a → a = b

Tactic:
induction a using Real.ind_mk

Goal state after:
case h
x b : ℝ
y✝ : CauSeq ℚ abs
⊢ mk y✝ ≤ b → b ≤ mk y✝ → mk y✝ = b
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b : ℝ
⊢ 0 < a → 0 < b → 0 < a * b

Tactic:
induction a using Real.ind_mk

Goal state after:
case h
x b : ℝ
y✝ : CauSeq ℚ abs
⊢ 0 < mk y✝ → 0 < b → 0 < mk y✝ * b
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b : ℝ
⊢ a ≤ a ⊔ b

Tactic:
induction a using Real.ind_mk

Goal state after:
case h
x b : ℝ
y✝ : CauSeq ℚ abs
⊢ mk y✝ ≤ mk y✝ ⊔ b
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |↑(a₁ - a₂) j| < ε
bi : ℕ
hbi : ∀ j ≥ bi, |↑(b₁ - b₂) j| < ε
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) j| < ε

Tactic:
exact
    ⟨ai ⊔ bi, fun i hi =>
      (abs_min_sub_min_le_max (a₁ i) (b₁ i) (a₂ i) (b₂ i)).trans_lt
        (max_lt (hai i (sup_le_iff.mp hi).1) (hbi i (sup_le_iff.mp hi).2))⟩

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b : ℝ
⊢ b ≤ a ⊔ b

Tactic:
induction a using Real.ind_mk

Goal state after:
case h
x b : ℝ
y✝ : CauSeq ℚ abs
⊢ b ≤ mk y✝ ⊔ b
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b c : ℝ
⊢ a ≤ c → b ≤ c → a ⊔ b ≤ c

Tactic:
induction a using Real.ind_mk

Goal state after:
case h
x b c : ℝ
y✝ : CauSeq ℚ abs
⊢ mk y✝ ≤ c → b ≤ c → mk y✝ ⊔ b ≤ c
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b : ℝ
⊢ a ⊓ b ≤ a

Tactic:
induction a using Real.ind_mk

Goal state after:
case h
x b : ℝ
y✝ : CauSeq ℚ abs
⊢ mk y✝ ⊓ b ≤ mk y✝
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b : ℝ
⊢ a ⊓ b ≤ b

Tactic:
induction a using Real.ind_mk

Goal state after:
case h
x b : ℝ
y✝ : CauSeq ℚ abs
⊢ mk y✝ ⊓ b ≤ b
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b c : ℝ
⊢ a ≤ b → a ≤ c → a ≤ b ⊓ c

Tactic:
induction a using Real.ind_mk

Goal state after:
case h
x b c : ℝ
y✝ : CauSeq ℚ abs
⊢ mk y✝ ≤ b → mk y✝ ≤ c → mk y✝ ≤ b ⊓ c
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b c : ℝ
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c

Tactic:
induction a using Real.ind_mk

Goal state after:
case h
x b c : ℝ
y✝ : CauSeq ℚ abs
⊢ (mk y✝ ⊔ b) ⊓ (mk y✝ ⊔ c) ≤ mk y✝ ⊔ b ⊓ c
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x a b : ℝ
⊢ a ≤ b ∨ b ≤ a

Tactic:
induction a using Real.ind_mk

Goal state after:
case h
x b : ℝ
y✝ : CauSeq ℚ abs
⊢ mk y✝ ≤ b ∨ b ≤ mk y✝
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
hl : f.lim ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero
⊢ (f.inv hf - const abv f.lim⁻¹ - const abv f.lim * (f.inv hf * const abv f.lim⁻¹) +
      f * (f.inv hf * const abv f.lim⁻¹)).LimZero

Tactic:
sub_right_comm,

Goal state after:
α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
hl : f.lim ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero
⊢ (f.inv hf - const abv f.lim * (f.inv hf * const abv f.lim⁻¹) - const abv f.lim⁻¹ +
      f * (f.inv hf * const abv f.lim⁻¹)).LimZero
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hD : D.IsHermitian
⊢ (Matrix.fromBlocks D Bᴴ B A).IsHermitian ↔ (A - B * D⁻¹ * Bᴴ).IsHermitian

Tactic:
convert! IsHermitian.fromBlocks₁₁ _ _ hD

Goal state after:
case e'_1.e'_4.e'_8
α : Type u_1
m : Type u_3
n : Type u_4
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hD : D.IsHermitian
⊢ B = Bᴴᴴ

case e'_2
α : Type u_1
m : Type u_3
n : Type u_4
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hD : D.IsHermitian
⊢ B = Bᴴᴴ
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: case succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (A ^ ↑z).det ↔ IsUnit A.det ∨ ↑z = 0
⊢ IsUnit (A ^ (↑z + 1)).det ↔ IsUnit A.det ∨ ↑z + 1 = 0

Tactic:
| succ z =>

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

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ (A ^ n)ᵀ = Aᵀ ^ n

Tactic:
transpose_pow

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ Aᵀ ^ n = Aᵀ ^ n
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ (A ^ (n + 1))ᵀ⁻¹ = (Aᵀ ^ (n + 1))⁻¹

Tactic:
transpose_pow

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ (Aᵀ ^ (n + 1))⁻¹ = (Aᵀ ^ (n + 1))⁻¹
Module: Mathlib.Data.Nat.Factorial.BigOperators

Goal state before:
pp: n k : ℕ
⊢ n.descFactorial (k + 1) = ∏ i ∈ range (k + 1), (n - i)

Tactic:
rw [descFactorial, prod_range_succ_comm, descFactorial_eq_prod_range n k]

Goal state after: