mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : (insert j u).card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i (insert j u)), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
hp' : ∀ k ∈ insert i u, (f k).IsPrime
hiu : i ∉ u
⊢ (insert i u).card = n

Tactic:
Finset.card_insert_of_notMem

Goal state after:
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : u.card + 1 = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i (insert j u)), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
hp' : ∀ k ∈ insert i u, (f k).IsPrime
hiu : i ∉ u
⊢ u.card + 1 = n

ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : u.card + 1 = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i (insert j u)), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
hp' : ∀ k ∈ insert i u, (f k).IsPrime
hiu : i ∉ u
⊢ i ∉ u

ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : (insert j u).card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i (insert j u)), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
hp' : ∀ k ∈ insert i u, (f k).IsPrime
hiu : i ∉ u
⊢ j ∉ u
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
S : Submodule R M
h : S.IsPrincipal
⊢ span R ↑{generator S} = S

Tactic:
by simp only [Finset.coe_singleton, span_singleton_generator]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝ : EuclideanDomain R
S : Ideal R
h : {x | x ∈ S ∧ x ≠ 0}.Nonempty
wf : WellFounded EuclideanDomain.r
hmin : wf.min {x | x ∈ S ∧ x ≠ 0} h ∈ S ∧ wf.min {x | x ∈ S ∧ x ≠ 0} h ≠ 0
x : R
hx : x ∈ S
this✝ : x % wf.min {x | x ∈ S ∧ x ≠ 0} h ∉ {x | x ∈ S ∧ x ≠ 0}
this : x % wf.min {x | x ∈ S ∧ x ≠ 0} h = 0
⊢ wf.min {x | x ∈ S ∧ x ≠ 0} h ∣ x % wf.min {x | x ∈ S ∧ x ≠ 0} h

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
a b : G₀
⊢ (if a = 0 ∧ b = 0 then 0 else 1) ∣ a

Tactic:
by simp +contextual

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

Goal state before:
pp: α : Type u_1
G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
a b : G₀
⊢ (if a = 0 ∧ b = 0 then 0 else 1) ∣ b

Tactic:
by simp +contextual

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
κ : Type w
v : κ → M
i : LinearIndependent R v
⊢ #κ ≤ #ι

Tactic:
by
  classical
  -- We split into cases depending on whether `ι` is infinite.
  cases fintypeOrInfinite ι
  · rw [Cardinal.mk_fintype ι] -- When `ι` is finite, we have `linearIndependent_le_span`,
    have : Nontrivial R := nontrivial_of_invariantBasisNumber R
    rw [Fintype.card_congr (Equiv.ofInjective b b.injective)]
    exact linearIndependent_le_span v i (range b) b.span_eq
  · -- and otherwise we have `linearIndependent_le_infinite_basis`.
    exact linearIndependent_le_infinite_basis b v i

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
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
L L' : Submodule R M
inst✝ : Module.Finite R ↥L'
s : S
hr : IsSMulRegular M s
h : ∀ x ∈ L, s • x ∈ L'
⊢ finrank R ↥L ≤ finrank R ↥L'

