mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, motive (Polynomial.C a * X ^ n)
B : ∀ (s : Finset ℕ), motive (∑ n ∈ s, Polynomial.C (p.coeff n) * X ^ n)
⊢ motive (∑ n ∈ p.support, Polynomial.C (p.coeff n) * X ^ n)

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, motive (Polynomial.C a * X ^ n)
B : ∀ (s : Finset ℕ), motive (∑ n ∈ s, Polynomial.C (p.coeff n) * X ^ n)
⊢ motive (∑ n ∈ p.support, Polynomial.C (p.coeff n) * X ^ n)
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive ((Polynomial.monomial n) a)
n : ℕ
a : R
_h : motive (C a * X ^ n)
⊢ motive ((Polynomial.monomial (n + 1)) a)

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive ((Polynomial.monomial n) a)
n : ℕ
a : R
_h : motive (C a * X ^ n)
⊢ motive ((Polynomial.monomial (n + 1)) a)
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
⊢ p ⊓ q = ⊥ ↔ p ⊓ q = ⊥

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
⊢ a = a

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n i : ℕ
a : R
h : i ≠ n
⊢ p.coeff i = p.coeff i

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
⊢ (if n✝ = n then 0 else p.coeff n✝) = if n✝ = n then 0 else p.coeff n✝

Tactic:
]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
⊢ p ⊔ q = ⊤ ↔ p ⊔ q = ⊤

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
ha : a ≠ 0
⊢ insert n p.support = insert n p.support

Tactic:
]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R ↥p
x : M
hx : x ∈ p
hq : ⟨f ↑⟨x, hx⟩, ⋯⟩ ∈ q
hx' : ⟨x, hx⟩ ∈ ↑q
⊢ p.subtype ⟨x, hx⟩ ∈ Submodule.comap f (Submodule.map p.subtype q)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R ↥p
x : M
hx : x ∈ p
hq : ⟨f ↑⟨x, hx⟩, ⋯⟩ ∈ q
hx' : ⟨x, hx⟩ ∈ ↑q
⊢ p.subtype ⟨x, hx⟩ ∈ Submodule.comap f (Submodule.map p.subtype q)
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.support.Nonempty
⊢ p.coeffs.Nonempty

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.support.Nonempty
⊢ p.coeffs.Nonempty
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.coeff n ≠ 0
⊢ p.coeffs.Nonempty

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.coeff n ≠ 0
⊢ p.coeffs.Nonempty
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
c : R
hc : c ≠ 0
⊢ image (fun n_1 ↦ ((monomial n) c).coeff n_1) {n} = {c}

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
c : R
hc : c ≠ 0
⊢ image (fun n_1 ↦ ((monomial n) c).coeff n_1) {n} = {c}
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
a : R
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u
a b : R
inst✝ : Ring R
n : ℕ
⊢ (monomial n) a + -(monomial n) b = (monomial n) a + -(monomial n) b

Tactic:
]

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
this : ↑e.symm ∘ₗ ((↑e ∘ₗ f) ∘ₗ ↑e.symm) ∘ₗ ↑e = f
⊢ p ≤ Submodule.comap f p ↔ p ≤ Submodule.comap f p

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : DivisionSemiring R
q : ℚ≥0
f : R[X]
⊢ q • f = q • f

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : DivisionRing R
a : ℚ
f : R[X]
⊢ a • f = a • f

Tactic:
]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
G : Type u_3
inst✝² : Monoid G
inst✝¹ : DistribMulAction G M
inst✝ : SMulCommClass G R M
x : M
g : G
⊢ MulAction.orbit G x ⊆ ⇑(DistribSMul.toLinearMap R M g) ⁻¹' ↑(span R (MulAction.orbit G x))

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
G : Type u_3
inst✝² : Monoid G
inst✝¹ : DistribMulAction G M
inst✝ : SMulCommClass G R M
x : M
g : G
⊢ MulAction.orbit G x ⊆ ⇑(DistribSMul.toLinearMap R M g) ⁻¹' ↑(span R (MulAction.orbit G x))
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: ι : Type u_7
R : Type u_8
inst✝¹ : Semiring R
inst✝ : DecidableEq ι
⊢ LinearIndependent R ((fun i ↦ single i 1) ∘ ⇑(Equiv.sigmaPUnit ι))

