mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Small.{u, u_1} R
n : ℕ
s : Fin n → M
⊢ Small.{u, u_2} ↥(span R (Set.range s))

Tactic:
rw [← Fintype.range_linearCombination]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Small.{u, u_1} R
n : ℕ
s : Fin n → M
⊢ Small.{u, u_2} ↥(Fintype.linearCombination R s).range
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case e'_2
R : Type u_1
inst✝² : CommRing R
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
I : Ideal R
⊢ (TensorProduct.mk R (R ⧸ I) Q) 1 ∘ₗ ↑(TensorProduct.lid R Q) = rTensor Q (mkQ I)

Tactic:
ext

Goal state after:
case e'_2
R : Type u_1
inst✝² : CommRing R
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
I : Ideal R
x✝ : Q
⊢ ((AlgebraTensorModule.curry ((TensorProduct.mk R (R ⧸ I) Q) 1 ∘ₗ ↑(TensorProduct.lid R Q))) 1) x✝ =
    ((AlgebraTensorModule.curry (rTensor Q (mkQ I))) 1) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
h : s ⊆ ↑(map M'.subtype N'.subtype).range
hM : Submodule.map M₁.subtype M' ≤ M₁
hN : Submodule.map N₁.subtype N' ≤ N₁
⊢ M'.subtype = inclusion hM ∘ₗ M₁.subtype.submoduleMap M'

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
h : s ⊆ ↑(map M'.subtype N'.subtype).range
hM : Submodule.map M₁.subtype M' ≤ M₁
hN : Submodule.map N₁.subtype N' ≤ N₁
x✝ : ↥M'
⊢ ↑(M'.subtype x✝) = ↑((inclusion hM ∘ₗ M₁.subtype.submoduleMap M') x✝)
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
hM : Submodule.map M₁.subtype M' ≤ M₁
h : s ⊆ ↑(map (inclusion hM ∘ₗ M₁.subtype.submoduleMap M') N'.subtype).range
hN : Submodule.map N₁.subtype N' ≤ N₁
⊢ N'.subtype = inclusion hN ∘ₗ N₁.subtype.submoduleMap N'

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
hM : Submodule.map M₁.subtype M' ≤ M₁
h : s ⊆ ↑(map (inclusion hM ∘ₗ M₁.subtype.submoduleMap M') N'.subtype).range
hN : Submodule.map N₁.subtype N' ≤ N₁
x✝ : ↥N'
⊢ ↑(N'.subtype x✝) = ↑((inclusion hN ∘ₗ N₁.subtype.submoduleMap N') x✝)
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
inst✝⁹ : Ring A
inst✝⁸ : Ring B
inst✝⁷ : Ring C
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra R C
inst✝³ : Algebra S A
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Surjective ⇑f
this :
  Submodule.restrictScalars R (RingHom.ker (map f (AlgHom.id R C))) =
    (LinearMap.rTensor C (AlgHom.restrictScalars R f).toLinearMap).ker
⊢ Submodule.restrictScalars R (RingHom.ker (map f (AlgHom.id R C))) =
    Submodule.restrictScalars R (Ideal.map includeLeft (RingHom.ker f))

Tactic:
rw [this, Ideal.map_includeLeft_eq]

Goal state after:
R : Type u_4
S : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
inst✝⁹ : Ring A
inst✝⁸ : Ring B
inst✝⁷ : Ring C
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra R C
inst✝³ : Algebra S A
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Surjective ⇑f
this :
  Submodule.restrictScalars R (RingHom.ker (map f (AlgHom.id R C))) =
    (LinearMap.rTensor C (AlgHom.restrictScalars R f).toLinearMap).ker
⊢ (LinearMap.rTensor C (AlgHom.restrictScalars R f).toLinearMap).ker =
    (LinearMap.rTensor C (Submodule.restrictScalars R (RingHom.ker f)).subtype).range
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ 0 ^ (0 + 1) = 0 ∧ 0 ^ 0 ≠ 0

Tactic:
constructor

Goal state after:
case left
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ 0 ^ (0 + 1) = 0

case right
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ 0 ^ 0 ≠ 0
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
F : Type u_3
inst✝² : FunLike F R S
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ⇑f
inst✝ : IsReduced S
⊢ IsReduced R

Tactic:
constructor

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
F : Type u_3
inst✝² : FunLike F R S
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ⇑f
inst✝ : IsReduced S
⊢ ∀ (x : R), IsNilpotent x → x = 0
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
x✝⁴ : Type u
x✝³ : AddCommMonoid x✝⁴
x✝² : Module R x✝⁴
x✝¹ : Module.Finite R x✝⁴
I : Submodule R x✝⁴
x✝ : I.FG
⊢ ⇑(TensorProduct.rid R x✝⁴).toAddEquiv.toEquiv ∘
      ⇑(rTensor R I.subtype) ∘ ⇑(TensorProduct.rid R ↥I).symm.toAddEquiv.toEquiv =
    fun a ↦ ↑a

Tactic:
ext

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
x✝⁵ : Type u
x✝⁴ : AddCommMonoid x✝⁵
x✝³ : Module R x✝⁵
x✝² : Module.Finite R x✝⁵
I : Submodule R x✝⁵
x✝¹ : I.FG
x✝ : ↥I
⊢ (⇑(TensorProduct.rid R x✝⁵).toAddEquiv.toEquiv ∘
        ⇑(rTensor R I.subtype) ∘ ⇑(TensorProduct.rid R ↥I).symm.toAddEquiv.toEquiv)
      x✝ =
    ↑x✝
Module: Mathlib.RingTheory.Flat.Basic

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

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: R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Flat R S
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
⊢ LinearIndependent S fun x ↦ 1 ⊗ₜ[R] v x

Tactic:
LinearIndependent,

Goal state after:
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Flat R S
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
⊢ Injective ⇑(Finsupp.linearCombination S fun x ↦ 1 ⊗ₜ[R] v x)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_4
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : Flat R M
⊢ ⇑((TensorProduct.mk R S M) 1) = ⇑(rTensor M (Algebra.linearMap R S)) ∘ ⇑(TensorProduct.lid R M).symm

Tactic:
ext

Goal state after:
R : Type u
M : Type v
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_4
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : Flat R M
x✝ : M
⊢ ((TensorProduct.mk R S M) 1) x✝ = (⇑(rTensor M (Algebra.linearMap R S)) ∘ ⇑(TensorProduct.lid R M).symm) x✝
Module: Mathlib.Algebra.Azumaya.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ ↑(tensorEquivEnd R) = AlgHom.mulLeftRight R R

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
x✝ : Rᵐᵒᵖ
⊢ (((AlgHom.restrictScalars R ↑(tensorEquivEnd R)).comp Algebra.TensorProduct.includeRight) x✝) 1 =
    (((AlgHom.restrictScalars R (AlgHom.mulLeftRight R R)).comp Algebra.TensorProduct.includeRight) x✝) 1
Module: Mathlib.Algebra.Azumaya.Basic

Goal state before:
pp: 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
⊢ (AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e)) =
    (↑(LinearEquiv.conjAlgEquiv R ↑e)).comp (AlgHom.mulLeftRight R A)

Tactic:
ext

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)
⊢ ⇑includeLeft = ⇑(LinearMap.lTensor A (Algebra.linearMap R B)) ∘ ⇑(_root_.TensorProduct.rid R A).symm

Tactic:
ext

Goal state after:
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)
x✝ : A
⊢ includeLeft x✝ = (⇑(LinearMap.lTensor A (Algebra.linearMap R B)) ∘ ⇑(_root_.TensorProduct.rid R A).symm) x✝
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u_1
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✝ : Module.Flat R B
ha : Function.Injective ⇑(algebraMap R A)
⊢ ⇑includeRight = ⇑(LinearMap.rTensor B (Algebra.linearMap R A)) ∘ ⇑(_root_.TensorProduct.lid R B).symm

Tactic:
ext

Goal state after:
R : Type u_1
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✝ : Module.Flat R B
ha : Function.Injective ⇑(algebraMap R A)
x✝ : B
⊢ includeRight x✝ = (⇑(LinearMap.rTensor B (Algebra.linearMap R A)) ∘ ⇑(_root_.TensorProduct.lid R B).symm) x✝
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: case inr.hb
α : Type u_2
inst✝ : Fintype α
s : Finset α
h✝ : Nonempty α
⊢ ↑(Fintype.card α) ≠ 0

