mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
⊢ #(α →₀ β) = max (lift.{v, u} #α) (lift.{u, v} #β)

Tactic:
mk_finsupp_lift_of_fintype

Goal state after:
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
⊢ lift.{u, v} #β ^ Fintype.card α = max (lift.{v, u} #α) (lift.{u, v} #β)
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
N' : Type v'
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
cnd : lift.{w, v} (Module.rank R M) ≤ lift.{v, w} #ι
a✝ : Nontrivial M
this : Nontrivial R
w✝ : Set M
B : Basis (↑w✝) R M
⊢ ∃ f, Injective ⇑f

Tactic:
replace cnd := (Cardinal.lift_le.2 B.linearIndependent.cardinal_le_rank).trans cnd

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
N' : Type v'
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
a✝ : Nontrivial M
this : Nontrivial R
w✝ : Set M
B : Basis (↑w✝) R M
cnd : lift.{w, v} #↑w✝ ≤ lift.{v, w} #ι
⊢ ∃ f, Injective ⇑f
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
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
β : Type v'
B' : Basis β R M'
this : lift.{v', v} #α = lift.{v, v'} #β
⊢ Nonempty (M ≃ₗ[R] M')

Tactic:
exact (Cardinal.lift_mk_eq.{v, v', 0}.1 this).map (B.equiv B')

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

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

Tactic:
have H' : a - b ∈ {x | t₂ x 0} := sub_self b ▸ t₂.sub H (t₂.refl b)

Goal state after:
case refine_2
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₂ a b
H' : a - b ∈ {x | t₂ x 0}
⊢ t₁ a b
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
ι : Sort u_1
S : ι → Subalgebra R A
motive : (x : A) → x ∈ ⨆ i, S i → Prop
x : A
mem : x ∈ ⨆ i, S i
basic : ∀ (i : ι) (x : A) (hx : x ∈ S i), motive x ⋯
add : ∀ (x y : A) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A) r) ⋯
⊢ motive x mem

Tactic:
refine Exists.elim ?_ fun (hx : x ∈ ⨆ i, S i) (hc : motive x hx) ↦ hc

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : (x : A) → x ∈ ⨆ i, S i → Prop
x : A
mem : x ∈ ⨆ i, S i
basic : ∀ (i : ι) (x : A) (hx : x ∈ S i), motive x ⋯
add : ∀ (x y : A) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A) r) ⋯
⊢ ∃ (x_1 : x ∈ ⨆ i, S i), motive x x_1
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
⊢ 0 ∈ {a | ϕ a = ψ a}

Tactic:
simp only [Set.mem_ofPred_eq, map_zero]

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

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : CommSemiring R
R' : Type u_2
inst✝¹⁵ : Monoid R'
R'' : Type u_3
inst✝¹⁴ : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : AddCommMonoid T
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : Module R T
inst✝² : DistribMulAction R' M
inst✝¹ : Module R'' M
inst✝ : Module R P
r : R
m : M
⊢ ((mk R R M) 1 ∘ₗ lift (LinearMap.lsmul R M)) (r ⊗ₜ[R] m) = LinearMap.id (r ⊗ₜ[R] m)

Tactic:
simp [← tmul_smul, ← smul_tmul, smul_eq_mul, mul_one]

Goal state after:
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
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
⊢ leftComm R M N P =
    (TensorProduct.assoc R M N P).symm ≪≫ₗ congr (TensorProduct.comm R M N) (LinearEquiv.refl R P) ≪≫ₗ
      TensorProduct.assoc R N M P

Tactic:
apply LinearEquiv.toLinearMap_injective

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
⊢ ↑(leftComm R M N P) =
    ↑((TensorProduct.assoc R M N P).symm ≪≫ₗ congr (TensorProduct.comm R M N) (LinearEquiv.refl R P) ≪≫ₗ
        TensorProduct.assoc R N M P)
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
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
⊢ rightComm R M N P =
    TensorProduct.assoc R M N P ≪≫ₗ congr (LinearEquiv.refl R M) (TensorProduct.comm R N P) ≪≫ₗ
      (TensorProduct.assoc R M P N).symm