Tactic:
refine finrank_le_finrank_of_rank_le_rank (lift_le.mpr <| rank_le_of_isSMulRegular L L' hr h) ?_

Goal state after:
R : Type u
M : Type v
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : StrongRankCondition R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
L L' : Submodule R M
inst✝ : Module.Finite R ↥L'
s : S
hr : IsSMulRegular M s
h : ∀ x ∈ L, s • x ∈ L'
⊢ Module.rank R ↥L' < ℵ₀
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 : Finset M
hts : ↑t ⊆ s
ht_card : t.card = finrank K ↥(span K s)
ht_span : span K ↑t = span K s
ht_indep : LinearIndepOn K id ↑t
e : Fin (finrank K ↥(span K s)) ≃ ↥t := (Finset.equivFinOfCardEq ht_card).symm
⊢ ∃ f, (∀ (i : Fin (finrank K ↥(span K s))), f i ∈ s) ∧ span K (range f) = span K s ∧ LinearIndependent K f

Tactic:
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: case pos
m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
a✝ : α
a : m
b : n
hi : i = a
hj : j = b
⊢ of (fun i' j' ↦ if i = i' ∧ j = j' then a✝ else 0) a b = of (Pi.single i (Pi.single j a✝)) a b

Tactic:
simp [*]

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

Goal state before:
pp: case neg
m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
a✝ : α
a : m
b : n
hi : i = a
hj : ¬j = b
⊢ of (fun i' j' ↦ if i = i' ∧ j = j' then a✝ else 0) a b = of (Pi.single i (Pi.single j a✝)) a b

Tactic:
simp [*]

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

Goal state before:
pp: case pos
m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
a✝ : α
a : m
b : n
hi : ¬i = a
hj : j = b
⊢ of (fun i' j' ↦ if i = i' ∧ j = j' then a✝ else 0) a b = of (Pi.single i (Pi.single j a✝)) a b

Tactic:
simp [*]

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

Goal state before:
pp: case neg
m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
a✝ : α
a : m
b : n
hi : ¬i = a
hj : ¬j = b
⊢ of (fun i' j' ↦ if i = i' ∧ j = j' then a✝ else 0) a b = of (Pi.single i (Pi.single j a✝)) a b

Tactic:
simp [*]

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq m
a : α
⊢ (diagonal fun i ↦ MulOpposite.op a • 1) = diagonal fun x ↦ a

Tactic:
op_smul_eq_mul,

Goal state after:
m : Type u_2
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq m
a : α
⊢ (diagonal fun i ↦ 1 * a) = diagonal fun x ↦ a
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic

Goal state before:
pp: case intro
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ Module.Finite R M

Tactic:
refine ⟨⟨Finset.univ.image b, ?_⟩⟩
    simp only [Set.image_univ, Finset.coe_univ, Finset.coe_image, Basis.span_eq]

Goal state after:
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
f✝ f : C →ₐ[A] D
⊢ (fun fg ↦
        let x := fg.fst.toAlgebra;
        AlgHom.restrictScalars A fg.snd)
      ((fun f ↦ ⟨AlgHom.domRestrict B f, AlgHom.extendScalars B f⟩) f) =
    f

Tactic:
dsimp only
    ext
    rfl

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : LinearOrder M
inst✝⁴ : CanonicallyOrderedAdd M
inst✝³ : Sub M
inst✝² : AddLeftReflectLE M
inst✝¹ : OrderedSub M
s : Finset ι
inst✝ : OrderBot M
hs : s.Nonempty
f : ι → M
a : M
⊢ s.sup f + a = s.sup fun i ↦ f i + a

Tactic:
← Finset.sup'_eq_sup hs,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : LinearOrder M
inst✝⁴ : CanonicallyOrderedAdd M
inst✝³ : Sub M
inst✝² : AddLeftReflectLE M
inst✝¹ : OrderedSub M
s : Finset ι
inst✝ : OrderBot M
hs : s.Nonempty
f : ι → M
a : M
⊢ s.sup' hs f + a = s.sup fun i ↦ f i + a
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : LinearOrder M
inst✝⁴ : CanonicallyOrderedAdd M
inst✝³ : Sub M
inst✝² : AddLeftReflectLE M
inst✝¹ : OrderedSub M
s : Finset ι
inst✝ : OrderBot M
hs : s.Nonempty
f : ι → M
a : M
⊢ s.sup' hs f + a = s.sup fun i ↦ f i + a

Tactic:
← Finset.sup'_eq_sup hs,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : LinearOrder M
inst✝⁴ : CanonicallyOrderedAdd M
inst✝³ : Sub M
inst✝² : AddLeftReflectLE M
inst✝¹ : OrderedSub M
s : Finset ι
inst✝ : OrderBot M
hs : s.Nonempty
f : ι → M
a : M
⊢ s.sup' hs f + a = s.sup' hs fun i ↦ f i + a
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : LinearOrder M
inst✝⁴ : CanonicallyOrderedAdd M
inst✝³ : Sub M
inst✝² : AddLeftReflectLE M
inst✝¹ : OrderedSub M
s : Finset ι
inst✝ : OrderBot M
hs : s.Nonempty
f : ι → M
a : M
⊢ a + s.sup f = s.sup fun i ↦ a + f i

Tactic:
← Finset.sup'_eq_sup hs,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : LinearOrder M
inst✝⁴ : CanonicallyOrderedAdd M
inst✝³ : Sub M
inst✝² : AddLeftReflectLE M
inst✝¹ : OrderedSub M
s : Finset ι
inst✝ : OrderBot M
hs : s.Nonempty
f : ι → M
a : M
⊢ a + s.sup' hs f = s.sup fun i ↦ a + f i
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : LinearOrder M
inst✝⁴ : CanonicallyOrderedAdd M
inst✝³ : Sub M
inst✝² : AddLeftReflectLE M
inst✝¹ : OrderedSub M
s : Finset ι
inst✝ : OrderBot M
hs : s.Nonempty
f : ι → M
a : M
⊢ a + s.sup' hs f = s.sup fun i ↦ a + f i

Tactic:
← Finset.sup'_eq_sup hs,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : LinearOrder M
inst✝⁴ : CanonicallyOrderedAdd M
inst✝³ : Sub M
inst✝² : AddLeftReflectLE M
inst✝¹ : OrderedSub M
s : Finset ι
inst✝ : OrderBot M
hs : s.Nonempty
f : ι → M
a : M
⊢ a + s.sup' hs f = s.sup' hs fun i ↦ a + f i
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_2
β : Sort u_3
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⟩
dir : Directed (fun x1 x2 ↦ x1 ⊆ x2) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi : ∀ (i : ι) (x y : ↑(S i)), inclusion ⋯ (opi i x y) = op (inclusion ⋯ x) (inclusion ⋯ y)
x y : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
j : ι
hj : ↑y ∈ S j
k : ι
hik : S i ⊆ S k
hjk : S j ⊆ S k
hx : x = inclusion ⋯ ⟨↑x, ⋯⟩
hy : y = inclusion ⋯ ⟨↑y, ⋯⟩
hxy : ↑(inclusion ⋯ (opi k ⟨↑x, ⋯⟩ ⟨↑y, ⋯⟩)) ∈ S k
| iUnionLift S f hf (iUnion S) ⋯ (op x y)

Tactic:
rw [hx, hy, ← hopi, iUnionLift_of_mem _ hxy]

Goal state after:
α : Type u_1
ι : Sort u_2
β : Sort u_3
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⟩
dir : Directed (fun x1 x2 ↦ x1 ⊆ x2) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi : ∀ (i : ι) (x y : ↑(S i)), inclusion ⋯ (opi i x y) = op (inclusion ⋯ x) (inclusion ⋯ y)
x y : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
j : ι
hj : ↑y ∈ S j
k : ι
hik : S i ⊆ S k
hjk : S j ⊆ S k
hx : x = inclusion ⋯ ⟨↑x, ⋯⟩
hy : y = inclusion ⋯ ⟨↑y, ⋯⟩
hxy : ↑(inclusion ⋯ (opi k ⟨↑x, ⋯⟩ ⟨↑y, ⋯⟩)) ∈ S k
| f k ⟨↑(inclusion ⋯ (opi k ⟨↑x, ⋯⟩ ⟨↑y, ⋯⟩)), hxy⟩
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'
cond : finrank R M = finrank R M'
⊢ lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')

Tactic:
by simp only [← finrank_eq_rank, cond, lift_natCast]

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:
simp only [← rank_lt_aleph0_iff, hVW, nsmul_lt_aleph0_iff_of_ne_zero hn]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ J ≤ { ringCon := I.ringCon ⊔ J.ringCon }

Tactic:
rw [ringCon_le_iff]; exact le_sup_right

Goal state after:
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)
κ : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
h : ι ≃ κ
k : κ
x : M (h.symm k)
⊢ (lequivCongrLeft R h).symm ((lof R κ (fun k ↦ M (h.symm k)) k) x) = (lof R ι M (h.symm k)) x