Tactic:
exact mod_cast Fintype.card_ne_zero

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
⊢ ↑j.succ = ⟨j, hj⟩.succ

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
⊢ ↑↑j.succ = ↑⟨j, hj⟩.succ
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case e_6
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
this : ↑j ≠ last k
⊢ (↑j).castPred ⋯ = ⟨j, hj⟩

Tactic:
ext

Goal state after:
case e_6
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
this : ↑j ≠ last k
⊢ ↑((↑j).castPred ⋯) = ↑⟨j, hj⟩
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: case inr
ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
hs : s.Nonempty
⊢ #s • 𝔼 i ∈ s, f i = ∑ i ∈ s, f i

Tactic:
· rw [expect, ← Nat.cast_smul_eq_nsmul ℚ≥0, smul_inv_smul₀]
    exact mod_cast hs.card_ne_zero

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

Goal state before:
pp: a b x : ℤ
⊢ (∃ a_1 < (b + 1 - a).toNat, a + ↑a_1 = x) ↔ a ≤ x ∧ x ≤ b

Tactic:
constructor

Goal state after:
case mp
a b x : ℤ
⊢ (∃ a_1 < (b + 1 - a).toNat, a + ↑a_1 = x) → a ≤ x ∧ x ≤ b

case mpr
a b x : ℤ
⊢ a ≤ x ∧ x ≤ b → ∃ a_2 < (b + 1 - a).toNat, a + ↑a_2 = x
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, a + ↑a_1 = x) ↔ a ≤ x ∧ x < b

Tactic:
constructor

Goal state after:
case mp
a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, a + ↑a_1 = x) → a ≤ x ∧ x < b

case mpr
a b x : ℤ
⊢ a ≤ x ∧ x < b → ∃ a_2 < (b - a).toNat, a + ↑a_2 = x
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, a + 1 + ↑a_1 = x) ↔ a < x ∧ x ≤ b

Tactic:
constructor

Goal state after:
case mp
a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, a + 1 + ↑a_1 = x) → a < x ∧ x ≤ b

case mpr
a b x : ℤ
⊢ a < x ∧ x ≤ b → ∃ a_2 < (b - a).toNat, a + 1 + ↑a_2 = x
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b x : ℤ
⊢ (∃ a_1 < (b - a - 1).toNat, a + 1 + ↑a_1 = x) ↔ a < x ∧ x < b

Tactic:
constructor

Goal state after:
case mp
a b x : ℤ
⊢ (∃ a_1 < (b - a - 1).toNat, a + 1 + ↑a_1 = x) → a < x ∧ x < b

case mpr
a b x : ℤ
⊢ a < x ∧ x < b → ∃ a_2 < (b - a - 1).toNat, a + 1 + ↑a_2 = x
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a : ℤ
⊢ Icc a (a + 1) = {a, a + 1}

Tactic:
ext

Goal state after:
a a✝ : ℤ
⊢ a✝ ∈ Icc a (a + 1) ↔ a✝ ∈ {a, a + 1}
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ 0 ≤ i ∧ i < a

Tactic:
constructor

Goal state after:
case inr.mp
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → 0 ≤ i ∧ i < a

case inr.mpr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ 0 ≤ i ∧ i < a → ∃ a_2, (n ≤ a_2 ∧ a_2 < n + a) ∧ a_2 % a = i
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: m n : ℕ
⊢ Icc (-(↑m + 1)) (↑n + 1) = Icc (-↑m) ↑n ∪ {-(↑m + 1), ↑n + 1}

Tactic:
ext

Goal state after:
m n : ℕ
a✝ : ℤ
⊢ a✝ ∈ Icc (-(↑m + 1)) (↑n + 1) ↔ a✝ ∈ Icc (-↑m) ↑n ∪ {-(↑m + 1), ↑n + 1}
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: m n : ℕ
⊢ Ico (-(↑m + 1)) (↑n + 1) = Ico (-↑m) ↑n ∪ {-(↑m + 1), ↑n}

Tactic:
ext

Goal state after:
m n : ℕ
a✝ : ℤ
⊢ a✝ ∈ Ico (-(↑m + 1)) (↑n + 1) ↔ a✝ ∈ Ico (-↑m) ↑n ∪ {-(↑m + 1), ↑n}
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: m n : ℕ
⊢ Ioc (-(↑m + 1)) (↑n + 1) = Ioc (-↑m) ↑n ∪ {-↑m, ↑n + 1}

Tactic:
ext

Goal state after:
m n : ℕ
a✝ : ℤ
⊢ a✝ ∈ Ioc (-(↑m + 1)) (↑n + 1) ↔ a✝ ∈ Ioc (-↑m) ↑n ∪ {-↑m, ↑n + 1}
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: m n : ℕ
⊢ Ioo (-(↑m + 1)) (↑n + 1) = Ioo (-↑m) ↑n ∪ {-↑m, ↑n}

Tactic:
ext

Goal state after:
m n : ℕ
a✝ : ℤ
⊢ a✝ ∈ Ioo (-(↑m + 1)) (↑n + 1) ↔ a✝ ∈ Ioo (-↑m) ↑n ∪ {-↑m, ↑n}
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : AddCommMonoid N
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module S N
inst✝⁶ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
x : N
⊢ (IsTensorProduct.lift h (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g))).toFun (r • x) =
    (RingHom.id S) r • (IsTensorProduct.lift h (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g))).toFun x

Tactic:
by
      let F := ((Algebra.linearMap S <| Module.End S (M →ₗ[R] Q)).flip g).restrictScalars R
      have hF : ∀ (s : S) (m : M), h.lift F (s • f m) = s • g m := h.lift_eq F
      change h.lift F (r • x) = r • h.lift F x
      induction x using h.inductionOn with
      | zero => rw [smul_zero, map_zero, smul_zero]
      | tmul s m =>
        change h.lift F (r • s • f m) = r • h.lift F (s • f m)
        rw [← mul_smul, hF, hF, mul_smul]
      | add x₁ x₂ e₁ e₂ => rw [map_add, smul_add, map_add, smul_add, e₁, e₂]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
⊢ ↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] S ⊗[R] M))).flip ((mk R S M) 1)) = mk R S M

Tactic:
ext s x

Goal state after:
R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
s : S
x : M
⊢ ((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] S ⊗[R] M))).flip ((mk R S M) 1))) s) x = ((mk R S M) s) x
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons.inr.inl
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
c : α
hc : c ∈ xs
h : s(a, b) = s(x, c)
⊢ a = x ∨ a ∈ xs

Tactic:
Sym2.eq_iff

Goal state after:
case cons.inr.inl
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
c : α
hc : c ∈ xs
h : a = x ∧ b = c ∨ a = c ∧ b = x
⊢ a = x ∨ a ∈ xs
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
a b : α
⊢ s(a, b) ∈ xs.sym2 ↔ a ∈ xs ∧ b ∈ xs

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
xs : List α
a b : α
⊢ s(a, b) ∈ xs.sym2 → a ∈ xs ∧ b ∈ xs

case mpr
α : Type u_1
xs : List α
a b : α
⊢ a ∈ xs ∧ b ∈ xs → s(a, b) ∈ xs.sym2
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
inst : Fintype (Sym2 α)
⊢ univ.sym2 = univ

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : Fintype α
inst : Fintype (Sym2 α)
a✝ : Sym2 α
⊢ a✝ ∈ univ.sym2 ↔ a✝ ∈ univ
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.sym2.Nonempty ↔ s.Nonempty

Tactic:
contrapose!; exact sym2_eq_empty

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ image (Function.uncurry Sym2.mk) s.diag ∪ image (Function.uncurry Sym2.mk) s.offDiag = s.sym2

Tactic:
← image_union,

