mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case insert.refine_1
R : Type u
I : Type v
inst✝ : CommSemiring R
z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsCoprime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ IsCoprime (s a) (∏ x ∈ r, s x)

pp: case insert.refine_2
R : Type u
I : Type v
inst✝ : CommSemiring R
z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsCoprime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ s a ∣ z

pp: case insert.refine_3
R : Type u
I : Type v
inst✝ : CommSemiring R
z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsCoprime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ ∏ x ∈ r, s x ∣ z

Tactic:
· refine IsCoprime.prod_right fun i hir ↦ ?_
      exact Hs (by simp) (by simp [hir]) (ne_of_mem_of_not_mem hir har).symm

Goal state after:
case insert.refine_2
R : Type u
I : Type v
inst✝ : CommSemiring R
z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsCoprime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ s a ∣ z

case insert.refine_3
R : Type u
I : Type v
inst✝ : CommSemiring R
z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsCoprime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ ∏ x ∈ r, s x ∣ z
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
ι : Sort u_2
t✝ : ι → Submodule R A
N : Submodule R M
t : A
ht : t ∈ ⨆ i, t✝ i
s : M
hs : s ∈ N
⊢ 0 • s ∈ ⨆ i, t✝ i • N

Tactic:
simp_rw [zero_smul]

Goal state after:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
ι : Sort u_2
t✝ : ι → Submodule R A
N : Submodule R M
t : A
ht : t ∈ ⨆ i, t✝ i
s : M
hs : s ∈ N
⊢ 0 ∈ ⨆ i, t✝ i • N
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective ⇑↑(opLinearEquiv R)
⊢ map (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R).symm) (M * N)) =
    map (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R).symm) N * map (↑(opLinearEquiv R).symm) M)

Tactic:
← map_comp,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective ⇑↑(opLinearEquiv R)
⊢ map (↑(opLinearEquiv R) ∘ₗ ↑(opLinearEquiv R).symm) (M * N) =
    map (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R).symm) N * map (↑(opLinearEquiv R).symm) M)
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective ⇑↑(opLinearEquiv R)
⊢ map (↑(opLinearEquiv R) ∘ₗ ↑(opLinearEquiv R).symm) (M * N) =
    map (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R).symm) M) *
      map (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R).symm) N)

Tactic:
← map_comp,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective ⇑↑(opLinearEquiv R)
⊢ map (↑(opLinearEquiv R) ∘ₗ ↑(opLinearEquiv R).symm) (M * N) =
    map (↑(opLinearEquiv R) ∘ₗ ↑(opLinearEquiv R).symm) M * map (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R).symm) N)
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective ⇑↑(opLinearEquiv R)
⊢ map (↑(opLinearEquiv R) ∘ₗ ↑(opLinearEquiv R).symm) (M * N) =
    map (↑(opLinearEquiv R) ∘ₗ ↑(opLinearEquiv R).symm) M * map (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R).symm) N)

Tactic:
← map_comp,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective ⇑↑(opLinearEquiv R)
⊢ map (↑(opLinearEquiv R) ∘ₗ ↑(opLinearEquiv R).symm) (M * N) =
    map (↑(opLinearEquiv R) ∘ₗ ↑(opLinearEquiv R).symm) M * map (↑(opLinearEquiv R) ∘ₗ ↑(opLinearEquiv R).symm) N
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ map (↑RingEquiv.prodComm) (I.prod J) = J.prod I

Tactic:
by
  refine Trans.trans (ideal_prod_eq _) ?_
  simp [map_map]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
| span (s ×ˢ t)

Tactic:
rw [Ideal.ideal_prod_eq (Ideal.span (s ×ˢ t))]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
| (map (RingHom.fst R S) (span (s ×ˢ t))).prod (map (RingHom.snd R S) (span (s ×ˢ t)))
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
I✝ J : Ideal R
K L : Ideal S
inst✝ : RingHomClass F R S
I : Ideal S
c x : R
hx : x ∈ ⇑f ⁻¹' ↑I
⊢ c • x ∈ ⇑f ⁻¹' ↑I

Tactic:
simp only [smul_eq_mul, Set.mem_preimage, map_mul, SetLike.mem_coe] at *
    exact mul_mem_left I _ hx

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
h : comap f I = ⊥
⊢ I = ⊥

Tactic:
by
  ext x
  obtain ⟨y, hy⟩ := hf x
  aesop (add norm [Submodule.eq_bot_iff])

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

Goal state before:
pp: case succ.inr
R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : J.IsTwoSided
h : I ⊔ J = ⊤
n : ℕ
ih : I ⊔ J ^ n = ⊤
hn : n ≠ 0
⊢ I ⊔ J ^ (n + 1) = ⊤

Tactic:
rwa [J.pow_succ' hn, sup_mul_eq_of_coprime_right ih]

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

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
⊢ j ∈ {J | map f I ≤ J ∧ J.IsPrime} → j ∈ map f '' {J | I ≤ J ∧ J.IsPrime}

pp: case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
⊢ j ∈ map f '' {J | I ≤ J ∧ J.IsPrime} → j ∈ {J | map f I ≤ J ∧ J.IsPrime}

Tactic:
· rintro ⟨hj, hj'⟩
    have : j.IsPrime := hj'
    exact
      ⟨comap f j, ⟨⟨map_le_iff_le_comap.1 hj, comap_isPrime f j⟩, map_comap_of_surjective f hf j⟩⟩

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
⊢ j ∈ map f '' {J | I ≤ J ∧ J.IsPrime} → j ∈ {J | map f I ≤ J ∧ J.IsPrime}
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : a ∉ s
ih : (s ∪ s₂).lcm f = GCDMonoid.lcm (s.lcm f) (s₂.lcm f)
⊢ (insert a (s ∪ s₂)).lcm f = GCDMonoid.lcm ((insert a s).lcm f) (s₂.lcm f)

Tactic:
lcm_insert,

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : a ∉ s
ih : (s ∪ s₂).lcm f = GCDMonoid.lcm (s.lcm f) (s₂.lcm f)
⊢ GCDMonoid.lcm (f a) ((s ∪ s₂).lcm f) = GCDMonoid.lcm ((insert a s).lcm f) (s₂.lcm f)
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : a ∉ s
ih : (s ∪ s₂).lcm f = GCDMonoid.lcm (s.lcm f) (s₂.lcm f)
⊢ GCDMonoid.lcm (f a) ((s ∪ s₂).lcm f) = GCDMonoid.lcm ((insert a s).lcm f) (s₂.lcm f)

Tactic:
lcm_insert,

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : a ∉ s
ih : (s ∪ s₂).lcm f = GCDMonoid.lcm (s.lcm f) (s₂.lcm f)
⊢ GCDMonoid.lcm (f a) ((s ∪ s₂).lcm f) = GCDMonoid.lcm (GCDMonoid.lcm (f a) (s.lcm f)) (s₂.lcm f)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : R
I J : Ideal R
⊢ (∀ {zI : R}, zI ∈ I → zI ∈ span {x} * J) ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI

Tactic:
simp only [mem_span_singleton_mul]

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : b = gcd a b * e
f : α
hf : a = gcd a b * f
⊢ c = b - (b - c)

Tactic:
sub_sub_cancel

Goal state after:
case h
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : b = gcd a b * e
f : α
hf : a = gcd a b * f
⊢ c = c
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ StrongRankCondition R ↔ ∀ (n : ℕ) (f : (ℕ →₀ R) →ₗ[R] Fin n → R), ¬Injective ⇑f

Tactic:
by
  rw [strongRankCondition_iff_succ, ← not_iff_not]; push Not
  constructor <;> refine fun ⟨n, f, inj⟩ ↦ ⟨n, ?_⟩
  · exact f.exists_finsupp_nat_of_fin_fun_injective inj
  · exact ⟨f ∘ₗ Finsupp.lmapDomain R R (↑) ∘ₗ (Finsupp.linearEquivFunOnFinite ..).symm.toLinearMap,
      inj.comp <| by simpa using! Finsupp.mapDomain_injective Fin.val_injective⟩

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

Goal state before:
pp: case inl.intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
ι' : Type w'
inst✝ : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this✝ : Nontrivial R
val✝¹ : Fintype ι
this : Finite ι'
val✝ : Fintype ι'
⊢ (ι → R) ≃ₗ[R] ι' → R

Tactic:
exact
      (Finsupp.linearEquivFunOnFinite R R ι).symm.trans v.repr.symm ≪≫ₗ v'.repr ≪≫ₗ
        Finsupp.linearEquivFunOnFinite R R ι'

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : κ → Finset ι := fun k ↦ (b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
v' : ↑(Φ ⁻¹' {s}) → M := fun k ↦ v ↑k
i' : LinearIndependent (ι := ↑(Φ ⁻¹' {s})) R v'
⊢ Finite ↑(Φ ⁻¹' {s})

Tactic:
apply i'.finite_of_le_span_finite v' (s.image b)

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : κ → Finset ι := ⋯
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
v' : ↑(Φ ⁻¹' {s}) → M := ⋯
i' : LinearIndependent (ι := ↑(Φ ⁻¹' {s})) R v'
⊢ range v' ⊆ ↑(span R ↑(Finset.image (⇑b) s))
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type w
b : Basis ι R M
κ : Type w
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
this : Nontrivial R
⊢ #κ ≤ ↑(Fintype.card ι)

Tactic:
rw [Fintype.card_congr (Equiv.ofInjective b b.injective)]

Goal state after:
case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type w
b : Basis ι R M
κ : Type w
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
this : Nontrivial R
⊢ #κ ≤ ↑(Fintype.card ↑(range ⇑b))
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : StrongRankCondition R
h : Bijective ⇑(algebraMap R S)
⊢ Module.rank R S = 1

Tactic:
rw [rank_eq_one_iff_finrank_eq_one, finrank_of_bijective_algebraMap h]

Goal state after:
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)
⊢ ∃ f, (∀ (i : Fin (finrank K ↥(span K s))), f i ∈ s) ∧ span K (range f) = span K s ∧ LinearIndependent K f

Tactic:
by
  rcases exists_finset_span_eq_linearIndepOn K s with ⟨t, hts, ht_card, ht_span, ht_indep⟩
  set e := (Finset.equivFinOfCardEq ht_card).symm
  exact ⟨(↑) ∘ e, fun i ↦ hts (e i).2, by simpa, ht_indep.comp _ e.injective⟩

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
a : α
⊢ (single i j a)ᵀ = single j i a

Tactic:
aesop (add unsafe unfold single)

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
i : m
j : n
a : α
β : Type u_10
inst✝² : Zero β
F : Type u_11
inst✝¹ : FunLike F α β
inst✝ : ZeroHomClass F α β
f : F
⊢ (single i j a).map ⇑f = single i j (f a)

Tactic:
aesop (add unsafe unfold single)

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

Goal state before:
pp: case intro.intro
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ P (∑ x ∈ Finset.univ ×ˢ Finset.univ, single x.1 x.2 (M x.1 x.2))

Tactic:
apply Finset.sum_induction _ _ h_add h_zero

Goal state after:
case intro.intro
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ ∀ x ∈ Finset.univ ×ˢ Finset.univ, P (single x.1 x.2 (M x.1 x.2))
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case inr.inl
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i j : n
⊢ diagonal (fun x ↦ M i i) j j = M j j

Tactic:
rw [diagonal_apply_eq]
    obtain rfl | hij := Decidable.eq_or_ne i j
    · rfl
    · exact diag_eq_of_commute_single (hM hij)

Goal state after:
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : α →₀ ℕ
a✝ : α
⊢ (f ⊓ g) a✝ = min (f a✝) (g a✝)

Tactic:
Finsupp.inf_apply

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

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✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ finrank R M = Fintype.card (ChooseBasisIndex R M)

Tactic:
by
  simp [finrank, rank_eq_card_chooseBasisIndex]

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

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✝ : StrongRankCondition R
n : ℕ
hn : finrank R M = n.succ
⊢ 0 < finrank R M

Tactic:
rw [hn]; exact n.succ_pos

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
a b c d : R
h1 : a - b ∈ carrier
h2 : c - d ∈ carrier
⊢ a + c - (b + d) ∈ carrier

Tactic:
rw [show a + c - (b + d) = (a - b) + (c - d) by abel]
        exact add_mem h1 h2

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ (S ⊔ T).toSubsemiring = S.toSubsemiring ⊔ T.toSubsemiring

