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

Goal state before:
pp: G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
a : G₀
h0 : a ≠ 0
⊢ normalize a = 1

Tactic:
simp [normalize_apply, h0]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ u, I ≤ f i
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
hp' : ∀ i ∈ u, (f i).IsPrime
⊢ I ≤ f a ∨ ∃ x ∈ insert b u, I ≤ f x

Tactic:
Finset.exists_mem_insert

Goal state after:
case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ u, I ≤ f i
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
hp' : ∀ i ∈ u, (f i).IsPrime
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ x ∈ u, I ≤ f x
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case neg
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f a ∨ ∃ i ∈ t, I ≤ f i
has : a ∈ insert a t
hbt : b ∉ t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i ∈ insert a t, I ≤ f i

Tactic:
Finset.exists_mem_insert

Goal state after:
case neg
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f a ∨ ∃ i ∈ t, I ≤ f i
has : a ∈ insert a t
hbt : b ∉ t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ I ≤ f a ∨ ∃ x ∈ t, I ≤ f x
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f b ∨ ∃ i ∈ t, I ≤ f i
has : a ∉ insert b t
hbs : b ∈ insert b t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i ∈ insert b t, I ≤ f i

Tactic:
Finset.exists_mem_insert

Goal state after:
case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : I ≤ f b ∨ ∃ i ∈ t, I ≤ f i
has : a ∉ insert b t
hbs : b ∈ insert b t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ I ≤ f b ∨ ∃ x ∈ t, I ≤ f x
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case neg.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
i : ι
t : Finset ι
left✝ : i ∉ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ b → (f i_1).IsPrime
h : I ≤ f i ∨ ∃ i ∈ t, I ≤ f i
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
Finset.exists_mem_insert

Goal state after:
case neg.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
i : ι
t : Finset ι
left✝ : i ∉ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ b → (f i_1).IsPrime
h : I ≤ f i ∨ ∃ i ∈ t, I ≤ f i
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ I ≤ f i ∨ ∃ x ∈ t, I ≤ f x
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype o
v : o → α
M : Matrix m n α
N : Matrix n o α
⊢ M *ᵥ N *ᵥ v = (M * N) *ᵥ v

Tactic:
ext
  symm
  apply dotProduct_assoc

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set R
I J : Ideal R
m : ↑s → ℕ
a b : ↑s → R
ha : ∀ (z : ↑s), a z ∈ I
hb : ∀ (z : ↑s), b z ∈ J
heq : ∀ (z : ↑s), a z + b z = ↑z ^ m z
⊢ Set.range a ⊆ ↑I