Tactic:
apply LinearEquiv.toLinearMap_injective

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
⊢ ↑(rightComm R M N P) =
    ↑(TensorProduct.assoc R M N P ≪≫ₗ congr (LinearEquiv.refl R M) (TensorProduct.comm R N P) ≪≫ₗ
        (TensorProduct.assoc R M P N).symm)
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
P : Type u_2
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Projective R M
i : P →ₗ[R] M
s : M →ₗ[R] P
H : s ∘ₗ i = LinearMap.id
⊢ Projective R P

Tactic:
by
  obtain ⟨g, hg⟩ := projective_lifting_property (Finsupp.linearCombination R id) s
    (fun x ↦ ⟨Finsupp.single x 1, by simp⟩)
  refine ⟨g.comp i, fun x ↦ ?_⟩
  rw [LinearMap.comp_apply, ← LinearMap.comp_apply, hg,
    ← LinearMap.comp_apply, H, LinearMap.id_apply]

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

Goal state before:
pp: R : Type u_1
ι : Type u_5
κ : Type u_6
inst✝ : CommSemiring R
⊢ (finsuppTensorFinsupp R R R R ι κ).trans (Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.rid R R)) =
    (finsuppTensorFinsupp R R R R ι κ).trans (Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.lid R R))

Tactic:
TensorProduct.lid_eq_rid

Goal state after:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst✝ : CommSemiring R
⊢ (finsuppTensorFinsupp R R R R ι κ).trans (Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.rid R R)) =
    (finsuppTensorFinsupp R R R R ι κ).trans (Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.rid R R))
Module: Mathlib.Data.Matrix.Composition

Goal state before:
pp: case inr.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
⊢ diagonal (fun j ↦ d i₁ j) j₁ j₁ = diagonal (fun ij ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₁)

Tactic:
rw [diagonal_apply_eq, diagonal_apply_eq]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_12
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix n n α
D : Matrix m m α
k : ℕ
⊢ fromBlocks A 0 0 D ^ k = fromBlocks (A ^ k) 0 0 (D ^ k)

Tactic:
induction k with

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 n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
⊢ x ᵥ* fromBlocks A B C D = Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D)

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

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

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

Tactic:
restrictScalars_apply,

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

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

Tactic:
restrictScalars_apply,

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

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

Tactic:
restrictScalars_apply,

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

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

Tactic:
restrictScalars_apply,

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ baseChange A p ≤ span A ↑(map ((TensorProduct.mk R A M) 1) p)

Tactic:
rw [baseChange, LinearMap.range_le_iff_comap, eq_top_iff,
      ← span_eq_top_of_span_eq_top R A _ (span_tmul_eq_top R ..), span_le]
    refine fun _ ⟨a, m, h⟩ ↦ ?_
    rw [← h, SetLike.mem_coe, mem_comap, LinearMap.baseChange_tmul, ← mul_one a, ← smul_eq_mul,
      ← smul_tmul']
    exact smul_mem _ a (subset_span ⟨m, m.2, rfl⟩)

Goal state after:
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

Goal state after:
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 : O
zN : z ∈ N
⊢ ∃ c, z + c • y ∈ N'
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
⊢ toLin' (M ^ k) = toLin' M ^ k

Tactic:
induction k with

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

Goal state before:
pp: case 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 : R
s : ↥S
⊢ 0 /ₒ s = 0 /ₒ 1

Tactic:
zero_oreDiv,

Goal state after:
case 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 : R
s : ↥S
⊢ 0 = 0 /ₒ 1
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
f : M₁ →ₗ[R] M₁
k : ℕ
⊢ (toMatrix v₁ v₁) f ^ k = (toMatrix v₁ v₁) (f ^ k)

Tactic:
induction k with

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
A : Matrix n n R
k : ℕ
⊢ (toLin v₁ v₁) (A ^ k) = (toLin v₁ v₁) A ^ k

Tactic:
induction k with

Goal state after:
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₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra) • r₃ = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ ((sc * sb) • (sa • r₂ + ra • r₃) /ₒ (sc * sb * (sa * s₂))) • (r₁ /ₒ s₁) =
    (sc • rb • r₁ + 1 • rc • r₁) /ₒ (sc * (sb * (sa * s₂)))

