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

Goal state before:
pp: R : Type u_5
R' : Type u_6
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring R'
r : R' → R' → Prop
f : R ≃+* R'
⊢ (ringConGen r).comap f ≤ ((ringConGen (r on ⇑f)).comap f.symm.toNonUnitalRingHom).comap f.toNonUnitalRingHom

pp: R : Type u_5
R' : Type u_6
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring R'
r : R' → R' → Prop
f : R ≃+* R'
⊢ ((ringConGen (r on ⇑f)).comap f.symm.toNonUnitalRingHom).comap f.toNonUnitalRingHom ≤ ringConGen (r on ⇑f)

Tactic:
·

Goal state after:
R : Type u_5
R' : Type u_6
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring R'
r : R' → R' → Prop
f : R ≃+* R'
⊢ (ringConGen r).comap f ≤ ((ringConGen (r on ⇑f)).comap f.symm.toNonUnitalRingHom).comap f.toNonUnitalRingHom
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: R : Type u_5
R' : Type u_6
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring R'
r : R' → R' → Prop
f : R ≃+* R'
⊢ ((ringConGen (r on ⇑f)).comap f.symm.toNonUnitalRingHom).comap f.toNonUnitalRingHom ≤ ringConGen (r on ⇑f)

Tactic:
·

Goal state after:
R : Type u_5
R' : Type u_6
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring R'
r : R' → R' → Prop
f : R ≃+* R'
⊢ ((ringConGen (r on ⇑f)).comap f.symm.toNonUnitalRingHom).comap f.toNonUnitalRingHom ≤ ringConGen (r on ⇑f)
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: R : Type u
inst✝ : Semiring R
h : IsField R
a : R
ha : a ≠ 0
⊢ (if ha : a = 0 then 0 else Classical.choose ⋯) = Classical.choose ⋯

Tactic:
exact dif_neg ha

Goal state after:
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: case hex
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃ x_1, x * x_1 = 1

pp: case hunique
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∀ (y₁ y₂ : R), x * y₁ = 1 → x * y₂ = 1 → y₁ = y₂

Tactic:
·

Goal state after:
case hex
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃ x_1, x * x_1 = 1
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: case hunique
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∀ (y₁ y₂ : R), x * y₁ = 1 → x * y₂ = 1 → y₁ = y₂

Tactic:
·

Goal state after:
case hunique
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∀ (y₁ y₂ : R), x * y₁ = 1 → x * y₂ = 1 → y₁ = y₂
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : IsMax a
⊢ Ico (succ a) b = Ioo a b

pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ico (succ a) b = Ioo a b

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : IsMax a
⊢ Ico (succ a) b = Ioo a b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ico (succ a) b = Ioo a b

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ico (succ a) b = Ioo a b
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case pos
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
hiI : i ∈ I
⊢ b i = 0 i

pp: case neg
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
hiI : i ∉ I
⊢ b i = 0 i

Tactic:
·

Goal state after:
case pos
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
hiI : i ∈ I
⊢ b i = 0 i
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case pos
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
hiI : i ∈ I
hiJ : i ∈ J
⊢ b i = 0 i

pp: case neg
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
hiI : i ∈ I
hiJ : i ∉ J
⊢ b i = 0 i

Tactic:
·

Goal state after:
case pos
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
hiI : i ∈ I
hiJ : i ∈ J
⊢ b i = 0 i
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case neg
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
hiI : i ∈ I
hiJ : i ∉ J
⊢ b i = 0 i

Tactic:
·

Goal state after:
case neg
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
hiI : i ∈ I
hiJ : i ∉ J
⊢ b i = 0 i
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case neg
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
hiI : i ∉ I
⊢ b i = 0 i

Tactic:
·

Goal state after:
case neg
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
hiI : i ∉ I
⊢ b i = 0 i
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (∃ y, (inl R M M₂) y = x) → (snd R M M₂) x = 0

pp: case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (snd R M M₂) x = 0 → ∃ y, (inl R M M₂) y = x

Tactic:
·

Goal state after:
case mp
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (∃ y, (inl R M M₂) y = x) → (snd R M M₂) x = 0
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (∃ y, (inl R M M₂) y = x) → (snd R M M₂) x = 0

Tactic:
rintro ⟨y, rfl⟩
    rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (snd R M M₂) x = 0 → ∃ y, (inl R M M₂) y = x

Tactic:
·

Goal state after:
case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (snd R M M₂) x = 0 → ∃ y, (inl R M M₂) y = x
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (∃ y, (inr R M M₂) y = x) → (fst R M M₂) x = 0

pp: case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (fst R M M₂) x = 0 → ∃ y, (inr R M M₂) y = x

Tactic:
·

Goal state after:
case mp
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (∃ y, (inr R M M₂) y = x) → (fst R M M₂) x = 0
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (∃ y, (inr R M M₂) y = x) → (fst R M M₂) x = 0

Tactic:
rintro ⟨y, rfl⟩
    rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (fst R M M₂) x = 0 → ∃ y, (inr R M M₂) y = x

Tactic:
·

Goal state after:
case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (fst R M M₂) x = 0 → ∃ y, (inr R M M₂) y = x
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : IsMin b
⊢ Ioc a (pred b) = Ioo a b

pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : ¬IsMin b
⊢ Ioc a (pred b) = Ioo a b

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : IsMin b
⊢ Ioc a (pred b) = Ioo a b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : ¬IsMin b
⊢ Ioc a (pred b) = Ioo a b

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : ¬IsMin b
⊢ Ioc a (pred b) = Ioo a b
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_1
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
⊢ ∀ (c : (i : ↑I) → φ ↑i), (pi fun i ↦ if h : i ∈ I then proj ⟨i, h⟩ else 0) c ∈ ⨅ i ∈ J, (proj i).ker

pp: case refine_2
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
⊢ (pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) ∘ₗ
      codRestrict (⨅ i ∈ J, (proj i).ker) (pi fun i ↦ if h : i ∈ I then proj ⟨i, h⟩ else 0) ?refine_1 =
    id

pp: case refine_3
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
⊢ (codRestrict (⨅ i ∈ J, (proj i).ker) (pi fun i ↦ if h : i ∈ I then proj ⟨i, h⟩ else 0) ?refine_1 ∘ₗ
      pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) =
    id

Tactic:
·

Goal state after:
case refine_1
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
⊢ ∀ (c : (i : ↑I) → φ ↑i), (pi fun i ↦ if h : i ∈ I then proj ⟨i, h⟩ else 0) c ∈ ⨅ i ∈ J, (proj i).ker
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : IsMin b
⊢ Icc (succ a) (pred b) = Ioo a b

pp: case neg
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : ¬IsMin b
⊢ Icc (succ a) (pred b) = Ioo a b

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : IsMin b
⊢ Icc (succ a) (pred b) = Ioo a b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : ¬IsMin b
⊢ Icc (succ a) (pred b) = Ioo a b

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : ¬IsMin b
⊢ Icc (succ a) (pred b) = Ioo a b
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_2
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
⊢ (pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) ∘ₗ
      codRestrict (⨅ i ∈ J, (proj i).ker) (pi fun i ↦ if h : i ∈ I then proj ⟨i, h⟩ else 0) ⋯ =
    id

pp: case refine_3
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
⊢ (codRestrict (⨅ i ∈ J, (proj i).ker) (pi fun i ↦ if h : i ∈ I then proj ⟨i, h⟩ else 0) ⋯ ∘ₗ
      pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) =
    id

Tactic:
·

Goal state after:
case refine_2
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
⊢ (pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) ∘ₗ
      codRestrict (⨅ i ∈ J, (proj i).ker) (pi fun i ↦ if h : i ∈ I then proj ⟨i, h⟩ else 0) ⋯ =
    id
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_3
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
⊢ (codRestrict (⨅ i ∈ J, (proj i).ker) (pi fun i ↦ if h : i ∈ I then proj ⟨i, h⟩ else 0) ⋯ ∘ₗ
      pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) =
    id

Tactic:
·

Goal state after:
case refine_3
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
⊢ (codRestrict (⨅ i ∈ J, (proj i).ker) (pi fun i ↦ if h : i ∈ I then proj ⟨i, h⟩ else 0) ⋯ ∘ₗ
      pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) =
    id
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case disjoint
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ Disjoint (inl R M M₂).range (inr R M M₂).range

pp: case codisjoint
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ Codisjoint (inl R M M₂).range (inr R M M₂).range

Tactic:
·

Goal state after:
case disjoint
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ Disjoint (inl R M M₂).range (inr R M M₂).range
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case codisjoint
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ Codisjoint (inl R M M₂).range (inr R M M₂).range

Tactic:
·

Goal state after:
case codisjoint
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ Codisjoint (inl R M M₂).range (inr R M M₂).range
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case pos
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb✝ : b ∈ ⨅ i ∈ J, (proj i).ker
j : ι
hb : ∀ i ∈ J, b i = 0
h : j ∈ I
⊢ (proj ⟨j, h⟩) ((pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) ⟨b, hb✝⟩) = b j

pp: case neg
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb✝ : b ∈ ⨅ i ∈ J, (proj i).ker
j : ι
hb : ∀ i ∈ J, b i = 0
h : j ∉ I
⊢ 0 ((pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) ⟨b, hb✝⟩) = b j

Tactic:
·

Goal state after:
case pos
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb✝ : b ∈ ⨅ i ∈ J, (proj i).ker
j : ι
hb : ∀ i ∈ J, b i = 0
h : j ∈ I
⊢ (proj ⟨j, h⟩) ((pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) ⟨b, hb✝⟩) = b j
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case neg
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb✝ : b ∈ ⨅ i ∈ J, (proj i).ker
j : ι
hb : ∀ i ∈ J, b i = 0
h : j ∉ I
⊢ 0 ((pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) ⟨b, hb✝⟩) = b j

Tactic:
·

Goal state after:
case neg
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb✝ : b ∈ ⨅ i ∈ J, (proj i).ker
j : ι
hb : ∀ i ∈ J, b i = 0
h : j ∉ I
⊢ 0 ((pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) ⟨b, hb✝⟩) = b j
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case pos
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : j = i
⊢ (update f i b j) c = update (fun i ↦ (f i) c) i (b c) j

pp: case neg
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : ¬j = i
⊢ (update f i b j) c = update (fun i ↦ (f i) c) i (b c) j

Tactic:
·

Goal state after:
case pos
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : j = i
⊢ (update f i b j) c = update (fun i ↦ (f i) c) i (b c) j
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case neg
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : ¬j = i
⊢ (update f i b j) c = update (fun i ↦ (f i) c) i (b c) j

Tactic:
·

Goal state after:
case neg
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : ¬j = i
⊢ (update f i b j) c = update (fun i ↦ (f i) c) i (b c) j
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : PredOrder α
a b : α
h : a < b
⊢ ↑(insert b (Ioc a (pred b))) = ↑(Ioc a b)

Tactic:
by simpa using Set.insert_Ioc_pred_right_eq_Ioc h

Goal state after: