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

Goal state before:
pp: case mp
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ (∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
      Injective ⇑(rTensor (M i) N.subtype)) →
    ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective ⇑(rTensor (M i) N.subtype)

pp: case mpr
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ (∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective ⇑(rTensor (M i) N.subtype)) →
    ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
      Injective ⇑(rTensor (M i) N.subtype)

Tactic:
<;>

Goal state after:
case mp
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ (∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
      Injective ⇑(rTensor (M i) N.subtype)) →
    ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective ⇑(rTensor (M i) N.subtype)

case mpr
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ (∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective ⇑(rTensor (M i) N.subtype)) →
    ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
      Injective ⇑(rTensor (M i) N.subtype)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: case mp
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ (∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
      Injective ⇑(rTensor (M i) N.subtype)) →
    ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective ⇑(rTensor (M i) N.subtype)

Tactic:
intro h; intros; apply h

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

Goal state before:
pp: case mpr
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ (∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective ⇑(rTensor (M i) N.subtype)) →
    ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
      Injective ⇑(rTensor (M i) N.subtype)

Tactic:
intro h; intros; apply h

Goal state after:
Module: Mathlib.Algebra.Azumaya.Basic

Goal state before:
pp: case ha
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
x✝¹ : A
x✝ : B
⊢ ((((AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e))).comp
          Algebra.TensorProduct.includeLeft)
        x✝¹)
      x✝ =
    ((((↑(LinearEquiv.conjAlgEquiv R ↑e)).comp (AlgHom.mulLeftRight R A)).comp Algebra.TensorProduct.includeLeft) x✝¹)
      x✝

pp: case hb
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
x✝¹ : Aᵐᵒᵖ
x✝ : B
⊢ (((AlgHom.restrictScalars R ((AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e)))).comp
          Algebra.TensorProduct.includeRight)
        x✝¹)
      x✝ =
    (((AlgHom.restrictScalars R ((↑(LinearEquiv.conjAlgEquiv R ↑e)).comp (AlgHom.mulLeftRight R A))).comp
          Algebra.TensorProduct.includeRight)
        x✝¹)
      x✝

Tactic:
<;>

Goal state after:
case ha
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
x✝¹ : A
x✝ : B
⊢ ((((AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e))).comp
          Algebra.TensorProduct.includeLeft)
        x✝¹)
      x✝ =
    ((((↑(LinearEquiv.conjAlgEquiv R ↑e)).comp (AlgHom.mulLeftRight R A)).comp Algebra.TensorProduct.includeLeft) x✝¹)
      x✝

case hb
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
x✝¹ : Aᵐᵒᵖ
x✝ : B
⊢ (((AlgHom.restrictScalars R ((AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e)))).comp
          Algebra.TensorProduct.includeRight)
        x✝¹)
      x✝ =
    (((AlgHom.restrictScalars R ((↑(LinearEquiv.conjAlgEquiv R ↑e)).comp (AlgHom.mulLeftRight R A))).comp
          Algebra.TensorProduct.includeRight)
        x✝¹)
      x✝
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : SMulCommClass R S A
inst✝ : Module.Flat R A
hb : Function.Injective ⇑(algebraMap R B)
⊢ Function.Injective ⇑includeLeft

Tactic:
convert!
    Module.Flat.lTensor_preserves_injective_linearMap (M := A) (Algebra.linearMap R B) hb |>.comp
      (_root_.TensorProduct.rid R A).symm.injective
  ext; simp

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

Goal state before:
pp: R : Type u_1
C : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring C
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Module.Flat R C
h : ∀ (B : Subalgebra R A), B.FG → IsReduced (C ⊗[R] ↥B)
h_contra : ¬IsReduced (C ⊗[R] A)
x : C ⊗[R] A
hx : x ≠ 0 ∧ IsNilpotent x
D : Subalgebra R A
hD : D.FG ∧ x ∈ Subalgebra.baseChange C D
h_inj : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id C C) D.val)
⊢ False

Tactic:
obtain ⟨z, rfl⟩ := hD.2