Tactic:
simp only [smul_eq_mul, one_smul, Submonoid.smul_def, mul_add, Submonoid.coe_mul] at hb hc ⊢

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₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra * r₃) = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ ((↑sc * ↑sb * (↑sa * r₂) + ↑sc * ↑sb * (ra * r₃)) /ₒ (sc * sb * (sa * s₂))) • (r₁ /ₒ s₁) =
    (↑sc • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))
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
R₀ : Type ?u.16
inst✝⁴ : Semiring R₀
inst✝³ : Module R₀ X
inst✝² : Module R₀ R
inst✝¹ : IsScalarTower R₀ R X
inst✝ : IsScalarTower R₀ R R
x : OreLocalization S X
⊢ (0 /ₒ 1) • x = 0

Tactic:
zero_oreDiv,

Goal state after:
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₀ : Type ?u.16
inst✝⁴ : Semiring R₀
inst✝³ : Module R₀ X
inst✝² : Module R₀ R
inst✝¹ : IsScalarTower R₀ R X
inst✝ : IsScalarTower R₀ R R
x : OreLocalization S X
⊢ 0 • x = 0
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
inst✝ : IsLocalization M S
z : S
⊢ (algebraMap R S) (sec M z).1 = (algebraMap R S) ↑(sec M z).2 * z

Tactic:
rw [mul_comm, sec_spec]

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

Goal state before:
pp: case inr
R : Type u_8
S : Type u_9
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : IsFractionRing R S
left✝ : Subsingleton R
right✝ : Nontrivial S
⊢ False

Tactic:
apply (h.map_units S 1).ne_zero

Goal state after:
case inr
R : Type u_8
S : Type u_9
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : IsFractionRing R S
left✝ : Subsingleton R
right✝ : Nontrivial S
⊢ (algebraMap R S) ↑1 = 0
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: 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 : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : ⊤ = R ∙ x
f : (R ⧸ (LinearMap.toSpanSingleton R (M ⧸ N) x).ker) ≃ₗ[R] M ⧸ N :=
  (LinearMap.toSpanSingleton R (M ⧸ N) x).quotKerEquivOfSurjective ⋯
e : (LinearMap.toSpanSingleton R (M ⧸ N) x).ker = ⊤
⊢ x = 0

Tactic:
simpa using LinearMap.congr_fun (LinearMap.ker_eq_top.mp e) 1

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : A
b : B
k : ℕ
⊢ a ⊗ₜ[R] b ^ k = (a ^ k) ⊗ₜ[R] (b ^ k)

Tactic:
induction k with

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Module A M
inst✝⁴ : Module B M
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R B M
r t : A
x✝¹ : B
x✝ : M
⊢ (((r + t) • (Algebra.lsmul R R M).toLinearMap) x✝¹) x✝ =
    ((r • (Algebra.lsmul R R M).toLinearMap + t • (Algebra.lsmul R R M).toLinearMap) x✝¹) x✝

Tactic:
simp only [add_smul, LinearMap.add_apply]

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

Goal state before:
pp: A : Type u_1
𝕜 : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : PartialOrder A
inst✝³ : CommSemiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Algebra 𝕜 A
inst✝ : NonnegSpectrumClass 𝕜 A
a : A
ha : IsStrictlyPositive a
x : 𝕜
hx : x ∈ spectrum 𝕜 a
h₁ : 0 ≤ x
h₂ : x ≠ 0
⊢ 0 < x

Tactic:
exact lt_of_le_of_ne h₁ h₂.symm

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
⊢ ↑(iSup K) = ⋃ i, ↑(K i)

Tactic:
let s : Subalgebra R A :=
    { __ := Subsemiring.copy _ _ (Subsemiring.coe_iSup_of_directed dir).symm
      algebraMap_mem' := fun _ ↦ Set.mem_iUnion.2
        ⟨Classical.arbitrary ι, Subalgebra.algebraMap_mem _ _⟩ }
  have : iSup K = s := le_antisymm
    (iSup_le fun i ↦ le_iSup (fun i ↦ (K i : Set A)) i) (Set.iUnion_subset fun _ ↦ le_iSup K _)
  simp [this, s]

Goal state after: