mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: case h
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
⊢ {p ∈ x.coeff.support ×ˢ y.coeff.support | p.1 * p.2 = m} = {p ∈ s | p.1 ∈ x.coeff.support ∧ p.2 ∈ y.coeff.support}

Tactic:
ext

Goal state after:
case h
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
a✝ : M × M
⊢ a✝ ∈ {p ∈ x.coeff.support ×ˢ y.coeff.support | p.1 * p.2 = m} ↔
    a✝ ∈ {p ∈ s | p.1 ∈ x.coeff.support ∧ p.2 ∈ y.coeff.support}
Module: Mathlib.Algebra.MonoidAlgebra.Opposite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
r : R
x : M
⊢ MonoidAlgebra.opRingEquiv (op (single x r)) = single (op x) (op r)

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
r : R
x : M
a✝ : Mᵐᵒᵖ
⊢ (MonoidAlgebra.opRingEquiv (op (single x r))).coeff a✝ = (single (op x) (op r)).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Opposite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
r : Rᵐᵒᵖ
x : Mᵐᵒᵖ
⊢ unop (MonoidAlgebra.opRingEquiv.symm (single x r)) = unop (op (single (unop x) (unop r)))

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
r : Rᵐᵒᵖ
x : Mᵐᵒᵖ
a✝ : M
⊢ (unop (MonoidAlgebra.opRingEquiv.symm (single x r))).coeff a✝ = (unop (op (single (unop x) (unop r)))).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
G : Type u_3
M✝ : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝³ : Semiring R✝
x y : R✝[M✝]
r r₁ r₂ : R✝
m m' m₁ m₂ m₁' m₂' : M✝
inst✝² : Mul M✝
R : Type u_8
M : Type u_9
inst✝¹ : Semiring R
inst✝ : Mul M
a b : M
⊢ single (a * b) 1 = single a 1 * single b 1

Tactic:
ext

Goal state after:
R✝ : Type u_1
S : Type u_2
G : Type u_3
M✝ : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝³ : Semiring R✝
x y : R✝[M✝]
r r₁ r₂ : R✝
m m' m₁ m₂ m₁' m₂' : M✝
inst✝² : Mul M✝
R : Type u_8
M : Type u_9
inst✝¹ : Semiring R
inst✝ : Mul M
a b a✝ : M
⊢ (single (a * b) 1).coeff a✝ = (single a 1 * single b 1).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : Monoid M
inst✝ : Subsingleton M
r : R
⊢ (uniqueRingEquiv M).symm r = single 1 r

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : Monoid M
inst✝ : Subsingleton M
r : R
a✝ : M
⊢ ((uniqueRingEquiv M).symm r).coeff a✝ = (single 1 r).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Ring R
m : M
r : R
⊢ single m (-r) = -single m r

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_4
inst✝ : Ring R
m : M
r : R
a✝ : M
⊢ (single m (-r)).coeff a✝ = (-single m r).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Ring R
m : M
r s : R
⊢ single m (r - s) = single m r - single m s

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_4
inst✝ : Ring R
m : M
r s : R
a✝ : M
⊢ (single m (r - s)).coeff a✝ = (single m r - single m s).coeff a✝
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : One α
inst✝ : One β
⊢ 1 ×ˢ 1 = 1

Tactic:
ext

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : One α
inst✝ : One β
a✝ : α × β
⊢ a✝ ∈ 1 ×ˢ 1 ↔ a✝ ∈ 1
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : InvolutiveInv α
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
⊢ ({x ∈ s | p x})⁻¹ = {x ∈ s⁻¹ | p x⁻¹}

Tactic:
ext

Goal state after:
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : InvolutiveInv α
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
a✝ : α
⊢ a✝ ∈ ({x ∈ s | p x})⁻¹ ↔ a✝ ∈ {x ∈ s⁻¹ | p x⁻¹}
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : InvolutiveInv α
inst✝ : Fintype α
⊢ univ⁻¹ = univ

Tactic:
ext

Goal state after:
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : InvolutiveInv α
inst✝ : Fintype α
a✝ : α
⊢ a✝ ∈ univ⁻¹ ↔ a✝ ∈ univ
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ IsUnit s ↔ ∃ a, s = {a} ∧ IsUnit a

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ IsUnit s → ∃ a, s = {a} ∧ IsUnit a

case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ (∃ a, s = {a} ∧ IsUnit a) → IsUnit s
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
n : ℤ
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
n : ℤ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
n : ℤ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a b : α
⊢ {b}.preimage (fun x ↦ a * x) ⋯ = {a⁻¹ * b}