Tactic:
by rwa [Set.range_subset_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ Fintype (ChooseBasisIndex R M)

Tactic:
refine @Fintype.ofFinite _ ?_

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ Finite (ChooseBasisIndex R M)
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
v : n → α
A : Matrix m n α
⊢ -(-A *ᵥ v) = A *ᵥ v

Tactic:
neg_mulVec,

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
v : n → α
A : Matrix m n α
⊢ - -(A *ᵥ v) = A *ᵥ v
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
k l : ℕ
i : n
h : (M ^ k).row i = 0
h' : k ≤ l
⊢ (M ^ l).row i = 0

Tactic:
by
  replace h' : l = k + (l - k) := by lia
  rw [← single_one_vecMul] at h ⊢
  rw [h', pow_add, ← vecMul_vecMul, h, zero_vecMul]

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

Goal state before:
pp: case mpr
α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : ↑T
⊢ (∃ i x_1, f i x_1 ∈ t ∧ inclusion ⋯ x_1 = inclusion hT x) → iUnionLift S f hf T hT x ∈ t

Tactic:
rintro ⟨i, ⟨y, hi⟩, h, hxy⟩

Goal state after:
case mpr
α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : ↑T
i : ι
y : α
hi : y ∈ S i
h : f i ⟨y, hi⟩ ∈ t
hxy : inclusion ⋯ ⟨y, hi⟩ = inclusion hT x
⊢ iUnionLift S f hf T hT x ∈ t
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq ι
f g : ι →₀ ℕ
⊢ Multiset.toFinsupp.symm.toEquiv f ≤ Multiset.toFinsupp.symm.toEquiv g ↔ f ≤ g

Tactic:
by simp [le_def, Multiset.le_iff_count]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) *
      lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{w, max v w} (lift.{w, v} #(Free.ChooseBasisIndex F K)) *
      lift.{w, max v w} (lift.{v, w} #(Free.ChooseBasisIndex K A))

Tactic:
lift_lift,

Goal state after:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{max v w, v} #(Free.ChooseBasisIndex F K) * lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{w, max v w} (lift.{w, v} #(Free.ChooseBasisIndex F K)) *
      lift.{w, max v w} (lift.{v, w} #(Free.ChooseBasisIndex K A))
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{max v w, v} #(Free.ChooseBasisIndex F K) * lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{w, max v w} (lift.{w, v} #(Free.ChooseBasisIndex F K)) *
      lift.{w, max v w} (lift.{v, w} #(Free.ChooseBasisIndex K A))

Tactic:
lift_lift,

Goal state after:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{max v w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A) =
    lift.{w, max v w} (lift.{w, v} #(Free.ChooseBasisIndex F K)) *
      lift.{w, max v w} (lift.{v, w} #(Free.ChooseBasisIndex K A))
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{max v w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A) =
    lift.{w, max v w} (lift.{w, v} #(Free.ChooseBasisIndex F K)) *
      lift.{w, max v w} (lift.{v, w} #(Free.ChooseBasisIndex K A))

Tactic:
lift_lift,

Goal state after:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{max v w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A) =
    lift.{w, v} #(Free.ChooseBasisIndex F K) * lift.{w, max v w} (lift.{v, w} #(Free.ChooseBasisIndex K A))
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{max v w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A) =
    lift.{w, v} #(Free.ChooseBasisIndex F K) * lift.{w, max v w} (lift.{v, w} #(Free.ChooseBasisIndex K A))

Tactic:
lift_lift,

Goal state after:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{max v w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A) =
    lift.{w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A)
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
⊢ t₁ = t₂

Tactic:
refine RingCon.ext fun a b ↦ ⟨fun H ↦ ?_, fun H ↦ ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₁ a b
⊢ t₂ a b

case refine_2
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₂ a b
⊢ t₁ a b
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
S : Subalgebra R A
inst✝³ : CommSemiring R'
inst✝² : SMul R' R
inst✝¹ : Algebra R' A
inst✝ : IsScalarTower R' R A
x : R'
⊢ (algebraMap R' A) x ∈ S

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
S : Subalgebra R A
inst✝³ : CommSemiring R'
inst✝² : SMul R' R
inst✝¹ : Algebra R' A
inst✝ : IsScalarTower R' R A
x : R'
⊢ x • 1 ∈ S
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)
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ (x + y) =
      Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ x +
        Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ y

Tactic:
apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· + ·))

Goal state after:
case hopi
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 : ι) (x y : ↑↑(K i)), Set.inclusion ⋯ (x + y) = Set.inclusion ⋯ x + Set.inclusion ⋯ y

case h
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 : ι) (x y : ↑↑(K i)), (f i) (x + y) = (f i) x + (f i) y
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁶ : CommSemiring E
inst✝⁵ : Semiring K
inst✝⁴ : SMul F E
inst✝³ : Algebra E K
inst✝² : Semiring F
inst✝¹ : Module F K
inst✝ : IsScalarTower F E K
L : Submonoid K
S : Set K
h : ↑L = ↑(span F S)
⊢ toSubmodule (adjoin E ↑L) = span E S

Tactic:
by
  rw [adjoin_eq_span, L.closure_eq, h]
  exact (span_le.mpr <| span_subset_span _ _ _).antisymm (span_mono subset_span)

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

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
P : Type v
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : Small.{w, u} R
inst✝ : Small.{w, v} P
⊢ Projective R P ↔ ∃ M x x_1, ∃ (_ : Free R M), ∃ i s, s ∘ₗ i = LinearMap.id

Tactic:
let e : (Shrink.{w, v} P →₀ Shrink.{w, u} R) ≃ₗ[R] P →₀ R :=
    Finsupp.mapDomain.linearEquiv _ R (equivShrink P).symm ≪≫ₗ
      Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R)
  refine ⟨fun ⟨i, hi⟩ ↦ ⟨(Shrink.{w} P) →₀ (Shrink.{w} R), _, _, Free.of_basis ⟨e⟩,
    e.symm.toLinearMap ∘ₗ i, (linearCombination R id) ∘ₗ e.toLinearMap, ?_⟩,
      fun ⟨_, _, _, _, i, s, H⟩ ↦ Projective.of_split i s H⟩
  apply LinearMap.ext
  simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply, e.apply_symm_apply]
  exact hi

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

Goal state before:
pp: I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
⊢ (comp I J K L R) (single i j (single k l r)) = single (i, k) (j, l) r

Tactic:
by
  ext ⟨i', k'⟩ ⟨j', l'⟩
  dsimp [comp_apply]
  obtain hi | rfl := ne_or_eq i i'
  · rw [single_apply_of_row_ne hi,
      single_apply_of_row_ne (ne_of_apply_ne Prod.fst hi), Matrix.zero_apply]
  obtain hj | rfl := ne_or_eq j j'
  · rw [single_apply_of_col_ne _ _ hj,
      single_apply_of_col_ne _ _ (ne_of_apply_ne Prod.fst hj), Matrix.zero_apply]
  rw [single_apply_same]
  obtain hk | rfl := ne_or_eq k k'
  · rw [single_apply_of_row_ne hk,
      single_apply_of_row_ne (ne_of_apply_ne Prod.snd hk)]
  obtain hj | rfl := ne_or_eq l l'
  · rw [single_apply_of_col_ne _ _ hj,
      single_apply_of_col_ne _ _ (ne_of_apply_ne Prod.snd hj)]
  rw [single_apply_same, single_apply_same]

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

Goal state before:
pp: case inl
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ : J
i₂ : I
j₂ : J
hi : i₁ ≠ i₂
⊢ diagonal (fun i ↦ diagonal fun j ↦ d i j) i₁ i₂ j₁ j₂ = diagonal (fun ij ↦ d ij.1 ij.2) (i₁, j₁) (i₂, j₂)

Tactic:
diagonal_apply_ne _ hi,

Goal state after:
case inl
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ : J
i₂ : I
j₂ : J
hi : i₁ ≠ i₂
⊢ 0 j₁ j₂ = diagonal (fun ij ↦ d ij.1 ij.2) (i₁, j₁) (i₂, j₂)
Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : Matrix m n α
⊢ M.map star = 0 ↔ M = 0

Tactic:
by simp [← ext_iff]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
r : R
x : A
⊢ ⟨⅟2 • (r • x - star (r • x)), ⋯⟩ = (RingHom.id R) r • ⟨⅟2 • (x - star x), ⋯⟩

Tactic:
ext
    simp [← mul_smul, ← smul_sub,
      show r * ⅟2 = ⅟2 * r from Commute.invOf_right <| (2 : ℕ).commute_cast r]

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

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
⊢ blockDiagonal' (fun k ↦ diagonal (d k)) ⟨i, k⟩ ⟨j, k'⟩ = diagonal (fun ik ↦ d ik.fst ik.snd) ⟨i, k⟩ ⟨j, k'⟩

Tactic:
simp only [blockDiagonal'_apply, diagonal]

Goal state after:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
⊢ (if h : i = j then of (fun i_1 j ↦ if i_1 = j then d i i_1 else 0) k (cast ⋯ k') else 0) =
    of (fun i j ↦ if i = j then d i.fst i.snd else 0) ⟨i, k⟩ ⟨j, k'⟩
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ ∑ j, A (↑i) j * B j ↑k = ∑ j, A ↑i ↑j * B ↑j ↑k

Tactic:
rw [Finset.sum_subtype]

Goal state after:
case h
R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ ∀ (x : n), x ∈ Finset.univ ↔ ⊤ x
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e₁ : A ≃⋆ₐ[R] B
e₂ : B ≃⋆ₐ[R] C
r : R
a : A
⊢ e₂.toFun (e₁.toFun (r • a)) = r • e₂.toFun (e₁.toFun a)

Tactic:
e₁.map_smul',

Goal state after:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e₁ : A ≃⋆ₐ[R] B
e₂ : B ≃⋆ₐ[R] C
r : R
a : A
⊢ e₂.toFun (r • e₁.toFun a) = r • e₂.toFun (e₁.toFun a)
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f₁ f₂ : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((TensorProduct.curry (↑R (map (f₁ + f₂) g))) x✝¹) x✝ = ((TensorProduct.curry (↑R (map f₁ g + map f₂ g))) x✝¹) x✝

Tactic:
TensorProduct.curry_apply,

Goal state after:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f₁ f₂ : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (↑R (map (f₁ + f₂) g)) (x✝¹ ⊗ₜ[R] x✝) = (↑R (map f₁ g + map f₂ g)) (x✝¹ ⊗ₜ[R] x✝)
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[A] P
g₁ g₂ : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((TensorProduct.curry (↑R (map f (g₁ + g₂)))) x✝¹) x✝ = ((TensorProduct.curry (↑R (map f g₁ + map f g₂))) x✝¹) x✝

Tactic:
TensorProduct.curry_apply,

Goal state after:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[A] P
g₁ g₂ : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (↑R (map f (g₁ + g₂))) (x✝¹ ⊗ₜ[R] x✝) = (↑R (map f g₁ + map f g₂)) (x✝¹ ⊗ₜ[R] x✝)