mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val✝¹ : n
val✝ : m
⊢ (fromBlocks A B C D).map f (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inl val✝¹) (Sum.inr val✝)

Tactic:
simp [fromBlocks]

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

Goal state before:
pp: case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val✝¹ : o
val✝ : l
⊢ (fromBlocks A B C D).map f (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inr val✝¹) (Sum.inl val✝)

Tactic:
simp [fromBlocks]

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

Goal state before:
pp: case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val✝¹ : o
val✝ : m
⊢ (fromBlocks A B C D).map f (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
simp [fromBlocks]

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

Goal state before:
pp: case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : l
val✝ : n
⊢ (fromBlocks A B C D)ᵀ (Sum.inl val✝¹) (Sum.inl val✝) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inl val✝¹) (Sum.inl val✝)

Tactic:
simp [fromBlocks]

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

Goal state before:
pp: case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : l
val✝ : o
⊢ (fromBlocks A B C D)ᵀ (Sum.inl val✝¹) (Sum.inr val✝) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inl val✝¹) (Sum.inr val✝)

Tactic:
simp [fromBlocks]

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

Goal state before:
pp: case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : m
val✝ : n
⊢ (fromBlocks A B C D)ᵀ (Sum.inr val✝¹) (Sum.inl val✝) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inr val✝¹) (Sum.inl val✝)

Tactic:
simp [fromBlocks]

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

Goal state before:
pp: case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : m
val✝ : o
⊢ (fromBlocks A B C D)ᵀ (Sum.inr val✝¹) (Sum.inr val✝) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
simp [fromBlocks]

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

Goal state before:
pp: case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : n
val✝ : l
⊢ (x • fromBlocks A B C D) (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inl val✝¹) (Sum.inl val✝)

Tactic:
simp [fromBlocks]

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

Goal state before:
pp: case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : n
val✝ : m
⊢ (x • fromBlocks A B C D) (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inl val✝¹) (Sum.inr val✝)

Tactic:
simp [fromBlocks]

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

Goal state before:
pp: case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : o
val✝ : l
⊢ (x • fromBlocks A B C D) (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val✝¹) (Sum.inl val✝)

Tactic:
simp [fromBlocks]

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

Goal state before:
pp: case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : o
val✝ : m
⊢ (x • fromBlocks A B C D) (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
simp [fromBlocks]

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

Goal state before:
pp: case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
val✝¹ : n
val✝ : l
⊢ (-fromBlocks A B C D) (Sum.inl val✝¹) (Sum.inl val✝) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val✝¹) (Sum.inl val✝)

Tactic:
simp [fromBlocks]

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

Goal state before:
pp: case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
val✝¹ : n
val✝ : m
⊢ (-fromBlocks A B C D) (Sum.inl val✝¹) (Sum.inr val✝) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val✝¹) (Sum.inr val✝)

Tactic:
simp [fromBlocks]

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

Goal state before:
pp: case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
val✝¹ : o
val✝ : l
⊢ (-fromBlocks A B C D) (Sum.inr val✝¹) (Sum.inl val✝) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val✝¹) (Sum.inl val✝)

Tactic:
simp [fromBlocks]

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

Goal state before:
pp: case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
val✝¹ : o
val✝ : m
⊢ (-fromBlocks A B C D) (Sum.inr val✝¹) (Sum.inr val✝) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
simp [fromBlocks]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
x : R
hx : x ∈ I
⊢ generator I ∈ Ideal.span {x} ↔ I ≤ Ideal.span {x}

Tactic:
conv_rhs => rw [← span_singleton_generator I, Submodule.span_singleton_le_iff_mem]

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

Goal state before:
pp: K : Type u
L : Type v
M : Type w
inst✝² : DivisionRing K
inst✝¹ : DivisionRing L
inst✝ : DivisionRing M
S : Set (Subfield K)
x : K
hx : x ∈ (sInf (toSubring '' S)).carrier
⊢ ∀ p ∈ toSubring '' S, x⁻¹ ∈ p

Tactic:
rintro _ ⟨p, p_mem, rfl⟩

