mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
⊢ Cardinal.lift.{?u.21, u} (Module.rank R R) = Cardinal.lift.{?u.21, u} 1

Tactic:
← (Basis.singleton PUnit R).mk_eq_rank,

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
⊢ Cardinal.lift.{u, ?u.24} #PUnit.{?u.24 + 1} = Cardinal.lift.{?u.24, u} 1
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: K : Type u_2
M : Type u_3
inst✝³ : DivisionRing K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
s : Set M
inst✝ : Module.Finite K ↥(span K s)
t : Set M
ht_sub : t ⊆ s
ht_span : span K t = span K s
ht_indep : LinearIndependent K Subtype.val
⊢ ∃ u, ↑u = t ∧ u.card = finrank K ↥(span K s)

Tactic:
← Cardinal.mk_set_eq_nat_iff_finset,

Goal state after:
K : Type u_2
M : Type u_3
inst✝³ : DivisionRing K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
s : Set M
inst✝ : Module.Finite K ↥(span K s)
t : Set M
ht_sub : t ⊆ s
ht_span : span K t = span K s
ht_indep : LinearIndependent K Subtype.val
⊢ #↑t = ↑(finrank K ↥(span K s))
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: K : Type u_2
M : Type u_3
inst✝³ : DivisionRing K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
s : Set M
inst✝ : Module.Finite K ↥(span K s)
t : Set M
ht_sub : t ⊆ s
ht_span : span K t = span K s
ht_indep : LinearIndependent K Subtype.val
⊢ #↑t = Module.rank K ↥(span K s)

Tactic:
← ht_span,

Goal state after:
K : Type u_2
M : Type u_3
inst✝³ : DivisionRing K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
s : Set M
inst✝ : Module.Finite K ↥(span K s)
t : Set M
ht_sub : t ⊆ s
ht_span : span K t = span K s
ht_indep : LinearIndependent K Subtype.val
⊢ #↑t = Module.rank K ↥(span K t)
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
⊢ (v ⬝ᵥ fun j ↦ diagonal w j i) = v i * w i

Tactic:
by
  have : ∀ j ≠ i, v j * diagonal w j i = 0 := fun j hij => by
    simp [diagonal_apply_ne _ hij]
  convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1 <;> simp

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : CommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
a : α
⊢ a • M = M * diagonal fun x ↦ a

Tactic:
ext
  simp [mul_comm]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
y : α
⊢ y ∈ s → a = y

Tactic:
hy

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
y : α
hy : y ∈ s
⊢ a = y
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R✝ : Type u
S : Type u_1
M✝ M₁ : Type v
M' : Type v'
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M✝
inst✝¹³ : Module R✝ M✝
inst✝¹² : Free R✝ M✝
inst✝¹¹ : AddCommMonoid M'
inst✝¹⁰ : Module R✝ M'
inst✝⁹ : Free R✝ M'
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : Module R✝ M₁
inst✝⁶ : Free R✝ M₁
inst✝⁵ : StrongRankCondition R✝
R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
c d : R
⊢ (c • d) • LinearMap.id = (RingHom.id R) c • d • LinearMap.id

Tactic:
ext; simp [mul_smul]

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Module R C
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : ϕ x = ψ x
hy : ϕ y = ψ y
⊢ ψ x + ϕ y = ψ x + ψ y

Tactic:
hy

Goal state after:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Module R C
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : ϕ x = ψ x
hy : ϕ y = ψ y
⊢ ψ x + ψ y = ψ x + ψ y
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Module R C
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : ϕ x = ψ x
hy : ϕ y = ψ y
⊢ ψ x * ϕ y = ψ x * ψ y

Tactic:
hy

Goal state after:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Module R C
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : ϕ x = ψ x
hy : ϕ y = ψ y
⊢ ψ x * ψ y = ψ x * ψ y
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
ι : Type v
M : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
i j : ι
⊢ component R ι M i ∘ₗ lof R ι M j = if h : j = i then h ▸ LinearMap.id else 0

Tactic:
by
  aesop (add simp component.of)

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : DecidableEq A
α : Type u_2
s : Finset α
f : ↥s → Finset A
⊢ adjoin R ↑(s.attach.biUnion f) = ⨆ x, adjoin R ↑(f x)

