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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁ ∪ s₂).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd

Tactic:
rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_add]
  simp

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

Goal state before:
pp: case h
a : ℤ
h : a = -↑a.natAbs
⊢ ↑a.natAbs = -1 * a

Tactic:
← neg_eq_iff_eq_neg.mpr h

Goal state after:
case h
a : ℤ
h : a = -↑a.natAbs
⊢ -a = -1 * a
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
g : A →+* C
hg : ker f ≤ ker g
⊢ g (f_inv 1) = 1

Tactic:
rw [← map_one g, ← sub_eq_zero, ← map_sub g, ← mem_ker]

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
g : A →+* C
hg : ker f ≤ ker g
⊢ f_inv 1 - 1 ∈ ker g
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
g : A →+* C
hg : ker f ≤ ker g
h : B →+* C
hh : h.comp f = g
⊢ h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩

Tactic:
simp_rw [← hh]

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
g : A →+* C
hg : ker f ≤ ker g
h : B →+* C
hh : h.comp f = g
⊢ h = (f.liftOfRightInverse f_inv hf) ⟨h.comp f, ⋯⟩
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
⊢ RingHom.ker (algebraMap R A) = ⊥

Tactic:
by
  ext; simp

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a : α
u : αˣ
ha : a ≠ 0
⊢ out (Associates.mk (a * ↑u)) = out (Associates.mk a)

Tactic:
Associates.mk_eq_mk_iff_associated.mpr (associated_mul_unit_right a u u.isUnit)

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a : α
u : αˣ
ha : a ≠ 0
⊢ out (Associates.mk (a * ↑u)) = out (Associates.mk (a * ↑u))
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}
hri : r ∉ I.radical
m : Ideal R
hIm : I ≤ m
hm : Maximal (fun x ↦ x ∈ {K | r ∉ K.radical}) m
hrm : r ∉ m.radical
this : ∀ x ∉ m, r ∈ (m ⊔ span {x}).radical
⊢ m ≠ ⊤

Tactic:
by rintro rfl; rw [radical_top] at hrm; exact hrm trivial

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₂ : a ≠ 0
u : Rˣ
ha₁ : (factors a).prod * ↑u ∈ I
hu : (factors a).prod * ↑u = a
⊢ (factors a).prod ∈ I

Tactic:
mul_unit_mem_iff_mem _ u.isUnit

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₂ : a ≠ 0
u : Rˣ
ha₁ : (factors a).prod ∈ I
hu : (factors a).prod * ↑u = a
⊢ (factors a).prod ∈ I
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
k : ℕ
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
⊢ d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * (b' * (d₁ ^ k * a'))

Tactic:
mul_comm a',

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
k : ℕ
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
⊢ d₂ ^ k * (d₁ ^ k * (b' * a')) = d₂ ^ k * (b' * (d₁ ^ k * a'))
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
s : Finset ι
x : ι → R
p : Ideal R
hp : p.IsPrime
⊢ ∏ i ∈ s, x i ∈ p ↔ ∃ i ∈ s, x i ∈ p

Tactic:
by
  simp_rw [← span_singleton_le_iff_mem, ← prod_span_singleton]
  exact hp.prod_le

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (⇑f) Associates.mk
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ Classical.choose ⋯ = Classical.choose ⋯ * if b = 0 then 1 else Classical.choose ⋯

Tactic:
if_neg hb,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (⇑f) Associates.mk
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ Classical.choose ⋯ = Classical.choose ⋯ * Classical.choose ⋯
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 u_2
v : ι → M
i : LinearIndependent R v
w : Finset M
s : span R ↑w = ⊤
⊢ #ι ≤ ↑w.card

Tactic:
simpa only [Finset.coe_sort_coe, Fintype.card_coe] using linearIndependent_le_span v i w s

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 v
v : Basis ι R M
this : Nontrivial R
⊢ #ι = Module.rank R M