Tactic:
]

Goal state after:
ι : Type u_7
R : Type u_8
inst✝¹ : Semiring R
inst✝ : DecidableEq ι
⊢ LinearIndependent R ((fun i ↦ single i 1) ∘ ⇑(Equiv.sigmaPUnit ι))
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
inst✝ : DecidableEq ι
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
⊢ LinearIndependent R ((fun i ↦ single i (v i)) ∘ ⇑(Equiv.sigmaPUnit ι))

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
inst✝ : DecidableEq ι
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
⊢ LinearIndependent R ((fun i ↦ single i (v i)) ∘ ⇑(Equiv.sigmaPUnit ι))
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: case neg
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ 0 = 0

pp: case neg
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ ⟨j', i'⟩ ≠ ⟨j, i⟩

Tactic:
]

Goal state after:
case neg
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ ⟨j', i'⟩ ≠ ⟨j, 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)
⊢ Function.Injective ⇑((mapRange.linearMap fun i ↦ linearCombination R (f i)) ∘ₗ ↑(sigmaFinsuppLequivDFinsupp R))

Tactic:
]

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 ⇑((mapRange.linearMap fun i ↦ linearCombination R (f i)) ∘ₗ ↑(sigmaFinsuppLequivDFinsupp R))
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
x✝¹ : G
x✝ : x✝¹ ≠ s
⊢ φ (Pi.single s 1 * Pi.single x✝¹ 1) = 0

Tactic:
]

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
x✝¹ : G
x✝ : x✝¹ ≠ s
⊢ φ (Pi.single s 1 * Pi.single x✝¹ 1) = 0
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
s : G
h1 : φ (Pi.single s 1) = 1
hs : φ (Pi.single s 1) ≠ 0
h2 : ∀ (t : G), t ≠ s → φ (Pi.single t 1) = 0
⊢ φ (Pi.single s 1) = 1

Tactic:
]

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
s : G
h1 : φ (Pi.single s 1) = 1
hs : φ (Pi.single s 1) ≠ 0
h2 : ∀ (t : G), t ≠ s → φ (Pi.single t 1) = 0
⊢ φ (Pi.single s 1) = 1
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case neg
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
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
]

Goal state after:
case neg
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
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: R : Type u_1
ι : Type u_3
inst✝ : Semiring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
huv : IsCompl (Set.range u) (Set.range v)
⊢ IsCompl (span R (Set.range fun x ↦ single (u x) 1)) (span R (Set.range fun x ↦ single (v x) 1))

Tactic:
]

Goal state after:
R : Type u_1
ι : Type u_3
inst✝ : Semiring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
huv : IsCompl (Set.range u) (Set.range v)
⊢ IsCompl (span R (Set.range fun x ↦ single (u x) 1)) (span R (Set.range fun x ↦ single (v x) 1))
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: R : Type u_1
ι : Type u_3
inst✝ : Semiring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
huv : IsCompl (Set.range u) (Set.range v)
this :
  IsCompl (span R (Set.range fun x ↦ Finsupp.basisSingleOne (u x))) (span R (Set.range (⇑Finsupp.basisSingleOne ∘ v)))
⊢ IsCompl (span R (Set.range fun x ↦ single (u x) 1)) (span R (Set.range fun x ↦ single (v x) 1))

Tactic:
]

Goal state after:
R : Type u_1
ι : Type u_3
inst✝ : Semiring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
huv : IsCompl (Set.range u) (Set.range v)
this :
  IsCompl (span R (Set.range fun x ↦ Finsupp.basisSingleOne (u x))) (span R (Set.range (⇑Finsupp.basisSingleOne ∘ v)))
⊢ IsCompl (span R (Set.range fun x ↦ single (u x) 1)) (span R (Set.range fun x ↦ single (v x) 1))
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝³ : Finite ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
⊢ span R (Set.range v) = ⊤ ↔ span R (Set.range v) = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : IsDomain R
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
⊢ LinearIndependent R ((fun i ↦ single i (v i)) ∘ ⇑(Equiv.sigmaPUnit ι))

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : IsDomain R
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
⊢ LinearIndependent R ((fun i ↦ single i (v i)) ∘ ⇑(Equiv.sigmaPUnit ι))
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: R : Type u_1
ι : Type u_3
inst✝ : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : ι
⊢ i ∈ ⊤

Tactic:
]

Goal state after:
R : Type u_1
ι : Type u_3
inst✝ : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : ι
⊢ i ∈ ⊤
Module: Mathlib.RingTheory.Finiteness.Cardinality

Goal state before:
pp: M : Type u_3
inst✝ : AddCommMonoid M
S : AddSubmonoid M
⊢ (∃ n f, f.range = toNatSubmodule S) ↔ ∃ n f, AddMonoidHom.mrange f = (toNatSubmodule S).toAddSubmonoid

Tactic:
]

Goal state after:
M : Type u_3
inst✝ : AddCommMonoid M
S : AddSubmonoid M
⊢ (∃ n f, f.range = toNatSubmodule S) ↔ ∃ n f, AddMonoidHom.mrange f = (toNatSubmodule S).toAddSubmonoid
Module: Mathlib.RingTheory.Finiteness.Cardinality

Goal state before:
pp: M : Type u_3
inst✝ : AddCommGroup M
H : AddSubgroup M
⊢ (∃ n f, f.range = toIntSubmodule H) ↔ ∃ n f, f.range = (toIntSubmodule H).toAddSubgroup

Tactic:
]

Goal state after:
M : Type u_3
inst✝ : AddCommGroup M
H : AddSubgroup M
⊢ (∃ n f, f.range = toIntSubmodule H) ↔ ∃ n f, f.range = (toIntSubmodule H).toAddSubgroup
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: case inl
R : Type u_1
ι : Type u_3
inst✝ : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : α
this : single (u i) 1 = (lmapDomain R R u) (single i 1)
⊢ single i 1 = single i 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Cardinality

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : f.range = ⊤
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: case inr
R : Type u_1
ι : Type u_3
inst✝ : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : β
⊢ (lcomapDomain u hu) (Finsupp.basisSingleOne (v i)) = 0

pp: case inr.hx
R : Type u_1
ι : Type u_3
inst✝ : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : β
⊢ Finsupp.basisSingleOne (v i) ∈ span R (Set.range fun x ↦ single (v x) 1)

Tactic:
]

Goal state after:
case inr
R : Type u_1
ι : Type u_3
inst✝ : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : β
⊢ (lcomapDomain u hu) (Finsupp.basisSingleOne (v i)) = 0

case inr.hx
R : Type u_1
ι : Type u_3
inst✝ : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : β
⊢ Finsupp.basisSingleOne (v i) ∈ span R (Set.range fun x ↦ single (v x) 1)
Module: Mathlib.RingTheory.Finiteness.Cardinality

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite R
s : Finset M
⊢ Module.Finite R ↑↑(span R ↑s)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite R
s : Finset M
⊢ Module.Finite R ↑↑(span R ↑s)
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
ι : Type u_3
B : Basis ι R S
i : ι
r : R
s : S
⊢ r • (B.repr s) i = r • (B.repr s) i

Tactic:
]

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

Goal state before:
pp: case pos
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 : ι
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}
hc : 1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
hA' : A' = A
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B', UniqueMul A B' a0 b0

Tactic:
]

Goal state after:
case pos
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 : ι
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}
hc : 1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
hA' : A' = A
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B', UniqueMul A B' a0 b0
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case neg
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 : (i : ι) → G i
ha0 : a0 ∈ A ∧ a0 i = ai
b0 : (i : ι) → G i
hb0 : b0 ∈ B ∧ b0 i = bi
hu : UniqueMul A' B' a0 b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
]

Goal state after:
case neg
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 : (i : ι) → G i
ha0 : a0 ∈ A ∧ a0 i = ai
b0 : (i : ι) → G i
hb0 : b0 ∈ B ∧ b0 i = bi
hu : UniqueMul A' B' a0 b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case inr
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 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
]

Goal state after:
case inr
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 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2