Goal state after:
K : Type u
L : Type v
M : Type w
inst✝² : DivisionRing K
inst✝¹ : DivisionRing L
inst✝ : DivisionRing M
S : Set (Subfield K)
x : K
hx : x ∈ (sInf (toSubring '' S)).carrier
p : Subfield K
p_mem : p ∈ S
⊢ x⁻¹ ∈ p.toSubring
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
ha' : r₁ /ₒ s₁ + r₂ /ₒ s₂ = (sa • r₁ + ra • r₂) /ₒ (sa * s₁)
⊢ r₁ /ₒ s₁ + r₂ /ₒ s₂ + r₃ /ₒ s₃ = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + r₃ /ₒ s₃)

Tactic:
ha'

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
ha' : r₁ /ₒ s₁ + r₂ /ₒ s₂ = (sa • r₁ + ra • r₂) /ₒ (sa * s₁)
⊢ (sa • r₁ + ra • r₂) /ₒ (sa * s₁) + r₃ /ₒ s₃ = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + r₃ /ₒ s₃)
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
q : (sa • r₁ + ra • r₂) /ₒ (sa * s₁) + r₃ /ₒ s₃ = (sc • (sa • r₁ + ra • r₂) + rc • r₃) /ₒ (sc * (sa * s₁))
⊢ (sa • r₁ + ra • r₂) /ₒ (sa * s₁) + r₃ /ₒ s₃ = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + r₃ /ₒ s₃)

Tactic:
q

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
q : (sa • r₁ + ra • r₂) /ₒ (sa * s₁) + r₃ /ₒ s₃ = (sc • (sa • r₁ + ra • r₂) + rc • r₃) /ₒ (sc * (sa * s₁))
⊢ (sc • (sa • r₁ + ra • r₂) + rc • r₃) /ₒ (sc * (sa * s₁)) = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + r₃ /ₒ s₃)
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
ha' : r₁ /ₒ s₁ + r₂ /ₒ s₂ = (sa • r₁ + ra • r₂) /ₒ (sa * s₁)
⊢ (r₃ /ₒ s₃) • (r₁ /ₒ s₁ + r₂ /ₒ s₂) = (r₃ /ₒ s₃) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₂ /ₒ s₂)

Tactic:
ha'

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
ha' : r₁ /ₒ s₁ + r₂ /ₒ s₂ = (sa • r₁ + ra • r₂) /ₒ (sa * s₁)
⊢ (r₃ /ₒ s₃) • ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) = (r₃ /ₒ s₃) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₂ /ₒ s₂)
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
q : r₂ /ₒ s₂ + r₃ /ₒ s₃ = (sa • r₂ + ra • r₃) /ₒ (sa * s₂)
⊢ (r₂ /ₒ s₂ + r₃ /ₒ s₃) • (r₁ /ₒ s₁) = (r₂ /ₒ s₂) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)

Tactic:
q

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
q : r₂ /ₒ s₂ + r₃ /ₒ s₃ = (sa • r₂ + ra • r₃) /ₒ (sa * s₂)
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = (r₂ /ₒ s₂) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
q : (sa • r₂ /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = rb • r₁ /ₒ (sb * (sa * s₂))
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = (sa • r₂ /ₒ (sa * s₂)) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)

