mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case refine_3
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
⊢ {x | K x = D}.card = D.index → {x | x ∈ s ∧ (H x).FiniteIndex}.PairwiseDisjoint fun i ↦ g i • ↑(H i)

Tactic:
]

Goal state after:
case refine_3
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
⊢ {x | K x = D}.card = D.index → {x | x ∈ s ∧ (H x).FiniteIndex}.PairwiseDisjoint fun i ↦ g i • ↑(H i)
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case refine_3
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
h : {x | K x = D}.card = D.index
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i ≠ j
c : Set G
hi' : c ⊆ (fun i ↦ g i • ↑(H i)) i
hj' : c ⊆ (fun i ↦ g i • ↑(H i)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x | K x = D}).PairwiseDisjoint fun x ↦ f x • ↑D
⊢ x ∈ ⊥

Tactic:
]

Goal state after:
case refine_3
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
h : {x | K x = D}.card = D.index
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i ≠ j
c : Set G
hi' : c ⊆ (fun i ↦ g i • ↑(H i)) i
hj' : c ⊆ (fun i ↦ g i • ↑(H i)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x | K x = D}).PairwiseDisjoint fun x ↦ f x • ↑D
⊢ x ∈ ⊥
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
h : {x | K x = D}.card = D.index
i✝ : ι
hi✝ : i✝ ∈ s ∧ (H i✝).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i✝ ≠ j
c : Set G
hi'✝ : c ⊆ (fun i ↦ g i • ↑(H i)) i✝
hj' : c ⊆ (fun i ↦ g i • ↑(H i)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x | K x = D}).PairwiseDisjoint fun x ↦ f x • ↑D
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
hi' : c ⊆ g i • ⋃ g ∈ t i ⋯ ⋯, ↑g • ↑D
⊢ ∃ k, ↑k.fst = i ∧ K k = D ∧ x ∈ f k • ↑D

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
h : {x | K x = D}.card = D.index
i✝ : ι
hi✝ : i✝ ∈ s ∧ (H i✝).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i✝ ≠ j
c : Set G
hi'✝ : c ⊆ (fun i ↦ g i • ↑(H i)) i✝
hj' : c ⊆ (fun i ↦ g i • ↑(H i)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x | K x = D}).PairwiseDisjoint fun x ↦ f x • ↑D
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
hi' : c ⊆ g i • ⋃ g ∈ t i ⋯ ⋯, ↑g • ↑D
⊢ ∃ k, ↑k.fst = i ∧ K k = D ∧ x ∈ f k • ↑D
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
B : Subalgebra R S
⊢ Submodule.LinearDisjoint 1 (toSubmodule B)

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
B : Subalgebra R S
⊢ Submodule.LinearDisjoint 1 (toSubmodule B)
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
A : Subalgebra R S
⊢ (toSubmodule A).LinearDisjoint 1

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
A : Subalgebra R S
⊢ (toSubmodule A).LinearDisjoint 1
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
B : Type w
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Function.Injective
    ⇑((toSubmodule Algebra.TensorProduct.includeLeft.range).mulMap
        (toSubmodule Algebra.TensorProduct.includeRight.range))

Tactic:
]

Goal state after:
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
B : Type w
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Function.Injective
    ⇑((toSubmodule Algebra.TensorProduct.includeLeft.range).mulMap
        (toSubmodule Algebra.TensorProduct.includeRight.range))
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
B : Type w
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Function.Injective ⇑↑(Algebra.TensorProduct.linearEquivIncludeRange R A B).symm

Tactic:
]