Tactic:
by simp [adjoin_iUnion]

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: case mem.add
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : A) (hx : x ∈ adjoin R s), p 0 x ⋯ hx
zero_right : ∀ (x : A) (hx : x ∈ adjoin R s), p x 0 hx ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
smul_left : ∀ (r : R) (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (r • x) y ⋯ hy
smul_right : ∀ (r : R) (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (r • y) hx ⋯
x y z : A
hz : z ∈ s
x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p x✝ z hx✝ ⋯
h₂ : p y✝ z hy✝ ⋯
⊢ p (x✝ + y✝) z ⋯ ⋯

Tactic:
exact add_left _ _ _ _ _ _ h₁ h₂

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case mem.add
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : A
hz : z ∈ s
x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p x✝ z hx✝ ⋯
h₂ : p y✝ z hy✝ ⋯
⊢ p (x✝ + y✝) z ⋯ ⋯

Tactic:
exact add_left _ _ _ _ _ _ h₁ h₂

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case algebraMap.add
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : A
r : R
x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p x✝ ((algebraMap R A) r) hx✝ ⋯
h₂ : p y✝ ((algebraMap R A) r) hy✝ ⋯
⊢ p (x✝ + y✝) ((algebraMap R A) r) ⋯ ⋯

Tactic:
exact add_left _ _ _ _ _ _ h₁ h₂

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
ϕ ψ : A →ₐ[R] B
x y : A
hx : ϕ x = ψ x
hy : ϕ y = ψ y
⊢ ψ x * ϕ y = ψ x * ψ y

Tactic:
hy

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
ϕ ψ : A →ₐ[R] B
x y : A
hx : ϕ x = ψ x
hy : ϕ y = ψ y
⊢ ψ x * ψ y = ψ x * ψ y
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
ϕ ψ : A →ₐ[R] B
x y : A
hx : ϕ x = ψ x
hy : ϕ y = ψ y
⊢ ψ x + ϕ y = ψ x + ψ y

Tactic:
hy

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
ϕ ψ : A →ₐ[R] B
x y : A
hx : ϕ x = ψ x
hy : ϕ y = ψ y
⊢ ψ x + ψ y = ψ x + ψ y
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i j : ι
x : A
hxi : x ∈ ↑(K i)
hxj : x ∈ ↑(K j)
k : ι
hik : (fun x1 x2 ↦ x1 ≤ x2) (K i) (K k)
hjk : (fun x1 x2 ↦ x1 ≤ x2) (K j) (K k)
⊢ (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩

Tactic:
rw [hf i k hik, hf j k hjk]

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i j : ι
x : A
hxi : x ∈ ↑(K i)
hxj : x ∈ ↑(K j)
k : ι
hik : (fun x1 x2 ↦ x1 ≤ x2) (K i) (K k)
hjk : (fun x1 x2 ↦ x1 ≤ x2) (K j) (K k)
⊢ ((f k).comp (inclusion hik)) ⟨x, hxi⟩ = ((f k).comp (inclusion hjk)) ⟨x, hxj⟩
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x : A
t : Subalgebra R A
⊢ adjoin R (insert x ↑(adjoin R s)) ≤ t ↔ adjoin R (insert x s) ≤ t

Tactic:
by simp [adjoin_le_iff, Set.insert_subset_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
𝒞 : Basis κ R N
x : M ⊗[R] N
⊢ ∃ b, (b.sum fun i m ↦ m ⊗ₜ[R] 𝒞 i) = x

Tactic:
by
  classical simpa using (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm.surjective x

Goal state after:
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
ι : Type u_6
A : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : (i : ι) → Module R (A i)
h : ∀ (i : ι), Projective R (A i)
f : ((Π₀ (i : ι), A i) →₀ R) →ₗ[R] Π₀ (i : ι), A i
hf : Function.Surjective ⇑f
⊢ ∃ h, f ∘ₗ h = LinearMap.id

Tactic:
choose g hg using fun i ↦ projective_lifting_property f (DFinsupp.lsingle i) hf

Goal state after:
R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
ι : Type u_6
A : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : (i : ι) → Module R (A i)
h : ∀ (i : ι), Projective R (A i)
f : ((Π₀ (i : ι), A i) →₀ R) →ₗ[R] Π₀ (i : ι), A i
hf : Function.Surjective ⇑f
g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R
hg : ∀ (i : ι), f ∘ₗ g i = DFinsupp.lsingle i
⊢ ∃ h, f ∘ₗ h = LinearMap.id
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : ι →₀ R
g : κ →₀ N
a : ι
b : κ
⊢ ((finsuppTensorFinsuppLid R N ι κ) (f ⊗ₜ[R] g)) (a, b) = f a • g b

Tactic:
by
  simp [finsuppTensorFinsuppLid]

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

Goal state before:
pp: R : Type u_1
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
a : ι
b : κ
r : R
n : N
⊢ (finsuppTensorFinsuppLid R N ι κ) (Finsupp.single a r ⊗ₜ[R] Finsupp.single b n) = Finsupp.single (a, b) (r • n)

Tactic:
by
  simp [finsuppTensorFinsuppLid]

Goal state after:
Module: Mathlib.Algebra.Module.Rat

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
n : ℕ
hn : n ≠ 0
x y : M
hxy : (fun a ↦ n • a) x = (fun a ↦ n • a) y
⊢ x = y

Tactic:
simpa [← Nat.cast_smul_eq_nsmul ℚ≥0 n, *] using congr((n⁻¹ : ℚ≥0) • $hxy)

Goal state after:
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ (selfAdjoint R).carrier ↔ star x = x

Tactic:
exact Iff.rfl

Goal state after:
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ (skewAdjoint R).carrier ↔ star x = -x

Tactic:
exact Iff.rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Fin

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
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ N = span R (Set.range (⇑N.subtype ∘ ⇑b))

Tactic:
rw [Set.range_comp, Submodule.span_image, b.span_eq, Submodule.map_subtype_top]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Fin

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
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
b : Basis (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ N = span R (Set.range (⇑N.subtype ∘ ⇑b))

Tactic:
rw [Set.range_comp, Submodule.span_image, b.span_eq, Submodule.map_subtype_top]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst✝ : DecidableEq m
i' : m
h : ¬i' = i
⊢ M i' j = if i' = i then b j else M i' j

Tactic:
if_neg h

Goal state after:
case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst✝ : DecidableEq m
i' : m
h : ¬i' = i
⊢ M i' j = M i' j
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst✝ : DecidableEq n
j' : n
h : ¬j' = j
⊢ M i j' = if j' = j then c i else M i j'

Tactic:
if_neg h

Goal state after:
case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst✝ : DecidableEq n
j' : n
h : ¬j' = j
⊢ M i j' = M i j'
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
f : α → β
i✝ : m
j✝ : n
⊢ (M.updateRow i b).map f i✝ j✝ = (M.map f).updateRow i (f ∘ b) i✝ j✝

Tactic:
rw [updateRow_apply, map_apply, map_apply, updateRow_apply]

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
f : α → β
i✝ : m
j✝ : n
⊢ f (if i✝ = i then b j✝ else M i✝ j✝) = if i✝ = i then (f ∘ b) j✝ else f (M i✝ j✝)
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inr.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j k : n
hjk : j ≠ k
⊢ Pi.single k x j = 0

Tactic:
Pi.single_eq_of_ne hjk

Goal state after:
case inr.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j k : n
hjk : j ≠ k
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: n : ℕ
m' : Type uₘ
α : Type u_1
inst✝ : NonUnitalCommSemiring α
A : m' → Fin n.succ → α
x : α
v : Fin n → α
i : m'
⊢ (of A *ᵥ vecCons x v) i = (x • vecHead ∘ A + of (vecTail ∘ A) *ᵥ v) i

Tactic:
simp [mulVec, mul_comm]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
x : OreLocalization S X
⊢ ∀ (a b : X × ↥S), a ≈ b → add' a.fst a.snd x = add' b.fst b.snd x

Tactic:
by
      rintro ⟨r₁, s₁⟩ ⟨r₂, s₂⟩ ⟨sb, rb, hb, hb'⟩
      induction x with | _ r₃ s₃
      change add'' _ _ _ _ = add'' _ _ _ _
      dsimp only at *
      rcases oreCondition (s₃ : R) s₂ with ⟨rc, sc, hc⟩
      rcases oreCondition rc sb with ⟨rd, sd, hd⟩
      have : rd * rb * s₁ = sd * sc * s₃ := by
        rw [mul_assoc, ← hb', ← mul_assoc, ← hd, mul_assoc, ← hc, mul_assoc]
      rw [add''_char _ _ _ _ rc sc hc (sc * s₃).2]
      rw [add''_char _ _ _ _ _ _ this.symm (sd * sc * s₃).2]
      refine oreDiv_eq_iff.mpr ?_
      simp only [smul_add]
      use sd, 1
      simp only [one_smul, one_mul, mul_smul, ← hb, Submonoid.smul_def, ← mul_assoc, and_true]
      simp only [smul_smul, hd]

Goal state after:
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
s : Set K
p : (x : K) → x ∈ closure s → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : x ∈ closure s), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : x ∈ closure s), p x hx → p x⁻¹ ⋯
mul : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯
x : K
h : x ∈ closure s
a✝ b✝ : K
w✝¹ : a✝ ∈ closure s
hx : p a✝ w✝¹
w✝ : b✝ ∈ closure s
hy : p b✝ w✝
⊢ a✝ * b✝ ∈ {x | ∃ (hx : x ∈ closure s), p x hx}

Tactic:
exact ⟨_, mul _ _ _ _ hx hy⟩

Goal state after:
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : K
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
let s : Subfield K :=
    { __ := Subring.copy _ _ (Subring.coe_iSup_of_directed hS).symm
      inv_mem' := fun _ hx ↦ have ⟨i, hi⟩ := Set.mem_iUnion.mp hx
        Set.mem_iUnion.mpr ⟨i, (S i).inv_mem hi⟩ }

Goal state after:
K : Type u
inst✝ : DivisionRing K
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : K
s : Subfield K :=
  let __spread.0 := (⨆ i, (S i).toSubring).copy (⋃ i, ↑(S i).toSubring) ⋯;
  { toSubring := __spread.0, inv_mem' := ⋯ }
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : K
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ s ∈ S, ↑s

Tactic:
by simp [mem_sSup_of_directedOn Sne hS]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
f g : M₁ →ₗ[R] M₁
⊢ (toMatrix v₁ v₁) (f * g) = (toMatrix v₁ v₁) f * (toMatrix v₁ v₁) g

Tactic:
rw [Module.End.mul_eq_comp, LinearMap.toMatrix_comp v₁ v₁ v₁ f g]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Divisibility

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m₁ m₂ : M
x✝ : f m₁ ∣ f m₂
n : N
eq : f m₂ = f m₁ * n
⊢ ∃ s ∈ S, m₁ ∣ s * m₂

Tactic:
have ⟨⟨m, s⟩, hn⟩ := f.surj n
    replace hn := congr(f m₁ * $hn)
    rw [← mul_assoc, ← eq, ← map_mul, ← map_mul] at hn
    have ⟨s', hs'⟩ := f.eq_iff_exists.mp hn
    refine ⟨_, mul_mem s'.2 s.2, s' * m, ?_⟩
    rwa [mul_left_comm, mul_assoc, mul_comm s.1]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case succ
R : Type u_1
inst✝⁴ : CommSemiring R
n✝ : Type u_4
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n✝ R M₁
A : Matrix n✝ n✝ R
n : ℕ
ih : (toLin v₁ v₁) (A ^ n) = (toLin v₁ v₁) A ^ n
⊢ (toLin v₁ v₁) (A ^ n * A) = (toLin v₁ v₁) A ^ n * (toLin v₁ v₁) A

Tactic:
toLin_mul v₁ v₁,

Goal state after:
case succ
R : Type u_1
inst✝⁴ : CommSemiring R
n✝ : Type u_4
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n✝ R M₁
A : Matrix n✝ n✝ R
n : ℕ
ih : (toLin v₁ v₁) (A ^ n) = (toLin v₁ v₁) A ^ n
⊢ (toLin v₁ v₁) (A ^ n) ∘ₗ (toLin v₁ v₁) A = (toLin v₁ v₁) A ^ n * (toLin v₁ v₁) A
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
r₁ r₂ : R
h : ∃ u v, u • r₂ = v • r₁ ∧ ↑u * ↑1 = v * ↑1
⊢ r₁ = r₂

Tactic:
rcases h with ⟨u, v, h₁, h₂⟩

Goal state after:
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
r₁ r₂ : R
u : ↥S
v : R
h₁ : u • r₂ = v • r₁
h₂ : ↑u * ↑1 = v * ↑1
⊢ r₁ = r₂