Goal state after:
R : Type u_1
C : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring C
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Module.Flat R C
h : ∀ (B : Subalgebra R A), B.FG → IsReduced (C ⊗[R] ↥B)
h_contra : ¬IsReduced (C ⊗[R] A)
D : Subalgebra R A
h_inj : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id C C) D.val)
z : C ⊗[R] ↥D
hx :
  (Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z ≠ 0 ∧
    IsNilpotent ((Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z)
hD : D.FG ∧ (Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z ∈ Subalgebra.baseChange C D
⊢ False
Module: Mathlib.Algebra.BigOperators.Balance

Goal state before:
pp: case inl
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
h✝ : IsEmpty ι
⊢ ∑ x, balance f x = 0

pp: case inr
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
h✝ : Nonempty ι
⊢ ∑ x, balance f x = 0

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
h✝ : IsEmpty ι
⊢ ∑ x, balance f x = 0

case inr
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
h✝ : Nonempty ι
⊢ ∑ x, balance f x = 0
Module: Mathlib.Algebra.BigOperators.Balance

Goal state before:
pp: case inl
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
h✝ : IsEmpty ι
⊢ balance (balance f) = balance f

pp: case inr
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
h✝ : Nonempty ι
⊢ balance (balance f) = balance f

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
h✝ : IsEmpty ι
⊢ balance (balance f) = balance f

case inr
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
h✝ : Nonempty ι
⊢ balance (balance f) = balance f
Module: Mathlib.Algebra.BigOperators.Balance

Goal state before:
pp: case inl
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
h✝ : IsEmpty ι
x : ι
⊢ balance (balance f) x = balance f x

pp: case inr
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
h✝ : Nonempty ι
x : ι
⊢ balance (balance f) x = balance f x

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
h✝ : IsEmpty ι
x : ι
⊢ balance (balance f) x = balance f x

case inr
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
h✝ : Nonempty ι
x : ι
⊢ balance (balance f) x = balance f x
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
t : Finset κ
f : ι → κ → M
⊢ 𝔼 i ∈ s, ∑ j ∈ t, f i j = ∑ j ∈ t, 𝔼 i ∈ s, f i j

Tactic:
by
  simpa only [expect, smul_sum] using sum_comm

Goal state after:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h✝ : ∃ i ∈ s, p i
⊢ (𝔼 i ∈ s, if p i then a else 0) = (↑(#s))⁻¹ • a

pp: case neg
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h✝ : ¬∃ i ∈ s, p i
⊢ (𝔼 i ∈ s, if p i then a else 0) = 0

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h✝ : ∃ i ∈ s, p i
⊢ (𝔼 i ∈ s, if p i then a else 0) = (↑(#s))⁻¹ • a

case neg
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h✝ : ¬∃ i ∈ s, p i
⊢ (𝔼 i ∈ s, if p i then a else 0) = 0
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → i = j → M
h✝ : i ∈ s
⊢ (𝔼 j ∈ s, if h : i = j then f j h else 0) = (↑(#s))⁻¹ • f i ⋯

pp: case neg
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → i = j → M
h✝ : i ∉ s
⊢ (𝔼 j ∈ s, if h : i = j then f j h else 0) = 0

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → i = j → M
h✝ : i ∈ s
⊢ (𝔼 j ∈ s, if h : i = j then f j h else 0) = (↑(#s))⁻¹ • f i ⋯

case neg
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → i = j → M
h✝ : i ∉ s
⊢ (𝔼 j ∈ s, if h : i = j then f j h else 0) = 0
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → j = i → M
h✝ : i ∈ s
⊢ (𝔼 j ∈ s, if h : j = i then f j h else 0) = (↑(#s))⁻¹ • f i ⋯

pp: case neg
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → j = i → M
h✝ : i ∉ s
⊢ (𝔼 j ∈ s, if h : j = i then f j h else 0) = 0

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → j = i → M
h✝ : i ∈ s
⊢ (𝔼 j ∈ s, if h : j = i then f j h else 0) = (↑(#s))⁻¹ • f i ⋯

case neg
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → j = i → M
h✝ : i ∉ s
⊢ (𝔼 j ∈ s, if h : j = i then f j h else 0) = 0
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
h✝ : i ∈ s
⊢ (𝔼 j ∈ s, if i = j then f j else 0) = (↑(#s))⁻¹ • f i

pp: case neg
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
h✝ : i ∉ s
⊢ (𝔼 j ∈ s, if i = j then f j else 0) = 0

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
h✝ : i ∈ s
⊢ (𝔼 j ∈ s, if i = j then f j else 0) = (↑(#s))⁻¹ • f i

case neg
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
h✝ : i ∉ s
⊢ (𝔼 j ∈ s, if i = j then f j else 0) = 0
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
h✝ : i ∈ s
⊢ (𝔼 j ∈ s, if j = i then f j else 0) = (↑(#s))⁻¹ • f i

pp: case neg
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
h✝ : i ∉ s
⊢ (𝔼 j ∈ s, if j = i then f j else 0) = 0

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
h✝ : i ∈ s
⊢ (𝔼 j ∈ s, if j = i then f j else 0) = (↑(#s))⁻¹ • f i

case neg
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
h✝ : i ∉ s
⊢ (𝔼 j ∈ s, if j = i then f j else 0) = 0
Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps

Goal state before:
pp: case i_inj.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
i : ℕ
hi : i < k
j : ℕ
hj : j < k
hij : ((p ↑i).2, (p ↑i.succ).1) = ((p ↑j).2, (p ↑j.succ).1)
⊢ i ∈ Set.Iio k

pp: case i_inj.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
i : ℕ
hi : i < k
j : ℕ
hj : j < k
hij : ((p ↑i).2, (p ↑i.succ).1) = ((p ↑j).2, (p ↑j.succ).1)
⊢ j ∈ Set.Iio k

pp: case i_inj.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
i : ℕ
hi : i < k
j : ℕ
hj : j < k
hij : ((p ↑i).2, (p ↑i.succ).1) = ((p ↑j).2, (p ↑j.succ).1)
⊢ (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) i =
    (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) j

Tactic:
<;>

Goal state after:
case i_inj.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
i : ℕ
hi : i < k
j : ℕ
hj : j < k
hij : ((p ↑i).2, (p ↑i.succ).1) = ((p ↑j).2, (p ↑j.succ).1)
⊢ i ∈ Set.Iio k

case i_inj.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
i : ℕ
hi : i < k
j : ℕ
hj : j < k
hij : ((p ↑i).2, (p ↑i.succ).1) = ((p ↑j).2, (p ↑j.succ).1)
⊢ j ∈ Set.Iio k

case i_inj.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
i : ℕ
hi : i < k
j : ℕ
hj : j < k
hij : ((p ↑i).2, (p ↑i.succ).1) = ((p ↑j).2, (p ↑j.succ).1)
⊢ (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) i =
    (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) j
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case e'_3
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
this : ∀ j < k + 1, (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2
hj : ¬j < k + 1
⊢ ↑j = ↑↑↑j

pp: case e'_4
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
this : ∀ j < k + 1, (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2
hj : ¬j < k + 1
⊢ ↑j = ↑↑↑j

Tactic:
<;>

Goal state after:
case e'_3
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
this : ∀ j < k + 1, (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2
hj : ¬j < k + 1
⊢ ↑j = ↑↑↑j

case e'_4
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
this : ∀ j < k + 1, (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2
hj : ¬j < k + 1
⊢ ↑j = ↑↑↑j
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case add.a
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((f x) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
x✝ y✝ : M₁ ⊗[R] M₂
a✝¹ : motive ((TensorProduct.lift f) x✝)
a✝ : motive ((TensorProduct.lift f) y✝)
⊢ motive ((TensorProduct.lift f) x✝)

pp: case add.a
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((f x) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
x✝ y✝ : M₁ ⊗[R] M₂
a✝¹ : motive ((TensorProduct.lift f) x✝)
a✝ : motive ((TensorProduct.lift f) y✝)
⊢ motive ((TensorProduct.lift f) y✝)

Tactic:
<;>

Goal state after:
case add.a
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((f x) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
x✝ y✝ : M₁ ⊗[R] M₂
a✝¹ : motive ((TensorProduct.lift f) x✝)
a✝ : motive ((TensorProduct.lift f) y✝)
⊢ motive ((TensorProduct.lift f) x✝)

case add.a
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((f x) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
x✝ y✝ : M₁ ⊗[R] M₂
a✝¹ : motive ((TensorProduct.lift f) x✝)
a✝ : motive ((TensorProduct.lift f) y✝)
⊢ motive ((TensorProduct.lift f) y✝)
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: case nil
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
h : ∀ x ∈ [], f x ≡ g x [MOD n]
⊢ (List.map f []).prod ≡ (List.map g []).prod [MOD n]

pp: case cons
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ x ∈ tail✝, f x ≡ g x [MOD n]) → (List.map f tail✝).prod ≡ (List.map g tail✝).prod [MOD n]
h : ∀ x ∈ head✝ :: tail✝, f x ≡ g x [MOD n]
⊢ (List.map f (head✝ :: tail✝)).prod ≡ (List.map g (head✝ :: tail✝)).prod [MOD n]

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
h : ∀ x ∈ [], f x ≡ g x [MOD n]
⊢ (List.map f []).prod ≡ (List.map g []).prod [MOD n]

case cons
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ x ∈ tail✝, f x ≡ g x [MOD n]) → (List.map f tail✝).prod ≡ (List.map g tail✝).prod [MOD n]
h : ∀ x ∈ head✝ :: tail✝, f x ≡ g x [MOD n]
⊢ (List.map f (head✝ :: tail✝)).prod ≡ (List.map g (head✝ :: tail✝)).prod [MOD n]
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: case nil
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
h : ∀ x ∈ [], f x ≡ g x [MOD n]
⊢ (List.map f []).sum ≡ (List.map g []).sum [MOD n]

pp: case cons
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ x ∈ tail✝, f x ≡ g x [MOD n]) → (List.map f tail✝).sum ≡ (List.map g tail✝).sum [MOD n]
h : ∀ x ∈ head✝ :: tail✝, f x ≡ g x [MOD n]
⊢ (List.map f (head✝ :: tail✝)).sum ≡ (List.map g (head✝ :: tail✝)).sum [MOD n]

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
h : ∀ x ∈ [], f x ≡ g x [MOD n]
⊢ (List.map f []).sum ≡ (List.map g []).sum [MOD n]

case cons
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ x ∈ tail✝, f x ≡ g x [MOD n]) → (List.map f tail✝).sum ≡ (List.map g tail✝).sum [MOD n]
h : ∀ x ∈ head✝ :: tail✝, f x ≡ g x [MOD n]
⊢ (List.map f (head✝ :: tail✝)).sum ≡ (List.map g (head✝ :: tail✝)).sum [MOD n]
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: case h₀
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 1
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 1
⊢ ∀ b ∈ s, b ≠ a → ↑(f b) = 1

pp: case h₁
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 1
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 1
⊢ a ∉ s → ↑(f a) = 1

Tactic:
<;>

Goal state after:
case h₀
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 1
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 1
⊢ ∀ b ∈ s, b ≠ a → ↑(f b) = 1

case h₁
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 1
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 1
⊢ a ∉ s → ↑(f a) = 1
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: case h₀
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 0
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 0
⊢ ∀ b ∈ s, b ≠ a → ↑(f b) = 0

pp: case h₁
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 0
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 0
⊢ a ∉ s → ↑(f a) = 0

Tactic:
<;>

Goal state after:
case h₀
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 0
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 0
⊢ ∀ b ∈ s, b ≠ a → ↑(f b) = 0

case h₁
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 0
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 0
⊢ a ∉ s → ↑(f a) = 0
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: case nil
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
h : ∀ x ∈ [], f x ≡ g x [ZMOD n]
⊢ (List.map f []).prod ≡ (List.map g []).prod [ZMOD n]

pp: case cons
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ x ∈ tail✝, f x ≡ g x [ZMOD n]) → (List.map f tail✝).prod ≡ (List.map g tail✝).prod [ZMOD n]
h : ∀ x ∈ head✝ :: tail✝, f x ≡ g x [ZMOD n]
⊢ (List.map f (head✝ :: tail✝)).prod ≡ (List.map g (head✝ :: tail✝)).prod [ZMOD n]

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
h : ∀ x ∈ [], f x ≡ g x [ZMOD n]
⊢ (List.map f []).prod ≡ (List.map g []).prod [ZMOD n]

case cons
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ x ∈ tail✝, f x ≡ g x [ZMOD n]) → (List.map f tail✝).prod ≡ (List.map g tail✝).prod [ZMOD n]
h : ∀ x ∈ head✝ :: tail✝, f x ≡ g x [ZMOD n]
⊢ (List.map f (head✝ :: tail✝)).prod ≡ (List.map g (head✝ :: tail✝)).prod [ZMOD n]