Tactic:
← image_mul_left',

Goal state after:
α : Type u_2
inst✝ : Group α
a b : α
⊢ image (fun b ↦ a⁻¹ * b) {b} = {a⁻¹ * b}
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a : α
⊢ preimage 1 (fun x ↦ a * x) ⋯ = {a⁻¹}

Tactic:
← image_mul_left',

Goal state after:
α : Type u_2
inst✝ : Group α
a : α
⊢ image (fun b ↦ a⁻¹ * b) 1 = {a⁻¹}
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
⊢ { toFinsupp := f.toFinsupp } = f

Tactic:
constructor

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
L : Sublattice α
M : Sublattice β
e : β ≃o α
⊢ ↑(map { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ } L) = ↑M ↔
    ↑L = ↑(map { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ } M)

Tactic:
exact (Equiv.eq_image_iff_symm_image_eq _ _ _).symm

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
L : Sublattice α
M : Sublattice β
e : β ≃o α
⊢ map { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ } L = M ↔ L = map { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ } M

Tactic:
simp_rw [← coe_inj]; exact (Equiv.eq_image_iff_symm_image_eq _ _ _).symm

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
toFinsupp✝ : R[ℕ]
⊢ single 1 1 * toFinsupp✝ = toFinsupp✝ * single 1 1

Tactic:
ext

Goal state after:
R : Type u
inst✝ : Semiring R
toFinsupp✝ : R[ℕ]
a✝ : ℕ
⊢ (single 1 1 * toFinsupp✝).coeff a✝ = (toFinsupp✝ * single 1 1).coeff a✝
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k n : ℕ
r : R
⊢ X ^ k * (monomial n) r = (monomial (n + k)) r

Tactic:
by
  rw [X_pow_mul, monomial_mul_X_pow]

Goal state after:
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : GeneralLinearGroup R M
⊢ (x * y).toLinearEquiv = x.toLinearEquiv * y.toLinearEquiv

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : GeneralLinearGroup R M
x✝ : M
⊢ (x * y).toLinearEquiv x✝ = (x.toLinearEquiv * y.toLinearEquiv) x✝
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
⊢ ↑((generalLinearEquiv R M) f) = ↑f

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
x✝ : M
⊢ ↑((generalLinearEquiv R M) f) x✝ = ↑f x✝
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (p.update n a).coeff = Function.update p.coeff n a

Tactic:
ext

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
x✝ : ℕ
⊢ (p.update n a).coeff x✝ = Function.update p.coeff n a x✝
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.update n 0 = erase n p

Tactic:
ext

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
⊢ (p.update n 0).coeff n✝ = (erase n p).coeff n✝
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
n : ℕ
a : R
inst✝ : Decidable (a = 0)
⊢ (p.update n a).support = if a = 0 then p.support.erase n else insert n p.support

Tactic:
by
  classical simp [support, update, Finsupp.support_update]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : End R M
e : M ≃ₗ[R] N
p : Submodule R M
⊢ ↑e.symm ∘ₗ ((↑e ∘ₗ f) ∘ₗ ↑e.symm) ∘ₗ ↑e = f

Tactic:
ext

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : End R M
e : M ≃ₗ[R] N
p : Submodule R M
x✝ : M
⊢ (↑e.symm ∘ₗ ((↑e ∘ₗ f) ∘ₗ ↑e.symm) ∘ₗ ↑e) x✝ = f x✝
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ (linearCombination R fun ix ↦ single ix.fst (f ix.fst ix.snd)) =
    (mapRange.linearMap fun i ↦ linearCombination R (f i)) ∘ₗ ↑(sigmaFinsuppLequivDFinsupp R)

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
a✝ : (i : ι) × φ i
i✝ : ι
⊢ (((linearCombination R fun ix ↦ single ix.fst (f ix.fst ix.snd)) ∘ₗ Finsupp.lsingle a✝) 1) i✝ =
    ((((mapRange.linearMap fun i ↦ linearCombination R (f i)) ∘ₗ ↑(sigmaFinsuppLequivDFinsupp R)) ∘ₗ Finsupp.lsingle a✝)
        1)
      i✝
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
this :
  (linearCombination R fun ix ↦ single ix.fst (f ix.fst ix.snd)) =
    (mapRange.linearMap fun i ↦ linearCombination R (f i)) ∘ₗ ↑(sigmaFinsuppLequivDFinsupp R)
⊢ LinearIndependent R fun ix ↦ single ix.fst (f ix.fst ix.snd)