Tactic:
q

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
q : (sa • r₂ /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = rb • r₁ /ₒ (sb * (sa * s₂))
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = rb • r₁ /ₒ (sb * (sa * s₂)) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
b✝ : ι → M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
N : Submodule R M
inst✝ : Fintype ι
b : Basis ι R M
h : finrank R ↥N = finrank R M
n : ℕ
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
⊢ Fintype.card (Fin n) = Fintype.card (Fin (Fintype.card ι))

Tactic:
by
    simp only [Fintype.card_fin, ← Module.finrank_eq_card_basis bM, ← h,
      Module.finrank_eq_card_basis bN]

Goal state after:
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
h : 0 ∈ M
⊢ 0 = 1

Tactic:
simpa using IsLocalization.map_units S ⟨0, h⟩

Goal state after:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : FaithfulSMul R K
surj : ∀ (z : K), ∃ x y, z = (algebraMap R K) x / (algebraMap R K) y
inj : Function.Injective ⇑(algebraMap R K)
this✝ : NoZeroDivisors R
this : Nontrivial R
z : K
⊢ ∃ x, z * (algebraMap R K) ↑x.2 = (algebraMap R K) x.1

Tactic:
have ⟨x, y, eq⟩ := surj z

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : FaithfulSMul R K
surj : ∀ (z : K), ∃ x y, z = (algebraMap R K) x / (algebraMap R K) y
inj : Function.Injective ⇑(algebraMap R K)
this✝ : NoZeroDivisors R
this : Nontrivial R
z : K
x y : R
eq : z = (algebraMap R K) x / (algebraMap R K) y
⊢ ∃ x, z * (algebraMap R K) ↑x.2 = (algebraMap R K) x.1
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: case tmul
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
x : A
y : M
⊢ x ⊗ₜ[R] y ∈ Submodule.span A (Set.range ⇑((TensorProduct.mk R A M) 1))

Tactic:
← mul_one x,

Goal state after:
case tmul
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
x : A
y : M
⊢ (x * 1) ⊗ₜ[R] y ∈ Submodule.span A (Set.range ⇑((TensorProduct.mk R A M) 1))
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: case e'_6
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
this : Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (Order.succ (sSup s))) = ⊤
x✝ : Fin n
⊢ x✝ ∈ Fin.val ⁻¹' {sSup s} ↔ x✝ ∈ {⟨sSup s, ⋯⟩}

Tactic:
simp [Fin.ext_iff]

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