Goal state after:
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
B : Type w
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Function.Injective ⇑↑(Algebra.TensorProduct.linearEquivIncludeRange R A B).symm
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
⊢ Function.Injective ⇑((toSubmodule A).mulMap (toSubmodule B)) ↔ Function.Injective ⇑(A.mulMap B)

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
⊢ Function.Injective ⇑((toSubmodule A).mulMap (toSubmodule B)) ↔ Function.Injective ⇑(A.mulMap B)
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
⊢ restrictScalars R (Algebra.TensorProduct.productLeftAlgHom (Algebra.ofId (↥A) S) B.val).range = A ⊔ B

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
⊢ restrictScalars R (Algebra.TensorProduct.productLeftAlgHom (Algebra.ofId (↥A) S) B.val).range = A ⊔ B
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case refine_3
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
h : {x | K x = D}.card = D.index
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i ≠ j
c : Set G
hi' : c ⊆ (fun i ↦ g i • ↑(H i)) i
hj' : c ⊆ (fun i ↦ g i • ↑(H i)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x | K x = D}).PairwiseDisjoint fun x ↦ f x • ↑D
hk' : ∀ (i : ι), i ∈ s ∧ (H i).FiniteIndex → c ⊆ g i • ↑(H i) → ∃ k, ↑k.fst = i ∧ K k = D ∧ x ∈ f k • ↑D
k₁ : κ
hik₁ : ↑k₁.fst = i
hk₁ : K k₁ = D
hxk₁ : {x} ⊆ f k₁ • ↑D
k₂ : κ
hjk₂ : ↑k₂.fst = j
hk₂ : K k₂ = D
hxk₂ : {x} ⊆ f k₂ • ↑D
⊢ {x} ⊆ ⊥

Tactic:
]

Goal state after:
case refine_3
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
h : {x | K x = D}.card = D.index
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i ≠ j
c : Set G
hi' : c ⊆ (fun i ↦ g i • ↑(H i)) i
hj' : c ⊆ (fun i ↦ g i • ↑(H i)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x | K x = D}).PairwiseDisjoint fun x ↦ f x • ↑D
hk' : ∀ (i : ι), i ∈ s ∧ (H i).FiniteIndex → c ⊆ g i • ↑(H i) → ∃ k, ↑k.fst = i ∧ K k = D ∧ x ∈ f k • ↑D
k₁ : κ
hik₁ : ↑k₁.fst = i
hk₁ : K k₁ = D
hxk₁ : {x} ⊆ f k₁ • ↑D
k₂ : κ
hjk₂ : ↑k₂.fst = j
hk₂ : K k₂ = D
hxk₂ : {x} ⊆ f k₂ • ↑D
⊢ {x} ⊆ ⊥
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
ι : Type u_1
b : Basis ι R ↥A
⊢ A ⊔ B = ⊤

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
ι : Type u_1
b : Basis ι R ↥A
⊢ A ⊔ B = ⊤
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
ι : Type u_1
b : Basis ι R ↥A
i : ι
⊢ A ⊔ B = ⊤

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
ι : Type u_1
b : Basis ι R ↥A
i : ι
⊢ A ⊔ B = ⊤
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
ι : Type u_1
b : Basis ι R ↥A
x : ↥A
i : ι
⊢ A ⊔ B = ⊤

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
ι : Type u_1
b : Basis ι R ↥A
x : ↥A
i : ι
⊢ A ⊔ B = ⊤
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : ι → ↥A
i : (ι →₀ ↥B) →ₗ[R] S := Submodule.mulLeftMap (toSubmodule B) a
j : (ι →₀ ↥B) →ₗ[R] S :=
  ↑(MulOpposite.opLinearEquiv R).symm ∘ₗ
    ↑R (Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)) ∘ₗ
      ↑(Finsupp.mapRange.linearEquiv B.linearEquivOp)
this : i = j
⊢ Function.Injective ⇑(Submodule.mulLeftMap (toSubmodule B) a) ↔
    Function.Injective ⇑(Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a))

Tactic:
change Function.Injective i ↔ _

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : ι → ↥A
i : (ι →₀ ↥B) →ₗ[R] S := Submodule.mulLeftMap (toSubmodule B) a
j : (ι →₀ ↥B) →ₗ[R] S :=
  ↑(MulOpposite.opLinearEquiv R).symm ∘ₗ
    ↑R (Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)) ∘ₗ
      ↑(Finsupp.mapRange.linearEquiv B.linearEquivOp)
this : i = j
⊢ Function.Injective ⇑i ↔ Function.Injective ⇑(Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a))
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
i : ι
hi : i ∈ s
hindex : (H i).index = 0
⊢ 0 < s.card