Tactic:
LinearIndependent,

Goal state after:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
this :
  (linearCombination R fun ix ↦ single ix.fst (f ix.fst ix.snd)) =
    (mapRange.linearMap fun i ↦ linearCombination R (f i)) ∘ₗ ↑(sigmaFinsuppLequivDFinsupp R)
⊢ Function.Injective ⇑(linearCombination R fun ix ↦ single ix.fst (f ix.fst ix.snd))
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: R : Type u_2
η : Type u_4
inst✝¹ : Semiring R
inst✝ : Finite η
x : η → R
i : η
⊢ ((basisFun R η).repr x) i = x i

Tactic:
simp [basisFun]

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), UniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B✝ : Finset ((i : ι) → G i)
hA✝ : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB✝ : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
hc :
  (1 < #(image (fun x ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
    1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
⊢ ∃ a0 ∈ A', ∃ b0 ∈ B', UniqueMul A' B' a0 b0

Tactic:
rcases hc with hc | hc; · exact ihA A' (hc.2 ai) hA hB
      by_cases hA' : A' = A
      · rw [hA']
        exact ihB B' (hc.2 bi) hB
      · exact ihA A' ((A.filter_subset _).ssubset_of_ne hA') hA hB

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case inr.intro.intro
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #(A ×ˢ B)
hc' : #(image (⇑f) A ×ˢ image (⇑f) B) ≤ 1
p1 : H × H
h1 : p1 ∈ ↑(A ×ˢ B)
p2 : H × H
h2 : p2 ∈ ↑(A ×ˢ B)
hne : p1 ≠ p2
left✝¹ : p1.1 ∈ A
right✝¹ : p1.2 ∈ B
left✝ : p2.1 ∈ A
right✝ : p2.2 ∈ B
⊢ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
constructor

Goal state after:
case inr.intro.intro.left
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #(A ×ˢ B)
hc' : #(image (⇑f) A ×ˢ image (⇑f) B) ≤ 1
p1 : H × H
h1 : p1 ∈ ↑(A ×ˢ B)
p2 : H × H
h2 : p2 ∈ ↑(A ×ˢ B)
hne : p1 ≠ p2
left✝¹ : p1.1 ∈ A
right✝¹ : p1.2 ∈ B
left✝ : p2.1 ∈ A
right✝ : p2.2 ∈ B
⊢ UniqueMul A B p1.1 p1.2

case inr.intro.intro.right
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #(A ×ˢ B)
hc' : #(image (⇑f) A ×ˢ image (⇑f) B) ≤ 1
p1 : H × H
h1 : p1 ∈ ↑(A ×ˢ B)
p2 : H × H
h2 : p2 ∈ ↑(A ×ˢ B)
hne : p1 ≠ p2
left✝¹ : p1.1 ∈ A
right✝¹ : p1.2 ∈ B
left✝ : p2.1 ∈ A
right✝ : p2.2 ∈ B
⊢ UniqueMul A B p2.1 p2.2
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
this :
  ∀ (M : Type u_1) (N : Type u_5) (α : Type (max u_3 u_4)) [inst : SMul M α] [inst_1 : SMul N α] [SMulCommClass M N α],
    SMulCommClass N M α
x✝¹ x✝ : M
⊢ mapRange.linearMap (id.flip (x✝¹ + x✝)) = mapRange.linearMap (id.flip x✝¹) + mapRange.linearMap (id.flip x✝)

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
this :
  ∀ (M : Type u_1) (N : Type u_5) (α : Type (max u_3 u_4)) [inst : SMul M α] [inst_1 : SMul N α] [SMulCommClass M N α],
    SMulCommClass N M α
x✝² x✝¹ : M
a✝¹ : ι
x✝ : M →ₗ[R] N
a✝ : ι
⊢ ((mapRange.linearMap (id.flip (x✝² + x✝¹)) ∘ₗ lsingle a✝¹) x✝) a✝ =
    (((mapRange.linearMap (id.flip x✝²) + mapRange.linearMap (id.flip x✝¹)) ∘ₗ lsingle a✝¹) x✝) a✝
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
this :
  ∀ (M : Type u_1) (N : Type u_5) (α : Type (max u_3 u_4)) [inst : SMul M α] [inst_1 : SMul N α] [SMulCommClass M N α],
    SMulCommClass N M α
x✝¹ : R
x✝ : M
⊢ mapRange.linearMap (id.flip (x✝¹ • x✝)) = (RingHom.id R) x✝¹ • mapRange.linearMap (id.flip x✝)

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
this :
  ∀ (M : Type u_1) (N : Type u_5) (α : Type (max u_3 u_4)) [inst : SMul M α] [inst_1 : SMul N α] [SMulCommClass M N α],
    SMulCommClass N M α
x✝² : R
x✝¹ : M
a✝¹ : ι
x✝ : M →ₗ[R] N
a✝ : ι
⊢ ((mapRange.linearMap (id.flip (x✝² • x✝¹)) ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((((RingHom.id R) x✝² • mapRange.linearMap (id.flip x✝¹)) ∘ₗ lsingle a✝¹) x✝) a✝
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Module S N
inst✝¹ : SMulCommClass R S N
inst✝ : Module.Finite R M
s : Finset M
span_s : Submodule.span R ↑s = ⊤
x : M →ₗ[R] ι →₀ N
⊢ (finsuppLinearMap S) (onFinset (s.sup fun m ↦ (x m).support) (fun x_1 ↦ lapply x_1 ∘ₗ x) ⋯) = x

Tactic:
ext

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Module S N
inst✝¹ : SMulCommClass R S N
inst✝ : Module.Finite R M
s : Finset M
span_s : Submodule.span R ↑s = ⊤
x : M →ₗ[R] ι →₀ N
x✝ : M
a✝ : ι
⊢ (((finsuppLinearMap S) (onFinset (s.sup fun m ↦ (x m).support) (fun x_1 ↦ lapply x_1 ∘ₗ x) ⋯)) x✝) a✝ = (x x✝) a✝
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Module S N
inst✝¹ : SMulCommClass R S N
inst✝ : Finite ι
x : M →ₗ[R] ι →₀ N
⊢ (finsuppLinearMap S) (equivFunOnFinite.symm fun i ↦ lapply i ∘ₗ x) = x

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Module S N
inst✝¹ : SMulCommClass R S N
inst✝ : Finite ι
x : M →ₗ[R] ι →₀ N
x✝ : M
a✝ : ι
⊢ (((finsuppLinearMap S) (equivFunOnFinite.symm fun i ↦ lapply i ∘ₗ x)) x✝) a✝ = (x x✝) a✝
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : (y : P) → y ∈ t1 → M
hg1 : ∀ (y : P) (a : y ∈ t1), g y a ∈ s
hg2 : ∀ (y : P) (a : y ∈ t1), f (g y a) = y
y : P
H : y ∈ t1
⊢ (fun y ↦ if H : y ∈ t1 then g y H else 0) y ∈ s ∧ f ((fun y ↦ if H : y ∈ t1 then g y H else 0) y) = y

Tactic:
constructor

Goal state after:
case left
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : (y : P) → y ∈ t1 → M
hg1 : ∀ (y : P) (a : y ∈ t1), g y a ∈ s
hg2 : ∀ (y : P) (a : y ∈ t1), f (g y a) = y
y : P
H : y ∈ t1
⊢ (fun y ↦ if H : y ∈ t1 then g y H else 0) y ∈ s

case right
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : (y : P) → y ∈ t1 → M
hg1 : ∀ (y : P) (a : y ∈ t1), g y a ∈ s
hg2 : ∀ (y : P) (a : y ∈ t1), f (g y a) = y
y : P
H : y ∈ t1
⊢ f ((fun y ↦ if H : y ∈ t1 then g y H else 0) y) = y
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
⊢ IsCompl p f.ker

Tactic:
constructor

Goal state after:
case disjoint
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
⊢ Disjoint p f.ker

case codisjoint
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
⊢ Codisjoint p f.ker
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ Function.Bijective ⇑(p.subtype.coprod q.subtype)

Tactic:
constructor

Goal state after:
case left
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ Function.Injective ⇑(p.subtype.coprod q.subtype)

case right
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ Function.Surjective ⇑(p.subtype.coprod q.subtype)
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝² : DecidableEq R
this✝¹ : DecidableEq M
this✝ : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
this : f x ∈ map f s
⊢ x ∈ span R (g '' ↑t1) ⊔ span R ↑t2

Tactic:
rw [← ht1, ← Set.image_id (t1 : Set P), Finsupp.mem_span_image_iff_linearCombination] at this

Goal state after:
case a
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝² : DecidableEq R
this✝¹ : DecidableEq M
this✝ : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
this : ∃ l ∈ supported R R ↑t1, (linearCombination R id) l = f x
⊢ x ∈ span R (g '' ↑t1) ⊔ span R ↑t2