mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : ⨆ i ∈ s, f i = ⊤
i : ι
hi : i ∈ s
h : IsAtomistic ↑(Iic (f i))
u : Set ↑(Iic (f i))
hu : ⊤ = sSup u
hu' : ∀ a ∈ u, IsAtom a
⊢ ∀ a ∈ Subtype.val '' u, IsAtom a

Tactic:
·

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : ⨆ i ∈ s, f i = ⊤
i : ι
hi : i ∈ s
h : IsAtomistic ↑(Iic (f i))
u : Set ↑(Iic (f i))
hu : ⊤ = sSup u
hu' : ∀ a ∈ u, IsAtom a
⊢ ∀ a ∈ Subtype.val '' u, IsAtom a
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2.mp
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
⊢ (∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1) →
    ((↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤

pp: case refine_2.mpr
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
⊢ (((↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤) →
    ∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1

Tactic:
·

Goal state after:
case refine_2.mp
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
⊢ (∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1) →
    ((↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : ∑ x ∈ t, (Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
hi : i = Exists.choose h
⊢ ↑(Pi.single (Exists.choose h) ⟨↑(μ a), ⋯⟩ i) + ↑⟨↑(μ i), ⋯⟩ = Pi.single (Exists.choose h) (↑(μ a)) i + ↑(μ i)

pp: case neg
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : ∑ x ∈ t, (Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
hi : ¬i = Exists.choose h
⊢ ↑(Pi.single (Exists.choose h) ⟨↑(μ a), ⋯⟩ i) + ↑⟨↑(μ i), ⋯⟩ = Pi.single (Exists.choose h) (↑(μ a)) i + ↑(μ i)

Tactic:
·

Goal state after:
case pos
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : ∑ x ∈ t, (Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
hi : i = Exists.choose h
⊢ ↑(Pi.single (Exists.choose h) ⟨↑(μ a), ⋯⟩ i) + ↑⟨↑(μ i), ⋯⟩ = Pi.single (Exists.choose h) (↑(μ a)) i + ↑(μ i)
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case inl
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
heq : normalizer ↑P = ⊤
⊢ normalizer ↑↑P = ⊤

pp: case inr
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer ↑P ≤ K
⊢ normalizer ↑↑P = ⊤

Tactic:
·

Goal state after:
case inl
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
heq : normalizer ↑P = ⊤
⊢ normalizer ↑↑P = ⊤
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case inr
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer ↑P ≤ K
⊢ normalizer ↑↑P = ⊤

Tactic:
·

Goal state after:
case inr
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer ↑P ≤ K
⊢ normalizer ↑↑P = ⊤
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : ∑ x ∈ t, (Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
hi : ¬i = Exists.choose h
⊢ ↑(Pi.single (Exists.choose h) ⟨↑(μ a), ⋯⟩ i) + ↑⟨↑(μ i), ⋯⟩ = Pi.single (Exists.choose h) (↑(μ a)) i + ↑(μ i)

Tactic:
·

Goal state after:
case neg
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : ∑ x ∈ t, (Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
hi : ¬i = Exists.choose h
⊢ ↑(Pi.single (Exists.choose h) ⟨↑(μ a), ⋯⟩ i) + ↑⟨↑(μ i), ⋯⟩ = Pi.single (Exists.choose h) (↑(μ a)) i + ↑(μ i)
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case refine_1
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ ((p : ↥ps) → (P : Sylow (↑p) G) → ↥P) ≃* ((p : ↥ps) → ↥(P ↑p))

pp: case refine_2
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ ((p : ↥ps) → ↥(P ↑p)) ≃* G

Tactic:
·

Goal state after:
case refine_1
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ ((p : ↥ps) → (P : Sylow (↑p) G) → ↥P) ≃* ((p : ↥ps) → ↥(P ↑p))
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case refine_2.left
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := ⋯
P : (p : ℕ) → Sylow p G := ⋯
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ Injective ⇑(noncommPiCoprod hcomm)

pp: case refine_2.right
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := ⋯
P : (p : ℕ) → Sylow p G := ⋯
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ Fintype.card ((i : ↥ps) → ↥↑(P ↑i)) = Fintype.card G

Tactic:
·

Goal state after:
case refine_2.left
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := ⋯
P : (p : ℕ) → Sylow p G := ⋯
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ Injective ⇑(noncommPiCoprod hcomm)
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
e : X × X → X × X → Prop
h_refl : ∀ {x : X × X}, e x x
h_symm : ∀ {x y : X × X}, e x y → e y x
h_trans : ∀ {x y z : X × X}, e x y → e y z → e x z
h_rel : ∀ {x y : X}, IsMaximal x (x ⊔ y) → e (x, x ⊔ y) (x ⊓ y, y)
x y : X × X
h_iso : Iso x y
⊢ e x y

Tactic:
by
  have : IsEquiv (X × X) e := { refl _ := h_refl, symm _ _ := h_symm, trans _ _ _ := h_trans }
  refine Relation.EqvGen.eqvGen_le ?_ _ _ h_iso
  rintro ⟨a, b⟩ ⟨c, d⟩ ⟨h, rfl : b = a ⊔ d, rfl : c = a ⊓ d⟩
  exact h_rel h

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case refine_2.right
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := ⋯
P : (p : ℕ) → Sylow p G := ⋯
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ Fintype.card ((i : ↥ps) → ↥↑(P ↑i)) = Fintype.card G

Tactic:
·

Goal state after:
case refine_2.right
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := ⋯
P : (p : ℕ) → Sylow p G := ⋯
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ Fintype.card ((i : ↥ps) → ↥↑(P ↑i)) = Fintype.card G
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ∑ x ∈ t, ↑(μ x) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ ∑ x ∈ t, ↑(μ x) ∈ I a

pp: case refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ∑ x ∈ t, ↑(μ x) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ ↑(μ a) ∈ I b

Tactic:
·

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ∑ x ∈ t, ↑(μ x) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ ∑ x ∈ t, ↑(μ x) ∈ I a
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case mp
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ (x ∈ range fun i ↦ s.toFun ⟨↑i, ⋯⟩) → x ≠ last s ∧ x ∈ range s.toFun

pp: case mpr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ x ≠ last s ∧ x ∈ range s.toFun → x ∈ range fun i ↦ s.toFun ⟨↑i, ⋯⟩

Tactic:
·

Goal state after:
case mp
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ (x ∈ range fun i ↦ s.toFun ⟨↑i, ⋯⟩) → x ≠ last s ∧ x ∈ range s.toFun
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case mpr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ x ≠ last s ∧ x ∈ range s.toFun → x ∈ range fun i ↦ s.toFun ⟨↑i, ⋯⟩

Tactic:
·

Goal state after:
case mpr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ x ≠ last s ∧ x ∈ range s.toFun → x ∈ range fun i ↦ s.toFun ⟨↑i, ⋯⟩
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
⊢ s.length - 1 < s.length

Tactic:
by lia

Goal state after:
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ∑ x ∈ t, ↑(μ x) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ ↑(μ a) ∈ I b

Tactic:
·

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ∑ x ∈ t, ↑(μ x) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ ↑(μ a) ∈ I b
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i : Fin (smash s₁ s₂ hs).length
⊢ ∀ (i : Fin s₁.length),
    Iso
      ((smash s₁ s₂ hs).toFun (Fin.castAdd s₂.length i).castSucc, (smash s₁ s₂ hs).toFun (Fin.castAdd s₂.length i).succ)
      ((smash t₁ t₂ ht).toFun (e (Fin.castAdd s₂.length i)).castSucc,
        (smash t₁ t₂ ht).toFun (e (Fin.castAdd s₂.length i)).succ)

pp: case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i : Fin (smash s₁ s₂ hs).length
⊢ ∀ (i : Fin s₂.length),
    Iso ((smash s₁ s₂ hs).toFun (Fin.natAdd s₁.length i).castSucc, (smash s₁ s₂ hs).toFun (Fin.natAdd s₁.length i).succ)
      ((smash t₁ t₂ ht).toFun (e (Fin.natAdd s₁.length i)).castSucc,
        (smash t₁ t₂ ht).toFun (e (Fin.natAdd s₁.length i)).succ)

Tactic:
·

Goal state after:
case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i : Fin (smash s₁ s₂ hs).length
⊢ ∀ (i : Fin s₁.length),
    Iso
      ((smash s₁ s₂ hs).toFun (Fin.castAdd s₂.length i).castSucc, (smash s₁ s₂ hs).toFun (Fin.castAdd s₂.length i).succ)
      ((smash t₁ t₂ ht).toFun (e (Fin.castAdd s₂.length i)).castSucc,
        (smash t₁ t₂ ht).toFun (e (Fin.castAdd s₂.length i)).succ)
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i : Fin (smash s₁ s₂ hs).length
⊢ ∀ (i : Fin s₂.length),
    Iso ((smash s₁ s₂ hs).toFun (Fin.natAdd s₁.length i).castSucc, (smash s₁ s₂ hs).toFun (Fin.natAdd s₁.length i).succ)
      ((smash t₁ t₂ ht).toFun (e (Fin.natAdd s₁.length i)).castSucc,
        (smash t₁ t₂ ht).toFun (e (Fin.natAdd s₁.length i)).succ)

Tactic:
·

Goal state after:
case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i : Fin (smash s₁ s₂ hs).length
⊢ ∀ (i : Fin s₂.length),
    Iso ((smash s₁ s₂ hs).toFun (Fin.natAdd s₁.length i).castSucc, (smash s₁ s₂ hs).toFun (Fin.natAdd s₁.length i).succ)
      ((smash t₁ t₂ ht).toFun (e (Fin.natAdd s₁.length i)).castSucc,
        (smash t₁ t₂ ht).toFun (e (Fin.natAdd s₁.length i)).succ)
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
he_castSucc : ∀ (j : Fin s₁.length), e j.castSucc = ((Exists.choose hequiv) j).castSucc
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ Iso
    ((snoc s₁ x₁ hsat₁).toFun
        (Fin.last (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)).castSucc,
      (snoc s₁ x₁ hsat₁).toFun (Fin.last (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)).succ)
    ((snoc s₂ x₂ hsat₂).toFun
        (e (Fin.last (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length))).castSucc,
      (snoc s₂ x₂ hsat₂).toFun
        (e (Fin.last (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length))).succ)

pp: case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
he_castSucc : ∀ (j : Fin s₁.length), e j.castSucc = ((Exists.choose hequiv) j).castSucc
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ ∀ (i : Fin (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)),
    Iso ((snoc s₁ x₁ hsat₁).toFun i.castSucc.castSucc, (snoc s₁ x₁ hsat₁).toFun i.castSucc.succ)
      ((snoc s₂ x₂ hsat₂).toFun (e i.castSucc).castSucc, (snoc s₂ x₂ hsat₂).toFun (e i.castSucc).succ)

Tactic:
·

Goal state after:
case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
he_castSucc : ∀ (j : Fin s₁.length), e j.castSucc = ((Exists.choose hequiv) j).castSucc
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ Iso
    ((snoc s₁ x₁ hsat₁).toFun
        (Fin.last (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)).castSucc,
      (snoc s₁ x₁ hsat₁).toFun (Fin.last (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)).succ)
    ((snoc s₂ x₂ hsat₂).toFun
        (e (Fin.last (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length))).castSucc,
      (snoc s₂ x₂ hsat₂).toFun
        (e (Fin.last (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length))).succ)
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2.mpr
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
⊢ (((↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤) →
    ∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1

Tactic:
·

Goal state after:
case refine_2.mpr
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
⊢ (((↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤) →
    ∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
he_castSucc : ∀ (j : Fin s₁.length), e j.castSucc = ((Exists.choose hequiv) j).castSucc
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ ∀ (i : Fin (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)),
    Iso ((snoc s₁ x₁ hsat₁).toFun i.castSucc.castSucc, (snoc s₁ x₁ hsat₁).toFun i.castSucc.succ)
      ((snoc s₂ x₂ hsat₂).toFun (e i.castSucc).castSucc, (snoc s₂ x₂ hsat₂).toFun (e i.castSucc).succ)

Tactic:
·

Goal state after:
case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
he_castSucc : ∀ (j : Fin s₁.length), e j.castSucc = ((Exists.choose hequiv) j).castSucc
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ ∀ (i : Fin (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)),
    Iso ((snoc s₁ x₁ hsat₁).toFun i.castSucc.castSucc, (snoc s₁ x₁ hsat₁).toFun i.castSucc.succ)
      ((snoc s₂ x₂ hsat₂).toFun (e i.castSucc).castSucc, (snoc s₂ x₂ hsat₂).toFun (e i.castSucc).succ)