Tactic:
]

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
i : ι
hi : i ∈ s
hindex : (H i).index = 0
⊢ 0 < s.card
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝ : Flat R ↥B
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent R a
h : LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)
⊢ LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝ : Flat R ↥B
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent R a
h : LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)
⊢ LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : Basis ι R ↥A
H : (Submodule.mulLeftMap (toSubmodule B) ⇑a).ker = ⊥
⊢ A.LinearDisjoint B

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : Basis ι R ↥A
H : (Submodule.mulLeftMap (toSubmodule B) ⇑a).ker = ⊥
⊢ A.LinearDisjoint B
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : ι → ↥B
i : (ι →₀ ↥A) →ₗ[R] S := (toSubmodule A).mulRightMap b
j : (ι →₀ ↥A) →ₗ[R] S := ↑R (Finsupp.linearCombination (↥A) (⇑B.val ∘ b))
this : i = j
⊢ Function.Injective ⇑j ↔ Function.Injective ⇑j

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
hlt : ∀ i ∈ s, (↑(H i).index)⁻¹ < (↑s.card)⁻¹
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝ : Flat R ↥A
ι : Type u_1
b : ι → ↥B
hb : LinearIndependent R b
h : LinearIndependent (↥A) (⇑B.val ∘ b)
⊢ LinearIndependent (↥A) (⇑B.val ∘ b)

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝ : Flat R ↥A
ι : Type u_1
b : ι → ↥B
hb : LinearIndependent R b
h : LinearIndependent (↥A) (⇑B.val ∘ b)
⊢ LinearIndependent (↥A) (⇑B.val ∘ b)
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : Basis ι R ↥B
H : ((toSubmodule A).mulRightMap ⇑b).ker = ⊥
⊢ A.LinearDisjoint B

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : Basis ι R ↥B
H : ((toSubmodule A).mulRightMap ⇑b).ker = ⊥
⊢ A.LinearDisjoint B
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
⊢ x = 0 ↔ x = 0

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : L
⊢ x✝ = 0 ↔ x✝ = 0

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: case h.h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : L
H : ∀ (x_1 : L), mk K x_1 = mk K x ↔ mk K x_1 = mk K y
⊢ mk K x = mk K x

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
S : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field S
inst✝³ : Algebra K L
inst✝² : Algebra K S
inst✝¹ : Algebra L S
inst✝ : IsScalarTower K L S
x✝ : L
⊢ mk K x✝ = mk K x✝

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat R ↥A ∨ Flat R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
a✝ : Nontrivial R
this : Module.rank R ↥⊥ = 1
⊢ 1 ≤ Module.rank R ↥(A ⊓ B)

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat R ↥A ∨ Flat R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
a✝ : Nontrivial R
this : Module.rank R ↥⊥ = 1
⊢ 1 ≤ Module.rank R ↥(A ⊓ B)
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
a b : L
h : a + b = 0
⊢ IsConjRoot K (-b) (-b)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat R ↥A ∨ Flat R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
a✝ : Nontrivial R
this : Module.rank R ↥⊥ = 1
⊢ Module.rank R ↥⊥ ≤ Module.rank R ↥(A ⊓ B)

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat R ↥A ∨ Flat R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
a✝ : Nontrivial R
this : Module.rank R ↥⊥ = 1
⊢ Module.rank R ↥⊥ ≤ Module.rank R ↥(A ⊓ B)
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
n : Normal K L
x✝ : L
⊢ (map (algebraMap K L) (minpoly K x✝)).Splits

Tactic:
]

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
n : Normal K L
x✝ : L
⊢ (map (algebraMap K L) (minpoly K x✝)).Splits
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
x✝ : L
⊢ (minpoly K x✝).Monic

Tactic:
]

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
x✝ : L
⊢ (minpoly K x✝).Monic
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
x✝ : L
⊢ Irreducible (minpoly K x✝)

Tactic:
]

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
x✝ : L
⊢ Irreducible (minpoly K x✝)