Goal state before:
pp: case tmul
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := (Algebra.linearMap R A).range
h✝ : Nontrivial (A ⧸ R')
x y s : A
hs : 1 ⊗ₜ[R] s = x ⊗ₜ[R] y
this : R'.mkQ 1 = 0
⊢ 0 ⊗ₜ[R] R'.mkQ s = 0

Tactic:
zero_tmul

Goal state after:
case tmul
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := (Algebra.linearMap R A).range
h✝ : Nontrivial (A ⧸ R')
x y s : A
hs : 1 ⊗ₜ[R] s = x ⊗ₜ[R] y
this : R'.mkQ 1 = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsEpi R A
a✝ b✝ a b : A
⊢ a ⊗ₜ[R] b = a • 1 ⊗ₜ[R] b

Tactic:
tmul_eq_smul_one_tmul

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsEpi R A
a✝ b✝ a b : A
⊢ a • 1 ⊗ₜ[R] b = a • 1 ⊗ₜ[R] b
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsEpi R A
a✝ b✝ a b : A
⊢ a • b ⊗ₜ[R] 1 = a • b • 1 ⊗ₜ[R] 1

Tactic:
tmul_eq_smul_one_tmul

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsEpi R A
a✝ b✝ a b : A
⊢ a • b • 1 ⊗ₜ[R] 1 = a • b • 1 ⊗ₜ[R] 1
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this✝¹ : Algebra S S' := f.toAlgebra
this✝ : IsScalarTower R S S'
this : Module.Finite S S'
⊢ Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T) =
    (↑((Algebra.TensorProduct.comm S (TensorProduct R S T) S').trans
            (Algebra.TensorProduct.cancelBaseChange R S S S' T))).comp
      Algebra.TensorProduct.includeLeft

pp: R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this✝¹ : Algebra S S' := f.toAlgebra
this✝ : IsScalarTower R S S'
this : Module.Finite S S'
⊢ ((↑((Algebra.TensorProduct.comm S (TensorProduct R S T) S').trans
            (Algebra.TensorProduct.cancelBaseChange R S S S' T))).comp
      Algebra.TensorProduct.includeLeft).Finite

Tactic:
· ext; simp

Goal state after:
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this✝¹ : Algebra S S' := f.toAlgebra
this✝ : IsScalarTower R S S'
this : Module.Finite S S'
⊢ ((↑((Algebra.TensorProduct.comm S (TensorProduct R S T) S').trans
            (Algebra.TensorProduct.cancelBaseChange R S S S' T))).comp
      Algebra.TensorProduct.includeLeft).Finite
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : InvolutiveStar α
⊢ star '' s = s⋆

Tactic:
simp only [← star_preimage]
  rw [image_eq_preimage_of_inverse] <;> intro <;> simp only [star_star]

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
⊢ NonUnitalCommSemiring α

Tactic:
apply e.injective.nonUnitalCommSemiring _ <;> intros <;> exact e.apply_symm_apply _

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
⊢ σ (r • a) = r • σ a

Tactic:
ext x
  have x_eq : x = r • r⁻¹ • x := by simp
  nth_rw 1 [x_eq]
  rw [smul_mem_smul_iff]
  constructor
  · exact fun h => ⟨r⁻¹ • x, ⟨h, show r • r⁻¹ • x = x by simp⟩⟩
  · rintro ⟨w, _, (x'_eq : r • w = x)⟩
    simpa [← x'_eq]

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

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹ : Ring A
inst✝ : Ring B
⊢ Ring (A ⊗[ℤ] B)

Tactic:
by infer_instance

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

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹ : CommRing A
inst✝ : CommRing B
⊢ CommRing (A ⊗[ℤ] B)

Tactic:
by infer_instance

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

Goal state before:
pp: R : Type u_1
S : Type u_3
T : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
⊢ {t | ∃ m n, m ⊗ₜ[R] n = t} ⊆ ↑((mk R S T).flip 1).range

Tactic:
rintro _ ⟨s, t, rfl⟩

Goal state after:
R : Type u_1
S : Type u_3
T : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
s : S
t : T
⊢ s ⊗ₜ[R] t ∈ ↑((mk R S T).flip 1).range
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ ∀ (x y : R),
    x ∈ AddSubmonoid.closure (range fun s ↦ star s * s) →
      y ∈ AddSubmonoid.closure (range fun s ↦ star s * s) →
        (∀ (x_1 y : R), y = x_1 + x → x_1 ≤ y) →
          (∀ (x y_1 : R), y_1 = x + y → x ≤ y_1) → ∀ (x_1 y_1 : R), y_1 = x_1 + (x + y) → x_1 ≤ y_1

Tactic:
rintro _ _ _ _ ha hb x y rfl
        rw [← add_assoc]
        exact (ha _ _ rfl).trans (hb _ _ rfl)

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : StrongRankCondition R
inst✝² : Free R M
m : Type w
n : Type w'
inst✝¹ : Finite m
inst✝ : Finite n
⊢ Module.rank R (Matrix m n M) = lift.{max v w', w} #m * lift.{max v w, w'} #n * lift.{max w w', v} (Module.rank R M)

Tactic:
cases nonempty_fintype m

Goal state after:
case intro
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : StrongRankCondition R
inst✝² : Free R M
m : Type w
n : Type w'
inst✝¹ : Finite m
inst✝ : Finite n
val✝ : Fintype m
⊢ Module.rank R (Matrix m n M) = lift.{max v w', w} #m * lift.{max v w, w'} #n * lift.{max w w', v} (Module.rank R M)
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ e ∈ t', g e • e = 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
x₁ : M
x₁_mem' : x₁ ∈ t.erase x₀
x₁_mem : shift x₁ ∈ t'
nz : g (shift x₁) ≠ 0
⊢ ∃ x ∈ t, f x ≠ 0

Tactic:
have := mem_erase.mp x₁_mem'

Goal state after:
case refine_3
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ e ∈ t', g e • e = 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
x₁ : M
x₁_mem' : x₁ ∈ t.erase x₀
x₁_mem : shift x₁ ∈ t'
nz : g (shift x₁) ≠ 0
this : x₁ ≠ x₀ ∧ x₁ ∈ t
⊢ ∃ x ∈ t, f x ≠ 0
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
x✝ : ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : ⟨v₀, hv₀⟩ ≠ 0
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
v : V
hv : v ∈ s
r : K
hr : r • ⟨v₀, hv₀⟩ = ⟨v, hv⟩
⊢ r • v₀ = v

Tactic:
by rwa [Subtype.ext_iff, coe_smul] at hr

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
h_inj : f.ker = ⊥
⊢ IsUnit f

Tactic:
ker_eq_bot

Goal state after:
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
h_inj : Injective ⇑f
⊢ IsUnit f