mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
n : ℕ
rank_ih : (N : Submodule R M) → (∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n) → P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n + 1
N' : Submodule R M
N'_le : N' ≤ N
x : M
x_mem : x ∈ N
x_ortho : ∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0
m : ℕ
v : Fin m → ↥N'
hli : LinearIndependent R (Subtype.val ∘ v)
i : Fin m.succ
⊢ (Subtype.val ∘ Fin.cons ⟨x, x_mem⟩ fun i ↦ ⟨↑(v i), ⋯⟩) i = Fin.cons x (Subtype.val ∘ v) i

Tactic:
refine Fin.cases ?_ ?_ i

Goal state after:
case refine_1
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
n : ℕ
rank_ih : (N : Submodule R M) → (∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n) → P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n + 1
N' : Submodule R M
N'_le : N' ≤ N
x : M
x_mem : x ∈ N
x_ortho : ∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0
m : ℕ
v : Fin m → ↥N'
hli : LinearIndependent R (Subtype.val ∘ v)
i : Fin m.succ
⊢ (Subtype.val ∘ Fin.cons ⟨x, x_mem⟩ fun i ↦ ⟨↑(v i), ⋯⟩) 0 = Fin.cons x (Subtype.val ∘ v) 0

case refine_2
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
n : ℕ
rank_ih : (N : Submodule R M) → (∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n) → P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n + 1
N' : Submodule R M
N'_le : N' ≤ N
x : M
x_mem : x ∈ N
x_ortho : ∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0
m : ℕ
v : Fin m → ↥N'
hli : LinearIndependent R (Subtype.val ∘ v)
i : Fin m.succ
⊢ ∀ (i : Fin m), (Subtype.val ∘ Fin.cons ⟨x, x_mem⟩ fun i ↦ ⟨↑(v i), ⋯⟩) i.succ = Fin.cons x (Subtype.val ∘ v) i.succ
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H = ⊥ → Nat.card ↥H = 1

Tactic:
by rintro rfl; exact card_bot

Goal state after:
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
⊢ ENat.card ↑s < ENat.card ↑t

Tactic:
suffices ENat.card t ≤ ENat.card s → t ⊆ s from
    lt_of_le_not_ge (ecard_le_ecard hsub.subset) fun hle ↦ not_subset_of_ssubset hsub <| this hle
  intro hle
  suffices ENat.card ↑(t \ s) ≤ 0 by
    rwa [← sdiff_eq_empty, ← Set.isEmpty_coe_sort, ← ENat.card_eq_zero_iff_empty,
      ← nonpos_iff_eq_zero]
  suffices ENat.card ↑(t \ s) + ENat.card ↑s ≤ 0 + ENat.card ↑s from
    WithTop.le_of_add_le_add_right (ENat.card_lt_top.mpr hs).ne this
  suffices ENat.card ↑t ≤ 0 + ENat.card ↑s by
    rwa [← ENat.card_sum, ← ENat.card_congr <| Equiv.Set.union disjoint_sdiff_left,
      sdiff_union_of_subset hsub.subset]
  exact le_add_of_le_right hle

Goal state after:
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
s : Set α
e : α ≃ α
hs : s.Finite
h : ⇑e '' s = s
⊢ ⇑e '' s ⊆ s

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case e'_3
α : Type u_1
P : α → Prop
s : Set α
⊢ s ∩ ofPred P = (fun a ↦ ↑a) '' {x | ↑x ∈ s}

Tactic:
ext x

Goal state after:
case e'_3
α : Type u_1
P : α → Prop
s : Set α
x : α
⊢ x ∈ s ∩ ofPred P ↔ x ∈ (fun a ↦ ↑a) '' {x | ↑x ∈ s}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun i ↦ f ↑i ⋯
⊢ s = f' '' univ

Tactic:
ext x

Goal state after:
α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun i ↦ f ↑i ⋯
x : α
⊢ x ∈ s ↔ x ∈ f' '' univ
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
hc : t.ncard < s.ncard
f : α → β
hf : ∀ a ∈ s, f a ∈ t
ht : t.Finite
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