Tactic:
rw [LinearEquiv.symm_apply_eq]
  symm
  exact lequivCongrLeft_lof _ rfl _ _ rfl

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i ↦ A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o ↑(Set.Iic p) := p.mapIic
this : (⇑e ∘ fun i ↦ Submodule.comap p.subtype (A ↑i)) = fun i ↦ ⟨A ↑i, ⋯⟩
⊢ iSupIndep fun i ↦ ⟨A ↑i, ⋯⟩

Tactic:
exact .of_coe_Iic_comp h

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
⊢ ↑⊥ = {0}

Tactic:
simp [Set.ext_iff, NonUnitalAlgebra.mem_bot]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b : A
⊢ Commute (r • a) b

Tactic:
by rw [commute_iff_eq, mul_smul_comm, smul_mul_assoc, ha.comm]

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

Goal state before:
pp: case add
R : Type u_11
A : Type u_12
A' : Type u_13
B : Type u_14
B' : Type u_15
C : Type u_16
C' : Type u_17
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A'
inst✝⁴ : AddCommMonoid B'
inst✝³ : AddCommMonoid C'
inst✝² : Module R A'
inst✝¹ : Module R B'
inst✝ : Module R C'
eA : A ≃ A'
eB : B ≃ B'
eC : C ≃ C'
x✝ y✝ : A ⊗[R] B ⊗[R] C
a✝¹ :
  (TensorProduct.assoc R A B C) x✝ =
    (TensorProduct.congr (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB)) (linearEquiv R eC) ≪≫ₗ
        (TensorProduct.assoc R A' B' C' ≪≫ₗ
          TensorProduct.congr (linearEquiv R eA).symm
            (TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eC).symm)))
      x✝