Tactic:
by
  rw [← S.toSubsemiring.closure_eq, ← T.toSubsemiring.closure_eq, ← Subsemiring.closure_union]
  simp_rw [sup_def, adjoin_toSubsemiring, Subalgebra.coe_toSubsemiring]
  congr 1
  rw [Set.union_eq_right]
  rintro _ ⟨x, rfl⟩
  exact Set.mem_union_left _ (algebraMap_mem S x)

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
⊢ (sSup S).toSubsemiring = sSup (Subsemiring.closure '' SetLike.coe '' S)

Tactic:
sSup_image,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
⊢ (sSup S).toSubsemiring = ⨆ a ∈ SetLike.coe '' S, Subsemiring.closure a
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
n : S
hn : n ∈ M
hb : n * b ∈ s
⊢ a * b ∈ {x | ∃ m ∈ M, m * x ∈ s}

Tactic:
refine ⟨_, mul_mem hm hn, mul_mul_mul_comm m n a b ▸ mul_mem ha hb⟩

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
s : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
x : A
hx : x ∈ adjoin R s
a✝ b✝ : A
w✝¹ : a✝ ∈ adjoin R s
hpx : p a✝ w✝¹
w✝ : b✝ ∈ adjoin R s
hpy : p b✝ w✝
⊢ a✝ + b✝ ∈ {x | ∃ (hx : x ∈ adjoin R s), p x hx}

Tactic:
exact ⟨_, add _ _ _ _ hpx hpy⟩

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

Goal state before:
pp: 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
x : A
⊢ x ∈ R ∙ 0 ↔ x = 0

Tactic:
Submodule.span_zero_singleton,

Goal state after:
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
x : A
⊢ x ∈ ⊥ ↔ x = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Associator

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
x : M →ₗ[R] N
⊢ map id (map x id) ∘ₗ ↑(assoc R P M Q) = ↑(assoc R P N Q) ∘ₗ map (map id x) id

Tactic:
map_map_comp_assoc_eq

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

Goal state before:
pp: R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
i : ι₁
x : M₁ i
y : M₂'
⊢ (lof S ι₁ (fun i ↦ M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y) = (directSumLeft R S M₁ M₂') ((lof S ι₁ M₁ i) x ⊗ₜ[R] y)

Tactic:
directSumLeft_tmul_lof

Goal state after:
R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
i : ι₁
x : M₁ i
y : M₂'
⊢ (lof S ι₁ (fun i ↦ M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y) = (lof S ι₁ (fun i ↦ M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)
Module: Mathlib.Algebra.Module.Rat

Goal state before:
pp: M : Type u_1
M₂ : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_3
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
c : ℚ≥0
x : M
⊢ f (↑c • x) = ↑c • f x

Tactic:
by
  rw [NNRat.cast_def, NNRat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_natCast_smul f R S, map_inv_natCast_smul f R S]

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
x✝ : ↥(skewAdjoint.submodule R A)
x : A
hx : star x = -x
⊢ ↑((skewAdjointPart R ∘ₗ (skewAdjoint.submodule R A).subtype) ⟨x, hx⟩) = ↑(LinearMap.id ⟨x, hx⟩)

Tactic:
simp only [LinearMap.comp_apply, Submodule.subtype_apply, skewAdjointPart_apply_coe, hx,
      sub_neg_eq_add, smul_add, invOf_two_smul_add_invOf_two_smul]; rfl

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : l ⊕ m → α
⊢ fromBlocks A B C D *ᵥ x = Sum.elim (A *ᵥ x ∘ Sum.inl + B *ᵥ x ∘ Sum.inr) (C *ᵥ x ∘ Sum.inl + D *ᵥ x ∘ Sum.inr)

Tactic:
by
  ext i
  cases i <;> simp [mulVec, dotProduct]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
⊢ blockDiagonal (M + N) = blockDiagonal M + blockDiagonal N

Tactic:
by
  ext
  simp only [blockDiagonal_apply, Pi.add_apply, add_apply]
  split_ifs <;> simp

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

Goal state before:
pp: case inl.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
hji : j ≠ i
⊢ v j = Function.update v i x j

Tactic:
Function.update_of_ne hji

Goal state after:
case inl.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
hji : j ≠ i
⊢ v j = v j