Tactic:
by
  by_contra h'
  simp only [Ne, not_exists, not_and, not_imp_not] at h'
  exact (ncard_le_ncard_of_injOn f hf h' ht).not_gt hc

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
N : s.Normal
g a : α
⊢ a ∈ g • ↑s ↔ a ∈ op g • ↑s

Tactic:
by simp [mem_leftCoset_iff, mem_rightCoset_iff, N.mem_comm_iff]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
⊢ (s ∪ t).encard ≤ ↑s.ncard + ↑t.ncard

Tactic:
(h.subset subset_union_left).cast_ncard_eq,

Goal state after:
case inl
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
⊢ (s ∪ t).encard ≤ s.encard + ↑t.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
⊢ (s ∩ t).ncard + (s \ t).ncard = s.ncard

Tactic:
rw [← ncard_union_eq (disjoint_of_subset_left inter_subset_right disjoint_sdiff_right)
    (hs.inter_of_left _) hs.sdiff, union_comm, sdiff_union_inter]

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
⊢ g • ⇑(mk' N) ⁻¹' U = ⇑(mk' N) ⁻¹' U

Tactic:
ext x

Goal state after:
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
x : G
⊢ x ∈ g • ⇑(mk' N) ⁻¹' U ↔ x ∈ ⇑(mk' N) ⁻¹' U
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝⁵ : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝⁴ : Group H
M : Type x
inst✝³ : Monoid M
φ : G →* H
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
f : A →* B
g✝ : B →* A
e : A ≃* B
d : B ≃* C
n : ℤ
g : A
x✝ : g ∈ (zpowGroupHom n).range
h : A
hg : h ^ n = g
⊢ (zpowGroupHom n) (f h) = f g

Tactic:
simp only [← hg, map_zpow, zpowGroupHom_apply]

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: A : Type u
inst✝ : CommGroup A
n : ℤ
⊢ MulEquiv.refl (A ⧸ (zpowGroupHom n).range) = equivQuotientZPowOfEquiv (MulEquiv.refl A) n

Tactic:
ext x

Goal state after:
A : Type u
inst✝ : CommGroup A
n : ℤ
x : A ⧸ (zpowGroupHom n).range
⊢ (MulEquiv.refl (A ⧸ (zpowGroupHom n).range)) x = (equivQuotientZPowOfEquiv (MulEquiv.refl A) n) x
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
e : A ≃* B
d : B ≃* C
n : ℤ
⊢ (equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n) = equivQuotientZPowOfEquiv (e.trans d) n

Tactic:
ext x

Goal state after:
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
e : A ≃* B
d : B ≃* C
n : ℤ
x : A ⧸ (zpowGroupHom n).range
⊢ ((equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n)) x = (equivQuotientZPowOfEquiv (e.trans d) n) x
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case e'_2
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (fun a ↦ a ∉ s ∧ insert a hs.toFinset = ht.toFinset) = fun a ↦ a ∉ s ∧ insert a s = t

Tactic:
ext x

Goal state after:
case e'_2
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
x : α
⊢ x ∉ s ∧ insert x hs.toFinset = ht.toFinset ↔ x ∉ s ∧ insert x s = t
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard

Tactic:
rw [ncard_eq_toFinset_card _ hs, ncard_eq_toFinset_card _ ht,
      ← @Finite.toFinset_subset_toFinset _ _ _ hs ht, ← Finset.exists_eq_insert_iff]
    convert! Iff.rfl using 2; simp only [Finite.mem_toFinset]
    ext x
    simp [Finset.ext_iff, Set.ext_iff]

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
H₁ : Subgroup G
inst✝¹ : H₁.Normal
H₂ : Subgroup (G ⧸ H₁)
inst✝ : H₂.Normal
⊢ Subgroup.comap (mk' H₁) (Subgroup.comap (mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) =
    Subgroup.comap (mk' (Subgroup.comap (mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (mk' H₁) H₂))

Tactic:
ext x

Goal state after:
G : Type u
inst✝² : Group G
H₁ : Subgroup G
inst✝¹ : H₁.Normal
H₂ : Subgroup (G ⧸ H₁)
inst✝ : H₂.Normal
x : G
⊢ x ∈ Subgroup.comap (mk' H₁) (Subgroup.comap (mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) ↔
    x ∈ Subgroup.comap (mk' (Subgroup.comap (mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (mk' H₁) H₂))
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: case mk.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c : Con M
d : Con N
e : M ≃* N
h : c = comap ⇑e ⋯ d
x✝ : c.Quotient
x : M
y✝ : c.Quotient
y : M
⊢ (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) x * Quot.mk (⇑c.toSetoid) y) =
    (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) x) * (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) y)