a✝ :
  (TensorProduct.assoc R A B C) y✝ =
    (TensorProduct.congr (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB)) (linearEquiv R eC) ≪≫ₗ
        (TensorProduct.assoc R A' B' C' ≪≫ₗ
          TensorProduct.congr (linearEquiv R eA).symm
            (TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eC).symm)))
      y✝
⊢ (TensorProduct.assoc R A B C) (x✝ + y✝) =
    (TensorProduct.congr (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB)) (linearEquiv R eC) ≪≫ₗ
        (TensorProduct.assoc R A' B' C' ≪≫ₗ
          TensorProduct.congr (linearEquiv R eA).symm
            (TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eC).symm)))
      (x✝ + y✝)

Tactic:
simp [*]

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

Goal state before:
pp: case inl
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
i' : I
k' : K
j' : J
l' : L
hi : i ≠ i'
⊢ single i j (single k l r) i' j' k' l' = single (i, k) (j, l) r (i', k') (j', l')

pp: case inr
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
k' : K
j' : J
l' : L
⊢ single i j (single k l r) i j' k' l' = single (i, k) (j, l) r (i, k') (j', l')

Tactic:
· rw [single_apply_of_row_ne hi,
      single_apply_of_row_ne (ne_of_apply_ne Prod.fst hi), Matrix.zero_apply]

Goal state after:
case inr
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
k' : K
j' : J
l' : L
⊢ single i j (single k l r) i j' k' l' = single (i, k) (j, l) r (i, k') (j', l')
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: case refine_1
R : Type u
inst✝² : Semiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
H : Projective R (⨁ (i : ι), M i)
i : ι
⊢ Projective R (M i)

pp: case refine_2
R : Type u
inst✝² : Semiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
H : ∀ (i : ι), Projective R (M i)
⊢ Projective R (⨁ (i : ι), M i)

Tactic:
· exact .of_split (DirectSum.lof ..) (DirectSum.component ..) (by simp)

Goal state after:
case refine_2
R : Type u
inst✝² : Semiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
H : ∀ (i : ι), Projective R (M i)
⊢ Projective R (⨁ (i : ι), M i)
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Nonempty ι
⊢ Function.Injective (replicateCol ι)

Tactic:
by
  inhabit ι
  exact fun _x _y h => funext fun i => congr_fun₂ h i default

Goal state after:
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
⊢ closure {p | Irreducible p} = ⊤

Tactic:
obtain ⟨S, hSgen, hSmax⟩ := Submonoid.exists_minimal_closure_eq_top M

Goal state after:
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
⊢ closure {p | Irreducible p} = ⊤
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case neg.intro.refine_1.refine_2
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
⊢ ∀ z ∈ N, ∃ c, z + c • y ∈ N'

Tactic:
intro z zN
      obtain ⟨b, hb⟩ : _ ∣ ϕ ⟨z, N_le_M zN⟩ := generator_submoduleImage_dvd_of_mem N_le_M ϕ zN
      refine ⟨-b, Submodule.mem_map.mpr ⟨⟨_, N.sub_mem zN (N.smul_mem b yN)⟩, ?_, ?_⟩⟩
      · refine LinearMap.mem_ker.mpr (show ϕ (⟨z, N_le_M zN⟩ - b • ⟨y, N_le_M yN⟩) = 0 from ?_)
        rw [map_sub, map_smul, hb, ϕy_eq, smul_eq_mul, mul_comm, sub_self]
      · simp only [sub_eq_add_neg, neg_smul, coe_subtype]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : n → R
⊢ (toLinearMapRight' (M' * M)) x = x

Tactic:
hM'M,

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : n → R
⊢ (toLinearMapRight' 1) x = x
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : n → R
⊢ (toLin' (M' * M)) x = x

Tactic:
hM'M,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : n → R
⊢ (toLin' 1) x = x
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝³ : Fintype m
M₃ : Type u_7
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
v₃ : Basis l R M₃
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₁
⊢ ((toLin v₁ v₁) (M' * M)) x = x

Tactic:
hM'M,

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝³ : Fintype m
M₃ : Type u_7
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
v₃ : Basis l R M₃
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₁
⊢ ((toLin v₁ v₁) 1) x = x