Goal state after:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ image (Function.uncurry Sym2.mk) (s.diag ∪ s.offDiag) = s.sym2
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
F : Sym2 α → Sym2 β → γ
a₁ a₂ : α
b₁ b₂ : β
⊢ (fun a₁ a₂ b₁ b₂ ↦ F s(a₁, a₂) s(b₁, b₂)) a₁ a₂ b₁ b₂ = (fun a₁ a₂ b₁ b₂ ↦ F s(a₁, a₂) s(b₁, b₂)) a₂ a₁ b₁ b₂ ∧
    (fun a₁ a₂ b₁ b₂ ↦ F s(a₁, a₂) s(b₁, b₂)) a₁ a₂ b₁ b₂ = (fun a₁ a₂ b₁ b₂ ↦ F s(a₁, a₂) s(b₁, b₂)) a₁ a₂ b₂ b₁

Tactic:
constructor

Goal state after:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
F : Sym2 α → Sym2 β → γ
a₁ a₂ : α
b₁ b₂ : β
⊢ (fun a₁ a₂ b₁ b₂ ↦ F s(a₁, a₂) s(b₁, b₂)) a₁ a₂ b₁ b₂ = (fun a₁ a₂ b₁ b₂ ↦ F s(a₁, a₂) s(b₁, b₂)) a₂ a₁ b₁ b₂

case right
α : Type u_1
β : Type u_2
γ : Type u_3
F : Sym2 α → Sym2 β → γ
a₁ a₂ : α
b₁ b₂ : β
⊢ (fun a₁ a₂ b₁ b₂ ↦ F s(a₁, a₂) s(b₁, b₂)) a₁ a₂ b₁ b₂ = (fun a₁ a₂ b₁ b₂ ↦ F s(a₁, a₂) s(b₁, b₂)) a₁ a₂ b₂ b₁
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case refl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x✝ y✝ : α
⊢ Rel β (Prod.map f f (x✝, y✝)) (Prod.map f f (x✝, y✝))

Tactic:
constructor

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case swap
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x✝ y✝ : α
⊢ Rel β (Prod.map f f (x✝, y✝)) (Prod.map f f (y✝, x✝))

Tactic:
constructor

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ : Module R Q
g : M →ₗ[R] Q
I₄ : IsScalarTower R R Q
⊢ (fun g' ↦ ↑R g' ∘ₗ ↑e = g) (g ∘ₗ ↑e.symm)

Tactic:
ext

Goal state after:
R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ : Module R Q
g : M →ₗ[R] Q
I₄ : IsScalarTower R R Q
x✝ : M
⊢ (↑R (g ∘ₗ ↑e.symm) ∘ₗ ↑e) x✝ = g x✝
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refl
R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ : Module R Q
I₄ : IsScalarTower R R Q
y : N →ₗ[R] Q
⊢ y = (↑R y ∘ₗ ↑e) ∘ₗ ↑e.symm

Tactic:
ext

Goal state after:
case refl
R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ : Module R Q
I₄ : IsScalarTower R R Q
y : N →ₗ[R] Q
x✝ : N
⊢ y x✝ = ((↑R y ∘ₗ ↑e) ∘ₗ ↑e.symm) x✝
Module: Mathlib.Algebra.BigOperators.WithTop

Goal state before:
pp: ι : Type u_1
M₀ : Type u_3
inst✝³ : CommMonoidWithZero M₀
inst✝² : NoZeroDivisors M₀
inst✝¹ : Nontrivial M₀
inst✝ : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
⊢ ∏ j ∈ s, f j = ⊤ ↔ (∃ i ∈ s, f i = ⊤) ∧ ∀ i ∈ s, f i ≠ 0

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
M₀ : Type u_3
inst✝³ : CommMonoidWithZero M₀
inst✝² : NoZeroDivisors M₀
inst✝¹ : Nontrivial M₀
inst✝ : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
⊢ ∏ j ∈ s, f j = ⊤ → (∃ i ∈ s, f i = ⊤) ∧ ∀ i ∈ s, f i ≠ 0

case mpr
ι : Type u_1
M₀ : Type u_3
inst✝³ : CommMonoidWithZero M₀
inst✝² : NoZeroDivisors M₀
inst✝¹ : Nontrivial M₀
inst✝ : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
⊢ ((∃ i ∈ s, f i = ⊤) ∧ ∀ i ∈ s, f i ≠ 0) → ∏ j ∈ s, f j = ⊤