Tactic:
exact congrArg toQuotient (e.map_mul x y)

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c✝ : Con M
x✝ y✝ : M
f : M →* P
c d : Con M
h : c ≤ d
x y : (ker (c.map d h)).Quotient
w z : c.Quotient
a b : M
⊢ (c.quotientQuotientEquivQuotient d.toSetoid h).toFun (↑↑a * ↑↑b) = d.mk' a * d.mk' b

Tactic:
rw [← d.mk'.map_mul]; rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: 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)
f : M₂ →ₗ[R] M₃
I : Type u_1
c : R
h : I → M₂
⊢ ⇑f ∘ (c • h) = (RingHom.id R) c • ⇑f ∘ h

Tactic:
ext x

Goal state after:
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)
f : M₂ →ₗ[R] M₃
I : Type u_1
c : R
h : I → M₂
x : I
⊢ (⇑f ∘ (c • h)) x = ((RingHom.id R) c • ⇑f ∘ h) x
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
⊢ p.mapQ q f h ∘ₛₗ p.mkQ = q.mkQ ∘ₛₗ f

Tactic:
ext x

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
x : M
⊢ (p.mapQ q f h ∘ₛₗ p.mkQ) x = (q.mkQ ∘ₛₗ f) x
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:
ext x

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
b : α
⊢ Icc (succ a) b = Ioc a b

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
b x : α
⊢ x ∈ Icc (succ a) b ↔ x ∈ Ioc a b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ico a (succ b) = Icc a b

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
⊢ x ∈ Ico a (succ b) ↔ x ∈ Icc a b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ioo a (succ b) = Ioc a b

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
⊢ x ∈ Ioo a (succ b) ↔ x ∈ Ioc a b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
⊢ insert a (Icc (succ a) b) = Icc a b

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
x : α
⊢ x ∈ insert a (Icc (succ a) b) ↔ x ∈ Icc a b
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: 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₂
⊢ (inl R M M₂).range = (snd R M M₂).ker

Tactic:
ext x

Goal state after:
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₂
⊢ x ∈ (inl R M M₂).range ↔ x ∈ (snd R M M₂).ker
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: 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 ι
S : Type ?u.47
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Fintype ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : ((i : ι) → φ i) →ₗ[R] M
⊢ (fun f ↦ ∑ i, f i ∘ₗ proj i) ((fun f i ↦ f ∘ₗ single R φ i) f) = f

Tactic:
ext x

Goal state after:
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 ι
S : Type ?u.47
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Fintype ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : ((i : ι) → φ i) →ₗ[R] M
x : (i : ι) → φ i
⊢ ((fun f ↦ ∑ i, f i ∘ₗ proj i) ((fun f i ↦ f ∘ₗ single R φ i) f)) x = f x
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ succ b
⊢ insert (succ b) (Icc a b) = Icc a (succ b)

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ succ b
x : α
⊢ x ∈ insert (succ b) (Icc a b) ↔ x ∈ Icc a (succ b)
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: 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₂
⊢ (inr R M M₂).range = (fst R M M₂).ker

Tactic:
ext x

Goal state after:
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₂
⊢ x ∈ (inr R M M₂).range ↔ x ∈ (fst R M M₂).ker
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ insert (succ b) (Ioc a b) = Ioc a (succ b)

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
x : α
⊢ x ∈ insert (succ b) (Ioc a b) ↔ x ∈ Ioc a (succ 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:
ext x

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
a : α
⊢ Icc a (pred b) = Ico a b

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
a x : α
⊢ x ∈ Icc a (pred b) ↔ x ∈ Ico a b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (pred a) b = Icc a b

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b x : α
⊢ x ∈ Ioc (pred a) b ↔ x ∈ Icc a b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioo (pred a) b = Ico a b

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b x : α
⊢ x ∈ Ioo (pred a) b ↔ x ∈ Ico a b
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
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₃
g : M₂ →ₗ[R] M₃
S : Submodule R M
S' : Submodule R M₂
⊢ ↑(Submodule.map (f.coprod g) (S.prod S')) = ↑(Submodule.map f S ⊔ Submodule.map g S')

Tactic:
simp only [LinearMap.coprod_apply, Submodule.coe_sup, Submodule.map_coe]
    rw [← Set.image2_add, Set.image2_image_left, Set.image2_image_right]
    exact Set.image_prod fun m m₂ => f m + g m₂

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
⊢ insert b (Icc a (pred b)) = Icc a b

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
x : α
⊢ x ∈ insert b (Icc a (pred b)) ↔ x ∈ Icc a b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : pred a ≤ b
⊢ insert (pred a) (Icc a b) = Icc (pred a) b

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : pred a ≤ b
x : α
⊢ x ∈ insert (pred a) (Icc a b) ↔ x ∈ Icc (pred a) b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ insert (pred a) (Ico a b) = Ico (pred a) b

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
x : α
⊢ x ∈ insert (pred a) (Ico a b) ↔ x ∈ Ico (pred a) b
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
H : p ≤ p'
⊢ factor H ∘ₗ p.mkQ = p'.mkQ

Tactic:
ext x

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
H : p ≤ p'
x : M
⊢ (factor H ∘ₗ p.mkQ) x = p'.mkQ x
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
⊢ Iio (succ b) = Iic b

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
x : α
⊢ x ∈ Iio (succ b) ↔ x ∈ Iic b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
⊢ Iic (pred b) = Iio b

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
x : α
⊢ x ∈ Iic (pred b) ↔ x ∈ Iio b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
⊢ Ici (succ a) = Ioi a

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
x : α
⊢ x ∈ Ici (succ a) ↔ x ∈ Ioi a
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
⊢ Ioi (pred a) = Ici a

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
x : α
⊢ x ∈ Ioi (pred a) ↔ x ∈ Ici a
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:
rw [codisjoint_iff_le_sup]

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₂
⊢ ⊤ ≤ (inl R M M₂).range ⊔ (inr R M M₂).range
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝² : Semiring R
φ : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
I : Set ι
p : (i : ι) → Submodule R (φ i)
⊢ ⨅ i ∈ I, comap (proj i) (p i) = pi I p

Tactic:
ext x

Goal state after:
R : Type u
ι : Type x
inst✝² : Semiring R
φ : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
I : Set ι
p : (i : ι) → Submodule R (φ i)
x : (i : ι) → φ i
⊢ x ∈ ⨅ i ∈ I, comap (proj i) (p i) ↔ x ∈ pi I p
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case h
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : f y + g z = 0
⊢ f y - -g z = 0

Tactic:
sub_neg_eq_add

Goal state after:
case h
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : f y + g z = 0
⊢ f y + g z = 0
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝² : Semiring R
φ : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
p : (i : ι) → Submodule R (φ i)
⊢ ⨅ i, comap (proj i) (p i) = pi Set.univ p

Tactic:
ext x

Goal state after:
R : Type u
ι : Type x
inst✝² : Semiring R
φ : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
p : (i : ι) → Submodule R (φ i)
x : (i : ι) → φ i
⊢ x ∈ ⨅ i, comap (proj i) (p i) ↔ x ∈ pi Set.univ p