Tactic:
rw [Module.rank_def]

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ #ι = ⨆ ι, #↑↑ι
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case hd
R : Type u
S : Type u_1
M : Type v
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : Module.Finite R M
inst✝⁵ : Semiring S
inst✝⁴ : Module S M
inst✝³ : Module R S
inst✝² : IsScalarTower R S S
inst✝¹ : FaithfulSMul R S
inst✝ : IsScalarTower R S M
⊢ Module.rank R M < ℵ₀

Tactic:
exact Module.rank_lt_aleph0 _ _

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

Goal state before:
pp: case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i)
has : a ∈ s
⊢ ∃ i ∈ s, I ≤ f i

pp: case neg
ι : Type u_1
R : Type u
inst✝ : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i)
has : a ∉ s
⊢ ∃ i ∈ s, I ≤ f i

Tactic:
· obtain ⟨t, hat, rfl⟩ : ∃ t, a ∉ t ∧ insert a t = s :=
        ⟨s.erase a, Finset.notMem_erase a s, Finset.insert_erase has⟩
      by_cases hbt : b ∈ t
      · obtain ⟨u, hbu, rfl⟩ : ∃ u, b ∉ u ∧ insert b u = t :=
          ⟨t.erase b, Finset.notMem_erase b t, Finset.insert_erase hbt⟩
        have hp' : ∀ i ∈ u, IsPrime (f i) := by
          intro i hiu
          refine hp i (Finset.mem_insert_of_mem (Finset.mem_insert_of_mem hiu)) ?_ ?_ <;>
              rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Finset.coe_insert, Set.biUnion_insert, Set.biUnion_insert, ←
          Set.union_assoc, subset_union_prime' hp'] at h
        rwa [Finset.exists_mem_insert, Finset.exists_mem_insert]
      · have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f a : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
        rwa [Finset.exists_mem_insert]

Goal state after:
case neg
ι : Type u_1
R : Type u
inst✝ : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i)
has : a ∉ s
⊢ ∃ i ∈ s, I ≤ f i
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 ⬝ᵥ diagonal w i = v i * w i

Tactic:
have : ∀ j ≠ i, v j * diagonal w i j = 0 := fun j hij => by
    simp [diagonal_apply_ne' _ hij]

Goal state after:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w i j = 0
⊢ v ⬝ᵥ diagonal w i = v i * w i
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R✝ : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
R : Type u_10
inst✝¹ : NonAssocSemiring R
inst✝ : IsStablyFiniteRing R
f : R →* Matrix (Fin 1) (Fin 1) R := { toFun := fun r ↦ diagonal fun x ↦ r, map_one' := ⋯, map_mul' := ⋯ }
x✝¹ x✝ : R
eq : f x✝¹ = f x✝
⊢ x✝¹ = x✝

Tactic:
by simpa [f] using congr($eq 0 0)

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

Goal state before:
pp: R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Finite n
inst✝² : Semiring R
i : m
j : n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
⊢ (stdBasis R m n) (i, j) = single i j 1

Tactic:
simp [stdBasis, single_eq_of_single_single]

Goal state after:
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
x : A
ij : ι' × ι
⊢ ((b.smulTower' c).repr x) ij = (b.repr ((c.repr x) ij.1)) ij.2

Tactic:
by
  rw [smulTower', repr_reindex_apply, smulTower_repr]; rfl

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : (toMultiset f).toFinset = f.support
⊢ (n • {a}).toFinset ∪ f.support = (single a n + f).support

Tactic:
support_add_eq,

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : (toMultiset f).toFinset = f.support
⊢ (n • {a}).toFinset ∪ f.support = (single a n).support ∪ f.support

case refine_2
α : Type u_1
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : (toMultiset f).toFinset = f.support
⊢ Disjoint (single a n).support f.support
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: F : Type u
K : Type v
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : Module F K
inst✝⁷ : StrongRankCondition F
inst✝⁶ : StrongRankCondition K
inst✝⁵ : Free F K
A : Type v
inst✝⁴ : AddCommMonoid A
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : Free K A
⊢ Module.rank F K * Module.rank K A = Module.rank F A

Tactic:
convert! lift_rank_mul_lift_rank F K A <;> rw [lift_id]

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

Goal state before:
pp: R : Type u
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✝² : StrongRankCondition R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R M'
⊢ finrank R M ≤ finrank R M' ↔ ∃ f, Injective ⇑f

Tactic:
simp [← lift_rank_le_iff_exists_linearMap, ← finrank_eq_rank]

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
W : Type v
inst✝² : AddCommMonoid W
inst✝¹ : Module R W
inst✝ : Free R W
n : ℕ
hn : n ≠ 0
hVW : Module.rank R M = n • Module.rank R W
⊢ Module.Finite R M ↔ Module.Finite R W

Tactic:
by
  simp only [← rank_lt_aleph0_iff, hVW, nsmul_lt_aleph0_iff_of_ne_zero hn]

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

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ Submodule.restrictScalars R 1 = toSubmodule S

Tactic:
by
  ext; simp

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

Goal state before:
pp: ι : Type v
M : Type u_1
S : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike S M
inst✝² : AddSubmonoidClass S M
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
⊢ (support fun i ↦ ↑(x i)) ⊆ ↑(DFinsupp.support x)

Tactic:
intro m

Goal state after:
ι : Type v
M : Type u_1
S : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike S M
inst✝² : AddSubmonoidClass S M
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
m : ι
⊢ (m ∈ support fun i ↦ ↑(x i)) → m ∈ ↑(DFinsupp.support x)
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
⊢ n * (m * a) + m * (n * b) ∈ s

Tactic:
exact add_mem (mul_mem (H hn) ha) (mul_mem (H hm) hb)

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 : R
⊢ (algebraMap R A) x ∈ {a | ϕ a = ψ a}

Tactic:
by
    simp only [Set.mem_ofPred_eq, AlgHomClass.commutes]

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

Goal state before:
pp: case a.cons.cons.inl
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
tl : List A
ih : (∀ y ∈ tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = tl.prod
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = tl.prod
hd : R
HL : (algebraMap R A) hd ∈ Set.range ⇑(algebraMap R A) ∪ s ∧ ∀ x ∈ tl, x ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ ∃ z_1 r_1, ∃ (_ : r_1 ∈ Submonoid.closure s), z_1 • r_1 = (algebraMap R A) hd * z • r

Tactic:
refine ⟨hd * z, r, hr, ?_⟩

Goal state after:
case a.cons.cons.inl
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
tl : List A
ih : (∀ y ∈ tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = tl.prod
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = tl.prod
hd : R
HL : (algebraMap R A) hd ∈ Set.range ⇑(algebraMap R A) ∪ s ∧ ∀ x ∈ tl, x ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ (hd * z) • r = (algebraMap R A) hd * z • r
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case algebraMap
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : A
s : Set A
h : ∀ b ∈ s, Commute a b
r : R
⊢ Commute a ((algebraMap R A) r)

Tactic:
exact commutes r a |>.symm

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

Goal state before:
pp: case h
R : Type u_1
inst✝² : Semiring R
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_8
b : Basis ι R P
⊢ Function.LeftInverse ⇑(linearCombination R id) ⇑((b.constr ℕ) fun i ↦ Finsupp.single (b i) 1)

Tactic:
intro m

Goal state after:
case h
R : Type u_1
inst✝² : Semiring R
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_8
b : Basis ι R P
m : P
⊢ (linearCombination R id) (((b.constr ℕ) fun i ↦ Finsupp.single (b i) 1) m) = m
Module: Mathlib.LinearAlgebra.DirectSum.TensorProduct

Goal state before:
pp: R : Type u
inst✝⁷ : CommSemiring R
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₁'
inst✝³ : AddCommMonoid M₂'
inst✝² : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝¹ : Module R M₁'
inst✝ : Module R M₂'
f : M₁' →ₗ[R] M₂'
⊢ ↑(directSumRight R R M₂' M₁) ∘ₗ rTensor (⨁ (i : ι₁), M₁ i) f =
    (lmap fun x ↦ rTensor (M₁ x) f) ∘ₗ ↑(directSumRight R R M₁' M₁)

Tactic:
by
  ext; simp

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✝⁵ : AddCommMonoid M₁'
inst✝⁴ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝³ : Module R M₁'
inst✝² : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
m : M₁'
n : ⨁ (i : ι₂), M₂ i
i : ι₂
this :
  ↑R (component S ι₂ (fun i ↦ M₁' ⊗[R] M₂ i) i) ∘ₗ ↑R ↑(directSumRight R S M₁' M₂) ∘ₗ (mk R M₁' (⨁ (i : ι₂), M₂ i)) m =
    (mk R M₁' (M₂ i)) m ∘ₗ component R ι₂ M₂ i
⊢ ((directSumRight R S M₁' M₂) (m ⊗ₜ[R] n)) i = m ⊗ₜ[R] n i

Tactic:
by
    simpa using! LinearMap.congr_fun this n

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₂)

pp: case inr
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₂ : J
⊢ 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:
· rw [diagonal_apply_ne _ hi, diagonal_apply_ne _ (ne_of_apply_ne Prod.fst hi),
      Matrix.zero_apply]

Goal state after:
case inr
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₂ : J
⊢ 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₂)
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
⊢ IsSelfAdjoint (star x * x)

Tactic:
by
  simp only [IsSelfAdjoint, star_mul, star_star]

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
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
i✝ : m × o
j✝ : n × o
⊢ (blockDiagonal M).map f i✝ j✝ = blockDiagonal (fun k ↦ (M k).map f) i✝ j✝

Tactic:
simp only [map_apply, blockDiagonal_apply]

Goal state after:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
i✝ : m × o
j✝ : n × o
⊢ f (if i✝.2 = j✝.2 then M i✝.2 i✝.1 j✝.1 else 0) = if i✝.2 = j✝.2 then f (M i✝.2 i✝.1 j✝.1) else 0
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 α
j : n
c : m → α
inst✝ : DecidableEq n
f : α → β
⊢ (M.updateCol j c).map f = (M.map f).updateCol j (f ∘ c)

Tactic:
by
  ext
  rw [updateCol_apply, map_apply, map_apply, updateCol_apply]
  exact apply_ite f _ _ _

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
Q : Type uQ
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring A
inst✝¹⁵ : Semiring B
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra R B
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
inst✝¹⁰ : Module A M
inst✝⁹ : Module B M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : IsScalarTower R B M
inst✝⁶ : SMulCommClass A B M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
f : N →ₗ[R] Q
⊢ (lTensor B M) f ∘ₗ ↑(cancelBaseChange R A B M N) = ↑(cancelBaseChange R A B M Q) ∘ₗ (lTensor B M) ((lTensor A A) f)

Tactic:
by
  ext; simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ baseChange A id = id

Tactic:
by
  ext; simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
P : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ baseChange A (g ∘ₗ f) = baseChange A g ∘ₗ baseChange A f

Tactic:
by
  ext; simp

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

Goal state before:
pp: R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
A : Type u_7
B : Type u_8
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : M →ₗ[R] N
⊢ baseChange B (baseChange A f) = ↑(cancelBaseChange R A B B N).symm ∘ₗ baseChange B f ∘ₗ ↑(cancelBaseChange R A B B M)

Tactic:
by
  ext; simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : Module.End R M
⊢ baseChange A (f * g) = baseChange A f * baseChange A g

Tactic:
by
  ext; simp

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
⊢ (↑numeratorHom).toFun 0 = 0

Tactic:
exact OreLocalization.zero_def

Goal state after: